chore: remove redundant have:s in Geometry/ and GroupTheory/ (leanprover-community#28999)

Co-authored-by: euprunin <euprunin@users.noreply.github.com>

Author: euprunin

Mathlib/Geometry/Euclidean/Inversion/ImageHyperplane.lean

@@ -37,7 +37,6 @@ hyperplane. -/
 theorem inversion_mem_perpBisector_inversion_iff (hR : R ≠ 0) (hx : x ≠ c) (hy : y ≠ c) :
     inversion c R x ∈ perpBisector c (inversion c R y) ↔ dist x y = dist y c := by
   rw [mem_perpBisector_iff_dist_eq, dist_inversion_inversion hx hy, dist_inversion_center]
-  have hx' := dist_ne_zero.2 hx
   have hy' := dist_ne_zero.2 hy
   -- takes 300ms, but the "equivalent" simp call fails -> hard to speed up
   field_simp [mul_assoc, mul_comm, hx, hx.symm, eq_comm]

Mathlib/GroupTheory/FiniteAbelian/Duality.lean

@@ -43,8 +43,6 @@ lemma exists_apply_ne_one_aux
   obtain ⟨i, hi⟩ : ∃ i : ι, e a i ≠ 1 := by
     contrapose! ha
     exact (MulEquiv.map_eq_one_iff e).mp <| funext ha
-  have hi : (e a i).toAdd ≠ 0 := by
-    simp only [ne_eq, toAdd_eq_zero, hi, not_false_eq_true]
   obtain ⟨φi, hφi⟩ := H (n i) (dvd_exponent e i) ((e a i).toAdd) hi
   use (φi.comp (Pi.evalMonoidHom (fun (i : ι) ↦ Multiplicative (ZMod (n i))) i)).comp e
   simpa only [coe_comp, coe_coe, Function.comp_apply, Pi.evalMonoidHom_apply, ne_eq] using hφi

Mathlib/GroupTheory/Perm/Cycle/Basic.lean

@@ -448,7 +448,6 @@ theorem IsCycle.sign {f : Perm α} (hf : IsCycle f) : sign f = -(-1) ^ #f.suppor
         have h : #(swap x (f x) * f).support + 1 = #f.support := by
           rw [← insert_erase (mem_support.2 hx.1), support_swap_mul_eq _ _ h1,
             card_insert_of_notMem (notMem_erase _ _), sdiff_singleton_eq_erase]
-        have : #(swap x (f x) * f).support < #f.support := card_support_swap_mul hx.1
         rw [sign_mul, sign_swap hx.1.symm, (hf.swap_mul hx.1 h1).sign, ← h]
         simp only [mul_neg, neg_mul, one_mul, neg_neg, pow_add, pow_one, mul_one]
 termination_by #f.support

Mathlib/GroupTheory/Sylow.lean

@@ -622,7 +622,6 @@ theorem exists_subgroup_card_pow_prime_le [Finite G] (p : ℕ) :
     (lt_or_eq_of_le hnm).elim
       (fun hnm : n < m =>
         have h0m : 0 < m := lt_of_le_of_lt n.zero_le hnm
-        have _wf : m - 1 < m := Nat.sub_lt h0m zero_lt_one
         have hnm1 : n ≤ m - 1 := le_tsub_of_add_le_right hnm
         let ⟨K, hK⟩ :=
           @exists_subgroup_card_pow_prime_le _ _ n (m - 1) _