awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
cf cg N O : ℕ
f g : R[X]
Cf : #f.support ≤ cf.succ
Cg : #g.support ≤ cg.succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have zero : ∀ (f : R[X]) (Cf : #f.support ≤ Nat.succ 0) (Nf : f.natDegree ≤ N), reflect (N + O) (f * g) = reflect N f * reflect O g
Tactic: induction cf generalizing f with
  | zero =>
    induction cg generalizing g with
    | zero =>
      rw [← C_mul_X_pow_eq_self Cf, ← C_mul_X_pow_eq_self Cg]
      simp_rw [mul_assoc, X_pow_mul, mul_assoc, ← pow_add (X : R[X]), reflect_C_mul,
        reflect_monomial, add_comm, revAt_add Nf Og, mul_assoc, X_pow_mul, mul_assoc, ←
        pow_add (X : R[X]), add_comm]
    | succ cg hcg =>
      by_cases g0 : g = 0
      · rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]
      rw [← eraseLead_add_C_mul_X_pow g, mul_add, reflect_add, reflect_add, mul_add, hcg, hcg] <;>
        try assumption
      · exact le_add_left card_support_C_mul_X_pow_le_one
      · exact le_trans (natDegree_C_mul_X_pow_le g.leadingCoeff g.natDegree) Og
      · exact Nat.lt_succ_iff.mp (lt_of_lt_of_le (eraseLead_support_card_lt g0) Cg)
      · exact le_trans eraseLead_natDegree_le_aux Og
  | succ cf hcf =>
    by_cases f0 : f = 0
    · rw [f0, reflect_zero, zero_mul, zero_mul, reflect_zero]
    rw [← eraseLead_add_C_mul_X_pow f, add_mul, reflect_add, reflect_add, add_mul, hcf, hcf] <;>
      try assumption
    · exact le_add_left card_support_C_mul_X_pow_le_one
    · exact le_trans (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree) Nf
    · exact Nat.lt_succ_iff.mp (lt_of_lt_of_le (eraseLead_support_card_lt f0) Cf)
    · exact le_trans eraseLead_natDegree_le_aux Nf
Cleared hypotheses: cf, f, Cf, Nf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
cf cg N O : ℕ
f g : R[X]
Cf : #f.support ≤ cf.succ
Cg : #g.support ≤ cg.succ
Nf : f.natDegree ≤ N
Og : g.natDegree ≤ O
zero :
  ∀ (f : R[X]) (Cf : #f.support ≤ Nat.succ 0) (Nf : f.natDegree ≤ N),
    reflect (N + O) (f * g) = reflect N f * reflect O g
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have succ : ∀ (cf : ℕ)
  (hcf :
    ∀ (f : R[X]) (Cf : #f.support ≤ cf.succ) (Nf : f.natDegree ≤ N),
      reflect (N + O) (f * g) = reflect N f * reflect O g)
  (f : R[X]) (Cf : #f.support ≤ (cf + 1).succ) (Nf : f.natDegree ≤ N),
  reflect (N + O) (f * g) = reflect N f * reflect O g
Tactic: induction cf generalizing f with
  | zero =>
    induction cg generalizing g with
    | zero =>
      rw [← C_mul_X_pow_eq_self Cf, ← C_mul_X_pow_eq_self Cg]
      simp_rw [mul_assoc, X_pow_mul, mul_assoc, ← pow_add (X : R[X]), reflect_C_mul,
        reflect_monomial, add_comm, revAt_add Nf Og, mul_assoc, X_pow_mul, mul_assoc, ←
        pow_add (X : R[X]), add_comm]
    | succ cg hcg =>
      by_cases g0 : g = 0
      · rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]
      rw [← eraseLead_add_C_mul_X_pow g, mul_add, reflect_add, reflect_add, mul_add, hcg, hcg] <;>
        try assumption
      · exact le_add_left card_support_C_mul_X_pow_le_one
      · exact le_trans (natDegree_C_mul_X_pow_le g.leadingCoeff g.natDegree) Og
      · exact Nat.lt_succ_iff.mp (lt_of_lt_of_le (eraseLead_support_card_lt g0) Cg)
      · exact le_trans eraseLead_natDegree_le_aux Og
  | succ cf hcf =>
    by_cases f0 : f = 0
    · rw [f0, reflect_zero, zero_mul, zero_mul, reflect_zero]
    rw [← eraseLead_add_C_mul_X_pow f, add_mul, reflect_add, reflect_add, add_mul, hcf, hcf] <;>
      try assumption
    · exact le_add_left card_support_C_mul_X_pow_le_one
    · exact le_trans (natDegree_C_mul_X_pow_le f.leadingCoeff f.natDegree) Nf
    · exact Nat.lt_succ_iff.mp (lt_of_lt_of_le (eraseLead_support_card_lt f0) Cf)
    · exact le_trans eraseLead_natDegree_le_aux Nf
Cleared hypotheses: cf, f, Cf, Nf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = eval₂ i x f
have refine_1 : (fun (f : R[X]) ↦
    eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = eval₂ i x f)
  0
Tactic: refine
    induction_with_natDegree_le (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) _ ?_ ?_
      ?_ f hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
refine_1 : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N 0) * x ^ N = eval₂ i x 0
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = eval₂ i x f
have refine_2 : ∀ (n : ℕ) (r : R),
  r ≠ 0 →
    n ≤ N →
      (fun (f : R[X]) ↦
          eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = eval₂ i x f)
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
Tactic: refine
    induction_with_natDegree_le (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) _ ?_ ?_
      ?_ f hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
refine_1 : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N 0) * x ^ N = eval₂ i x 0
refine_2 :
  ∀ (n : ℕ) (r : R),
    r ≠ 0 →
      n ≤ N →
        (fun (f : R[X]) ↦
            eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = eval₂ i x f)
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = eval₂ i x f
have refine_3 : ∀ (f g : R[X]),
  f.natDegree < g.natDegree →
    g.natDegree ≤ N →
      (fun (f : R[X]) ↦
            eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = eval₂ i x f)
          f →
        (fun (f : R[X]) ↦
              eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N =
                eval₂ i x f)
            g →
          (fun (f : R[X]) ↦
              eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N =
                eval₂ i x f)
            (f + g)
Tactic: refine
    induction_with_natDegree_le (fun f => eval₂ i (⅟x) (reflect N f) * x ^ N = eval₂ i x f) _ ?_ ?_
      ?_ f hf
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
h : r ≠ 0
hnN : n ≤ N
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _)
        (reflect N (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) *
      x ^ N =
    eval₂ i x (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))
have refine_2 : HMul.hMul (α := S) ((i : (a : R) → S) r : S) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
    x ^ N =
  HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
Tactic: simp only [revAt_le hnN, reflect_C_mul_X_pow, eval₂_X_pow, eval₂_C, eval₂_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
h : r ≠ 0
hnN : n ≤ N
| x ^ N
have rw : x ^ (N - n + n)
Tactic: rw [← Nat.sub_add_cancel hnN]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
h : r ≠ 0
hnN : n ≤ N
⊢ HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      x ^ N =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
have refine_2 : HMul.hMul (α := S) ((i : (a : R) → S) r : S) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
    x ^ (N - n + n) =
  HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
Tactic: conv in x ^ N => rw [← Nat.sub_add_cancel hnN]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
h : r ≠ 0
hnN : n ≤ N
⊢ HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      x ^ (N - n + n) =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
have refine_2 : HMul.hMul (α := S) ((i : (a : R) → S) r : S) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
    (x ^ (N - n) * x ^ n) =
  HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
Tactic: rw [pow_add, ← mul_assoc, mul_assoc (i r), ← mul_pow, invOf_mul_self, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
h : r ≠ 0
hnN : n ≤ N
refine_2 :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      (x ^ (N - n) * x ^ n) =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
⊢ HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      x ^ (N - n + n) =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
have refine_2₁ : HMul.hMul (α := S) ((i : (a : R) → S) r : S) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      x ^ (N - n) *
    x ^ n =
  HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
Tactic: rw [pow_add, ← mul_assoc, mul_assoc (i r), ← mul_pow, invOf_mul_self, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
h : r ≠ 0
hnN : n ≤ N
refine_2 :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      (x ^ (N - n) * x ^ n) =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₁ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
        x ^ (N - n) *
      x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
⊢ HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      x ^ (N - n + n) =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
have refine_2₂ : HMul.hMul (α := S) ((i : (a : R) → S) r : S)
      (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n) * x ^ (N - n)) *
    x ^ n =
  HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
Tactic: rw [pow_add, ← mul_assoc, mul_assoc (i r), ← mul_pow, invOf_mul_self, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
h : r ≠ 0
hnN : n ≤ N
refine_2 :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      (x ^ (N - n) * x ^ n) =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₁ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
        x ^ (N - n) *
      x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₂ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n) * x ^ (N - n)) *
      x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
⊢ HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      x ^ (N - n + n) =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
have refine_2₃ : HMul.hMul (α := S) ((i : (a : R) → S) r : S)
      ((@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ * x) ^ (N - n)) *
    x ^ n =
  HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
Tactic: rw [pow_add, ← mul_assoc, mul_assoc (i r), ← mul_pow, invOf_mul_self, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
h : r ≠ 0
hnN : n ≤ N
refine_2 :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      (x ^ (N - n) * x ^ n) =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₁ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
        x ^ (N - n) *
      x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₂ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n) * x ^ (N - n)) *
      x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₃ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        ((@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ * x) ^ (N - n)) *
      x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
⊢ HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      x ^ (N - n + n) =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
have refine_2₄ : HMul.hMul (α := S) ((i : (a : R) → S) r : S) (HPow.hPow (α := S) 1 (N - n)) * x ^ n =
  HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
Tactic: rw [pow_add, ← mul_assoc, mul_assoc (i r), ← mul_pow, invOf_mul_self, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
h : r ≠ 0
hnN : n ≤ N
refine_2 :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      (x ^ (N - n) * x ^ n) =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₁ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
        x ^ (N - n) *
      x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₂ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n) * x ^ (N - n)) *
      x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₃ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        ((@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ * x) ^ (N - n)) *
      x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₄ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S) (HPow.hPow (α := S) 1 (N - n)) * x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
⊢ HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      x ^ (N - n + n) =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
have refine_2₅ : HMul.hMul (α := S) (β := S) ((i : (a : R) → S) r : S) (1 : S) * x ^ n =
  HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
Tactic: rw [pow_add, ← mul_assoc, mul_assoc (i r), ← mul_pow, invOf_mul_self, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
n : ℕ
r : R
h : r ≠ 0
hnN : n ≤ N
refine_2 :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      (x ^ (N - n) * x ^ n) =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₁ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
          (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
        x ^ (N - n) *
      x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₂ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n) * x ^ (N - n)) *
      x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₃ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        ((@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ * x) ^ (N - n)) *
      x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₄ :
  HMul.hMul (α := S) ((i : (a : R) → S) r : S) (HPow.hPow (α := S) 1 (N - n)) * x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
refine_2₅ :
  HMul.hMul (α := S) (β := S) ((i : (a : R) → S) r : S) (1 : S) * x ^ n =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
⊢ HMul.hMul (α := S) ((i : (a : R) → S) r : S)
        (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _ ^ (N - n)) *
      x ^ (N - n + n) =
    HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
have refine_2₆ : HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n) = HMul.hMul (α := S) ((i : (a : R) → S) r : S) (x ^ n)
Tactic: rw [pow_add, ← mul_assoc, mul_assoc (i r), ← mul_pow, invOf_mul_self, one_pow, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
| eval₂ i x f = 0
have rw : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0
Tactic: rw [← eval₂_reflect_mul_pow i x N f hf]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0 ↔ eval₂ i x f = 0
have conv_rhs : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0 ↔
  eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0
Tactic: conv_rhs => rw [← eval₂_reflect_mul_pow i x N f hf]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0 ↔
    eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0
have mp : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0 →
  eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
mp :
  eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0 →
    eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0 ↔
    eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0
have mpr : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0 →
  eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0
have mp : 0 * x ^ N = 0
Tactic: rw [h, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0
mp : 0 * x ^ N = 0
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0
have mp₁ : Eq.{u_2 + 1} (α := S) 0 0
Tactic: rw [h, zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0
have mpr : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * 1 = 0
Tactic: rw [← mul_one (eval₂ i (⅟x) _), ← one_pow N, ← mul_invOf_self x, mul_pow, ← mul_assoc, h,
      zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0
mpr : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * 1 = 0
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0
have mpr₁ : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * HPow.hPow (α := S) 1 N = 0
Tactic: rw [← mul_one (eval₂ i (⅟x) _), ← one_pow N, ← mul_invOf_self x, mul_pow, ← mul_assoc, h,
      zero_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : CommSemiring S
i : R →+* S
x : S
inst_2 : Invertible x
N : ℕ
f : R[X]
hf : f.natDegree ≤ N
h : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * x ^ N = 0
mpr : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * 1 = 0
mpr₁ : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) * HPow.hPow (α := S) 1 N = 0
⊢ eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) = 0
have mpr₂ : eval₂ i (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) (reflect N f) *
    (x * @Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne x _) ^ N =
  0
Tactic: rw [← mul_one (eval₂ i (⅟x) _), ← one_pow N, ← mul_invOf_self x, mul_pow, ← mul_assoc, h,
      zero_mul]