awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p q : R[X]
rw : (HSMul.hSMul (β := R) s 1 • p).comp q = s • p.comp q
rw₁ : eval₂ C q (HSMul.hSMul (β := R) s 1 • p) = s • p.comp q
rw₂ : eval₂ C q (HSMul.hSMul (β := R) s 1 • p) = s • eval₂ C q p
rw₃ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HSMul.hSMul (β := R) s 1) : R[X]) (eval₂ C q p) = s • eval₂ C q p
rw₄ : HSMul.hSMul (β := R) s 1 • eval₂ C q p = s • eval₂ C q p
⊢ (s • p).comp q = s • p.comp q
have rw₅ : s • HSMul.hSMul (α := R) 1 (eval₂ C q p) = s • eval₂ C q p
Tactic: rw [← smul_one_smul R s p, comp, comp, eval₂_smul, ← smul_eq_C_mul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : SMulZeroClass S R
inst_2 : IsScalarTower S R R
s : S
p q : R[X]
rw : (HSMul.hSMul (β := R) s 1 • p).comp q = s • p.comp q
rw₁ : eval₂ C q (HSMul.hSMul (β := R) s 1 • p) = s • p.comp q
rw₂ : eval₂ C q (HSMul.hSMul (β := R) s 1 • p) = s • eval₂ C q p
rw₃ : HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (HSMul.hSMul (β := R) s 1) : R[X]) (eval₂ C q p) = s • eval₂ C q p
rw₄ : HSMul.hSMul (β := R) s 1 • eval₂ C q p = s • eval₂ C q p
rw₅ : s • HSMul.hSMul (α := R) 1 (eval₂ C q p) = s • eval₂ C q p
⊢ (s • p).comp q = s • p.comp q
have rw₆ : s • eval₂ C q p = s • eval₂ C q p
Tactic: rw [← smul_one_smul R s p, comp, comp, eval₂_smul, ← smul_eq_C_mul, smul_assoc, one_smul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
r : R
⊢ map f (r • p) = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (map f p)
have rw : eval₂ (RingHom.comp C f) X (r • p) = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (eval₂ (RingHom.comp C f) X p)
Tactic: rw [map, eval₂_smul, RingHom.comp_apply, C_mul']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
r : R
rw : eval₂ (RingHom.comp C f) X (r • p) = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (eval₂ (RingHom.comp C f) X p)
⊢ map f (r • p) = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (map f p)
have rw₁ : HMul.hMul (α := S[X]) ((RingHom.comp C f : (a : R) → S[X]) r : S[X]) (eval₂ (RingHom.comp C f) X p) =
  HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (eval₂ (RingHom.comp C f) X p)
Tactic: rw [map, eval₂_smul, RingHom.comp_apply, C_mul']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
r : R
rw : eval₂ (RingHom.comp C f) X (r • p) = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (eval₂ (RingHom.comp C f) X p)
rw₁ :
  HMul.hMul (α := S[X]) ((RingHom.comp C f : (a : R) → S[X]) r : S[X]) (eval₂ (RingHom.comp C f) X p) =
    HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (eval₂ (RingHom.comp C f) X p)
⊢ map f (r • p) = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (map f p)
have rw₂ : HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X]) (eval₂ (RingHom.comp C f) X p) =
  HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (eval₂ (RingHom.comp C f) X p)
Tactic: rw [map, eval₂_smul, RingHom.comp_apply, C_mul']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.SMul (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
p : R[X]
inst_1 : Semiring S
f : R →+* S
r : R
rw : eval₂ (RingHom.comp C f) X (r • p) = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (eval₂ (RingHom.comp C f) X p)
rw₁ :
  HMul.hMul (α := S[X]) ((RingHom.comp C f : (a : R) → S[X]) r : S[X]) (eval₂ (RingHom.comp C f) X p) =
    HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (eval₂ (RingHom.comp C f) X p)
rw₂ :
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) r) : S[X]) (eval₂ (RingHom.comp C f) X p) =
    HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (eval₂ (RingHom.comp C f) X p)
⊢ map f (r • p) = HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (map f p)
have rw₃ : HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (eval₂ (RingHom.comp C f) X p) =
  HSMul.hSMul (α := S) ((f : (a : R) → S) r : S) (eval₂ (RingHom.comp C f) X p)
Tactic: rw [map, eval₂_smul, RingHom.comp_apply, C_mul']
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Subring (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
⊢ p ∈ (mapRingHom f).rangeS ↔ ∀ (n : ℕ), p.coeff n ∈ f.rangeS
have mp : p ∈ (mapRingHom f).rangeS → ∀ (n : ℕ), p.coeff n ∈ f.rangeS
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Subring (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
mp : p ∈ (mapRingHom f).rangeS → ∀ (n : ℕ), p.coeff n ∈ f.rangeS
⊢ p ∈ (mapRingHom f).rangeS ↔ ∀ (n : ℕ), p.coeff n ∈ f.rangeS
have mpr : (∀ (n : ℕ), p.coeff n ∈ f.rangeS) → p ∈ (mapRingHom f).rangeS
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Subring (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : R[X]
n : ℕ
⊢ coeff ((mapRingHom f : (a : R[X]) → S[X]) p) n ∈ f.rangeS
have mp : Membership.mem (α := S) f.rangeS ((f : (a : R) → S) (p.coeff n) : S)
Tactic: rw [coe_mapRingHom, coeff_map]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Subring (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
⊢ p ∈ (mapRingHom f).rangeS
have mpr : ∑ i ∈ Finset.range (p.natDegree + 1),
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i) ∈
  (mapRingHom f).rangeS
Tactic: rw [p.as_sum_range_C_mul_X_pow]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Subring (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
⊢ ∑ i ∈ Finset.range (p.natDegree + 1),
      HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i) ∈
    (mapRingHom f).rangeS
have mpr : ∀ c ∈ Finset.range (p.natDegree + 1),
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff c) : S[X]) (HPow.hPow (α := S[X]) X c) ∈ (mapRingHom f).rangeS
Tactic: refine (mapRingHom f).rangeS.sum_mem ?_
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Subring (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
⊢ HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i) ∈ (mapRingHom f).rangeS
have mpr : ∀ (c : R) (hc : (f : (a : R) → S) c = p.coeff i),
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i) ∈ (mapRingHom f).rangeS
Tactic: rcases h i with ⟨c, hc⟩
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Subring (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : (f : (a : R) → S) c = p.coeff i
⊢ HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i) ∈ (mapRingHom f).rangeS
have h₁ : (mapRingHom f : (a : R[X]) → S[X]) (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X i)) =
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
Tactic: use C c * X ^ i
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Subring (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : (f : (a : R) → S) c = p.coeff i
⊢ (mapRingHom f : (a : R[X]) → S[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
have h₁ : map f (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X i)) =
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
Tactic: rw [coe_mapRingHom, Polynomial.map_mul, map_C, hc, Polynomial.map_pow, map_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Subring (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : (f : (a : R) → S) c = p.coeff i
h₁ :
  map f (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
⊢ (mapRingHom f : (a : R[X]) → S[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
have h₂ : map f ((C : (a : R) → R[X]) c) * map f (HPow.hPow (α := R[X]) X i) =
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
Tactic: rw [coe_mapRingHom, Polynomial.map_mul, map_C, hc, Polynomial.map_pow, map_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Subring (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : (f : (a : R) → S) c = p.coeff i
h₁ :
  map f (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
h₂ :
  map f ((C : (a : R) → R[X]) c) * map f (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
⊢ (mapRingHom f : (a : R[X]) → S[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
have h₃ : HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) c) : S[X]) (map f (HPow.hPow (α := R[X]) X i)) =
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
Tactic: rw [coe_mapRingHom, Polynomial.map_mul, map_C, hc, Polynomial.map_pow, map_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Subring (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : (f : (a : R) → S) c = p.coeff i
h₁ :
  map f (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
h₂ :
  map f ((C : (a : R) → R[X]) c) * map f (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
h₃ :
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) c) : S[X]) (map f (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
⊢ (mapRingHom f : (a : R[X]) → S[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
have h₄ : HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (map f (HPow.hPow (α := R[X]) X i)) =
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
Tactic: rw [coe_mapRingHom, Polynomial.map_mul, map_C, hc, Polynomial.map_pow, map_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Subring (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : (f : (a : R) → S) c = p.coeff i
h₁ :
  map f (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
h₂ :
  map f ((C : (a : R) → R[X]) c) * map f (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
h₃ :
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) c) : S[X]) (map f (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
h₄ :
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (map f (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
⊢ (mapRingHom f : (a : R[X]) → S[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
have h₅ : HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (map f X ^ i) =
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
Tactic: rw [coe_mapRingHom, Polynomial.map_mul, map_C, hc, Polynomial.map_pow, map_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Eval.Subring (goal)
Goal:
R : Type u
S : Type v
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
p : S[X]
h : ∀ (n : ℕ), p.coeff n ∈ f.rangeS
i : ℕ
_hi : i ∈ Finset.range (p.natDegree + 1)
c : R
hc : (f : (a : R) → S) c = p.coeff i
h₁ :
  map f (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
h₂ :
  map f ((C : (a : R) → R[X]) c) * map f (HPow.hPow (α := R[X]) X i) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
h₃ :
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) ((f : (a : R) → S) c) : S[X]) (map f (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
h₄ :
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (map f (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
h₅ :
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (map f X ^ i) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
⊢ (mapRingHom f : (a : R[X]) → S[X])
      (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) c : R[X]) (HPow.hPow (α := R[X]) X i)) =
    HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
have h₆ : HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i) =
  HMul.hMul (α := S[X]) ((C : (a : S) → S[X]) (p.coeff i) : S[X]) (HPow.hPow (α := S[X]) X i)
Tactic: rw [coe_mapRingHom, Polynomial.map_mul, map_C, hc, Polynomial.map_pow, map_X]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
r : R
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((monomial q : (a : R) → R[X]) r) : R[X])
    ((monomial (q * p) : (a : R) → R[X]) r : R[X])
have simp_rw : (expand R p : (a : R[X]) → R[X]) (r • HPow.hPow (α := R[X]) X q) = r • HPow.hPow (α := R[X]) X (q * p)
Tactic: simp_rw [← smul_X_eq_monomial, map_smul, map_pow, expand_X, mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
r : R
simp_rw : (expand R p : (a : R[X]) → R[X]) (r • HPow.hPow (α := R[X]) X q) = r • HPow.hPow (α := R[X]) X (q * p)
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((monomial q : (a : R) → R[X]) r) : R[X])
    ((monomial (q * p) : (a : R) → R[X]) r : R[X])
have simp_rw₁ : HSMul.hSMul (β := R[X]) r ((expand R p : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X q) : R[X]) =
  r • HPow.hPow (α := R[X]) X (q * p)
Tactic: simp_rw [← smul_X_eq_monomial, map_smul, map_pow, expand_X, mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
r : R
simp_rw : (expand R p : (a : R[X]) → R[X]) (r • HPow.hPow (α := R[X]) X q) = r • HPow.hPow (α := R[X]) X (q * p)
simp_rw₁ :
  HSMul.hSMul (β := R[X]) r ((expand R p : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X q) : R[X]) =
    r • HPow.hPow (α := R[X]) X (q * p)
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((monomial q : (a : R) → R[X]) r) : R[X])
    ((monomial (q * p) : (a : R) → R[X]) r : R[X])
have simp_rw₂ : r • HPow.hPow (α := R[X]) ((expand R p : (a : R[X]) → R[X]) X : R[X]) q = r • HPow.hPow (α := R[X]) X (q * p)
Tactic: simp_rw [← smul_X_eq_monomial, map_smul, map_pow, expand_X, mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
r : R
simp_rw : (expand R p : (a : R[X]) → R[X]) (r • HPow.hPow (α := R[X]) X q) = r • HPow.hPow (α := R[X]) X (q * p)
simp_rw₁ :
  HSMul.hSMul (β := R[X]) r ((expand R p : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X q) : R[X]) =
    r • HPow.hPow (α := R[X]) X (q * p)
simp_rw₂ : r • HPow.hPow (α := R[X]) ((expand R p : (a : R[X]) → R[X]) X : R[X]) q = r • HPow.hPow (α := R[X]) X (q * p)
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((monomial q : (a : R) → R[X]) r) : R[X])
    ((monomial (q * p) : (a : R) → R[X]) r : R[X])
have simp_rw₃ : r • HPow.hPow (α := R[X]) X p ^ q = r • HPow.hPow (α := R[X]) X (q * p)
Tactic: simp_rw [← smul_X_eq_monomial, map_smul, map_pow, expand_X, mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
r : R
simp_rw : (expand R p : (a : R[X]) → R[X]) (r • HPow.hPow (α := R[X]) X q) = r • HPow.hPow (α := R[X]) X (q * p)
simp_rw₁ :
  HSMul.hSMul (β := R[X]) r ((expand R p : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X q) : R[X]) =
    r • HPow.hPow (α := R[X]) X (q * p)
simp_rw₂ : r • HPow.hPow (α := R[X]) ((expand R p : (a : R[X]) → R[X]) X : R[X]) q = r • HPow.hPow (α := R[X]) X (q * p)
simp_rw₃ : r • HPow.hPow (α := R[X]) X p ^ q = r • HPow.hPow (α := R[X]) X (q * p)
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((monomial q : (a : R) → R[X]) r) : R[X])
    ((monomial (q * p) : (a : R) → R[X]) r : R[X])
have simp_rw₄ : r • HPow.hPow (α := R[X]) X p ^ q = r • HPow.hPow (α := R[X]) X (p * q)
Tactic: simp_rw [← smul_X_eq_monomial, map_smul, map_pow, expand_X, mul_comm, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f_1 f g : R[X]
ihf :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) f) : R[X])
    ((expand R (p * q) : (a : R[X]) → R[X]) f : R[X])
ihg :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) g) : R[X])
    ((expand R (p * q) : (a : R[X]) → R[X]) g : R[X])
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) (f + g)) : R[X])
    ((expand R (p * q) : (a : R[X]) → R[X]) (f + g) : R[X])
have simp_rw : HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) f) : R[X])
    ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) g) : R[X]) =
  HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) f : R[X])
    ((expand R (p * q) : (a : R[X]) → R[X]) g : R[X])
Tactic: simp_rw [map_add, ihf, ihg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f_1 f g : R[X]
ihf :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) f) : R[X])
    ((expand R (p * q) : (a : R[X]) → R[X]) f : R[X])
ihg :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) g) : R[X])
    ((expand R (p * q) : (a : R[X]) → R[X]) g : R[X])
simp_rw :
  HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) f) : R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) g) : R[X]) =
    HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) f : R[X])
      ((expand R (p * q) : (a : R[X]) → R[X]) g : R[X])
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) (f + g)) : R[X])
    ((expand R (p * q) : (a : R[X]) → R[X]) (f + g) : R[X])
have simp_rw₁ : HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) f : R[X])
    ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) g) : R[X]) =
  HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) f : R[X])
    ((expand R (p * q) : (a : R[X]) → R[X]) g : R[X])
Tactic: simp_rw [map_add, ihf, ihg]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
h :
  Eq (α := R[X])
    ((expand R p : (a : R[X]) → R[X])
        ((expand R q : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) :
      R[X])
    ((expand R (p * q) : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) :
      R[X])
⊢ Eq (α := R[X])
    ((expand R p : (a : R[X]) → R[X])
        ((expand R q : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))) :
      R[X])
    ((expand R (p * q) : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
      R[X])
have simp_rw : HMul.hMul (α := R[X]) (β := R[X])
    ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)) : R[X])
    ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1))) : R[X]) =
  HMul.hMul (α := R[X]) (β := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X])
    ((expand R (p * q) : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X])
Tactic: simp_rw [map_mul, expand_C, map_pow, expand_X, map_pow, expand_X, pow_mul]
-- Lean 4 proof step from Mathlib.Algebra.Polynomial.Expand (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : ℕ
f : R[X]
n : ℕ
r : R
h :
  Eq (α := R[X])
    ((expand R p : (a : R[X]) → R[X])
        ((expand R q : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n))) :
      R[X])
    ((expand R (p * q) : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X n)) :
      R[X])
simp_rw :
  HMul.hMul (α := R[X]) (β := R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r)) : R[X])
      ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1))) : R[X]) =
    HMul.hMul (α := R[X]) (β := R[X]) ((expand R (p * q) : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X])
      ((expand R (p * q) : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X])
⊢ Eq (α := R[X])
    ((expand R p : (a : R[X]) → R[X])
        ((expand R q : (a : R[X]) → R[X])
          (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1)))) :
      R[X])
    ((expand R (p * q) : (a : R[X]) → R[X])
        (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) r : R[X]) (HPow.hPow (α := R[X]) X (n + 1))) :
      R[X])
have simp_rw₁ : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
    ((expand R p : (a : R[X]) → R[X]) ((expand R q : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1))) : R[X]) =
  HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) r : R[X])
    ((expand R (p * q) : (a : R[X]) → R[X]) (HPow.hPow (α := R[X]) X (n + 1)) : R[X])
Tactic: simp_rw [map_mul, expand_C, map_pow, expand_X, map_pow, expand_X, pow_mul]