awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
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
h :
  Eq (α := (a : Fin 2) → 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)
    (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))
⊢ Eq (α := (a : Fin 2) → 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)
    (⇑((Module.Basis.repr (basis a b) : (a : QuadraticAlgebra R a b) → Fin 2 →₀ R)
            ((((LinearEquiv.symm (LinearMap.toMatrix (basis a b) (basis a b)) :
                      (a_1 : Matrix (Fin 2) (Fin 2) R) → QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b)
                    !![z.re, a * z.im; z.im, z.re + b * z.im] :
                  QuadraticAlgebra R a b →ₗ[R] QuadraticAlgebra R a b) :
                (a_1 : QuadraticAlgebra R a b) → QuadraticAlgebra R a b)
              w) :
          Fin 2 →₀ R) :
      (a : Fin 2) → R)

Tactic:
rw [LinearMap.toMatrix_symm, Matrix.repr_toLin]

Premises used: Matrix.repr_toLin, LinearMap.toMatrix_symm
-- Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
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
h :
  ∀ (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)
⊢ Eq (α := (a : Fin 2) → 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)
    (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))

Tactic:
ext i
-- Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
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)
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, ⋯⟩) :
      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)
⊢ 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)

Tactic:
fin_cases i
-- Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
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
h : z.re * w.re + a * z.im * w.im = w.re * z.re + w.im * (a * z.im)
⊢ 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)

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
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
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)
⊢ 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)

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
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
⊢ z.re * w.re + a * z.im * w.im = w.re * z.re + w.im * (a * z.im)

Tactic:
ring
-- Module: Mathlib.Algebra.QuadraticAlgebra.NormDeterminant
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
⊢ 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:
ring
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
R : Type u_1
inst : Ring R
a b c : R
⊢ discrim (-a) (-b) (-c) = discrim a b c

Tactic:
simp [discrim]

Premises used: discrim
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
R : Type u_1
inst : CommRing R
a b c x : R
h : a * (x * x) + b * x + c = 0
rw : HPow.hPow (β := ℕ) b 2 - 4 * a * c = HPow.hPow (β := ℕ) (2 * a * x + b) 2
⊢ discrim a b c = HPow.hPow (β := ℕ) (2 * a * x + b) 2

Tactic:
rw [discrim]

Premises used: discrim
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
R : Type u_1
inst : CommRing R
a b c x : R
h : a * (x * x) + b * x + c = 0
⊢ HPow.hPow (β := ℕ) b 2 - 4 * a * c = HPow.hPow (β := ℕ) (2 * a * x + b) 2

Tactic:
linear_combination -4 * a * h
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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

Tactic:
⟨discrim_eq_sq_of_quadratic_eq_zero, fun h ↦ ?_⟩

Premises used: Iff.intro, discrim_eq_sq_of_quadratic_eq_zero
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
refine : ∀ (h : discrim a b c = HPow.hPow (β := ℕ) (2 * a * x + b) 2), a * (x * x) + b * x + c = 0
⊢ a * (x * x) + b * x + c = 0 ↔ discrim a b c = HPow.hPow (β := ℕ) (2 * a * x + b) 2

Tactic:
refine ⟨discrim_eq_sq_of_quadratic_eq_zero, fun h ↦ ?_⟩
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
⊢ HPow.hPow (β := ℕ) b 2 - 4 * a * c = HPow.hPow (β := ℕ) (2 * a * x + b) 2

Tactic:
rw [discrim] at h

Premises used: discrim
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
⊢ 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
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
apply : HMul.hMul (α := R) 2 2 * a * (a * (x * x) + b * x + c) = HMul.hMul (α := R) 2 2 * a * 0
⊢ a * (x * x) + b * x + c = 0

Tactic:
apply mul_left_cancel₀ ha

Premises used: mul_left_cancel₀
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
⊢ HMul.hMul (α := R) 2 2 * a * (a * (x * x) + b * x + c) = HMul.hMul (α := R) 2 2 * a * 0

Tactic:
linear_combination -h
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
R : Type u_1
inst : CommRing R
a b c : R
h : ∀ (s : R), discrim a b c ≠ HPow.hPow (β := ℕ) s 2
x : R
⊢ a * (x * x) + b * x + c ≠ 0

Tactic:
mt discrim_eq_sq_of_quadratic_eq_zero (h _)

Premises used: mt, discrim_eq_sq_of_quadratic_eq_zero
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
rw : s = 2 * a * x + b ∨ s = -(2 * a * x + b) ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)
⊢ a * (x * x) + b * x + c = 0 ↔ 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]

Premises used: mul_self_eq_mul_self_iff, quadratic_eq_zero_iff_discrim_eq_sq, sq
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
field_simp : s = 2 * a * x + b ∨ s = -(2 * a * x + b) ↔ 2 * a * x = -b + s ∨ 2 * a * x = -b - s
⊢ s = 2 * a * x + b ∨ s = -(2 * a * x + b) ↔ x = (-b + s) / (2 * a) ∨ x = (-b - s) / (2 * a)

Tactic:
field_simp
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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) ↔ 2 * a * x = -b + s ∨ 2 * a * x = -b - s

Tactic:
grind
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
rcases : ∀ (s : K) (hs : discrim a b c = s * s), ∃ (x : K), a * (x * x) + b * x + c = 0
⊢ ∃ (x : K), a * (x * x) + b * x + c = 0

Tactic:
rcases h with ⟨s, hs⟩
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
h : a * ((-b + s) / (2 * a) * ((-b + s) / (2 * a))) + b * ((-b + s) / (2 * a)) + c = 0
⊢ ∃ (x : K), a * (x * x) + b * x + c = 0

Tactic:
use (-b + s) / (2 * a)

Premises used: HMul.hMul, HAdd.hAdd, OfNat.ofNat, Neg.neg
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
h : (-b + s) / (2 * a) = (-b + s) / (2 * a) ∨ (-b + s) / (2 * a) = (-b - s) / (2 * a)
⊢ a * ((-b + s) / (2 * a) * ((-b + s) / (2 * a))) + b * ((-b + s) / (2 * a)) + c = 0

Tactic:
rw [quadratic_eq_zero_iff ha hs]

Premises used: quadratic_eq_zero_iff
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
⊢ (-b + s) / (2 * a) = (-b + s) / (2 * a) ∨ (-b + s) / (2 * a) = (-b - s) / (2 * a)

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
rw₁ rw₂ : Eq.{u_1 + 1} (α := K) 0 0
⊢ discrim a b c = HMul.hMul (α := K) 0 0

Tactic:
rw [h, mul_zero]

Premises used: MulZeroClass.mul_zero
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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

Tactic:
have : discrim a b c = 0 * 0 := by rw [h, mul_zero]
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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)
rw₃ rw₄ : x = -b / (2 * a) ↔ x = -b / (2 * a)
⊢ a * (x * x) + b * x + c = 0 ↔ x = -b / (2 * a)

Tactic:
rw [quadratic_eq_zero_iff ha this, add_zero, sub_zero, or_self_iff]

Premises used: sub_zero, or_self_iff, quadratic_eq_zero_iff, add_zero
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
⊢ ∃! 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

Premises used: quadratic_eq_zero_iff_discrim_eq_sq
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
generalize : ∀ (d : K) (h : ∃! x : K, d = HPow.hPow (β := ℕ) (2 * a * x + b) 2), d = 0
⊢ discrim a b c = 0

Tactic:
generalize discrim a b c = d at h

Premises used: discrim
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
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
⊢ d = 0

Tactic:
obtain ⟨x, rfl, hx⟩ := h

Premises used: rfl
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
⊢ (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))

Premises used: HDiv.hDiv, HAdd.hAdd, Neg.neg
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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 :
  (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
⊢ HPow.hPow (β := ℕ) (2 * a * x + b) 2 = 0

Tactic:
grind
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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

Tactic:
⟨fun hd => ?_, discrim_eq_zero_of_existsUnique ha⟩

Premises used: discrim_eq_zero_of_existsUnique, Iff.intro
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
K : Type u_1
inst : Field K
inst_1 : NeZero.{u_1} (R := K) 2
a b c : K
ha : a ≠ 0
refine : ∀ (hd : discrim a b c = 0), ∃! x : K, a * (x * x) + b * x + c = 0
⊢ discrim a b c = 0 ↔ ∃! x : K, a * (x * x) + b * x + c = 0

Tactic:
refine ⟨fun hd => ?_, discrim_eq_zero_of_existsUnique ha⟩
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
simp_rw : ∃! x : K, x = -b / (2 * a)
⊢ ∃! x : K, a * (x * x) + b * x + c = 0

Tactic:
simp_rw [quadratic_eq_zero_iff_of_discrim_eq_zero ha hd, existsUnique_eq]

Premises used: existsUnique_eq, quadratic_eq_zero_iff_of_discrim_eq_zero
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
rw : b * b - 4 * a * c ≤ 0
⊢ discrim a b c ≤ 0

Tactic:
rw [discrim, sq]

Premises used: discrim, sq
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
⊢ a < 0 ∨ a = 0 ∨ 0 < a

Tactic:
lt_trichotomy a 0

Premises used: OfNat.ofNat, lt_trichotomy
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
inr₁ : ∀ (ha : 0 < a), b * b - 4 * a * c ≤ 0
⊢ b * b - 4 * a * c ≤ 0

Tactic:
obtain ha | rfl | ha : a < 0 ∨ a = 0 ∨ 0 < a := lt_trichotomy a 0

Premises used: OfNat.ofNat, rfl, lt_trichotomy
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
⊢ 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
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
inl : ∀ (x : K) (hx : (a * x + b) * x + c < 0), b * b - 4 * a * c ≤ 0
⊢ b * b - 4 * a * c ≤ 0

Tactic:
rcases (this.eventually (eventually_lt_atBot 0)).exists with ⟨x, hx⟩

Premises used: Filter.Eventually.exists, Filter.eventually_lt_atBot, Filter.Tendsto.eventually, OfNat.ofNat
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
rwa : a * x * x + b * x + c < 0
rwa₁ rwa₂ rwa₃ rwa₄ : (a * x + b) * x + c < 0
⊢ a * (x * x) + b * x + c < 0

Tactic:
rwa [← mul_assoc, ← add_mul]

Premises used: add_mul, mul_assoc
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
⊢ b * b - 4 * a * c ≤ 0

Tactic:
exact False.elim ((h x).not_gt <| by rwa [← mul_assoc, ← add_mul])

Premises used: False.elim, LE.le.not_gt
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
inr₁ : ∀ (hb : b ≠ 0), b * b - HMul.hMul (α := K) 4 0 * c ≤ 0
⊢ b * b - HMul.hMul (α := K) 4 0 * c ≤ 0

Tactic:
rcases eq_or_ne b 0 with (rfl | hb)

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.QuadraticDiscriminant
Goal:
K : Type u_1
inst : Field K
inst_1 : LinearOrder K
inst_2 : IsStrictOrderedRing K
c : K
h : ∀ (x : K), 0 ≤ 0 * (x * x) + 0 * x + c
⊢ HMul.hMul (α := K) 0 0 - HMul.hMul (α := K) 4 0 * c ≤ 0

Tactic:
simp
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
⊢ 0 ≤ 0 * ((-c - 1) / b * ((-c - 1) / b)) + b * ((-c - 1) / b) + c

Tactic:
have := h ((-c - 1) / b)
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
⊢ 0 ≤ 0 * ((-c - 1) / b * ((-c - 1) / b)) + (-c - 1) + c

Tactic:
rw [mul_div_cancel₀ _ hb] at this

Premises used: mul_div_cancel₀
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
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
⊢ b * b - HMul.hMul (α := K) 4 0 * c ≤ 0

Tactic:
linarith
-- Module: Mathlib.Algebra.QuadraticDiscriminant
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
⊢ 0 ≤ 4 * a

Tactic:
have ha' : 0 ≤ 4 * a := mul_nonneg zero_le_four ha.le