awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
q : MvPolynomial σ R
i : σ
hi : i ∈ n.support
n' : σ →₀ ℕ := n - Finsupp.single i 1
hn' : n' + Finsupp.single i 1 = n
hnn' : n' ≤ n
hd' : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n' = d
p' : MvPolynomial σ R
hp_1 : X i ∣ X i * p' ∧ (X i * p').divMonomial (Finsupp.single i 1) ∣ (monomial n' : (a : R) → MvPolynomial σ R) 1 * q
m : σ →₀ ℕ
r : MvPolynomial σ R
hm : m ≤ n'
hr : r ∣ q
hp : (X i * p').divMonomial (Finsupp.single i 1) = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
right : X i * p' = (monomial (m + Finsupp.single i 1) : (a : R) → MvPolynomial σ R) 1 * r
⊢ ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ X i * p' = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
have left : m + Finsupp.single i 1 ≤ n
Tactic: use m + Finsupp.single i 1, r, ?_, hr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
h : ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hrq : r ∣ q
hp : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q
have inr : (monomial m : (a : R) → MvPolynomial σ R) 1 * r ∣
  (monomial m : (a : R) → MvPolynomial σ R) 1 * ((monomial (n - m) : (a : R) → MvPolynomial σ R) 1 * q)
Tactic: rw [hp, ← add_tsub_cancel_of_le hmn, ← mul_one 1, ← monomial_mul, mul_one, mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p_1 q_1 : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n_1 : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
hd :
  ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
n : σ →₀ ℕ
hn : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1
p q : MvPolynomial σ R
h : ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
m : σ →₀ ℕ
r : MvPolynomial σ R
hmn : m ≤ n
hrq : r ∣ q
hp : p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ (monomial m : (a : R) → MvPolynomial σ R) 1 * r ∣
    (monomial m : (a : R) → MvPolynomial σ R) 1 * ((monomial (n - m) : (a : R) → MvPolynomial σ R) 1 * q)
have inr : r ∣ (monomial (n - m) : (a : R) → MvPolynomial σ R) 1 * q
Tactic: apply mul_dvd_mul dvd_rfl
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
⊢ ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
have inr : ∀ (n : σ →₀ ℕ) (hd : Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n : ℕ) (0 : ℕ)) (p q : MvPolynomial σ R),
  p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
    ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
Tactic: induction d with
  | zero =>
    intro n hn p
    rw [Finsupp.degree_eq_zero_iff] at hn
    simp only [hn, monomial_zero', C_1, one_mul, nonpos_iff_eq_zero, exists_and_left,
      exists_eq_left, exists_eq_right', implies_true]
  | succ d hd =>
    intro n hn p q
    refine ⟨fun hp ↦ ?_, fun ⟨m, r, hmn, hrq, hp⟩ ↦ ?_⟩
    · obtain ⟨i, hi⟩ : n.support.Nonempty := by
        rw [Finsupp.support_nonempty_iff]
        intro hn'
        simp [hn'] at hn
      let n' := n - Finsupp.single i 1
      have hn' : n' + Finsupp.single i 1 = n := by
        apply Finsupp.sub_add_single_one_cancel
        rwa [← Finsupp.mem_support_iff]
      have hnn' : n' ≤ n := by simp [← hn']
      have hd' : n'.degree = d := by
        rw [← add_left_inj, ← hn, ← hn']
        simp
      rw [← hn', monomial_add_single, pow_one, mul_comm _ (X i), mul_assoc, dvd_X_mul_iff] at hp
      rcases hp with hp | hp
      · obtain ⟨m, r, hm, hr, hp⟩ := (hd n' hd' p q).mp hp
        exact ⟨m, r, le_trans hm hnn', hr, hp⟩
      · obtain ⟨p', rfl⟩ := hp.1
        obtain ⟨m, r, hm, hr, hp⟩ := (hd n' hd' _ _).mp hp.2
        use m + Finsupp.single i 1, r, ?_, hr
        · simp [monomial_add_single, pow_one, mul_comm _ (X i), mul_assoc, ← hp]
        · simpa [← hn'] using hm
    · rw [hp, ← add_tsub_cancel_of_le hmn, ← mul_one 1, ← monomial_mul, mul_one, mul_assoc]
      apply mul_dvd_mul dvd_rfl
      apply dvd_mul_of_dvd_right hrq
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Division (goal)
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n : σ →₀ ℕ
hR : Nontrivial R
d : ℕ
inr :
  ∀ (n : σ →₀ ℕ) (hd : Eq (α := ℕ) ((Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n : ℕ) (0 : ℕ)) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
⊢ ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
    p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
      ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
have inr₁ : ∀ (d : ℕ)
  (hd :
    ∀ (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d) (p q : MvPolynomial σ R),
      p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
        ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r)
  (n : σ →₀ ℕ) (hd : (Finsupp.degree : (a : σ →₀ ℕ) → ℕ) n = d + 1) (p q : MvPolynomial σ R),
  p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q ↔
    ∃ (m : σ →₀ ℕ) (r : MvPolynomial σ R), m ≤ n ∧ r ∣ q ∧ p = (monomial m : (a : R) → MvPolynomial σ R) 1 * r
Tactic: induction d with
  | zero =>
    intro n hn p
    rw [Finsupp.degree_eq_zero_iff] at hn
    simp only [hn, monomial_zero', C_1, one_mul, nonpos_iff_eq_zero, exists_and_left,
      exists_eq_left, exists_eq_right', implies_true]
  | succ d hd =>
    intro n hn p q
    refine ⟨fun hp ↦ ?_, fun ⟨m, r, hmn, hrq, hp⟩ ↦ ?_⟩
    · obtain ⟨i, hi⟩ : n.support.Nonempty := by
        rw [Finsupp.support_nonempty_iff]
        intro hn'
        simp [hn'] at hn
      let n' := n - Finsupp.single i 1
      have hn' : n' + Finsupp.single i 1 = n := by
        apply Finsupp.sub_add_single_one_cancel
        rwa [← Finsupp.mem_support_iff]
      have hnn' : n' ≤ n := by simp [← hn']
      have hd' : n'.degree = d := by
        rw [← add_left_inj, ← hn, ← hn']
        simp
      rw [← hn', monomial_add_single, pow_one, mul_comm _ (X i), mul_assoc, dvd_X_mul_iff] at hp
      rcases hp with hp | hp
      · obtain ⟨m, r, hm, hr, hp⟩ := (hd n' hd' p q).mp hp
        exact ⟨m, r, le_trans hm hnn', hr, hp⟩
      · obtain ⟨p', rfl⟩ := hp.1
        obtain ⟨m, r, hm, hr, hp⟩ := (hd n' hd' _ _).mp hp.2
        use m + Finsupp.single i 1, r, ?_, hr
        · simp [monomial_add_single, pow_one, mul_comm _ (X i), mul_assoc, ← hp]
        · simpa [← hn'] using hm
    · rw [hp, ← add_tsub_cancel_of_le hmn, ← mul_one 1, ← monomial_mul, mul_one, mul_assoc]
      apply mul_dvd_mul dvd_rfl
      apply dvd_mul_of_dvd_right hrq
Cleared hypotheses: d
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun (x : σ) ↦ Polynomial.X
⊢ LeftInverse (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default)) (eval₂ Polynomial.C fun (x : σ) ↦ Polynomial.X)
have change : ∀ (p : MvPolynomial σ R), (f.comp g : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p
Tactic: change ∀ p, f.comp g p = p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun (x : σ) ↦ Polynomial.X
⊢ ∀ (p : MvPolynomial σ R), (f.comp g : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p
have hC : (f.comp g).comp C = C
Tactic: apply is_id
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun (x : σ) ↦ Polynomial.X
hC : (f.comp g).comp C = C
⊢ ∀ (p : MvPolynomial σ R), (f.comp g : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p
have hX : ∀ (n : σ),
  Eq (α := MvPolynomial σ R) ((f.comp g : (a : MvPolynomial σ R) → MvPolynomial σ R) (X n) : MvPolynomial σ R)
    (X n : MvPolynomial σ R)
Tactic: apply is_id
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun (x : σ) ↦ Polynomial.X
⊢ (f.comp g).comp C = C
have hC : ∀ (a : R) (m : σ →₀ ℕ),
  Eq.{u + 1} (α := R) (coeff m (((f.comp g).comp C : (a : R) → MvPolynomial σ R) a))
    (coeff m ((C : (a : R) → MvPolynomial σ R) a))
Tactic: ext a
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a_1 a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun (x : σ) ↦ Polynomial.X
a : R
m : σ →₀ ℕ
⊢ Eq.{u + 1} (α := R) (coeff m (((f.comp g).comp C : (a : R) → MvPolynomial σ R) a))
    (coeff m ((C : (a : R) → MvPolynomial σ R) a))
have hC : Eq.{u + 1} (α := R)
  (coeff m
    (Polynomial.eval₂ C (X default)
      (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) ((C : (a : R) → MvPolynomial σ R) a))))
  (coeff m ((C : (a : R) → MvPolynomial σ R) a))
Tactic: dsimp [f, g]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a_1 a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun (x : σ) ↦ Polynomial.X
a : R
m : σ →₀ ℕ
⊢ Eq.{u + 1} (α := R)
    (coeff m
      (Polynomial.eval₂ C (X default)
        (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) ((C : (a : R) → MvPolynomial σ R) a))))
    (coeff m ((C : (a : R) → MvPolynomial σ R) a))
have hC : Eq.{u + 1} (α := R) (coeff m (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) a)))
  (coeff m ((C : (a : R) → MvPolynomial σ R) a))
Tactic: rw [eval₂_C, Polynomial.eval₂_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a_1 a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun (x : σ) ↦ Polynomial.X
a : R
m : σ →₀ ℕ
hC :
  Eq.{u + 1} (α := R) (coeff m (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) a)))
    (coeff m ((C : (a : R) → MvPolynomial σ R) a))
⊢ Eq.{u + 1} (α := R)
    (coeff m
      (Polynomial.eval₂ C (X default)
        (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) ((C : (a : R) → MvPolynomial σ R) a))))
    (coeff m ((C : (a : R) → MvPolynomial σ R) a))
have hC₁ : Eq.{u + 1} (α := R) (coeff m ((C : (a : R) → MvPolynomial σ R) a)) (coeff m ((C : (a : R) → MvPolynomial σ R) a))
Tactic: rw [eval₂_C, Polynomial.eval₂_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun (x : σ) ↦ Polynomial.X
i : σ
⊢ Eq (α := MvPolynomial σ R) ((f.comp g : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
    (X i : MvPolynomial σ R)
have hX : Eq (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (X i)))
  (X i)
Tactic: dsimp [f, g]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun (x : σ) ↦ Polynomial.X
i : σ
⊢ Eq (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (X i)))
    (X i)
have hX : Eq (α := MvPolynomial σ R) (X default) (X i)
Tactic: rw [eval₂_X, Polynomial.eval₂_X]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
f : R[X] →+* MvPolynomial σ R := eval₂RingHom C (X default)
g : MvPolynomial σ R →+* R[X] := eval₂Hom Polynomial.C fun (x : σ) ↦ Polynomial.X
i : σ
⊢ Eq (α := MvPolynomial σ R) (X default) (X i)
have hX : Eq (α := MvPolynomial σ R) (X i) (X i)
Tactic: rw [← Unique.eq_default i]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a_1 a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
p : R[X]
a : R
⊢ Eq.{u + 1} (α := R[X])
    (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) a)))
    ((Polynomial.C : (a : R) → R[X]) a)
have rw : Eq.{u + 1} (α := R[X]) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) ((C : (a : R) → MvPolynomial σ R) a))
  ((Polynomial.C : (a : R) → R[X]) a)
Tactic: rw [Polynomial.eval₂_C, MvPolynomial.eval₂_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a_1 a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
p : R[X]
a : R
rw :
  Eq.{u + 1} (α := R[X]) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) ((C : (a : R) → MvPolynomial σ R) a))
    ((Polynomial.C : (a : R) → R[X]) a)
⊢ Eq.{u + 1} (α := R[X])
    (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) a)))
    ((Polynomial.C : (a : R) → R[X]) a)
have rw₁ : Eq (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X])
Tactic: rw [Polynomial.eval₂_C, MvPolynomial.eval₂_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
p_1 p q : R[X]
hp : eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p) = p
hq : eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) = q
⊢ eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (p + q)) = p + q
have rw : eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
    (HAdd.hAdd (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) p) (Polynomial.eval₂ C (X default) q)) =
  p + q
Tactic: rw [Polynomial.eval₂_add, MvPolynomial.eval₂_add, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
p_1 p q : R[X]
hp : eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p) = p
hq : eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) = q
rw :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (HAdd.hAdd (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) p) (Polynomial.eval₂ C (X default) q)) =
    p + q
⊢ eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (p + q)) = p + q
have rw₁ : eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p) +
    eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) =
  p + q
Tactic: rw [Polynomial.eval₂_add, MvPolynomial.eval₂_add, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
p_1 p q : R[X]
hp : eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p) = p
hq : eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) = q
rw :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (HAdd.hAdd (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) p) (Polynomial.eval₂ C (X default) q)) =
    p + q
rw₁ :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p) +
      eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) =
    p + q
⊢ eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (p + q)) = p + q
have rw₂ : p + eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) = p + q
Tactic: rw [Polynomial.eval₂_add, MvPolynomial.eval₂_add, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
p_1 p q : R[X]
hp : eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p) = p
hq : eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) = q
rw :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (HAdd.hAdd (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) p) (Polynomial.eval₂ C (X default) q)) =
    p + q
rw₁ :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) p) +
      eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) =
    p + q
rw₂ : p + eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) q) = p + q
⊢ eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (p + q)) = p + q
have rw₃ : p + q = p + q
Tactic: rw [Polynomial.eval₂_add, MvPolynomial.eval₂_add, hp, hq]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
p_1 : R[X]
p : ℕ
n : R
h :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default)
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X p))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X p)
⊢ eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default)
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X])
          (HPow.hPow (α := R[X]) Polynomial.X (p + 1)))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
have rw : eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
    (HMul.hMul (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n))
      (Polynomial.eval₂ C (X default) (HPow.hPow (α := R[X]) Polynomial.X (p + 1)))) =
  HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
Tactic: rw [Polynomial.eval₂_mul, Polynomial.eval₂_pow, Polynomial.eval₂_X, Polynomial.eval₂_C,
        eval₂_mul, eval₂_C, eval₂_pow, eval₂_X]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Equiv (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ_1 : Type u_1
a a' a₁ a₂ : R
e : ℕ
s : σ_1 →₀ ℕ
inst : CommSemiring R
σ : Type u_2
inst_1 : Unique σ
p_1 : R[X]
p : ℕ
n : R
h :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default)
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X p))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X p)
rw :
  eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (HMul.hMul (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n))
        (Polynomial.eval₂ C (X default) (HPow.hPow (α := R[X]) Polynomial.X (p + 1)))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
⊢ eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
      (Polynomial.eval₂ C (X default)
        (HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X])
          (HPow.hPow (α := R[X]) Polynomial.X (p + 1)))) =
    HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
have rw₁ : eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X)
    (Polynomial.eval₂ C (X default) ((Polynomial.C : (a : R) → R[X]) n) *
      HPow.hPow (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) Polynomial.X) (p + 1)) =
  HMul.hMul (α := R[X]) ((Polynomial.C : (a : R) → R[X]) n : R[X]) (HPow.hPow (α := R[X]) Polynomial.X (p + 1))
Tactic: rw [Polynomial.eval₂_mul, Polynomial.eval₂_pow, Polynomial.eval₂_X, Polynomial.eval₂_C,
        eval₂_mul, eval₂_C, eval₂_pow, eval₂_X]