awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.TerminatedStable (goal)
Goal:
K : Type u_1
g : GenContFract K
n m : ℕ
inst : DivisionRing K
n_lt_m : n < m
terminatedAt_n : g.TerminatedAt n
k : ℕ
hnk : n.succ ≤ n + k + 1
hk : g.contsAux (n + k + 1) = g.contsAux (n + 1)
⊢ g.contsAux (n + k + 1 + 1) = g.contsAux (n + 1)
have refine : g.TerminatedAt (n + k)
Tactic: refine (contsAux_stable_step_of_terminated ?_).trans hk
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.TerminatedStable (hypothesis)
Goal:
K : Type u_1
n : ℕ
inst : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.TerminatedAt n
⊢ convs'Aux s (n + 1) = convs'Aux s n
have terminatedAt_n₁ : s.get? n = none
Tactic: change s.get? n = none at terminatedAt_n
Cleared hypotheses: terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.TerminatedStable (hypothesis)
Goal:
K : Type u_1
n_1 : ℕ
inst : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? n = none), convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)
have this : s.tail.TerminatedAt n
Tactic: have : s.tail.TerminatedAt n := by
        simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminatedAt_n]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.TerminatedStable (hypothesis)
Goal:
K : Type u_1
n_1 : ℕ
inst : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? n = none), convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
this : s.tail.TerminatedAt n
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)
have this₁ : convs'Aux s.tail (n + 1) = convs'Aux s.tail n
Tactic: have := IH this
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.TerminatedStable (hypothesis)
Goal:
K : Type u_1
n_1 : ℕ
inst : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? n = none), convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
gp_head : Pair K
s_head_eq : s.head = some gp_head
this_1 : s.tail.TerminatedAt n
this : convs'Aux s.tail (n + 1) = convs'Aux s.tail n
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)
have this₁ : (match (motive := Option (Pair K) → K) s.tail.head with
  | none => 0
  | some gp => gp.a / (gp.b + convs'Aux s.tail.tail n)) =
  convs'Aux s.tail n
Tactic: rw [convs'Aux] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.TerminatedStable (goal)
Goal:
K : Type u_1
n_1 : ℕ
inst : DivisionRing K
n : ℕ
IH : ∀ {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? n = none), convs'Aux s (n + 1) = convs'Aux s n
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? (n + 1) = none
⊢ convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)
have succ : ∀ (x : Option (Pair K)) (s_head_eq : s.head = x), convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)
Tactic: cases s_head_eq : s.head with
    | none => simp only [convs'Aux, s_head_eq]
    | some gp_head =>
      have : s.tail.TerminatedAt n := by
        simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminatedAt_n]
      have := IH this
      rw [convs'Aux] at this
      simp [this, convs'Aux, s_head_eq]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.TerminatedStable (goal)
Goal:
K : Type u_1
n : ℕ
inst : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? n = none
⊢ convs'Aux s (n + 1) = convs'Aux s n
have zero : ∀ {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? 0 = none), convs'Aux s (HAdd.hAdd (α := ℕ) 0 1) = convs'Aux s 0
Tactic: induction n generalizing s with
  | zero => simp only [convs'Aux, terminatedAt_n, Stream'.Seq.head]
  | succ n IH =>
    cases s_head_eq : s.head with
    | none => simp only [convs'Aux, s_head_eq]
    | some gp_head =>
      have : s.tail.TerminatedAt n := by
        simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminatedAt_n]
      have := IH this
      rw [convs'Aux] at this
      simp [this, convs'Aux, s_head_eq]
Cleared hypotheses: s, terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.TerminatedStable (goal)
Goal:
K : Type u_1
n : ℕ
inst : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.get? n = none
zero :
  ∀ {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? 0 = none), convs'Aux s (HAdd.hAdd (α := ℕ) 0 1) = convs'Aux s 0
⊢ convs'Aux s (n + 1) = convs'Aux s n
have succ : ∀ (n : ℕ) (IH : ∀ {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? n = none), convs'Aux s (n + 1) = convs'Aux s n)
  {s : Stream'.Seq (Pair K)} (terminatedAt_n : s.get? (n + 1) = none), convs'Aux s (n + 1 + 1) = convs'Aux s (n + 1)
Tactic: induction n generalizing s with
  | zero => simp only [convs'Aux, terminatedAt_n, Stream'.Seq.head]
  | succ n IH =>
    cases s_head_eq : s.head with
    | none => simp only [convs'Aux, s_head_eq]
    | some gp_head =>
      have : s.tail.TerminatedAt n := by
        simp only [Stream'.Seq.TerminatedAt, s.get?_tail, terminatedAt_n]
      have := IH this
      rw [convs'Aux] at this
      simp [this, convs'Aux, s_head_eq]
Cleared hypotheses: s, terminatedAt_n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.TerminatedStable (goal)
Goal:
K : Type u_1
n m : ℕ
inst : DivisionRing K
s : Stream'.Seq (Pair K)
terminatedAt_n : s.TerminatedAt n
m_1 : ℕ
n_le_m : n.le m_1
IH : convs'Aux s m_1 = convs'Aux s n
⊢ convs'Aux s m_1.succ = convs'Aux s n
have step : s.TerminatedAt m_1
Tactic: refine (convs'Aux_stable_step_of_terminated (?_)).trans IH
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.TerminatedStable (goal)
Goal:
K : Type u_1
n m : ℕ
inst : DivisionRing K
s : Stream'.Seq (Pair K)
n_le_m : n ≤ m
terminatedAt_n : s.TerminatedAt n
⊢ convs'Aux s m = convs'Aux s n
have refl : convs'Aux s n = convs'Aux s n
Tactic: induction n_le_m with
  | refl => rfl
  | step n_le_m IH =>
    refine (convs'Aux_stable_step_of_terminated (?_)).trans IH
    exact s.terminated_stable n_le_m terminatedAt_n
Cleared hypotheses: n_le_m
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.TerminatedStable (goal)
Goal:
K : Type u_1
n m : ℕ
inst : DivisionRing K
s : Stream'.Seq (Pair K)
n_le_m : n ≤ m
terminatedAt_n : s.TerminatedAt n
refl : convs'Aux s n = convs'Aux s n
⊢ convs'Aux s m = convs'Aux s n
have step : ∀ {m : ℕ} (n_le_m : n.le m) (IH : convs'Aux s m = convs'Aux s n), convs'Aux s m.succ = convs'Aux s n
Tactic: induction n_le_m with
  | refl => rfl
  | step n_le_m IH =>
    refine (convs'Aux_stable_step_of_terminated (?_)).trans IH
    exact s.terminated_stable n_le_m terminatedAt_n
Cleared hypotheses: n_le_m
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Translations (goal)
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.partNums.get? n = none ↔ g.s.get? n = none
have none : ∀ (s_nth_eq : g.s.get? n = none), g.partNums.get? n = none ↔ Eq.{u_1 + 1} (α := Option (Pair α)) none none
Tactic: cases s_nth_eq : g.s.get? n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Translations (goal)
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
none :
  ∀ (s_nth_eq : g.s.get? n = Option.none),
    g.partNums.get? n = Option.none ↔ Eq.{u_1 + 1} (α := Option (Pair α)) Option.none Option.none
⊢ g.partNums.get? n = Option.none ↔ g.s.get? n = Option.none
have some : ∀ (val : Pair α) (s_nth_eq : g.s.get? n = some val), g.partNums.get? n = Option.none ↔ some val = Option.none
Tactic: cases s_nth_eq : g.s.get? n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Translations (goal)
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.TerminatedAt n ↔ g.partNums.get? n = none
have rw : g.s.get? n = none ↔ g.partNums.get? n = none
Tactic: rw [terminatedAt_iff_s_none, partNum_none_iff_s_none]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Translations (goal)
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
rw : g.s.get? n = none ↔ g.partNums.get? n = none
⊢ g.TerminatedAt n ↔ g.partNums.get? n = none
have rw₁ : g.s.get? n = none ↔ g.s.get? n = none
Tactic: rw [terminatedAt_iff_s_none, partNum_none_iff_s_none]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Translations (goal)
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.partDens.get? n = none ↔ g.s.get? n = none
have none : ∀ (s_nth_eq : g.s.get? n = none), g.partDens.get? n = none ↔ Eq.{u_1 + 1} (α := Option (Pair α)) none none
Tactic: cases s_nth_eq : g.s.get? n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Translations (goal)
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
none :
  ∀ (s_nth_eq : g.s.get? n = Option.none),
    g.partDens.get? n = Option.none ↔ Eq.{u_1 + 1} (α := Option (Pair α)) Option.none Option.none
⊢ g.partDens.get? n = Option.none ↔ g.s.get? n = Option.none
have some : ∀ (val : Pair α) (s_nth_eq : g.s.get? n = some val), g.partDens.get? n = Option.none ↔ some val = Option.none
Tactic: cases s_nth_eq : g.s.get? n
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Translations (goal)
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.TerminatedAt n ↔ g.partDens.get? n = none
have rw : g.s.get? n = none ↔ g.partDens.get? n = none
Tactic: rw [terminatedAt_iff_s_none, partDen_none_iff_s_none]
-- Lean 4 proof step from Mathlib.Algebra.ContinuedFractions.Translations (goal)
Goal:
α : Type u_1
g : GenContFract α
n : ℕ
rw : g.s.get? n = none ↔ g.partDens.get? n = none
⊢ g.TerminatedAt n ↔ g.partDens.get? n = none
have rw₁ : g.s.get? n = none ↔ g.s.get? n = none
Tactic: rw [terminatedAt_iff_s_none, partDen_none_iff_s_none]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
S : Type u_2
inst : CommRing S
w x y z : S
⊢ HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) w : S[X])
          (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := w, b := w * -(x + y + z), c := w * (x * y + x * z + y * z), d := w * -(x * y * z) }.toPoly
have simp : HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) w : S[X])
        (HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X])) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
    HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) w : S[X]) (HPow.hPow (α := S[X]) (β := ℕ) X 3) +
        HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) w : S[X])
            (-HAdd.hAdd (β := S[X])
                (HAdd.hAdd (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) ((C : (a : S) → S[X]) y : S[X]))
                ((C : (a : S) → S[X]) z : S[X])) *
          HPow.hPow (α := S[X]) (β := ℕ) X 2 +
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) w : S[X])
          (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) ((C : (a : S) → S[X]) y : S[X]) +
              HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) ((C : (a : S) → S[X]) z : S[X]) +
            HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) y : S[X]) ((C : (a : S) → S[X]) z : S[X])) *
        X +
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) w : S[X])
      (-HMul.hMul (β := S[X])
          (HMul.hMul (α := S[X]) (β := S[X]) ((C : (a : S) → S[X]) x : S[X]) ((C : (a : S) → S[X]) y : S[X]))
          ((C : (a : S) → S[X]) z : S[X]))
Tactic: simp only [toPoly, C_neg, C_add, C_mul]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
S : Type u_2
inst : CommRing S
x y z : S
⊢ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
have rw : 1 * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
    HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
  { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
Tactic: rw [← one_mul <| X - C x, ← C_1, C_mul_prod_X_sub_C_eq, one_mul, one_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
S : Type u_2
inst : CommRing S
x y z : S
rw :
  1 * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
⊢ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
have rw₁ : (C : (a : S) → S[X]) 1 * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
    HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
  { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
Tactic: rw [← one_mul <| X - C x, ← C_1, C_mul_prod_X_sub_C_eq, one_mul, one_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
S : Type u_2
inst : CommRing S
x y z : S
rw :
  1 * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
rw₁ :
  (C : (a : S) → S[X]) 1 * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
⊢ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
have rw₂ : Eq (α := S[X]) { a := 1, b := 1 * -(x + y + z), c := 1 * (x * y + x * z + y * z), d := 1 * -(x * y * z) }.toPoly
  { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
Tactic: rw [← one_mul <| X - C x, ← C_1, C_mul_prod_X_sub_C_eq, one_mul, one_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
S : Type u_2
inst : CommRing S
x y z : S
rw :
  1 * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
rw₁ :
  (C : (a : S) → S[X]) 1 * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
rw₂ :
  Eq (α := S[X]) { a := 1, b := 1 * -(x + y + z), c := 1 * (x * y + x * z + y * z), d := 1 * -(x * y * z) }.toPoly
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
⊢ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
have rw₃ : Eq (α := S[X]) { a := 1, b := -(x + y + z), c := 1 * (x * y + x * z + y * z), d := 1 * -(x * y * z) }.toPoly
  { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
Tactic: rw [← one_mul <| X - C x, ← C_1, C_mul_prod_X_sub_C_eq, one_mul, one_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
S : Type u_2
inst : CommRing S
x y z : S
rw :
  1 * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
rw₁ :
  (C : (a : S) → S[X]) 1 * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
rw₂ :
  Eq (α := S[X]) { a := 1, b := 1 * -(x + y + z), c := 1 * (x * y + x * z + y * z), d := 1 * -(x * y * z) }.toPoly
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
rw₃ :
  Eq (α := S[X]) { a := 1, b := -(x + y + z), c := 1 * (x * y + x * z + y * z), d := 1 * -(x * y * z) }.toPoly
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
⊢ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
have rw₄ : Eq (α := S[X]) { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := 1 * -(x * y * z) }.toPoly
  { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
Tactic: rw [← one_mul <| X - C x, ← C_1, C_mul_prod_X_sub_C_eq, one_mul, one_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
S : Type u_2
inst : CommRing S
x y z : S
rw :
  1 * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
rw₁ :
  (C : (a : S) → S[X]) 1 * HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
rw₂ :
  Eq (α := S[X]) { a := 1, b := 1 * -(x + y + z), c := 1 * (x * y + x * z + y * z), d := 1 * -(x * y * z) }.toPoly
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
rw₃ :
  Eq (α := S[X]) { a := 1, b := -(x + y + z), c := 1 * (x * y + x * z + y * z), d := 1 * -(x * y * z) }.toPoly
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
rw₄ :
  Eq (α := S[X]) { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := 1 * -(x * y * z) }.toPoly
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
⊢ HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) x : S[X]) *
        HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) y : S[X]) *
      HSub.hSub (α := S[X]) (β := S[X]) X ((C : (a : S) → S[X]) z : S[X]) =
    { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
have rw₅ : Eq (α := S[X]) { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
  { a := 1, b := -(x + y + z), c := x * y + x * z + y * z, d := -(x * y * z) }.toPoly
Tactic: rw [← one_mul <| X - C x, ← C_1, C_mul_prod_X_sub_C_eq, one_mul, one_mul, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P : Cubic R
inst : Semiring R
⊢ (∀ n > 3, coeff P.toPoly n = 0) ∧
    coeff P.toPoly 3 = P.a ∧ coeff P.toPoly 2 = P.b ∧ coeff P.toPoly 1 = P.c ∧ coeff P.toPoly 0 = P.d
have simp : (∀ n > 3,
    ((((if n = 3 then P.a else 0) + if n = 2 then P.b else 0) + if n = 1 then P.c else 0) + if n = 0 then P.d else 0) =
      0) ∧
  ((((if True then P.a else 0) + if Eq (α := ℕ) 3 2 then P.b else 0) + if Eq (α := ℕ) 3 1 then P.c else 0) +
        if Eq (α := ℕ) 3 0 then P.d else 0) =
      P.a ∧
    ((((if Eq (α := ℕ) 2 3 then P.a else 0) + if True then P.b else 0) + if Eq (α := ℕ) 2 1 then P.c else 0) +
          if Eq (α := ℕ) 2 0 then P.d else 0) =
        P.b ∧
      ((((if Eq (α := ℕ) 1 3 then P.a else 0) + if Eq (α := ℕ) 1 2 then P.b else 0) + if True then P.c else 0) +
            if Eq (α := ℕ) 1 0 then P.d else 0) =
          P.c ∧
        ((((if Eq (α := ℕ) 0 3 then P.a else 0) + if Eq (α := ℕ) 0 2 then P.b else 0) +
              if Eq (α := ℕ) 0 1 then P.c else 0) +
            if True then P.d else 0) =
          P.d
Tactic: simp only [Cubic.toPoly, Polynomial.coeff_add, Polynomial.coeff_C, Polynomial.coeff_C_mul_X,
    Polynomial.coeff_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P Q : Cubic R
inst : Semiring R
h : Eq (α := R[X]) P.toPoly Q.toPoly
⊢ P.a = Q.a
have rw : coeff P.toPoly 3 = Q.a
Tactic: rw [← coeff_eq_a, h, coeff_eq_a]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P Q : Cubic R
inst : Semiring R
h : Eq (α := R[X]) P.toPoly Q.toPoly
rw : coeff P.toPoly 3 = Q.a
⊢ P.a = Q.a
have rw₁ : coeff Q.toPoly 3 = Q.a
Tactic: rw [← coeff_eq_a, h, coeff_eq_a]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P Q : Cubic R
inst : Semiring R
h : Eq (α := R[X]) P.toPoly Q.toPoly
rw : coeff P.toPoly 3 = Q.a
rw₁ : coeff Q.toPoly 3 = Q.a
⊢ P.a = Q.a
have rw₂ : Q.a = Q.a
Tactic: rw [← coeff_eq_a, h, coeff_eq_a]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P Q : Cubic R
inst : Semiring R
h : Eq (α := R[X]) P.toPoly Q.toPoly
⊢ P.b = Q.b
have rw : coeff P.toPoly 2 = Q.b
Tactic: rw [← coeff_eq_b, h, coeff_eq_b]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P Q : Cubic R
inst : Semiring R
h : Eq (α := R[X]) P.toPoly Q.toPoly
rw : coeff P.toPoly 2 = Q.b
⊢ P.b = Q.b
have rw₁ : coeff Q.toPoly 2 = Q.b
Tactic: rw [← coeff_eq_b, h, coeff_eq_b]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P Q : Cubic R
inst : Semiring R
h : Eq (α := R[X]) P.toPoly Q.toPoly
rw : coeff P.toPoly 2 = Q.b
rw₁ : coeff Q.toPoly 2 = Q.b
⊢ P.b = Q.b
have rw₂ : Q.b = Q.b
Tactic: rw [← coeff_eq_b, h, coeff_eq_b]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P Q : Cubic R
inst : Semiring R
h : Eq (α := R[X]) P.toPoly Q.toPoly
⊢ P.c = Q.c
have rw : coeff P.toPoly 1 = Q.c
Tactic: rw [← coeff_eq_c, h, coeff_eq_c]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P Q : Cubic R
inst : Semiring R
h : Eq (α := R[X]) P.toPoly Q.toPoly
rw : coeff P.toPoly 1 = Q.c
⊢ P.c = Q.c
have rw₁ : coeff Q.toPoly 1 = Q.c
Tactic: rw [← coeff_eq_c, h, coeff_eq_c]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P Q : Cubic R
inst : Semiring R
h : Eq (α := R[X]) P.toPoly Q.toPoly
rw : coeff P.toPoly 1 = Q.c
rw₁ : coeff Q.toPoly 1 = Q.c
⊢ P.c = Q.c
have rw₂ : Q.c = Q.c
Tactic: rw [← coeff_eq_c, h, coeff_eq_c]
-- Lean 4 proof step from Mathlib.Algebra.CubicDiscriminant (goal)
Goal:
R : Type u_1
P Q : Cubic R
inst : Semiring R
h : Eq (α := R[X]) P.toPoly Q.toPoly
⊢ P.d = Q.d
have rw : coeff P.toPoly 0 = Q.d
Tactic: rw [← coeff_eq_d, h, coeff_eq_d]