awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ map φ P =
    { a := (φ : (a : F) → K) P.a, b := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)),
      c := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z),
      d := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) }
have apply_fun : Eq (α := K[X]) (map φ P).toPoly
  (toPoly
    { a := (φ : (a : F) → K) P.a, b := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)),
      c := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z),
      d := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) })
Tactic: apply_fun toPoly
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
apply_fun :
  Eq (α := K[X]) (map φ P).toPoly
    (toPoly
      { a := (φ : (a : F) → K) P.a, b := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)),
        c := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z),
        d := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) })
⊢ map φ P =
    { a := (φ : (a : F) → K) P.a, b := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)),
      c := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z),
      d := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) }
have inj : Function.Injective.{u_4 + 1, u_4 + 1} (α := Cubic K) (β := K[X]) toPoly
Tactic: apply_fun toPoly
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ Eq (α := K[X]) (map φ P).toPoly
    (toPoly
      { a := (φ : (a : F) → K) P.a, b := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)),
        c := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z),
        d := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) })
have rw : HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
        (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
    HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X]) =
  toPoly
    { a := (φ : (a : F) → K) P.a, b := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)),
      c := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z),
      d := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) }
Tactic: rw [eq_prod_three_roots ha h3, C_mul_prod_X_sub_C_eq]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
rw :
  HMul.hMul (α := K[X]) ((C : (a : K) → K[X]) ((φ : (a : F) → K) P.a) : K[X])
          (HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) x : K[X])) *
        HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) y : K[X]) *
      HSub.hSub (α := K[X]) (β := K[X]) X ((C : (a : K) → K[X]) z : K[X]) =
    toPoly
      { a := (φ : (a : F) → K) P.a, b := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)),
        c := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z),
        d := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) }
⊢ Eq (α := K[X]) (map φ P).toPoly
    (toPoly
      { a := (φ : (a : F) → K) P.a, b := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)),
        c := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z),
        d := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) })
have rw₁ : Eq.{u_4 + 1} (α := K[X])
  (toPoly
      { a := (φ : (a : F) → K) P.a, b := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)),
        c := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z),
        d := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) } :
    K[X])
  (toPoly
      { a := (φ : (a : F) → K) P.a, b := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)),
        c := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z),
        d := HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) } :
    K[X])
Tactic: rw [eq_prod_three_roots ha h3, C_mul_prod_X_sub_C_eq]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ (φ : (a : F) → K) P.discr =
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) *
        (y - z))
      2
have simp : HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.b : K) 2 * HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.c : K) 2 -
          HMul.hMul (α := K) (β := K) (4 : K) ((φ : (a : F) → K) P.a : K) *
            HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.c : K) 3 -
        HMul.hMul (β := K) (4 * HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.b : K) 3) ((φ : (a : F) → K) P.d : K) -
      27 * HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.a : K) 2 *
        HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.d : K) 2 +
    HMul.hMul (β := K)
      (HMul.hMul (β := K)
        (HMul.hMul (β := K) (HMul.hMul (α := K) (β := K) (18 : K) ((φ : (a : F) → K) P.a : K))
          ((φ : (a : F) → K) P.b : K))
        ((φ : (a : F) → K) P.c : K))
      ((φ : (a : F) → K) P.d : K) =
  HPow.hPow (β := ℕ)
    (HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) * (y - z))
    2
Tactic: simp only [discr, RingHom.map_add, map_sub, map_mul, map_pow, map_ofNat]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.b : K) 2 *
              HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.c : K) 2 -
            HMul.hMul (α := K) (β := K) (4 : K) ((φ : (a : F) → K) P.a : K) *
              HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.c : K) 3 -
          HMul.hMul (β := K) (4 * HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.b : K) 3)
            ((φ : (a : F) → K) P.d : K) -
        27 * HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.a : K) 2 *
          HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.d : K) 2 +
      HMul.hMul (β := K)
        (HMul.hMul (β := K)
          (HMul.hMul (β := K) (HMul.hMul (α := K) (β := K) (18 : K) ((φ : (a : F) → K) P.a : K))
            ((φ : (a : F) → K) P.b : K))
          ((φ : (a : F) → K) P.c : K))
        ((φ : (a : F) → K) P.d : K) =
    HPow.hPow (β := ℕ)
      (HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) *
        (y - z))
      2
have rw : HPow.hPow (β := ℕ) (HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z))) 2 *
            HPow.hPow (β := ℕ) (HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z)) 2 -
          HMul.hMul (α := K) (β := K) (4 : K) ((φ : (a : F) → K) P.a : K) *
            HPow.hPow (β := ℕ) (HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z)) 3 -
        4 * HPow.hPow (β := ℕ) (HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z))) 3 *
          HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) -
      27 * HPow.hPow (α := K) (β := ℕ) ((φ : (a : F) → K) P.a : K) 2 *
        HPow.hPow (β := ℕ) (HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z))) 2 +
    HMul.hMul (α := K) (β := K) (18 : K) ((φ : (a : F) → K) P.a : K) *
          HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x + y + z)) *
        HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (x * y + x * z + y * z) *
      HMul.hMul (α := K) ((φ : (a : F) → K) P.a : K) (-(x * y * z)) =
  HPow.hPow (β := ℕ)
    (HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) * (y - z))
    2
Tactic: rw [b_eq_three_roots ha h3, c_eq_three_roots ha h3, d_eq_three_roots ha h3]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ P.discr ≠ 0 ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z
have rw : HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) * (y - z) *
      (HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) *
        (y - z)) ≠
    0 ↔
  x ≠ y ∧ x ≠ z ∧ y ≠ z
Tactic: rw [← map_ne_zero φ, discr_eq_prod_three_roots ha h3, pow_two]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
⊢ HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) * (y - z) *
        (HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) *
          (y - z)) ≠
      0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
have simp_rw : ((((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
            Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
          x - y ≠ 0) ∧
        x - z ≠ 0) ∧
      y - z ≠ 0) ∧
    (((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
            Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
          x - y ≠ 0) ∧
        x - z ≠ 0) ∧
      y - z ≠ 0 ↔
  x ≠ y ∧ x ≠ z ∧ y ≠ z
Tactic: simp_rw [mul_ne_zero_iff, sub_ne_zero, _root_.map_ne_zero, and_self_iff, and_iff_right ha,
    and_assoc]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
simp_rw :
  ((((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x - y ≠ 0) ∧
          x - z ≠ 0) ∧
        y - z ≠ 0) ∧
      (((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x - y ≠ 0) ∧
          x - z ≠ 0) ∧
        y - z ≠ 0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
⊢ HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) * (y - z) *
        (HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) *
          (y - z)) ≠
      0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
have simp_rw₁ : ((((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
            Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
          x ≠ y) ∧
        x ≠ z) ∧
      y ≠ z) ∧
    (((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
            Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
          x ≠ y) ∧
        x ≠ z) ∧
      y ≠ z ↔
  x ≠ y ∧ x ≠ z ∧ y ≠ z
Tactic: simp_rw [mul_ne_zero_iff, sub_ne_zero, _root_.map_ne_zero, and_self_iff, and_iff_right ha,
    and_assoc]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
simp_rw :
  ((((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x - y ≠ 0) ∧
          x - z ≠ 0) ∧
        y - z ≠ 0) ∧
      (((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x - y ≠ 0) ∧
          x - z ≠ 0) ∧
        y - z ≠ 0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
simp_rw₁ :
  ((((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x ≠ y) ∧
          x ≠ z) ∧
        y ≠ z) ∧
      (((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x ≠ y) ∧
          x ≠ z) ∧
        y ≠ z ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
⊢ HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) * (y - z) *
        (HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) *
          (y - z)) ≠
      0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
have simp_rw₂ : ((((P.a ≠ 0 ∧ P.a ≠ 0) ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z) ∧ (((P.a ≠ 0 ∧ P.a ≠ 0) ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z ↔
  x ≠ y ∧ x ≠ z ∧ y ≠ z
Tactic: simp_rw [mul_ne_zero_iff, sub_ne_zero, _root_.map_ne_zero, and_self_iff, and_iff_right ha,
    and_assoc]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
simp_rw :
  ((((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x - y ≠ 0) ∧
          x - z ≠ 0) ∧
        y - z ≠ 0) ∧
      (((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x - y ≠ 0) ∧
          x - z ≠ 0) ∧
        y - z ≠ 0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
simp_rw₁ :
  ((((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x ≠ y) ∧
          x ≠ z) ∧
        y ≠ z) ∧
      (((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x ≠ y) ∧
          x ≠ z) ∧
        y ≠ z ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
simp_rw₂ :
  ((((P.a ≠ 0 ∧ P.a ≠ 0) ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z) ∧ (((P.a ≠ 0 ∧ P.a ≠ 0) ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
⊢ HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) * (y - z) *
        (HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) *
          (y - z)) ≠
      0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
have simp_rw₃ : ((P.a ≠ 0 ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z
Tactic: simp_rw [mul_ne_zero_iff, sub_ne_zero, _root_.map_ne_zero, and_self_iff, and_iff_right ha,
    and_assoc]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
x y z : K
ha : P.a ≠ 0
h3 : (map φ P).roots = {x, y, z}
simp_rw :
  ((((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x - y ≠ 0) ∧
          x - z ≠ 0) ∧
        y - z ≠ 0) ∧
      (((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x - y ≠ 0) ∧
          x - z ≠ 0) ∧
        y - z ≠ 0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
simp_rw₁ :
  ((((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x ≠ y) ∧
          x ≠ z) ∧
        y ≠ z) ∧
      (((Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K) ∧
              Ne.{u_4 + 1} (α := K) ((φ : (a : F) → K) P.a : K) (0 : K)) ∧
            x ≠ y) ∧
          x ≠ z) ∧
        y ≠ z ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
simp_rw₂ :
  ((((P.a ≠ 0 ∧ P.a ≠ 0) ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z) ∧ (((P.a ≠ 0 ∧ P.a ≠ 0) ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
simp_rw₃ : ((P.a ≠ 0 ∧ x ≠ y) ∧ x ≠ z) ∧ y ≠ z ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z
⊢ HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) * (y - z) *
        (HMul.hMul (α := K) (β := K) ((φ : (a : F) → K) P.a : K) ((φ : (a : F) → K) P.a : K) * (x - y) * (x - z) *
          (y - z)) ≠
      0 ↔
    x ≠ y ∧ x ≠ z ∧ y ≠ z
have simp_rw₄ : (x ≠ y ∧ x ≠ z) ∧ y ≠ z ↔ x ≠ y ∧ x ≠ z ∧ y ≠ z
Tactic: simp_rw [mul_ne_zero_iff, sub_ne_zero, _root_.map_ne_zero, and_self_iff, and_iff_right ha,
    and_assoc]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
⊢ P.discr ≠ 0 ↔ (map φ P).roots.Nodup
have have : ∀ (x y z : K) (h3 : (map φ P).roots = {x, y, z}), P.discr ≠ 0 ↔ (map φ P).roots.Nodup
Tactic: have ⟨x, y, z, h3⟩ := (splits_iff_roots_eq_three ha).mp hP
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
⊢ P.discr ≠ 0 ↔ (map φ P).roots.Nodup
have rw : x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ Nodup (α := K) {x, y, z}
Tactic: rw [discr_ne_zero_iff_roots_ne ha h3, h3]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ (x ::ₘ y ::ₘ {z}).Nodup
have rw : x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ Nodup (α := K) {z}
Tactic: rw [nodup_cons, nodup_cons, mem_cons, mem_singleton, mem_singleton]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ Nodup (α := K) {z}
have simp : x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
Tactic: simp only [nodup_singleton]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
have mp : x ≠ y ∧ x ≠ z ∧ y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
mp : x ≠ y ∧ x ≠ z ∧ y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
have mpr : ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True → x ≠ y ∧ x ≠ z ∧ y ≠ z
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
mp : x ≠ y ∧ x ≠ z ∧ y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
mpr : ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True → x ≠ y ∧ x ≠ z ∧ y ≠ z
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
have mp₁ : x ≠ y → x ≠ z → y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
mp : x ≠ y ∧ x ≠ z ∧ y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
mpr : ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True → x ≠ y ∧ x ≠ z ∧ y ≠ z
mp₁ mp₂ : x ≠ y → x ≠ z → y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
have mp₃ : x ≠ y → x ≠ z → y ≠ z → ¬(x = y ∨ x = z)
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
mp : x ≠ y ∧ x ≠ z ∧ y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
mpr : ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True → x ≠ y ∧ x ≠ z ∧ y ≠ z
mp₁ mp₂ : x ≠ y → x ≠ z → y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
mp₃ : x ≠ y → x ≠ z → y ≠ z → ¬(x = y ∨ x = z)
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
have mp₄ : x ≠ y → x ≠ z → y ≠ z → ¬y = z
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
mp : x ≠ y ∧ x ≠ z ∧ y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
mpr : ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True → x ≠ y ∧ x ≠ z ∧ y ≠ z
mp₁ mp₂ : x ≠ y → x ≠ z → y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
mp₃ : x ≠ y → x ≠ z → y ≠ z → ¬(x = y ∨ x = z)
mp₄ : x ≠ y → x ≠ z → y ≠ z → ¬y = z
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
have mpr₁ : ¬(x = y ∨ x = z) → ¬y = z → True → x ≠ y ∧ x ≠ z ∧ y ≠ z
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
mp : x ≠ y ∧ x ≠ z ∧ y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
mpr : ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True → x ≠ y ∧ x ≠ z ∧ y ≠ z
mp₁ mp₂ : x ≠ y → x ≠ z → y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
mp₃ : x ≠ y → x ≠ z → y ≠ z → ¬(x = y ∨ x = z)
mp₄ : x ≠ y → x ≠ z → y ≠ z → ¬y = z
mpr₁ mpr₂ : ¬(x = y ∨ x = z) → ¬y = z → True → x ≠ y ∧ x ≠ z ∧ y ≠ z
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
have mpr₃ : ¬(x = y ∨ x = z) → ¬y = z → True → x ≠ y
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
mp : x ≠ y ∧ x ≠ z ∧ y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
mpr : ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True → x ≠ y ∧ x ≠ z ∧ y ≠ z
mp₁ mp₂ : x ≠ y → x ≠ z → y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
mp₃ : x ≠ y → x ≠ z → y ≠ z → ¬(x = y ∨ x = z)
mp₄ : x ≠ y → x ≠ z → y ≠ z → ¬y = z
mpr₁ mpr₂ : ¬(x = y ∨ x = z) → ¬y = z → True → x ≠ y ∧ x ≠ z ∧ y ≠ z
mpr₃ : ¬(x = y ∨ x = z) → ¬y = z → True → x ≠ y
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
have mpr₄ : ¬(x = y ∨ x = z) → ¬y = z → True → x ≠ z
Tactic: tauto
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
F : Type u_3
K : Type u_4
P : Cubic F
inst : Field F
inst_1 : Field K
φ : F →+* K
ha : P.a ≠ 0
hP : (Polynomial.map φ P.toPoly).Splits
x y z : K
h3 : (map φ P).roots = {x, y, z}
mp : x ≠ y ∧ x ≠ z ∧ y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
mpr : ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True → x ≠ y ∧ x ≠ z ∧ y ≠ z
mp₁ mp₂ : x ≠ y → x ≠ z → y ≠ z → ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
mp₃ : x ≠ y → x ≠ z → y ≠ z → ¬(x = y ∨ x = z)
mp₄ : x ≠ y → x ≠ z → y ≠ z → ¬y = z
mpr₁ mpr₂ : ¬(x = y ∨ x = z) → ¬y = z → True → x ≠ y ∧ x ≠ z ∧ y ≠ z
mpr₃ : ¬(x = y ∨ x = z) → ¬y = z → True → x ≠ y
mpr₄ : ¬(x = y ∨ x = z) → ¬y = z → True → x ≠ z
⊢ x ≠ y ∧ x ≠ z ∧ y ≠ z ↔ ¬(x = y ∨ x = z) ∧ ¬y = z ∧ True
have mpr₅ : ¬(x = y ∨ x = z) → ¬y = z → True → y ≠ z
Tactic: tauto