-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
theorem weight_add_weight_pairMap {k : ℕ} (t : Finset σ × σ) (h : t ∈ pairs σ k) :
    weight σ R k t + weight σ R k (pairMap σ t) = 0

Proof state:
case inr
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∉ t.1
⊢ (∏ a ∈ t.1, X a) * (X t.2 ^ (k - #t.1) * (-1) ^ #t.1) + (∏ a ∈ t.1, X a) * (X t.2 ^ (k - #t.1) * (-1) ^ (#t.1 + 1)) =
    0

Tactic:
rw [← neg_neg ((-1 : MvPolynomial σ R) ^ #t.1), h2]

Result:
case inr
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∉ t.1
⊢ (∏ a ∈ t.1, X a) * (X t.2 ^ (k - #t.1) * -(-1) ^ (#t.1 + 1)) +
      (∏ a ∈ t.1, X a) * (X t.2 ^ (k - #t.1) * (-1) ^ (#t.1 + 1)) =
    0

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(MvPolynomial.NewtonIdentities.pairMap σ t).1 *
        ((∏ a ∈ (MvPolynomial.NewtonIdentities.pairMap σ t).1, X a) *
          X (MvPolynomial.NewtonIdentities.pairMap σ t).2 ^ (k - #(MvPolynomial.NewtonIdentities.pairMap σ t).1)) =
    0

Tactic:
rcases (em (t.snd ∈ t.fst)) with h1 | h1

Result:
case inl
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∈ t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(MvPolynomial.NewtonIdentities.pairMap σ t).1 *
        ((∏ a ∈ (MvPolynomial.NewtonIdentities.pairMap σ t).1, X a) *
          X (MvPolynomial.NewtonIdentities.pairMap σ t).2 ^ (k - #(MvPolynomial.NewtonIdentities.pairMap σ t).1)) =
    0

case inr
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∉ t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(MvPolynomial.NewtonIdentities.pairMap σ t).1 *
        ((∏ a ∈ (MvPolynomial.NewtonIdentities.pairMap σ t).1, X a) *
          X (MvPolynomial.NewtonIdentities.pairMap σ t).2 ^ (k - #(MvPolynomial.NewtonIdentities.pairMap σ t).1)) =
    0

Proof state:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(MvPolynomial.NewtonIdentities.pairMap σ t).1 *
        ((∏ a ∈ (MvPolynomial.NewtonIdentities.pairMap σ t).1, X a) *
          X (MvPolynomial.NewtonIdentities.pairMap σ t).2 ^ (k - #(MvPolynomial.NewtonIdentities.pairMap σ t).1)) =
    0

Tactic:
have h2 (n : ℕ) : -(-1 : MvPolynomial σ R) ^ n = (-1) ^ (n + 1) := by
  rw [← neg_one_mul ((-1 : MvPolynomial σ R) ^ n), pow_add, pow_one, mul_comm]

Result:
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(MvPolynomial.NewtonIdentities.pairMap σ t).1 *
        ((∏ a ∈ (MvPolynomial.NewtonIdentities.pairMap σ t).1, X a) *
          X (MvPolynomial.NewtonIdentities.pairMap σ t).2 ^ (k - #(MvPolynomial.NewtonIdentities.pairMap σ t).1)) =
    0

Proof state:
case inr
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∉ t.1
⊢ (∏ a ∈ t.1, X a) * (X t.2 ^ (k - #t.1) * (-1) ^ #t.1) +
      (∏ a ∈ t.1, X a) * (X t.2 ^ 1 * X t.2 ^ (k - (#t.1 + 1)) * (-1) ^ (#t.1 + 1)) =
    0

Tactic:
simp only [← pow_add, ← Nat.add_sub_assoc (Nat.lt_of_le_of_ne h.left (mt h.right h1)), add_comm,
  Nat.succ_eq_add_one, Nat.add_sub_add_right]

Result:
case inr
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∉ t.1
⊢ (∏ a ∈ t.1, X a) * (X t.2 ^ (k - #t.1) * (-1) ^ #t.1) + (∏ a ∈ t.1, X a) * (X t.2 ^ (k - #t.1) * (-1) ^ (#t.1 + 1)) =
    0

Proof state:
case inr
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∉ t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(MvPolynomial.NewtonIdentities.pairMap σ t).1 *
        ((∏ a ∈ (MvPolynomial.NewtonIdentities.pairMap σ t).1, X a) *
          X (MvPolynomial.NewtonIdentities.pairMap σ t).2 ^ (k - #(MvPolynomial.NewtonIdentities.pairMap σ t).1)) =
    0

Tactic:
rw [pairMap_of_snd_nmem_fst σ h1]

Result:
case inr
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∉ t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(cons t.2 t.1 h1, t.2).1 *
        ((∏ a ∈ (cons t.2 t.1 h1, t.2).1, X a) * X (cons t.2 t.1 h1, t.2).2 ^ (k - #(cons t.2 t.1 h1, t.2).1)) =
    0

Proof state:
case inl
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∈ t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1.erase t.2, X a) * (X t.2 ^ 1 * X t.2 ^ (k - #t.1))) +
      (-1) ^ (#t.1 - 1) * ((∏ a ∈ t.1.erase t.2, X a) * X t.2 ^ (k - (#t.1 - 1))) =
    0

Tactic:
simp only [← pow_add, add_comm]

Result:
case inl
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∈ t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1.erase t.2, X a) * X t.2 ^ (k - #t.1 + 1)) +
      (-1) ^ (#t.1 - 1) * ((∏ a ∈ t.1.erase t.2, X a) * X t.2 ^ (k - (#t.1 - 1))) =
    0

Proof state:
case inr
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∉ t.1
⊢ (-1) ^ #t.1 * ((∏ a ∈ t.1, X a) * X t.2 ^ (k - #t.1)) +
      (-1) ^ #(cons t.2 t.1 h1, t.2).1 *
        ((∏ a ∈ (cons t.2 t.1 h1, t.2).1, X a) * X (cons t.2 t.1 h1, t.2).2 ^ (k - #(cons t.2 t.1 h1, t.2).1)) =
    0

Tactic:
simp only [mul_comm, mul_assoc (∏ a ∈ t.fst, X a), card_cons, prod_cons]

Result:
case inr
σ : Type u_1
R : Type u_2
inst✝² : CommRing R
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h2 : ∀ (n : ℕ), -(-1) ^ n = (-1) ^ (n + 1)
h1 : t.2 ∉ t.1
⊢ (∏ a ∈ t.1, X a) * (X t.2 ^ (k - #t.1) * (-1) ^ #t.1) +
      (∏ a ∈ t.1, X a) * (X t.2 * X t.2 ^ (k - (#t.1 + 1)) * (-1) ^ (#t.1 + 1)) =
    0