fixes

fpvandoorn · fpvandoorn · commit 40a138288fa9 · 2023-05-03T13:45:52.000+02:00
diff --git a/Mathlib/Data/Complex/Exponential.lean b/Mathlib/Data/Complex/Exponential.lean
@@ -180,7 +180,6 @@ theorem series_ratio_test {f : ℕ → β} (n : ℕ) (r : α) (hr0 : 0 ≤ r) (h
   replace hk : m = k + n.succ := (tsub_eq_iff_eq_add_of_le hmn).1 hk
   induction' k with k ih generalizing m n
   · rw [hk, Nat.zero_add, mul_right_comm, inv_pow _ _, ← div_eq_mul_inv, mul_div_cancel]
-    exact le_refl _
     exact (ne_of_lt (pow_pos r_pos _)).symm
   · have kn : k + n.succ ≥ n.succ := by
       rw [← zero_add n.succ]; exact add_le_add (Nat.zero_le _) (by simp)
diff --git a/Mathlib/Data/MvPolynomial/Variables.lean b/Mathlib/Data/MvPolynomial/Variables.lean
@@ -97,7 +97,6 @@ theorem degrees_monomial (s : σ →₀ ℕ) (a : R) : degrees (monomial s a) 
     have := Finsupp.support_single_subset h
     rw [Finset.mem_singleton] at this
     rw [this]
-    exact le_refl _
 #align mv_polynomial.degrees_monomial MvPolynomial.degrees_monomial
 
 theorem degrees_monomial_eq (s : σ →₀ ℕ) (a : R) (ha : a ≠ 0) :
diff --git a/Mathlib/LinearAlgebra/AffineSpace/Basis.lean b/Mathlib/LinearAlgebra/AffineSpace/Basis.lean
@@ -126,7 +126,6 @@ noncomputable def basisOf (i : ι) : Basis { j : ι // j ≠ i } k V :=
       suffices
         Submodule.span k (range fun j : { x // x ≠ i } => b ↑j -ᵥ b i) = vectorSpan k (range b) by
         rw [this, ← direction_affineSpan, b.tot, AffineSubspace.direction_top]
-        exact le_rfl
       conv_rhs => rw [← image_univ]
       rw [vectorSpan_image_eq_span_vsub_set_right_ne k b (mem_univ i)]
       congr
diff --git a/Mathlib/LinearAlgebra/FiniteDimensional.lean b/Mathlib/LinearAlgebra/FiniteDimensional.lean
@@ -1448,8 +1448,6 @@ theorem Subalgebra.eq_bot_of_finrank_one {S : Subalgebra F E} (h : finrank F S =
     -- porting note: fails without explicit type
     haveI : FiniteDimensional F S := finiteDimensional_of_finrank_eq_succ h
     rw [← finrank_eq_rank, h, Nat.cast_one]
-    -- porting note: added, `rw` forgot to close this
-    exact le_rfl
 #align subalgebra.eq_bot_of_finrank_one Subalgebra.eq_bot_of_finrank_one
 
 set_option synthInstance.etaExperiment true in
diff --git a/Mathlib/RingTheory/Multiplicity.lean b/Mathlib/RingTheory/Multiplicity.lean
@@ -243,8 +243,7 @@ theorem multiplicity_le_multiplicity_iff {a b c d : α} :
         exact le_multiplicity_of_pow_dvd (h _ (pow_multiplicity_dvd _))
     else by
       have : ∀ n : ℕ, c ^ n ∣ d := fun n => h n (not_finite_iff_forall.1 hab _)
-      rw [eq_top_iff_not_finite.2 hab, eq_top_iff_not_finite.2 (not_finite_iff_forall.2 this)]
-      apply le_refl⟩
+      rw [eq_top_iff_not_finite.2 hab, eq_top_iff_not_finite.2 (not_finite_iff_forall.2 this)]⟩
 #align multiplicity.multiplicity_le_multiplicity_iff multiplicity.multiplicity_le_multiplicity_iff
 
 theorem multiplicity_eq_multiplicity_iff {a b c d : α} :
