awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ (↑j : ℕ) → t j = 0
j : Fin n
hij : (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑j : ℕ)
hji : j ≠ ⟨i, hin⟩
⊢ m ≤ (↑j : ℕ)

Tactic:
hmi.trans_le (hij.lt_of_ne (Fin.val_ne_iff.2 hji).symm).nat_succ_le

Premises used: Iff.mpr, LT.lt.nat_succ_le, Ne.symm, Eq.trans_le, Fin.val_ne_iff, LE.le.lt_of_ne
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
i n m : ℕ
hin : i < n
hmi : m = i + 1
t : Fin n → ℕ
ht : ∀ (j : Fin n), m ≤ (↑j : ℕ) → t j = 0
j : Fin n
hij : (↑(⟨i, ⋯⟩ : Fin m) : ℕ) ≤ (↑j : ℕ)
hji : j ≠ ⟨i, hin⟩
⊢ m ≤ (↑j : ℕ)

Tactic:
exact hmi.trans_le (hij.lt_of_ne (Fin.val_ne_iff.2 hji).symm).nat_succ_le

Premises used: Iff.mpr, LT.lt.nat_succ_le, Ne.symm, Eq.trans_le, Fin.val_ne_iff, LE.le.lt_of_ne
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hnm : n ≤ m
⊢ Function.Injective (α := Fin n → ℕ) (β := Fin m → ℕ) (⇑(accumulate n m) : (a : Fin n → ℕ) → Fin m → ℕ)

Tactic:
fun t s he ↦ funext fun i ↦ ?_

Premises used: funext, Function.Injective
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hnm : n ≤ m
refine :
  ∀ (t s : Fin n → ℕ)
    (he :
      Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t : Fin m → ℕ)
        ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s : Fin m → ℕ))
    (i : Fin n), t i = s i
⊢ Function.Injective (α := Fin n → ℕ) (β := Fin m → ℕ) (⇑(accumulate n m) : (a : Fin n → ℕ) → Fin m → ℕ)

Tactic:
refine fun t s he ↦ funext fun i ↦ ?_

Premises used: funext
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he :
  Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t : Fin m → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s : Fin m → ℕ)
i : Fin n
inl : ∀ (h : (↑i : ℕ) + 1 < m), t i = s i
inr : ∀ (h : m ≤ (↑i : ℕ) + 1), t i = s i
⊢ t i = s i

Tactic:
obtain h | h := lt_or_ge (i.1 + 1) m

Premises used: Fin.val, HAdd.hAdd, lt_or_ge, OfNat.ofNat
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he :
  Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t : Fin m → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s : Fin m → ℕ)
i : Fin n
h : (↑i : ℕ) + 1 < m
⊢ (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s ⟨(↑i : ℕ), ⋯⟩ =
    HAdd.hAdd (β := ℕ) (s (⟨(↑i : ℕ), ⋯⟩ : Fin n))
      ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s (⟨(↑i : ℕ) + 1, h⟩ : Fin m) : ℕ)

Tactic:
have := accumulate_rec i.2 h s
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he :
  Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t : Fin m → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s : Fin m → ℕ)
i : Fin n
h : (↑i : ℕ) + 1 < m
this :
  (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s ⟨(↑i : ℕ), ⋯⟩ =
    HAdd.hAdd (β := ℕ) (s (⟨(↑i : ℕ), ⋯⟩ : Fin n))
      ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s (⟨(↑i : ℕ) + 1, h⟩ : Fin m) : ℕ)
inl :
  ∀
    (this :
      (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t ⟨(↑i : ℕ), ⋯⟩ =
        HAdd.hAdd (β := ℕ) (s (⟨(↑i : ℕ), ⋯⟩ : Fin n))
          ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t (⟨(↑i : ℕ) + 1, h⟩ : Fin m) : ℕ)),
    t i = s i
inl₁ :
  ∀
    (this :
      HAdd.hAdd (β := ℕ) (t (⟨(↑i : ℕ), ⋯⟩ : Fin n))
          ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t (⟨(↑i : ℕ) + 1, h⟩ : Fin m) : ℕ) =
        HAdd.hAdd (β := ℕ) (s (⟨(↑i : ℕ), ⋯⟩ : Fin n))
          ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t ⟨(↑i : ℕ) + 1, h⟩ : ℕ)),
    t i = s i
inl₂ inl₃ inl₄ inl₅ : ∀ (this : t (⟨(↑i : ℕ), ⋯⟩ : Fin n) = s ⟨(↑i : ℕ), ⋯⟩), t i = s i
⊢ t i = s i

Tactic:
rwa [← he, accumulate_rec i.2 h t, add_right_cancel_iff] at this

Premises used: Fin.isLt, Fin.accumulate_rec, add_right_cancel_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he :
  Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t : Fin m → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s : Fin m → ℕ)
i : Fin n
h : m ≤ (↑i : ℕ) + 1
⊢ m = (↑i : ℕ) + 1

Tactic:
have := h.antisymm (i.2.nat_succ_le.trans hnm)
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he :
  Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t : Fin m → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s : Fin m → ℕ)
i : Fin n
h : m ≤ (↑i : ℕ) + 1
this : m = (↑i : ℕ) + 1
inr : ∀ (j : Fin n), m ≤ (↑j : ℕ) → s j = 0
inr₁ : ∀ (j : Fin n), m ≤ (↑j : ℕ) → t j = 0
⊢ t i = s i

Tactic:
rw [← accumulate_last i.2 this t, ← accumulate_last i.2 this s, he]

Premises used: Fin.isLt, Fin.accumulate_last
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he :
  Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t : Fin m → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s : Fin m → ℕ)
i : Fin n
h : m ≤ (↑i : ℕ) + 1
this : m = (↑i : ℕ) + 1
j : Fin n
hj : m ≤ (↑j : ℕ)
⊢ s j = 0

Tactic:
((j.2.trans_le hnm).not_ge hj).elim

Premises used: False.elim, Fin.isLt, LT.lt.trans_le, LT.lt.not_ge
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he :
  Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t : Fin m → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s : Fin m → ℕ)
i : Fin n
h : m ≤ (↑i : ℕ) + 1
this : m = (↑i : ℕ) + 1
j : Fin n
hj : m ≤ (↑j : ℕ)
⊢ s j = 0

Tactic:
exact ((j.2.trans_le hnm).not_ge hj).elim

Premises used: False.elim, Fin.isLt, LT.lt.trans_le, LT.lt.not_ge
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he :
  Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t : Fin m → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s : Fin m → ℕ)
i : Fin n
h : m ≤ (↑i : ℕ) + 1
this : m = (↑i : ℕ) + 1
⊢ ∀ (j : Fin n), m ≤ (↑j : ℕ) → s j = 0

Tactic:
{ intro j hj; exact ((j.2.trans_le hnm).not_ge hj).elim }
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he :
  Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t : Fin m → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s : Fin m → ℕ)
i : Fin n
h : m ≤ (↑i : ℕ) + 1
this : m = (↑i : ℕ) + 1
j : Fin n
hj : m ≤ (↑j : ℕ)
⊢ t j = 0

Tactic:
((j.2.trans_le hnm).not_ge hj).elim

Premises used: False.elim, Fin.isLt, LT.lt.trans_le, LT.lt.not_ge
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he :
  Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t : Fin m → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s : Fin m → ℕ)
i : Fin n
h : m ≤ (↑i : ℕ) + 1
this : m = (↑i : ℕ) + 1
j : Fin n
hj : m ≤ (↑j : ℕ)
⊢ t j = 0

Tactic:
exact ((j.2.trans_le hnm).not_ge hj).elim

Premises used: False.elim, Fin.isLt, LT.lt.trans_le, LT.lt.not_ge
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hnm : n ≤ m
t s : Fin n → ℕ
he :
  Eq (α := Fin m → ℕ) ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) t : Fin m → ℕ)
    ((accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) s : Fin m → ℕ)
i : Fin n
h : m ≤ (↑i : ℕ) + 1
this : m = (↑i : ℕ) + 1
inr inr₁ inr₂ : ∀ (j : Fin n) (hj : m ≤ (↑j : ℕ)), t j = 0
⊢ ∀ (j : Fin n), m ≤ (↑j : ℕ) → t j = 0

Tactic:
{ intro j hj; exact ((j.2.trans_le hnm).not_ge hj).elim }
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i : ℕ
hi : i < m
⊢ i ≤ m - 1

Tactic:
have := Nat.le_sub_one_of_lt hi
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i : ℕ
hi : i < m
this : i ≤ m - 1
revert :
  ∀ (hi : i < m), (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i, hi⟩ = s (⟨i, hi⟩ : Fin m)
⊢ (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i, hi⟩ = s (⟨i, hi⟩ : Fin m)

Tactic:
revert hi
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i : ℕ
this : i ≤ m - 1
⊢ ∀ (hi : i < m), (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i, hi⟩ = s (⟨i, hi⟩ : Fin m)

Tactic:
Nat.decreasingInduction' (fun i hi _ ih him ↦ ?_) this fun hm ↦ ?_

Premises used: Nat.decreasingInduction'
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i : ℕ
this : i ≤ m - 1
refine_1 :
  ∀ (i_1 : ℕ) (hi : i_1 < m - 1),
    i ≤ i_1 →
      ∀
        (ih :
          ∀ (hi : i_1 + 1 < m),
            (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i_1 + 1, hi⟩ =
              s (⟨i_1 + 1, hi⟩ : Fin m))
        (him : i_1 < m),
        (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i_1, him⟩ = s (⟨i_1, him⟩ : Fin m)
refine_2 :
  ∀ (hm : m - 1 < m),
    (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨m - 1, hm⟩ = s (⟨m - 1, hm⟩ : Fin m)
⊢ ∀ (hi : i < m), (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i, hi⟩ = s (⟨i, hi⟩ : Fin m)

Tactic:
refine Nat.decreasingInduction' (fun i hi _ ih him ↦ ?_) this fun hm ↦ ?_
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i_1 : ℕ
this : i_1 ≤ m - 1
i : ℕ
hi : i < m - 1
h : i_1 ≤ i
ih :
  ∀ (hi : i + 1 < m),
    (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i + 1, hi⟩ = s (⟨i + 1, hi⟩ : Fin m)
him : i < m
refine_1 :
  ∀ (hi : i + 1 < m),
    i_1 ≤ i →
      ∀
        (ih :
          ∀ (hi : i + 1 < m),
            (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i + 1, hi⟩ = s (⟨i + 1, hi⟩ : Fin m))
        (him : i < m),
        (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i, him⟩ = s (⟨i, him⟩ : Fin m)
⊢ (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i, him⟩ = s (⟨i, him⟩ : Fin m)

Tactic:
rw [← Nat.pred_eq_sub_one, Nat.lt_pred_iff, Nat.succ_eq_add_one] at hi

Premises used: Nat.succ_eq_add_one, Nat.lt_pred_iff, Nat.pred_eq_sub_one
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i_1 : ℕ
this : i_1 ≤ m - 1
i : ℕ
hi : i + 1 < m
h : i_1 ≤ i
ih :
  ∀ (hi : i + 1 < m),
    (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i + 1, hi⟩ = s (⟨i + 1, hi⟩ : Fin m)
him : i < m
refine_1 :
  s (⟨(↑(⟨i, ⋯⟩ : Fin n) : ℕ), him⟩ : Fin m) - s (⟨(↑(⟨i, ⋯⟩ : Fin n) : ℕ) + 1, hi⟩ : Fin m) + s (⟨i + 1, hi⟩ : Fin m) =
    s ⟨i, him⟩
⊢ (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i, him⟩ = s (⟨i, him⟩ : Fin m)

Tactic:
rw [accumulate_rec (him.trans_le hmn) hi, ih hi, invAccumulate, dif_pos him, dif_pos hi]

Premises used: Fin.invAccumulate, Fin.accumulate_rec, dif_pos, LT.lt.trans_le
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i_1 : ℕ
this : i_1 ≤ m - 1
i : ℕ
hi : i + 1 < m
h : i_1 ≤ i
ih :
  ∀ (hi : i + 1 < m),
    (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i + 1, hi⟩ = s (⟨i + 1, hi⟩ : Fin m)
him : i < m
refine_1 : s (⟨i, him⟩ : Fin m) - s (⟨i + 1, hi⟩ : Fin m) + s (⟨i + 1, hi⟩ : Fin m) = s ⟨i, him⟩
⊢ s (⟨(↑(⟨i, ⋯⟩ : Fin n) : ℕ), him⟩ : Fin m) - s (⟨(↑(⟨i, ⋯⟩ : Fin n) : ℕ) + 1, hi⟩ : Fin m) + s (⟨i + 1, hi⟩ : Fin m) =
    s ⟨i, him⟩

Tactic:
simp only
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i_1 : ℕ
this : i_1 ≤ m - 1
i : ℕ
hi : i + 1 < m
h : i_1 ≤ i
ih :
  ∀ (hi : i + 1 < m),
    (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i + 1, hi⟩ = s (⟨i + 1, hi⟩ : Fin m)
him : i < m
⊢ s (⟨i, him⟩ : Fin m) - s (⟨i + 1, hi⟩ : Fin m) + s (⟨i + 1, hi⟩ : Fin m) = s ⟨i, him⟩

Tactic:
Nat.sub_add_cancel (hs i.le_succ)

Premises used: Nat.le_succ, Nat.sub_add_cancel
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i_1 : ℕ
this : i_1 ≤ m - 1
i : ℕ
hi : i + 1 < m
h : i_1 ≤ i
ih :
  ∀ (hi : i + 1 < m),
    (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨i + 1, hi⟩ = s (⟨i + 1, hi⟩ : Fin m)
him : i < m
⊢ s (⟨i, him⟩ : Fin m) - s (⟨i + 1, hi⟩ : Fin m) + s (⟨i + 1, hi⟩ : Fin m) = s ⟨i, him⟩

Tactic:
exact Nat.sub_add_cancel (hs i.le_succ)

Premises used: Nat.sub_add_cancel
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i : ℕ
this : i ≤ m - 1
hm : m - 1 < m
⊢ m = m - 1 + 1

Tactic:
have := (Nat.sub_one_add_one <| Nat.ne_zero_of_lt hm).symm
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i : ℕ
this_1 : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
refine_2 : ∀ (j : Fin n), m ≤ (↑j : ℕ) → invAccumulate n m s j = 0
⊢ (accumulate n m : (a : Fin n → ℕ) → Fin m → ℕ) (invAccumulate n m s) ⟨m - 1, hm⟩ = s (⟨m - 1, hm⟩ : Fin m)

Tactic:
rw [accumulate_last (hm.trans_le hmn) this, invAccumulate, dif_pos hm, dif_neg this.not_gt,
      Nat.sub_zero]

Premises used: Eq.not_gt, Fin.invAccumulate, dif_pos, dif_neg, LT.lt.trans_le, Nat.sub_zero, Fin.accumulate_last
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
n m : ℕ
hmn : m ≤ n
s : Fin m → ℕ
hs : Antitone s
x : Fin m
i : ℕ
this_1 : i ≤ m - 1
hm : m - 1 < m
this : m = m - 1 + 1
j : Fin n
hj : m ≤ (↑j : ℕ)
refine_2 :
  HSub.hSub (α := ℕ) (if hi : (↑j : ℕ) < m then s (⟨(↑j : ℕ), hi⟩ : Fin m) else 0)
      (if hi : (↑j : ℕ) + 1 < m then s (⟨(↑j : ℕ) + 1, hi⟩ : Fin m) else 0) =
    0
refine_2₁ : HSub.hSub (α := ℕ) 0 (if hi : (↑j : ℕ) + 1 < m then s (⟨(↑j : ℕ) + 1, hi⟩ : Fin m) else 0) = 0
refine_2₂ refine_2₃ : Eq (α := ℕ) 0 0
⊢ invAccumulate n m s j = 0

Tactic:
rw [invAccumulate, dif_neg hj.not_gt, Nat.zero_sub]

Premises used: Nat.zero_sub, Fin.invAccumulate, dif_neg, LE.le.not_gt
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
p : MvPolynomial (Fin n) R
⊢ Eq (α := MvPolynomial σ R)
    ((↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R)) p) : MvPolynomial σ R) :
      MvPolynomial σ R)
    ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R) p :
      MvPolynomial σ R)

Tactic:
(Subalgebra.mvPolynomial_aeval_coe _ _ _).symm

Premises used: Multiset.sum, Multiset.foldr, Set.Mem, Subalgebra.mvPolynomial_aeval_coe, MvPolynomial.esymm, Multiset.powersetCard, Eq.symm, Finset.sum
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
inst_2 : Fintype τ
e : σ ≃ τ
hf :
  ∀ (i : Fin n),
    Eq (α := MvPolynomial τ R)
      (↑((AlgHom.comp (↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R))
                (esymmAlgHom σ R n) :
              (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R))
            (X i)) :
        MvPolynomial τ R)
      (↑((esymmAlgHom τ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra τ R)) (X i)) : MvPolynomial τ R)
⊢ Eq (α := MvPolynomial (Fin n) R →ₐ[R] ↥(symmetricSubalgebra τ R))
    (AlgHom.comp (↑(renameSymmetricSubalgebra e) : ↥(symmetricSubalgebra σ R) →ₐ[R] ↥(symmetricSubalgebra τ R))
      (esymmAlgHom σ R n))
    (esymmAlgHom τ R n)

Tactic:
ext i : 2
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
t : Fin n →₀ ℕ
r : R
⊢ IsSymmetric (esymmAlgHomMonomial σ t r)

Tactic:
(esymmAlgHom _ _ _ _).2

Premises used: MvPolynomial.IsSymmetric, MvPolynomial.esymmAlgHomMonomial, Set.Mem, setOf, MvPolynomial.esymmAlgHom, DFunLike.coe, Subtype.property
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
n k : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
i : Fin n
r : R
rw : HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (esymm σ R ((↑i : ℕ) + 1)) 0 = 1
⊢ esymmAlgHomMonomial σ (fun₀ | i => k) r =
    HMul.hMul (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
      (HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k)

Tactic:
rw [esymmAlgHomMonomial, esymmAlgHom_apply, aeval_monomial, algebraMap_eq,
    Finsupp.prod_single_index]

Premises used: MvPolynomial.esymmAlgHomMonomial, MvPolynomial.algebraMap_eq, MvPolynomial.esymmAlgHom_apply, MvPolynomial.aeval_monomial, Finsupp.prod_single_index
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
n k : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
i : Fin n
r : R
⊢ HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (esymm σ R ((↑i : ℕ) + 1)) 0 = 1

Tactic:
pow_zero _

Premises used: pow_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
n k : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
i : Fin n
r : R
⊢ HPow.hPow (α := MvPolynomial σ R) (β := ℕ) (esymm σ R ((↑i : ℕ) + 1)) 0 = 1

Tactic:
exact pow_zero _

Premises used: pow_zero
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
n k : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
i : Fin n
rw :
  (C : (a : R) → MvPolynomial σ R) 1 * HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k =
    HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k
rw₁ :
  1 * HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k =
    HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k
rw₂ rw₃ :
  HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k =
    HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k
⊢ esymmAlgHomMonomial σ (fun₀ | i => k) 1 = HPow.hPow (α := MvPolynomial σ R) (esymm σ R ((↑i : ℕ) + 1)) k

Tactic:
rw [esymmAlgHomMonomial_single, map_one, one_mul]

Premises used: MvPolynomial.esymmAlgHomMonomial_single, map_one, one_mul
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
r : R
t s : Fin n →₀ ℕ
simp_rw :
  (↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
          ((monomial (t + s) : (a : R) → MvPolynomial (Fin n) R) r)) :
      MvPolynomial σ R) =
    HMul.hMul (α := MvPolynomial σ R)
      (↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            ((monomial t : (a : R) → MvPolynomial (Fin n) R) r)) :
        MvPolynomial σ R)
      (↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            ((monomial s : (a : R) → MvPolynomial (Fin n) R) 1)) :
        MvPolynomial σ R)
simp_rw₁ :
  (aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
      ((monomial (t + s) : (a : R) → MvPolynomial (Fin n) R) r) =
    HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
          ((monomial t : (a : R) → MvPolynomial (Fin n) R) r) :
        MvPolynomial σ R)
      ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
          ((monomial s : (a : R) → MvPolynomial (Fin n) R) 1) :
        MvPolynomial σ R)
simp_rw₂ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
        ((monomial (t + s) : (a : R) → MvPolynomial (Fin n) R) r) :
      MvPolynomial σ R)
    ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
        (HMul.hMul (α := MvPolynomial (Fin n) R) (β := MvPolynomial (Fin n) R)
          ((monomial t : (a : R) → MvPolynomial (Fin n) R) r : MvPolynomial (Fin n) R)
          ((monomial s : (a : R) → MvPolynomial (Fin n) R) 1 : MvPolynomial (Fin n) R)) :
      MvPolynomial σ R)
simp_rw₃ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
        ((monomial (t + s) : (a : R) → MvPolynomial (Fin n) R) r) :
      MvPolynomial σ R)
    ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
        ((monomial (t + s) : (a : R) → MvPolynomial (Fin n) R) (r * 1)) :
      MvPolynomial σ R)
⊢ esymmAlgHomMonomial σ (t + s) r =
    HMul.hMul (α := MvPolynomial σ R) (esymmAlgHomMonomial σ t r) (esymmAlgHomMonomial σ s 1)

Tactic:
simp_rw [esymmAlgHomMonomial, esymmAlgHom_apply, ← map_mul, monomial_mul, mul_one]

Premises used: MvPolynomial.esymmAlgHomMonomial, map_mul, MvPolynomial.monomial_mul, MvPolynomial.esymmAlgHom_apply, mul_one
-- Module: Mathlib.RingTheory.MvPolynomial.Symmetric.FundamentalTheorem
Goal:
σ : Type u_1
R : Type u_3
n : ℕ
inst : CommSemiring R
inst_1 : Fintype σ
r : R
rw :
  Eq (α := MvPolynomial σ R)
    ((↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            ((monomial 0 : (a : R) → MvPolynomial (Fin n) R) r)) :
        MvPolynomial σ R) :
      MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
rw₁ :
  Eq (α := MvPolynomial σ R)
    ((↑((esymmAlgHom σ R n : (a : MvPolynomial (Fin n) R) → ↥(symmetricSubalgebra σ R))
            ((C : (a : R) → MvPolynomial (Fin n) R) r)) :
        MvPolynomial σ R) :
      MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
rw₂ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : Fin n) ↦ esymm σ R ((↑i : ℕ) + 1) : (a : MvPolynomial (Fin n) R) → MvPolynomial σ R)
        ((C : (a : R) → MvPolynomial (Fin n) R) r) :
      MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
rw₃ :
  Eq (α := MvPolynomial σ R) ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
rw₄ rw₅ :
  Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
    ((C : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R) (esymmAlgHomMonomial σ (n := n) 0 r) ((C : (a : R) → MvPolynomial σ R) r)

Tactic:
rw [esymmAlgHomMonomial, monomial_zero', esymmAlgHom_apply, aeval_C, algebraMap_eq]

Premises used: MvPolynomial.esymmAlgHomMonomial, MvPolynomial.monomial_zero', MvPolynomial.algebraMap_eq, MvPolynomial.esymmAlgHom_apply, MvPolynomial.aeval_C