chore(*) Unused have statements in term mode (#5012)

Remove unneeded have statements.

src/algebra/quadratic_discriminant.lean

@@ -113,7 +113,6 @@ variables {K : Type*} [linear_ordered_field K] {a b c : K}
 
 /-- If a polynomial of degree 2 is always nonnegative, then its discriminant is nonpositive -/
 lemma discrim_le_zero (h : ∀ x : K, 0 ≤ a * x * x + b * x + c) : discrim a b c ≤ 0 :=
-have hc : 0 ≤ c, by { have := h 0, linarith },
 begin
   rw [discrim, pow_two],
   obtain ha|rfl|ha : a < 0 ∨ a = 0 ∨ 0 < a := lt_trichotomy a 0,

src/analysis/special_functions/trigonometric.lean

@@ -1445,7 +1445,6 @@ if hx₁ : 0 ≤ x.re
 then by rw [arg, if_pos hx₁];
   exact le_trans (real.arcsin_le_pi_div_two _) (le_of_lt (half_lt_self real.pi_pos))
 else
-  have hx : x ≠ 0, from λ h, by simpa [h, lt_irrefl] using hx₁,
   if hx₂ : 0 ≤ x.im
   then by rw [arg, if_neg hx₁, if_pos hx₂];
     exact le_sub_iff_add_le.1 (by rw sub_self;

src/analysis/specific_limits.lean

@@ -157,8 +157,6 @@ section geometric
 lemma has_sum_geometric_of_lt_1 {r : ℝ} (h₁ : 0 ≤ r) (h₂ : r < 1) :
   has_sum (λn:ℕ, r ^ n) (1 - r)⁻¹ :=
 have r ≠ 1, from ne_of_lt h₂,
-have r + -1 ≠ 0,
-  by rw [←sub_eq_add_neg, ne, sub_eq_iff_eq_add]; simp; assumption,
 have tendsto (λn, (r ^ n - 1) * (r - 1)⁻¹) at_top (𝓝 ((0 - 1) * (r - 1)⁻¹)),
   from ((tendsto_pow_at_top_nhds_0_of_lt_1 h₁ h₂).sub tendsto_const_nhds).mul tendsto_const_nhds,
 have (λ n, (∑ i in range n, r ^ i)) = (λ n, geom_series r n) := rfl,

src/category_theory/abelian/non_preadditive.lean

@@ -207,8 +207,6 @@ pullback (prod.lift (𝟙 X) f) (prod.lift (𝟙 X) g)
 /-- The equalizer of `f` and `g` exists. -/
 @[irreducible]
 lemma has_limit_parallel_pair {X Y : C} (f g : X ⟶ Y) : has_limit (parallel_pair f g) :=
-have h1f : mono (prod.lift (𝟙 X) f), from mono_of_mono_fac $ prod.lift_fst (𝟙 X) f,
-have h1g : mono (prod.lift (𝟙 X) g), from mono_of_mono_fac $ prod.lift_fst (𝟙 X) g,
 have huv : (pullback.fst : P f g ⟶ X) = pullback.snd, from
   calc (pullback.fst : P f g ⟶ X) = pullback.fst ≫ 𝟙 _ : eq.symm $ category.comp_id _
     ... = pullback.fst ≫ prod.lift (𝟙 X) f ≫ limits.prod.fst : by rw prod.lift_fst
@@ -243,8 +241,6 @@ pushout (coprod.desc (𝟙 Y) f) (coprod.desc (𝟙 Y) g)
 /-- The coequalizer of `f` and `g` exists. -/
 @[irreducible]
 lemma has_colimit_parallel_pair {X Y : C} (f g : X ⟶ Y) : has_colimit (parallel_pair f g) :=
-have h1f : epi (coprod.desc (𝟙 Y) f), from epi_of_epi_fac $ coprod.inl_desc _ _,
-have h1g : epi (coprod.desc (𝟙 Y) g), from epi_of_epi_fac $ coprod.inl_desc _ _,
 have huv : (pushout.inl : Y ⟶ Q f g) = pushout.inr, from
   calc (pushout.inl : Y ⟶ Q f g) = 𝟙 _ ≫ pushout.inl : eq.symm $ category.id_comp _
     ... = (coprod.inl ≫ coprod.desc (𝟙 Y) f) ≫ pushout.inl : by rw coprod.inl_desc

src/data/nat/basic.lean

@@ -982,7 +982,6 @@ else
   have ha : 0 < a, from nat.pos_of_ne_zero ha,
   have h1 : ∃ d, c = a * b * d, from h,
   let ⟨d, hd⟩ := h1 in
-  have hac : a ∣ c, from dvd_of_mul_right_dvd h,
   have h2 : c / a = b * d, from nat.div_eq_of_eq_mul_right ha (by simpa [mul_assoc] using hd),
   show ∃ d, c / a = b * d, from ⟨d, h2⟩
 

src/data/nat/modeq.lean

@@ -269,7 +269,6 @@ have h₃ : m < list.length (l ++ [a]), by simpa using hml,
       add_assoc m n 1 ▸ nat.modeq.modeq_add
         (hml'.trans (nat.mod_eq_of_lt (nat.lt_succ_self _)).symm) rfl
     ... = 0 : by simp,
-  have h₂ : l.length < (l ++ [a]).length, by simp [nat.lt_succ_self],
   by rw [list.length, list.rotate_cons_succ, nth_rotate h₃, list.length_append,
     list.length_cons, list.length, zero_add, hml', h₁, list.nth_concat_length]; refl)
 

src/data/padics/padic_norm.lean

@@ -282,8 +282,6 @@ have hqn : q.num ≠ 0, from rat.num_ne_zero_of_ne_zero hq,
 have hqd : (q.denom : ℤ) ≠ 0, by exact_mod_cast rat.denom_ne_zero _,
 have hrn : r.num ≠ 0, from rat.num_ne_zero_of_ne_zero hr,
 have hrd : (r.denom : ℤ) ≠ 0, by exact_mod_cast rat.denom_ne_zero _,
-have hqdv : q.num /. q.denom ≠ 0, from rat.mk_ne_zero_of_ne_zero hqn hqd,
-have hrdv : r.num /. r.denom ≠ 0, from rat.mk_ne_zero_of_ne_zero hrn hrd,
 have hqreq : q + r = (((q.num * r.denom + q.denom * r.num : ℤ)) /. (↑q.denom * ↑r.denom : ℤ)),
   from rat.add_num_denom _ _,
 have hqrd : q.num * ↑(r.denom) + ↑(q.denom) * r.num ≠ 0,

src/data/polynomial/div.lean

@@ -177,9 +177,6 @@ have zn0 : (0 : R) ≠ 1, from λ h, by haveI := subsingleton_of_zero_eq_one h;
   have hpnr0 : leading_coeff (p ^ (nat_degree q + 1)) * leading_coeff r ≠ 0,
     by simp only [leading_coeff_pow' hpn0', leading_coeff_eq_zero, hpn1,
       one_pow, one_mul, ne.def, hr0]; simp,
-  have hpn0 : p ^ (nat_degree q + 1) ≠ 0,
-    from mt leading_coeff_eq_zero.2 $
-      by rw [leading_coeff_pow' hpn0', show _ = _, from hmp, one_pow]; exact zn0.symm,
   have hnp : 0 < nat_degree p,
     by rw [← with_bot.coe_lt_coe, ← degree_eq_nat_degree hp0];
     exact hp,

src/data/real/hyperreal.lean

@@ -642,8 +642,7 @@ lemma infinite_neg_iff_infinitesimal_inv_neg {x : ℝ*} :
 ⟨ λ hin, have hin' : _ := infinite_pos_iff_infinitesimal_inv_pos.mp
   (infinite_pos_neg_of_infinite_neg hin),
   by rwa [infinitesimal_neg_iff, ←neg_pos, neg_inv],
-  λ hin, have h0 : x ≠ 0 := λ h0, (lt_irrefl (0 : ℝ*) (by convert hin.2; rw [h0, inv_zero])),
-  by rwa [←neg_pos, infinitesimal_neg_iff, neg_inv,
+  λ hin, by rwa [←neg_pos, infinitesimal_neg_iff, neg_inv,
     ←infinite_pos_iff_infinitesimal_inv_pos, ←infinite_neg_iff_infinite_pos_neg] at hin ⟩
 
 theorem infinitesimal_inv_of_infinite {x : ℝ*} : infinite x → infinitesimal x⁻¹ :=

src/group_theory/order_of_element.lean

@@ -216,8 +216,6 @@ have ft_s : fintype (gpowers a),
   from @fintype.fintype_prod_right _ _ _ ft_prod _,
 have ft_cosets : fintype (quotient (gpowers a)),
   from @fintype.fintype_prod_left _ _ _ ft_prod ⟨⟨1, (gpowers a).one_mem⟩⟩,
-have ft : fintype (quotient (gpowers a) × (gpowers a)),
-  from @prod.fintype _ _ ft_cosets ft_s,
 have eq₁ : fintype.card α = @fintype.card _ ft_cosets * @fintype.card _ ft_s,
   from calc fintype.card α = @fintype.card _ ft_prod :
       @fintype.card_congr _ _ _ ft_prod group_equiv_quotient_times_subgroup

src/group_theory/sylow.lean

@@ -220,10 +220,6 @@ have hm' : p ∣ card (quotient (subgroup.comap ((normalizer H).subtype : normal
   nat.dvd_of_mod_eq_zero
     (by rwa [nat.mod_eq_zero_of_dvd (dvd_mul_left _ _), eq_comm] at hm),
 let ⟨x, hx⟩ := @exists_prime_order_of_dvd_card _ (quotient_group.quotient.group _) _ _ hp hm' in
-have hxcard : ∀ {f : fintype (subgroup.gpowers x)}, card (subgroup.gpowers x) = p,
-  from λ f, by rw [← hx, order_eq_card_gpowers]; congr,
-have fintype (subgroup.comap (quotient_group.mk' (comap H.normalizer.subtype H)) (gpowers x)),
-  by apply_instance,
 have hequiv : H ≃ (subgroup.comap ((normalizer H).subtype : normalizer H →* G) H) :=
   ⟨λ a, ⟨⟨a.1, le_normalizer a.2⟩, a.2⟩, λ a, ⟨a.1.1, a.2⟩,
     λ ⟨_, _⟩, rfl, λ ⟨⟨_, _⟩, _⟩, rfl⟩,

src/linear_algebra/basic.lean

@@ -1319,9 +1319,7 @@ by simp [disjoint_def, @eq_comm M 0, @eq_comm M₂ 0] {contextual := tt}; intros
 
 theorem ker_eq_bot' {f : M →ₗ[R] M₂} :
   ker f = ⊥ ↔ (∀ m, f m = 0 → m = 0) :=
-have h : (∀ m ∈ (⊤ : submodule R M), f m = 0 → m = 0) ↔ (∀ m, f m = 0 → m = 0),
-  from ⟨λ h m, h m mem_top, λ h m _, h m⟩,
-by simpa [h, disjoint] using @disjoint_ker _ _ _ _ _ _ _ _ f ⊤
+by simpa [disjoint] using @disjoint_ker _ _ _ _ _ _ _ _ f ⊤
 
 lemma le_ker_iff_map {f : M →ₗ[R] M₂} {p : submodule R M} : p ≤ ker f ↔ map f p = ⊥ :=
 by rw [ker, eq_bot_iff, map_le_iff_le_comap]

src/number_theory/pell.lean

@@ -233,7 +233,6 @@ section
       (xy_coprime _).coprime_dvd_right (y_mul_dvd m (n / m)),
     have m0 : 0 < m, from m.eq_zero_or_pos.resolve_left $
       λe, by rw [e, nat.mod_zero] at hp; rw [e] at h; exact
-      have 0 < yn a1 n, from y_increasing _ hp,
       ne_of_lt (y_increasing a1 hp) (eq_zero_of_zero_dvd h).symm,
     by rw [← nat.mod_add_div n m, yn_add] at h; exact
     not_le_of_gt (y_increasing _ $ nat.mod_lt n m0)

src/number_theory/sum_four_squares.lean

@@ -28,7 +28,6 @@ lemma sum_two_squares_of_two_mul_sum_two_squares {m x y : ℤ} (h : 2 * m =  x^2
 have even (x^2 + y^2), by simp [h.symm, even_mul],
 have hxaddy : even (x + y), by simpa [pow_two] with parity_simps,
 have hxsuby : even (x - y), by simpa [pow_two] with parity_simps,
-have (x^2 + y^2) % 2 = 0, by simp [h.symm],
 (mul_right_inj' (show (2*2 : ℤ) ≠ 0, from dec_trivial)).1 $
 calc 2 * 2 * m = (x - y)^2 + (x + y)^2 : by rw [mul_assoc, h]; ring
 ... = (2 * ((x - y) / 2))^2 + (2 * ((x + y) / 2))^2 :