awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.NormDeterminant (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
z : QuadraticAlgebra R a b
this :
  Eq (α := R) (Matrix.det (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im] : R)
    ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
w : QuadraticAlgebra R a b
i : Fin 2
⊢ Eq (α := R)
    ((((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
              ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z :
                  (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
                w) :
            Fin 2 →₀ R) :
          (a : Fin 2) → R)
        i :
      R)
    (Matrix.mulVec (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im]
      (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R) w : Fin 2 →₀ R) : (a : Fin 2) → R)
      i)
have h : Eq (α := R)
  ((((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
            ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z :
                (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
              w) :
          Fin 2 →₀ R) :
        (a : Fin 2) → R)
      ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) :
    R)
  (Matrix.mulVec (m := Fin 2) (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im]
      (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R) w : Fin 2 →₀ R) : (a : Fin 2) → R)
      ((fun (i : Fin 2) ↦ i) ⟨0, sorry⟩) :
    R)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.NormDeterminant (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
z : QuadraticAlgebra R a b
this :
  Eq (α := R) (Matrix.det (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im] : R)
    ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
w : QuadraticAlgebra R a b
i : Fin 2
h :
  Eq (α := R)
    ((((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
              ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z :
                  (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
                w) :
            Fin 2 →₀ R) :
          (a : Fin 2) → R)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      R)
    (Matrix.mulVec (m := Fin 2) (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im]
        (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R) w : Fin 2 →₀ R) :
          (a : Fin 2) → R)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      R)
⊢ Eq (α := R)
    ((((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
              ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z :
                  (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
                w) :
            Fin 2 →₀ R) :
          (a : Fin 2) → R)
        i :
      R)
    (Matrix.mulVec (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im]
      (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R) w : Fin 2 →₀ R) : (a : Fin 2) → R)
      i)
have h₁ : Eq (α := R)
  ((((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
            ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z :
                (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
              w) :
          Fin 2 →₀ R) :
        (a : Fin 2) → R)
      ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) :
    R)
  (Matrix.mulVec (m := Fin 2) (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im]
      (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R) w : Fin 2 →₀ R) : (a : Fin 2) → R)
      ((fun (i : Fin 2) ↦ i) ⟨1, sorry⟩) :
    R)
Tactic: fin_cases i
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.NormDeterminant (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
z : QuadraticAlgebra R a b
this :
  Eq (α := R) (Matrix.det (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im] : R)
    ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
w : QuadraticAlgebra R a b
⊢ Eq (α := R)
    ((((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
              ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z :
                  (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
                w) :
            Fin 2 →₀ R) :
          (a : Fin 2) → R)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      R)
    (Matrix.mulVec (m := Fin 2) (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im]
        (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R) w : Fin 2 →₀ R) :
          (a : Fin 2) → R)
        ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩) :
      R)
have h : z.re * w.re + a * z.im * w.im = w.re * z.re + w.im * (a * z.im)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.QuadraticAlgebra.NormDeterminant (goal)
Goal:
R : Type u_1
inst : CommRing R
a b : R
z : QuadraticAlgebra R a b
this :
  Eq (α := R) (Matrix.det (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im] : R)
    ((norm : (a : QuadraticAlgebra R a b) → R) z : R)
w : QuadraticAlgebra R a b
⊢ Eq (α := R)
    ((((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
              ((DistribSMul.toLinearMap R (QuadraticAlgebra R a b) z :
                  (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
                w) :
            Fin 2 →₀ R) :
          (a : Fin 2) → R)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      R)
    (Matrix.mulVec (m := Fin 2) (n := Fin 2) !![z.re, a * z.im; z.im, z.re + b * z.im]
        (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R) w : Fin 2 →₀ R) :
          (a : Fin 2) → R)
        ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩) :
      R)
have h : z.re * w.im + z.im * w.re + b * z.im * w.im = w.re * z.im + w.im * (z.re + b * z.im)
Tactic: simp
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
R : Type u_1
inst : CommRing R
a b c x : R
h : a * (x * x) + b * x + c = 0
⊢ discrim a b c = HPow.hPow (β := ℕ) (2 * a * x + b) 2
have rw : HPow.hPow (β := ℕ) b 2 - 4 * a * c = HPow.hPow (β := ℕ) (2 * a * x + b) 2
Tactic: rw [discrim]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
R : Type u_1
inst : CommRing R
a b c : R
inst_1 : NeZero.{u_1} (R := R) 2
inst_2 : NoZeroDivisors R
ha : a ≠ 0
x : R
⊢ a * (x * x) + b * x + c = 0 ↔ discrim a b c = HPow.hPow (β := ℕ) (2 * a * x + b) 2
have refine : ∀ (h : discrim a b c = HPow.hPow (β := ℕ) (2 * a * x + b) 2), a * (x * x) + b * x + c = 0
Tactic: refine ⟨discrim_eq_sq_of_quadratic_eq_zero, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
a b c : R
inst_1 : NeZero.{u_1} (R := R) 2
inst_2 : NoZeroDivisors R
ha : a ≠ 0
x : R
h : discrim a b c = HPow.hPow (β := ℕ) (2 * a * x + b) 2
⊢ a * (x * x) + b * x + c = 0
have h₁ : HPow.hPow (β := ℕ) b 2 - 4 * a * c = HPow.hPow (β := ℕ) (2 * a * x + b) 2
Tactic: rw [discrim] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
a b c : R
inst_1 : NeZero.{u_1} (R := R) 2
inst_2 : NoZeroDivisors R
ha : a ≠ 0
x : R
h : HPow.hPow (β := ℕ) b 2 - 4 * a * c = HPow.hPow (β := ℕ) (2 * a * x + b) 2
⊢ a * (x * x) + b * x + c = 0
have ha₁ : HMul.hMul (α := R) 2 2 * a ≠ 0
Tactic: have ha : 2 * 2 * a ≠ 0 := mul_ne_zero (mul_ne_zero (NeZero.ne _) (NeZero.ne _)) ha
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
R : Type u_1
inst : CommRing R
a b c : R
inst_1 : NeZero.{u_1} (R := R) 2
inst_2 : NoZeroDivisors R
ha_1 : a ≠ 0
x : R
h : HPow.hPow (β := ℕ) b 2 - 4 * a * c = HPow.hPow (β := ℕ) (2 * a * x + b) 2
ha : HMul.hMul (α := R) 2 2 * a ≠ 0
⊢ a * (x * x) + b * x + c = 0
have apply : HMul.hMul (α := R) 2 2 * a * (a * (x * x) + b * x + c) = HMul.hMul (α := R) 2 2 * a * 0
Tactic: apply mul_left_cancel₀ ha
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ a * (x * x) + b * x + c = 0 ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
have rw : s = 2 * a * x + b ∨ s = -(2 * a * x + b) ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
Tactic: rw [quadratic_eq_zero_iff_discrim_eq_sq ha, h, sq, mul_self_eq_mul_self_iff]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
s : K
h : discrim a b c = s * s
x : K
⊢ s = 2 * a * x + b ∨ s = -(2 * a * x + b) ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
have field_simp : s = 2 * a * x + b ∨ s = -(2 * a * x + b) ↔ 2 * a * x = -b + s ∨ 2 * a * x = -b - s
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
h : ∃ (s : K), discrim a b c = s * s
⊢ ∃ (x : K), a * (x * x) + b * x + c = 0
have rcases : ∀ (s : K) (hs : discrim a b c = s * s), ∃ (x : K), a * (x * x) + b * x + c = 0
Tactic: rcases h with ⟨s, hs⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ ∃ (x : K), a * (x * x) + b * x + c = 0
have h : a * ((-b + s) / (2 * a) * ((-b + s) / (2 * a))) + b * ((-b + s) / (2 * a)) + c = 0
Tactic: use (-b + s) / (2 * a)
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
s : K
hs : discrim a b c = s * s
⊢ a * ((-b + s) / (2 * a) * ((-b + s) / (2 * a))) + b * ((-b + s) / (2 * a)) + c = 0
have h : (-b + s) / (2 * a) = (-b + s) / (2 * a) ∨ (-b + s) / (2 * a) = (-b - s) / (2 * a)
Tactic: rw [quadratic_eq_zero_iff ha hs]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
⊢ discrim a b c = HMul.hMul (α := K) 0 0
have rw : 0 = HMul.hMul (α := K) 0 0
Tactic: rw [h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
rw : 0 = HMul.hMul (α := K) 0 0
⊢ discrim a b c = HMul.hMul (α := K) 0 0
have rw₁ : Eq.{u_1 + 1} (α := K) 0 0
Tactic: rw [h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
⊢ a * (x * x) + b * x + c = 0 ↔ x = -b / (2 * a)
have this : discrim a b c = HMul.hMul (α := K) 0 0
Tactic: have : discrim a b c = 0 * 0 := by rw [h, mul_zero]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
this : discrim a b c = HMul.hMul (α := K) 0 0
⊢ a * (x * x) + b * x + c = 0 ↔ x = -b / (2 * a)
have rw : x = (-b + 0) / (2 * a) ∨ x = (-b - 0) / (2 * a) ↔ x = -b / (2 * a)
Tactic: rw [quadratic_eq_zero_iff ha this, add_zero, sub_zero, or_self_iff]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
this : discrim a b c = HMul.hMul (α := K) 0 0
rw : x = (-b + 0) / (2 * a) ∨ x = (-b - 0) / (2 * a) ↔ x = -b / (2 * a)
⊢ a * (x * x) + b * x + c = 0 ↔ x = -b / (2 * a)
have rw₁ : x = -b / (2 * a) ∨ x = (-b - 0) / (2 * a) ↔ x = -b / (2 * a)
Tactic: rw [quadratic_eq_zero_iff ha this, add_zero, sub_zero, or_self_iff]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
this : discrim a b c = HMul.hMul (α := K) 0 0
rw : x = (-b + 0) / (2 * a) ∨ x = (-b - 0) / (2 * a) ↔ x = -b / (2 * a)
rw₁ : x = -b / (2 * a) ∨ x = (-b - 0) / (2 * a) ↔ x = -b / (2 * a)
⊢ a * (x * x) + b * x + c = 0 ↔ x = -b / (2 * a)
have rw₂ : x = -b / (2 * a) ∨ x = -b / (2 * a) ↔ x = -b / (2 * a)
Tactic: rw [quadratic_eq_zero_iff ha this, add_zero, sub_zero, or_self_iff]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
h : discrim a b c = 0
x : K
this : discrim a b c = HMul.hMul (α := K) 0 0
rw : x = (-b + 0) / (2 * a) ∨ x = (-b - 0) / (2 * a) ↔ x = -b / (2 * a)
rw₁ : x = -b / (2 * a) ∨ x = (-b - 0) / (2 * a) ↔ x = -b / (2 * a)
rw₂ : x = -b / (2 * a) ∨ x = -b / (2 * a) ↔ x = -b / (2 * a)
⊢ a * (x * x) + b * x + c = 0 ↔ x = -b / (2 * a)
have rw₃ : x = -b / (2 * a) ↔ x = -b / (2 * a)
Tactic: rw [quadratic_eq_zero_iff ha this, add_zero, sub_zero, or_self_iff]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
h : ∃! x : K, a * (x * x) + b * x + c = 0
⊢ discrim a b c = 0
have h₁ : ∃! x : K, discrim a b c = HPow.hPow (β := ℕ) (2 * a * x + b) 2
Tactic: simp_rw [quadratic_eq_zero_iff_discrim_eq_sq ha] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
h : ∃! x : K, discrim a b c = HPow.hPow (β := ℕ) (2 * a * x + b) 2
⊢ discrim a b c = 0
have generalize : ∀ (d : K) (h : ∃! x : K, d = HPow.hPow (β := ℕ) (2 * a * x + b) 2), d = 0
Tactic: generalize discrim a b c = d at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
d : K
h : ∃! x : K, d = HPow.hPow (β := ℕ) (2 * a * x + b) 2
⊢ d = 0
have obtain : ∀ (x : K)
  (hx :
    ∀ (y : K),
      (fun (x_1 : K) ↦ HPow.hPow (β := ℕ) (2 * a * x + b) 2 = HPow.hPow (β := ℕ) (2 * a * x_1 + b) 2) y → y = x),
  HPow.hPow (β := ℕ) (2 * a * x + b) 2 = 0
Tactic: obtain ⟨x, rfl, hx⟩ := h
Cleared hypotheses: d, h
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
x : K
hx :
  ∀ (y : K), (fun (x_1 : K) ↦ HPow.hPow (β := ℕ) (2 * a * x + b) 2 = HPow.hPow (β := ℕ) (2 * a * x_1 + b) 2) y → y = x
⊢ HPow.hPow (β := ℕ) (2 * a * x + b) 2 = 0
have hx₁ : (fun (x_1 : K) ↦ HPow.hPow (β := ℕ) (2 * a * x + b) 2 = HPow.hPow (β := ℕ) (2 * a * x_1 + b) 2) (-(x + b / a)) →
  -(x + b / a) = x
Tactic: specialize hx (-(x + b / a))
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
⊢ discrim a b c = 0 ↔ ∃! x : K, a * (x * x) + b * x + c = 0
have refine : ∀ (hd : discrim a b c = 0), ∃! x : K, a * (x * x) + b * x + c = 0
Tactic: refine ⟨fun hd => ?_, discrim_eq_zero_of_existsUnique ha⟩
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
hd : discrim a b c = 0
⊢ ∃! x : K, a * (x * x) + b * x + c = 0
have simp_rw : ∃! x : K, x = -b / (2 * a)
Tactic: simp_rw [quadratic_eq_zero_iff_of_discrim_eq_zero ha hd, existsUnique_eq]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
⊢ discrim a b c ≤ 0
have rw : b * b - 4 * a * c ≤ 0
Tactic: rw [discrim, sq]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
⊢ b * b - 4 * a * c ≤ 0
have inl : ∀ (ha : a < 0), b * b - 4 * a * c ≤ 0
Tactic: obtain ha | rfl | ha : a < 0 ∨ a = 0 ∨ 0 < a := lt_trichotomy a 0
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
inl : ∀ (ha : a < 0), b * b - 4 * a * c ≤ 0
⊢ b * b - 4 * a * c ≤ 0
have inr : ∀ (h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c), b * b - HMul.hMul (α := K) 4 0 * c ≤ 0
Tactic: obtain ha | rfl | ha : a < 0 ∨ a = 0 ∨ 0 < a := lt_trichotomy a 0
Cleared hypotheses: a, h
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
inl : ∀ (ha : a < 0), b * b - 4 * a * c ≤ 0
inr : ∀ (h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c), b * b - HMul.hMul (α := K) 4 0 * c ≤ 0
⊢ b * b - 4 * a * c ≤ 0
have inr₁ : ∀ (ha : 0 < a), b * b - 4 * a * c ≤ 0
Tactic: obtain ha | rfl | ha : a < 0 ∨ a = 0 ∨ 0 < a := lt_trichotomy a 0
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : a < 0
⊢ b * b - 4 * a * c ≤ 0
have this : Tendsto (β := K) (fun (x : K) ↦ (a * x + b) * x + c) atTop atBot
Tactic: have : Tendsto (fun x => (a * x + b) * x + c) atTop atBot :=
      tendsto_atBot_add_const_right _ c <|
        (tendsto_atBot_add_const_right _ b (tendsto_id.const_mul_atTop_of_neg ha)).atBot_mul_atTop₀
          tendsto_id
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : a < 0
this : Tendsto (β := K) (fun (x : K) ↦ (a * x + b) * x + c) atTop atBot
⊢ b * b - 4 * a * c ≤ 0
have inl : ∀ (x : K) (hx : (a * x + b) * x + c < 0), b * b - 4 * a * c ≤ 0
Tactic: rcases (this.eventually (eventually_lt_atBot 0)).exists with ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : a < 0
this : Tendsto (β := K) (fun (x : K) ↦ (a * x + b) * x + c) atTop atBot
x : K
hx : (a * x + b) * x + c < 0
⊢ a * (x * x) + b * x + c < 0
have rwa : a * x * x + b * x + c < 0
Tactic: rwa [← mul_assoc, ← add_mul]
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
⊢ b * b - HMul.hMul (α := K) 4 0 * c ≤ 0
have inr : ∀ (h : ∀ (x : K), 0 ≤ 0 * (x * x) + 0 * x + c), HMul.hMul (α := K) 0 0 - HMul.hMul (α := K) 4 0 * c ≤ 0
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
Cleared hypotheses: b, h
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
inr : ∀ (h : ∀ (x : K), 0 ≤ 0 * (x * x) + 0 * x + c), HMul.hMul (α := K) 0 0 - HMul.hMul (α := K) 4 0 * c ≤ 0
⊢ b * b - HMul.hMul (α := K) 4 0 * c ≤ 0
have inr₁ : ∀ (hb : b ≠ 0), b * b - HMul.hMul (α := K) 4 0 * c ≤ 0
Tactic: rcases eq_or_ne b 0 with (rfl | hb)
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
hb : b ≠ 0
⊢ b * b - HMul.hMul (α := K) 4 0 * c ≤ 0
have this : 0 ≤ 0 * ((-c - 1) / b * ((-c - 1) / b)) + b * ((-c - 1) / b) + c
Tactic: have := h ((-c - 1) / b)
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
hb : b ≠ 0
this : 0 ≤ 0 * ((-c - 1) / b * ((-c - 1) / b)) + b * ((-c - 1) / b) + c
⊢ b * b - HMul.hMul (α := K) 4 0 * c ≤ 0
have this₁ : 0 ≤ 0 * ((-c - 1) / b * ((-c - 1) / b)) + (-c - 1) + c
Tactic: rw [mul_div_cancel₀ _ hb] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
hb : b ≠ 0
this : 0 ≤ 0 * ((-c - 1) / b * ((-c - 1) / b)) + (-c - 1) + c
⊢ b * b - HMul.hMul (α := K) 4 0 * c ≤ 0
have linarith : 0 < b * b - HMul.hMul (α := K) 4 0 * c → HMul.hMul (α := K) 1 1 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
b c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + b * x + c
hb : b ≠ 0
this : 0 ≤ 0 * ((-c - 1) / b * ((-c - 1) / b)) + (-c - 1) + c
linarith linarith₁ : 0 < b * b - HMul.hMul (α := K) 4 0 * c → HMul.hMul (α := K) 1 1 = 1
⊢ b * b - HMul.hMul (α := K) 4 0 * c ≤ 0
have linarith₂ : 0 < b * b - HMul.hMul (α := K) 4 0 * c →
  -1 +
      (HMul.hMul (α := K) 1 0 -
        (HMul.hMul (α := K) 1 0 * (1 * ((-c - 1) / b) * (1 * ((-c - 1) / b))) + (-(1 * c) - HMul.hMul (α := K) 1 1) +
          1 * c)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : 0 < a
⊢ b * b - 4 * a * c ≤ 0
have ha' : 0 ≤ 4 * a
Tactic: have ha' : 0 ≤ 4 * a := mul_nonneg zero_le_four ha.le
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
h : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
ha : 0 < a
ha' : 0 ≤ 4 * a
⊢ b * b - 4 * a * c ≤ 0
have h₁ : b * b - 4 * a * c = -(4 * a * (a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c))
Tactic: convert! neg_nonpos.2 (mul_nonneg ha' (h (-b / (2 * a)))) using 1
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
⊢ discrim a b c < 0
have this : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
Tactic: have : ∀ x : K, 0 ≤ a * (x * x) + b * x + c := fun x => le_of_lt (h x)
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
⊢ discrim a b c < 0
have refine : ∀ (h' : discrim a b c = 0), False
Tactic: refine lt_of_le_of_ne (discrim_le_zero this) fun h' ↦ ?_
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (hypothesis)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
⊢ False
have this₁ : 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c
Tactic: have := h (-b / (2 * a))
-- Lean 4 proof step from Mathlib.Algebra.QuadraticDiscriminant (goal)
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
a b c : K
ha : a ≠ 0
h : ∀ (x : K), 0 < a * (x * x) + b * x + c
this_1 : ∀ (x : K), 0 ≤ a * (x * x) + b * x + c
h' : discrim a b c = 0
this : 0 < a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c
⊢ a * (-b / (2 * a)) * (-b / (2 * a)) + b * (-b / (2 * a)) + c = 0
have rw : a * (-b / (2 * a) * (-b / (2 * a))) + b * (-b / (2 * a)) + c = 0
Tactic: rw [mul_assoc, quadratic_eq_zero_iff_of_discrim_eq_zero ha h' (-b / (2 * a))]