-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
theorem pairMap_mem_pairs {k : ℕ} (t : Finset σ × σ) (h : t ∈ pairs σ k) :
    pairMap σ t ∈ pairs σ k

Proof state:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∈ t.1
⊢ #(MvPolynomial.NewtonIdentities.pairMap σ t).1 ≤ k ∧
    (#(MvPolynomial.NewtonIdentities.pairMap σ t).1 = k →
      (MvPolynomial.NewtonIdentities.pairMap σ t).2 ∈ (MvPolynomial.NewtonIdentities.pairMap σ t).1)

Tactic:
rw [pairMap_of_snd_mem_fst σ h1]

Result:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∈ t.1
⊢ #(t.1.erase t.2, t.2).1 ≤ k ∧ (#(t.1.erase t.2, t.2).1 = k → (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1)

Proof state:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∈ t.1
⊢ #(t.1.erase t.2, t.2).1 ≤ k ∧ (#(t.1.erase t.2, t.2).1 = k → (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1)

Tactic:
simp only [h1, implies_true, and_true] at h

Result:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
⊢ #(t.1.erase t.2, t.2).1 ≤ k ∧ (#(t.1.erase t.2, t.2).1 = k → (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1)

Proof state:
case inr
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∉ t.1
⊢ #(MvPolynomial.NewtonIdentities.pairMap σ t).1 ≤ k ∧
    (#(MvPolynomial.NewtonIdentities.pairMap σ t).1 = k →
      (MvPolynomial.NewtonIdentities.pairMap σ t).2 ∈ (MvPolynomial.NewtonIdentities.pairMap σ t).1)

Tactic:
rw [pairMap_of_snd_nmem_fst σ h1]

Result:
case inr
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∉ t.1
⊢ #(cons t.2 t.1 h1, t.2).1 ≤ k ∧ (#(cons t.2 t.1 h1, t.2).1 = k → (cons t.2 t.1 h1, t.2).2 ∈ (cons t.2 t.1 h1, t.2).1)

Proof state:
case inr
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h : #t.1 ≤ k ∧ (#t.1 = k → False)
⊢ #(cons t.2 t.1 h1, t.2).1 ≤ k ∧ (#(cons t.2 t.1 h1, t.2).1 = k → (cons t.2 t.1 h1, t.2).2 ∈ (cons t.2 t.1 h1, t.2).1)

Tactic:
simp only [card_cons, mem_cons, true_or, implies_true, and_true]

Result:
case inr
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h : #t.1 ≤ k ∧ (#t.1 = k → False)
⊢ #t.1 + 1 ≤ k

Proof state:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
h2 : #t.1 - 1 = k
⊢ False

Tactic:
rw [← h2] at h

Result:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ #t.1 - 1
h2 : #t.1 - 1 = k
⊢ False

Proof state:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ #t.1 - 1
h2 : #t.1 - 1 = k
⊢ False

Tactic:
exact not_le_of_lt (sub_lt (card_pos.mpr ⟨t.snd, h1⟩) zero_lt_one) h

Result:
no goals

Proof state:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : t ∈ MvPolynomial.NewtonIdentities.pairs σ k
⊢ MvPolynomial.NewtonIdentities.pairMap σ t ∈ MvPolynomial.NewtonIdentities.pairs σ k

Tactic:
rw [mem_pairs] at h ⊢

Result:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
⊢ #(MvPolynomial.NewtonIdentities.pairMap σ t).1 ≤ k ∧
    (#(MvPolynomial.NewtonIdentities.pairMap σ t).1 = k →
      (MvPolynomial.NewtonIdentities.pairMap σ t).2 ∈ (MvPolynomial.NewtonIdentities.pairMap σ t).1)

Proof state:
case inr
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h : #t.1 ≤ k ∧ (#t.1 = k → False)
⊢ #t.1 + 1 ≤ k

Tactic:
exact (le_iff_eq_or_lt.mp h.left).resolve_left h.right

Result:
no goals

Proof state:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
⊢ #t.1 - 1 = k → ¬True ∧ True

Tactic:
by_contra h2

Result:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
h2 : ¬(#t.1 - 1 = k → ¬True ∧ True)
⊢ False

Proof state:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
h2 : ¬(#t.1 - 1 = k → ¬True ∧ True)
⊢ False

Tactic:
simp only [not_true_eq_false, and_true, not_forall, not_false_eq_true, exists_prop] at h2

Result:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
h2 : #t.1 - 1 = k
⊢ False

Proof state:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
⊢ #(t.1.erase t.2, t.2).1 ≤ k ∧ (#(t.1.erase t.2, t.2).1 = k → (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1)

Tactic:
simp only [card_erase_of_mem h1, tsub_le_iff_right, mem_erase, ne_eq, h1]

Result:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
⊢ #t.1 ≤ k + 1 ∧ (#t.1 - 1 = k → ¬True ∧ True)

Proof state:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
⊢ #t.1 ≤ k + 1 ∧ (#t.1 - 1 = k → ¬True ∧ True)

Tactic:
refine ⟨le_step h, ?_⟩

Result:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h : #t.1 ≤ k
⊢ #t.1 - 1 = k → ¬True ∧ True

Proof state:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
⊢ #(MvPolynomial.NewtonIdentities.pairMap σ t).1 ≤ k ∧
    (#(MvPolynomial.NewtonIdentities.pairMap σ t).1 = k →
      (MvPolynomial.NewtonIdentities.pairMap σ t).2 ∈ (MvPolynomial.NewtonIdentities.pairMap σ t).1)

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

Result:
case inl
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∈ t.1
⊢ #(MvPolynomial.NewtonIdentities.pairMap σ t).1 ≤ k ∧
    (#(MvPolynomial.NewtonIdentities.pairMap σ t).1 = k →
      (MvPolynomial.NewtonIdentities.pairMap σ t).2 ∈ (MvPolynomial.NewtonIdentities.pairMap σ t).1)

case inr
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∉ t.1
⊢ #(MvPolynomial.NewtonIdentities.pairMap σ t).1 ≤ k ∧
    (#(MvPolynomial.NewtonIdentities.pairMap σ t).1 = k →
      (MvPolynomial.NewtonIdentities.pairMap σ t).2 ∈ (MvPolynomial.NewtonIdentities.pairMap σ t).1)

Proof state:
case inr
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h : #t.1 ≤ k ∧ (#t.1 = k → t.2 ∈ t.1)
h1 : t.2 ∉ t.1
⊢ #(cons t.2 t.1 h1, t.2).1 ≤ k ∧ (#(cons t.2 t.1 h1, t.2).1 = k → (cons t.2 t.1 h1, t.2).2 ∈ (cons t.2 t.1 h1, t.2).1)

Tactic:
simp only [h1] at h

Result:
case inr
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h : #t.1 ≤ k ∧ (#t.1 = k → False)
⊢ #(cons t.2 t.1 h1, t.2).1 ≤ k ∧ (#(cons t.2 t.1 h1, t.2).1 = k → (cons t.2 t.1 h1, t.2).2 ∈ (cons t.2 t.1 h1, t.2).1)