awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
h : 0 < k
hesymm :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      HAdd.hAdd (α := MvPolynomial σ R)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides_1 :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) -
      HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k ∧ ¬0 < a.1,
      HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
a : ℕ × ℕ
ha : a.1 + a.2 = k
left : a.1 < k
ha0 : ¬0 < a.1
h₁ : a = (0, a.1 + a.2)
h₂ : a = (0, 0 + a.2)
h₃ : a = (0, a.2)
h₄ h₅ : a = (a.1, a.2)
⊢ a = (0, k)

Tactic:
rw [← ha, Nat.eq_zero_of_not_pos ha0, zero_add, ← Nat.eq_zero_of_not_pos ha0]

Premises used: zero_add, Nat.eq_zero_of_not_pos
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
h : 0 < k
hesymm :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      HAdd.hAdd (α := MvPolynomial σ R)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides_1 :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) -
      HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k ∧ ¬0 < a.1,
      HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
⊢ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k ∧ ¬0 < a.1} = {(0, k)}

Tactic:
have : {a ∈ antidiagonal k | a.fst < k ∧ ¬0 < a.fst} = {(0, k)} := by
    ext a
    rw [mem_filter, mem_antidiagonal, mem_singleton]
    refine ⟨?_, by rintro rfl; lia⟩
    rintro ⟨ha, ⟨_, ha0⟩⟩
    rw [← ha, Nat.eq_zero_of_not_pos ha0, zero_add, ← Nat.eq_zero_of_not_pos ha0]
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
h : 0 < k
hesymm :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      HAdd.hAdd (α := MvPolynomial σ R)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides_1 :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) -
      HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k ∧ ¬0 < a.1,
      HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
this : {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k ∧ ¬0 < a.1} = {(0, k)}
⊢ HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (-1) (0, k).1 * esymm σ R (0, k).1 * psum σ R (0, k).2

Tactic:
rw [this, sum_singleton] at sub_both_sides

Premises used: Finset.sum_singleton
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
h : 0 < k
hesymm :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      HAdd.hAdd (α := MvPolynomial σ R)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides_1 :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) -
      HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    ∑ a ∈ @antidiagonal _ instAddMonoid _ k with a.1 < k ∧ ¬0 < a.1,
      HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
this : {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k ∧ ¬0 < a.1} = {(0, k)}
sub_both_sides₁ :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (-1) (0, k).1 * esymm σ R (0, k).1 * psum σ R (0, k).2
⊢ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k ∧ ¬0 < a.1} = {(0, k)}

Tactic:
rw [this, sum_singleton] at sub_both_sides

Premises used: Finset.sum_singleton
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
h : 0 < k
hesymm :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      HAdd.hAdd (α := MvPolynomial σ R)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides_1 :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) -
      HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
sub_both_sides :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (-1) (0, k).1 * esymm σ R (0, k).1 * psum σ R (0, k).2
this : {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k ∧ ¬0 < a.1} = {(0, k)}
⊢ HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ x ∈ @antidiagonal _ instAddMonoid _ k with x.1 < k ∧ 0 < x.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2 =
    psum σ R k

Tactic:
simp only [_root_.pow_zero, esymm_zero, mul_one, one_mul, filter_filter] at sub_both_sides

Premises used: Finset.filter_filter, pow_zero, mul_one, MvPolynomial.esymm_zero, one_mul
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
h : 0 < k
hesymm :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      HAdd.hAdd (α := MvPolynomial σ R)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides_1 :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) -
      HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
this : {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k ∧ ¬0 < a.1} = {(0, k)}
sub_both_sides :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ x ∈ @antidiagonal _ instAddMonoid _ k with x.1 < k ∧ 0 < x.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2 =
    psum σ R k
⊢ psum σ R k =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ x ∈ @antidiagonal _ instAddMonoid _ k with x.1 < k ∧ 0 < x.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2

Tactic:
sub_both_sides.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
Goal:
σ : Type u_1
inst : Fintype σ
R : Type u_2
inst_1 : CommRing R
k : ℕ
h : 0 < k
hesymm :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      HAdd.hAdd (α := MvPolynomial σ R)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
        (∑ x ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < x.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2)
sub_both_sides_1 :
  HMul.hMul (α := MvPolynomial σ R) (↑k : MvPolynomial σ R) (esymm σ R k) -
      HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
        ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with 0 < a.1,
          HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2 =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) *
      ∑ a ∈ {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k} with ¬0 < a.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) a.1 * esymm σ R a.1 * psum σ R a.2
this : {a ∈ @antidiagonal _ instAddMonoid _ k | a.1 < k ∧ ¬0 < a.1} = {(0, k)}
sub_both_sides :
  HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ x ∈ @antidiagonal _ instAddMonoid _ k with x.1 < k ∧ 0 < x.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2 =
    psum σ R k
⊢ psum σ R k =
    HPow.hPow (α := MvPolynomial σ R) (-1) (k + 1) * (↑k : MvPolynomial σ R) * esymm σ R k -
      ∑ x ∈ @antidiagonal _ instAddMonoid _ k with x.1 < k ∧ 0 < x.1,
        HPow.hPow (α := MvPolynomial σ R) (-1) x.1 * esymm σ R x.1 * psum σ R x.2

Tactic:
exact sub_both_sides.symm

Premises used: Eq.symm
-- Module: Mathlib.RingTheory.MvPolynomial.Tower
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : σ → B
p : MvPolynomial σ R
rw :
  eval₂ (algebraMap A B) x ((map (algebraMap R A) : (a : MvPolynomial σ R) → MvPolynomial σ A) p) =
    (aeval x : (a : MvPolynomial σ R) → B) p
rw₁ :
  eval₂ (algebraMap A B) x ((map (algebraMap R A) : (a : MvPolynomial σ R) → MvPolynomial σ A) p) =
    eval₂ (algebraMap R B) x p
rw₂ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) x p =
    eval₂ (algebraMap R B) x p
rw₃ rw₄ :
  eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) x p =
    eval₂ (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) x p
⊢ Eq.{u_3 + 1} (α := B)
    ((aeval x : (a : MvPolynomial σ A) → B)
        ((map (algebraMap R A) : (a : MvPolynomial σ R) → MvPolynomial σ A) p : MvPolynomial σ A) :
      B)
    ((aeval x : (a : MvPolynomial σ R) → B) p : B)

Tactic:
rw [aeval_def, aeval_def, eval₂_map, IsScalarTower.algebraMap_eq R A B]

Premises used: MvPolynomial.eval₂_map, MvPolynomial.aeval_def, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.MvPolynomial.Tower
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
rw :
  eval₂ (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) p =
    (algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A)
rw₁ :
  eval₂ (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) p =
    (algebraMap A B : (a : A) → B) (eval₂ (algebraMap R A) x p)
rw₂ :
  Eq.{u_3 + 1} (α := B)
    ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((algebraMap A B : (a : A) → B) (eval₂ (algebraMap R A) x p) : B)
rw₃ :
  Eq.{u_3 + 1} (α := B)
    ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((algebraMap A B : (a : A) → B) ((eval₂Hom (algebraMap R A) x : (a : MvPolynomial σ R) → A) p : A) : B)
rw₄ :
  Eq.{u_3 + 1} (α := B)
    ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((eval₂Hom (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A B) (algebraMap R A)) fun (i : σ) ↦
            (algebraMap A B : (a : A) → B) (x i) :
          (a : MvPolynomial σ R) → B)
        p :
      B)
rw₅ :
  Eq.{u_3 + 1} (α := B)
    ((eval₂Hom (algebraMap R B) ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((eval₂Hom (algebraMap R B) fun (i : σ) ↦ (algebraMap A B : (a : A) → B) (x i) : (a : MvPolynomial σ R) → B) p : B)
rw₆ rw₇ :
  Eq.{u_3 + 1} (α := B)
    ((eval₂Hom (algebraMap R B) fun (x_1 : σ) ↦ (algebraMap A B : (a : A) → B) (x x_1) : (a : MvPolynomial σ R) → B) p :
      B)
    ((eval₂Hom (algebraMap R B) fun (i : σ) ↦ (algebraMap A B : (a : A) → B) (x i) : (a : MvPolynomial σ R) → B) p : B)
⊢ Eq.{u_3 + 1} (α := B) ((aeval ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B)
    ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B)

Tactic:
rw [aeval_def, aeval_def, ← coe_eval₂Hom, ← coe_eval₂Hom, map_eval₂Hom, ←
    IsScalarTower.algebraMap_eq, Function.comp_def]

Premises used: MvPolynomial.map_eval₂Hom, MvPolynomial.aeval_def, MvPolynomial.coe_eval₂Hom, Function.comp_def, IsScalarTower.algebraMap_eq
-- Module: Mathlib.RingTheory.MvPolynomial.Tower
Goal:
R : Type u_1
A : Type u_2
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
ι : Type u_5
f : σ → A
p : MvPolynomial σ R
⊢ Eq (α := MvPolynomial ι A)
    ((aeval ((⇑C : (a : A) → MvPolynomial ι A) ∘ f) : (a : MvPolynomial σ R) → MvPolynomial ι A) p : MvPolynomial ι A)
    ((C : (a : A) → MvPolynomial ι A) ((aeval f : (a : MvPolynomial σ R) → A) p) : MvPolynomial ι A)

Tactic:
aeval_algebraMap_apply ..

Premises used: Multiset.sum, Multiset.foldr, Finsupp.sum, MvPolynomial.aeval_algebraMap_apply, MvPolynomial.eval₂, Finset.sum
-- Module: Mathlib.RingTheory.MvPolynomial.Tower
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
inst_7 : IsDomain A
inst_8 : Module.IsTorsionFree A B
inst_9 : Nontrivial B
x : σ → A
p : MvPolynomial σ R
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
rw₁ :
  HSMul.hSMul.{u_2, u_3, u_3} (α := A) (β := B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) 1 = 0 ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
rw₂ :
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A) ∨ Eq.{u_3 + 1} (α := B) 1 0 ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
rw₃ :
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A) ∨ False ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
rw₄ rw₅ :
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := B) ((aeval ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)

Tactic:
rw [aeval_algebraMap_apply, Algebra.algebraMap_eq_smul_one, smul_eq_zero,
    iff_false_intro (one_ne_zero' B), or_false]

Premises used: one_ne_zero', MvPolynomial.aeval_algebraMap_apply, iff_false_intro, Algebra.algebraMap_eq_smul_one, or_false, smul_eq_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Tower
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : CommSemiring B
inst_3 : Algebra R A
inst_4 : Algebra A B
inst_5 : Algebra R B
inst_6 : IsScalarTower R A B
x : σ → A
p : MvPolynomial σ R
h : Function.Injective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑(algebraMap A B) : (a : A) → B)
rw :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
rw₁ :
  Eq.{u_3 + 1} (α := B) ((algebraMap A B : (a : A) → B) ((aeval x : (a : MvPolynomial σ R) → A) p : A) : B)
      ((algebraMap A B : (a : A) → B) 0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
rw₂ rw₃ :
  Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)
⊢ Eq.{u_3 + 1} (α := B) ((aeval ((⇑(algebraMap A B) : (a : A) → B) ∘ x) : (a : MvPolynomial σ R) → B) p : B) (0 : B) ↔
    Eq.{u_2 + 1} (α := A) ((aeval x : (a : MvPolynomial σ R) → A) p : A) (0 : A)

Tactic:
rw [aeval_algebraMap_apply, ← (algebraMap A B).map_zero, h.eq_iff]

Premises used: Algebra.algebraMap, Function.Injective.eq_iff, MvPolynomial.aeval_algebraMap_apply, RingHom.map_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Tower
Goal:
R : Type u_1
A : Type u_2
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
x : σ → ↥S
p : MvPolynomial σ R
⊢ Eq.{u_2 + 1} (α := A) ((aeval ((⇑(algebraMap (↥S) A) : (a : ↥S) → A) ∘ x) : (a : MvPolynomial σ R) → A) p : A)
    ((algebraMap (↥S) A : (a : ↥S) → A) ((aeval x : (a : MvPolynomial σ R) → ↥S) p : ↥S) : A)

Tactic:
aeval_algebraMap_apply A x p

Premises used: MvPolynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.MvPolynomial.Tower
Goal:
R : Type u_1
A : Type u_2
σ : Type u_4
inst : CommSemiring R
inst_1 : CommSemiring A
inst_2 : Algebra R A
S : Subalgebra R A
x : σ → ↥S
p : MvPolynomial σ R
⊢ Eq.{u_2 + 1} (α := A) ((aeval fun (i : σ) ↦ (↑(x i) : A) : (a : MvPolynomial σ R) → A) p : A)
    ((↑((aeval x : (a : MvPolynomial σ R) → ↥S) p) : A) : A)

Tactic:
convert! aeval_algebraMap_apply A x p

Premises used: MvPolynomial.aeval_algebraMap_apply
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
w : σ → M
p : MvPolynomial σ R
simp : (∀ (s : σ →₀ ℕ), coeff s p ≠ 0 → False) ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0
⊢ weightedTotalDegree' w p = ⊥ ↔ p = 0

Tactic:
simp only [weightedTotalDegree', Finset.sup_eq_bot_iff, mem_support_iff, WithBot.coe_ne_bot,
    MvPolynomial.eq_zero_iff]

Premises used: MvPolynomial.mem_support_iff, MvPolynomial.eq_zero_iff, MvPolynomial.weightedTotalDegree', Finset.sup_eq_bot_iff, WithBot.coe_ne_bot
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
w : σ → M
p : MvPolynomial σ R
⊢ (∀ (s : σ →₀ ℕ), coeff s p ≠ 0 → False) ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0

Tactic:
forall_congr' fun _ => Classical.not_not

Premises used: Classical.not_not, forall_congr'
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
w : σ → M
p : MvPolynomial σ R
⊢ (∀ (s : σ →₀ ℕ), coeff s p ≠ 0 → False) ↔ ∀ (d : σ →₀ ℕ), coeff d p = 0

Tactic:
exact forall_congr' fun _ => Classical.not_not

Premises used: Classical.not_not, forall_congr'
-- Module: Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
σ : Type u_3
inst_1 : AddCommMonoid M
inst_2 : SemilatticeSup M
w : σ → M
⊢ weightedTotalDegree'.{u_1, u_2, u_3} (R := R) w 0 = ⊥

Tactic:
simp only [weightedTotalDegree', support_zero, Finset.sup_empty]

Premises used: Finset.sup_empty, MvPolynomial.weightedTotalDegree', MvPolynomial.support_zero