awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.Division
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
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)
⊢ p ∣ (monomial n : (a : R) → MvPolynomial σ R) 1 * q

Tactic:
rw [hp, ← add_tsub_cancel_of_le hmn, ← mul_one 1, ← monomial_mul, mul_one, mul_assoc]

Premises used: mul_assoc, MvPolynomial.monomial_mul, mul_one, OfNat.ofNat, add_tsub_cancel_of_le
-- Module: Mathlib.Algebra.MvPolynomial.Division
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
inr : r ∣ (monomial (n - m) : (a : R) → MvPolynomial σ R) 1 * q
⊢ (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:
apply mul_dvd_mul dvd_rfl

Premises used: mul_dvd_mul
-- Module: Mathlib.Algebra.MvPolynomial.Division
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
⊢ r ∣ (monomial (n - m) : (a : R) → MvPolynomial σ R) 1 * q

Tactic:
apply dvd_mul_of_dvd_right hrq

Premises used: dvd_mul_of_dvd_right
-- Module: Mathlib.Algebra.MvPolynomial.Division
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
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
⊢ ∀ (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

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

Premises used: exists_eq_right', mul_assoc, Finsupp.support, MvPolynomial.C_1, mul_dvd_mul, exists_and_left, exists_eq_left, MvPolynomial.dvd_X_mul_iff, MvPolynomial.monomial_add_single, MvPolynomial.monomial_zero', MvPolynomial.monomial_mul, pow_one, Finset.Nonempty, implies_true, Finsupp.degree_eq_zero_iff, mul_one, OfNat.ofNat, one_mul, rfl, nonpos_iff_eq_zero
-- Module: Mathlib.Algebra.MvPolynomial.Division
Goal:
σ : Type u_1
R : Type u_3
inst : CommRing R
p q : MvPolynomial σ R
inst_1 : IsCancelMulZero R
n : σ →₀ ℕ
hR : Nontrivial R
inr :
  ∀ (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
⊢ ∀ (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

Tactic:
classical
  intro d
  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

Premises used: exists_eq_right', mul_assoc, Finsupp.support, MvPolynomial.C_1, mul_dvd_mul, exists_and_left, exists_eq_left, MvPolynomial.dvd_X_mul_iff, MvPolynomial.monomial_add_single, MvPolynomial.monomial_zero', MvPolynomial.monomial_mul, pow_one, Finset.Nonempty, implies_true, Finsupp.degree_eq_zero_iff, mul_one, OfNat.ofNat, one_mul, rfl, nonpos_iff_eq_zero
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
change : ∀ (p : MvPolynomial σ R), (f.comp g : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p
⊢ LeftInverse (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default)) (eval₂ Polynomial.C fun (x : σ) ↦ Polynomial.X)

Tactic:
change ∀ p, f.comp g p = p
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
hX :
  ∀ (n : σ),
    Eq (α := MvPolynomial σ R) ((f.comp g : (a : MvPolynomial σ R) → MvPolynomial σ R) (X n) : MvPolynomial σ R)
      (X n : MvPolynomial σ R)
⊢ ∀ (p : MvPolynomial σ R), (f.comp g : (a : MvPolynomial σ R) → MvPolynomial σ R) p = p

Tactic:
apply is_id

Premises used: MvPolynomial.is_id
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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 :
  ∀ (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))
⊢ (f.comp g).comp C = C

Tactic:
ext a
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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)
        (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) ((C : (a : R) → MvPolynomial σ R) a))))
    (coeff m ((C : (a : R) → MvPolynomial σ R) a))
⊢ 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:
dsimp [f, g]
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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))
hC₁ hC₂ :
  Eq.{u + 1} (α := R) (coeff m ((C : (a : R) → MvPolynomial σ R) 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))

Tactic:
rw [eval₂_C, Polynomial.eval₂_C]

Premises used: MvPolynomial.eval₂_C, Polynomial.eval₂_C
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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 : σ
hX :
  Eq (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (X i)))
    (X i)
⊢ Eq (α := MvPolynomial σ R) ((f.comp g : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
    (X i : MvPolynomial σ R)

Tactic:
dsimp [f, g]
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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 : σ
hX : Eq (α := MvPolynomial σ R) (X default) (X i)
⊢ Eq (α := MvPolynomial σ R) (Polynomial.eval₂ C (X default) (eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (X i)))
    (X i)

Tactic:
rw [eval₂_X, Polynomial.eval₂_X]

Premises used: MvPolynomial.eval₂_X, Polynomial.eval₂_X
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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 : σ
hX hX₁ : Eq (α := MvPolynomial σ R) (X i) (X i)
⊢ Eq (α := MvPolynomial σ R) (X default) (X i)

Tactic:
rw [← Unique.eq_default i]

Premises used: Unique.eq_default
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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)
rw₁ rw₂ : Eq (α := R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X]) ((Polynomial.C : (a : R) → R[X]) a : R[X])
⊢ 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)

Tactic:
rw [Polynomial.eval₂_C, MvPolynomial.eval₂_C]

Premises used: MvPolynomial.eval₂_C, Polynomial.eval₂_C
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
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
rw₃ rw₄ : p + q = p + q
⊢ eval₂ Polynomial.C (fun (x : σ) ↦ Polynomial.X) (Polynomial.eval₂ C (X default) (p + q)) = p + q

Tactic:
rw [Polynomial.eval₂_add, MvPolynomial.eval₂_add, hp, hq]

Premises used: MvPolynomial.eval₂_add, Polynomial.eval₂_add
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Unique σ
d : σ →₀ ℕ
r : R
⊢ Eq.{u + 1} (α := R[X])
    ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) ((monomial d : (a : R) → MvPolynomial σ R) r) : R[X])
    ((Polynomial.monomial ((d : (a : σ) → ℕ) default) : (a : R) → R[X]) r : R[X])

Tactic:
simp [Polynomial.C_mul_X_pow_eq_monomial]

Premises used: Polynomial.C_mul_X_pow_eq_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Unique σ
d : σ →₀ ℕ
r : R
⊢ Eq (α := MvPolynomial σ R)
    ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R)
        ((Polynomial.monomial ((d : (a : σ) → ℕ) default) : (a : R) → R[X]) r) :
      MvPolynomial σ R)
    ((monomial d : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)

Tactic:
simp [MvPolynomial.monomial_eq]

Premises used: MvPolynomial.monomial_eq
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Unique σ
n : ℕ
d : σ →₀ ℕ
r : R
monomial :
  Eq.{u + 1} (α := R)
    (Polynomial.coeff
      ((Polynomial.monomial (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default) :
          (a : R) → R[X])
        r)
      n)
    (coeff.{u, u_1} (σ := σ) (Finsupp.single default n)
      ((MvPolynomial.monomial (Finsupp.single default ((d : (a : σ) → ℕ) default)) : (a : R) → MvPolynomial σ R) r))
⊢ Eq.{u + 1} (α := R)
    (Polynomial.coeff
      ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r))
      n)
    (coeff.{u, u_1} (σ := σ) (Finsupp.single default n) ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r))

Tactic:
rw [uniqueAlgEquiv_monomial, Finsupp.unique_single d]

Premises used: Finsupp.unique_single, MvPolynomial.uniqueAlgEquiv_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Unique σ
n : ℕ
d : σ →₀ ℕ
r : R
⊢ Eq.{u + 1} (α := R)
    (Polynomial.coeff
      ((Polynomial.monomial (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default) :
          (a : R) → R[X])
        r)
      n)
    (coeff.{u, u_1} (σ := σ) (Finsupp.single default n)
      ((monomial (Finsupp.single default ((d : (a : σ) → ℕ) default)) : (a : R) → MvPolynomial σ R) r))

Tactic:
simp [Polynomial.coeff_monomial, MvPolynomial.coeff_monomial]

Premises used: Polynomial.coeff_monomial, MvPolynomial.coeff_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Unique σ
n : ℕ
P Q : MvPolynomial σ R
hP : Polynomial.coeff ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) P) n = coeff (Finsupp.single default n) P
hQ : Polynomial.coeff ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) Q) n = coeff (Finsupp.single default n) Q
⊢ Polynomial.coeff ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) (P + Q)) n =
    coeff (Finsupp.single default n) (P + Q)

Tactic:
simpa using congrArg₂ (· + ·) hP hQ

Premises used: congrArg₂, HAdd.hAdd
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Unique σ
P : MvPolynomial σ R
n : ℕ
monomial :
  ∀ (d : σ →₀ ℕ) (r : R),
    Eq.{u + 1} (α := R)
      (Polynomial.coeff
        ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X])
          ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r))
        n)
      (coeff.{u, u_1} (σ := σ) (Finsupp.single default n) ((MvPolynomial.monomial d : (a : R) → MvPolynomial σ R) r))
add :
  ∀ (P Q : MvPolynomial σ R)
    (hP :
      Polynomial.coeff ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) P) n = coeff (Finsupp.single default n) P)
    (hQ :
      Polynomial.coeff ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) Q) n = coeff (Finsupp.single default n) Q),
    Polynomial.coeff ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) (P + Q)) n =
      coeff (Finsupp.single default n) (P + Q)
⊢ Polynomial.coeff ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X]) P) n = coeff (Finsupp.single default n) P

Tactic:
induction P using induction_on' with
  | monomial d r =>
      rw [uniqueAlgEquiv_monomial, Finsupp.unique_single d]
      simp [Polynomial.coeff_monomial, MvPolynomial.coeff_monomial]
  | add P Q hP hQ =>
      simpa using congrArg₂ (· + ·) hP hQ

Premises used: MvPolynomial.monomial, MvPolynomial.uniqueAlgEquiv_monomial, Polynomial.coeff_monomial, MvPolynomial.coeff_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : Unique σ
P : R[X]
d : σ →₀ ℕ
rw :
  coeff.{u, u_1} (σ := σ) (Finsupp.single default ((d : (a : σ) → ℕ) default))
      ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) P) =
    P.coeff (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default)
rw₁ :
  Polynomial.coeff
      ((uniqueAlgEquiv R σ : (a : MvPolynomial σ R) → R[X])
        ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) P))
      ((d : (a : σ) → ℕ) default) =
    P.coeff (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default)
rw₂ :
  P.coeff ((d : (a : σ) → ℕ) default) =
    P.coeff (((Finsupp.single default ((d : (a : σ) → ℕ) default) : σ →₀ ℕ) : (a : σ) → ℕ) default)
rw₃ rw₄ : P.coeff ((d : (a : σ) → ℕ) default) = P.coeff ((d : (a : σ) → ℕ) default)
⊢ coeff d ((AlgEquiv.symm (uniqueAlgEquiv R σ) : (a : R[X]) → MvPolynomial σ R) P) = P.coeff ((d : (a : σ) → ℕ) default)

Tactic:
rw [Finsupp.unique_single d, ← coeff_uniqueAlgEquiv R, AlgEquiv.apply_symm_apply,
    Finsupp.single_eq_same]

Premises used: Finsupp.single_eq_same, MvPolynomial.coeff_uniqueAlgEquiv, Finsupp.unique_single, AlgEquiv.apply_symm_apply
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
d : PUnit.{1} →₀ ℕ
r : R
⊢ Eq (α := R[X])
    ((pUnitAlgEquiv R : (a : MvPolynomial PUnit.{1} R) → R[X]) ((monomial d : (a : R) → MvPolynomial PUnit.{1} R) r) :
      R[X])
    ((Polynomial.monomial ((d : (a : PUnit.{1}) → ℕ) ()) : (a : R) → R[X]) r : R[X])

Tactic:
uniqueAlgEquiv_monomial _

Premises used: MvPolynomial.uniqueAlgEquiv_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
inst : CommSemiring R
d : PUnit.{1} →₀ ℕ
r : R
⊢ Eq (α := MvPolynomial PUnit.{1} R)
    ((AlgEquiv.symm (pUnitAlgEquiv R) : (a : R[X]) → MvPolynomial PUnit.{1} R)
        ((Polynomial.monomial ((d : (a : PUnit.{1}) → ℕ) ()) : (a : R) → R[X]) r) :
      MvPolynomial PUnit.{1} R)
    ((monomial d : (a : R) → MvPolynomial PUnit.{1} R) r : MvPolynomial PUnit.{1} R)

Tactic:
uniqueAlgEquiv_symm_monomial _

Premises used: MvPolynomial.uniqueAlgEquiv_symm_monomial
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst : CommSemiring S₁
inst_1 : CommSemiring S₂
e : S₁ ≃+* S₂
x : MvPolynomial σ S₁
⊢ Eq (α := MvPolynomial σ S₂) ((mapEquiv σ e : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) x : MvPolynomial σ S₂)
    ((map (↑e : S₁ →+* S₂) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) x : MvPolynomial σ S₂)

Tactic:
rfl

Premises used: Finsupp.onFinset, AddMonoidAlgebra.ofCoeff, AddMonoidAlgebra.map, Finsupp.mapRange, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R ≃+* MvPolynomial σ R) (mapEquiv σ (RingEquiv.refl R)) (RingEquiv.refl (MvPolynomial σ R))

Tactic:
RingEquiv.ext map_id

Premises used: RingEquiv.ext, MvPolynomial.map_id
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst : CommSemiring S₁
inst_1 : CommSemiring S₂
e : S₁ ≃+* S₂
⊢ (mapEquiv σ e).symm = mapEquiv σ e.symm

Tactic:
rfl

Premises used: RingEquiv.ofRingHom, AddMonoidAlgebra.mapRingEquiv, Equiv.symm, MvPolynomial.mapEquiv, RingEquiv.symm, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Equiv
Goal:
S₁ : Type v
S₂ : Type w
S₃ : Type x
σ : Type u_1
inst : CommSemiring S₁
inst_1 : CommSemiring S₂
inst_2 : CommSemiring S₃
e : S₁ ≃+* S₂
f : S₂ ≃+* S₃
⊢ (mapEquiv σ e).trans (mapEquiv σ f) = mapEquiv σ (e.trans f)

Tactic:
(AddMonoidAlgebra.mapRingEquiv_trans _ _).symm

Premises used: Eq.symm, MvPolynomial.mapEquiv, AddMonoidAlgebra.mapRingEquiv_trans