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
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
zero :
  reflect (N + O)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) X f.natDegree *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))) =
    reflect N
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)) *
      reflect O
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))
zero₁ :
  reflect (N + O)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree) *
          HPow.hPow (α := R[X]) X f.natDegree)) =
    reflect N
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)) *
      reflect O
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))
⊢ reflect (N + O)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree) *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree)) =
    reflect N
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)) *
      reflect O
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))
have zero₂ : reflect (N + O)
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) X g.natDegree * HPow.hPow (α := R[X]) X f.natDegree))) =
  reflect N (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)) *
    reflect O (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
g : R[X]
Cg : #g.support ≤ Nat.succ 0
Og : g.natDegree ≤ O
zero :
  reflect (N + O)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) X f.natDegree *
          HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))) =
    reflect N
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)) *
      reflect O
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))
zero₁ :
  reflect (N + O)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree) *
          HPow.hPow (α := R[X]) X f.natDegree)) =
    reflect N
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)) *
      reflect O
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))
zero₂ :
  reflect (N + O)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X])
          (HPow.hPow (α := R[X]) X g.natDegree * HPow.hPow (α := R[X]) X f.natDegree))) =
    reflect N
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)) *
      reflect O
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))
⊢ reflect (N + O)
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree) *
        HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree)) =
    reflect N
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)) *
      reflect O
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))
have zero₃ : reflect (N + O)
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X])
        (HPow.hPow (α := R[X]) X (g.natDegree + f.natDegree)))) =
  reflect N (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)) *
    reflect O (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree))
Tactic: 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]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have pos : ∀ (g0 : g = 0), reflect (N + O) (f * g) = reflect N f * reflect O g
Tactic: by_cases g0 : g = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
pos : ∀ (g0 : g = 0), reflect (N + O) (f * g) = reflect N f * reflect O g
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have neg : ∀ (g0 : ¬g = 0), reflect (N + O) (f * g) = reflect N f * reflect O g
Tactic: by_cases g0 : g = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : g = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have pos : reflect (N + O) (f * 0) = reflect N f * reflect O 0
Tactic: rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : g = 0
pos : reflect (N + O) (f * 0) = reflect N f * reflect O 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have pos₁ : reflect (N + O) (f * 0) = reflect N f * 0
Tactic: rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : g = 0
pos : reflect (N + O) (f * 0) = reflect N f * reflect O 0
pos₁ : reflect (N + O) (f * 0) = reflect N f * 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have pos₂ : reflect (N + O) 0 = reflect N f * 0
Tactic: rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : g = 0
pos : reflect (N + O) (f * 0) = reflect N f * reflect O 0
pos₁ : reflect (N + O) (f * 0) = reflect N f * 0
pos₂ : reflect (N + O) 0 = reflect N f * 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have pos₃ : Eq.{u_1 + 1} (α := R[X]) (reflect (N + O) 0) 0
Tactic: rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : g = 0
pos : reflect (N + O) (f * 0) = reflect N f * reflect O 0
pos₁ : reflect (N + O) (f * 0) = reflect N f * 0
pos₂ : reflect (N + O) 0 = reflect N f * 0
pos₃ : Eq.{u_1 + 1} (α := R[X]) (reflect (N + O) 0) 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have pos₄ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [g0, reflect_zero, mul_zero, mul_zero, reflect_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have neg : #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree)).support ≤
  cg.succ
Tactic: rw [← eraseLead_add_C_mul_X_pow g, mul_add, reflect_add, reflect_add, mul_add, hcg, hcg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
neg :
  #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree)).support ≤
    cg.succ
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have neg₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree)).natDegree ≤ O
Tactic: rw [← eraseLead_add_C_mul_X_pow g, mul_add, reflect_add, reflect_add, mul_add, hcg, hcg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
neg :
  #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree)).support ≤
    cg.succ
neg₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree)).natDegree ≤
    O
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have neg₂ : #g.eraseLead.support ≤ cg.succ
Tactic: rw [← eraseLead_add_C_mul_X_pow g, mul_add, reflect_add, reflect_add, mul_add, hcg, hcg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
N O : ℕ
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
cg : ℕ
hcg :
  ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
g : R[X]
Cg : #g.support ≤ (cg + 1).succ
Og : g.natDegree ≤ O
g0 : ¬g = 0
neg :
  #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree)).support ≤
    cg.succ
neg₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) g.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X g.natDegree)).natDegree ≤
    O
neg₂ : #g.eraseLead.support ≤ cg.succ
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have neg₃ : g.eraseLead.natDegree ≤ O
Tactic: rw [← eraseLead_add_C_mul_X_pow g, mul_add, reflect_add, reflect_add, mul_add, hcg, hcg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have zero : ∀ (g : R[X]) (Cg : #g.support ≤ Nat.succ 0) (Og : g.natDegree ≤ O), reflect (N + O) (f * g) = reflect N f * reflect O g
Tactic: 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
Cleared hypotheses: cg, g, Cg, Og
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
f : R[X]
Cf : #f.support ≤ Nat.succ 0
Nf : f.natDegree ≤ N
zero :
  ∀ (g : R[X]) (Cg : #g.support ≤ Nat.succ 0) (Og : g.natDegree ≤ O),
    reflect (N + O) (f * g) = reflect N f * reflect O g
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have zero₁ : ∀ (cg : ℕ)
  (hcg :
    ∀ (g : R[X]) (Cg : #g.support ≤ cg.succ) (Og : g.natDegree ≤ O),
      reflect (N + O) (f * g) = reflect N f * reflect O g)
  (g : R[X]) (Cg : #g.support ≤ (cg + 1).succ) (Og : g.natDegree ≤ O),
  reflect (N + O) (f * g) = reflect N f * reflect O g
Tactic: 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
Cleared hypotheses: cg, g, Cg, Og
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
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
have pos : ∀ (f0 : f = 0), reflect (N + O) (f * g) = reflect N f * reflect O g
Tactic: by_cases f0 : f = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
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
pos : ∀ (f0 : f = 0), reflect (N + O) (f * g) = reflect N f * reflect O g
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have neg : ∀ (f0 : ¬f = 0), reflect (N + O) (f * g) = reflect N f * reflect O g
Tactic: by_cases f0 : f = 0
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
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
f0 : f = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have pos : reflect (N + O) (0 * g) = reflect N 0 * reflect O g
Tactic: rw [f0, reflect_zero, zero_mul, zero_mul, reflect_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
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
f0 : f = 0
pos : reflect (N + O) (0 * g) = reflect N 0 * reflect O g
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have pos₁ : reflect (N + O) (0 * g) = 0 * reflect O g
Tactic: rw [f0, reflect_zero, zero_mul, zero_mul, reflect_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
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
f0 : f = 0
pos : reflect (N + O) (0 * g) = reflect N 0 * reflect O g
pos₁ : reflect (N + O) (0 * g) = 0 * reflect O g
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have pos₂ : reflect (N + O) 0 = 0 * reflect O g
Tactic: rw [f0, reflect_zero, zero_mul, zero_mul, reflect_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
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
f0 : f = 0
pos : reflect (N + O) (0 * g) = reflect N 0 * reflect O g
pos₁ : reflect (N + O) (0 * g) = 0 * reflect O g
pos₂ : reflect (N + O) 0 = 0 * reflect O g
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have pos₃ : Eq.{u_1 + 1} (α := R[X]) (reflect (N + O) 0) 0
Tactic: rw [f0, reflect_zero, zero_mul, zero_mul, reflect_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
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
f0 : f = 0
pos : reflect (N + O) (0 * g) = reflect N 0 * reflect O g
pos₁ : reflect (N + O) (0 * g) = 0 * reflect O g
pos₂ : reflect (N + O) 0 = 0 * reflect O g
pos₃ : Eq.{u_1 + 1} (α := R[X]) (reflect (N + O) 0) 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have pos₄ : Eq.{u_1 + 1} (α := R[X]) 0 0
Tactic: rw [f0, reflect_zero, zero_mul, zero_mul, reflect_zero]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
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
f0 : ¬f = 0
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have neg : #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).support ≤
  cf.succ
Tactic: rw [← eraseLead_add_C_mul_X_pow f, add_mul, reflect_add, reflect_add, add_mul, hcf, hcf]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
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
f0 : ¬f = 0
neg :
  #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).support ≤
    cf.succ
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have neg₁ : (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree ≤ N
Tactic: rw [← eraseLead_add_C_mul_X_pow f, add_mul, reflect_add, reflect_add, add_mul, hcf, hcf]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
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
f0 : ¬f = 0
neg :
  #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).support ≤
    cf.succ
neg₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree ≤
    N
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have neg₂ : #f.eraseLead.support ≤ cf.succ
Tactic: rw [← eraseLead_add_C_mul_X_pow f, add_mul, reflect_add, reflect_add, add_mul, hcf, hcf]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Reverse (goal)
Goal:
R : Type u_1
inst : Semiring R
cg N O : ℕ
g : R[X]
Cg : #g.support ≤ cg.succ
Og : g.natDegree ≤ O
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
f0 : ¬f = 0
neg :
  #(HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).support ≤
    cf.succ
neg₁ :
  (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) f.leadingCoeff : R[X]) (HPow.hPow (α := R[X]) X f.natDegree)).natDegree ≤
    N
neg₂ : #f.eraseLead.support ≤ cf.succ
⊢ reflect (N + O) (f * g) = reflect N f * reflect O g
have neg₃ : f.eraseLead.natDegree ≤ N
Tactic: rw [← eraseLead_add_C_mul_X_pow f, add_mul, reflect_add, reflect_add, add_mul, hcf, hcf]