-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
theorem pairMap_involutive : (pairMap σ).Involutive

Proof state:
case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h2 : (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1
⊢ ((t.1.erase t.2, t.2).1.erase (t.1.erase t.2, t.2).2, (t.1.erase t.2, t.2).2) = t

Tactic:
simp at h2

Result:
no goals

Proof state:
case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h3 : (cons t.2 t.1 h1, t.2).2 ∉ (cons t.2 t.1 h1, t.2).1
⊢ (cons (cons t.2 t.1 h1, t.2).2 (cons t.2 t.1 h1, t.2).1 ⋯, (cons t.2 t.1 h1, t.2).2) = t

Tactic:
simp at h3

Result:
no goals

Proof state:
case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h2 : (t.1.erase t.2, t.2).2 ∉ (t.1.erase t.2, t.2).1
⊢ (cons (t.1.erase t.2, t.2).2 (t.1.erase t.2, t.2).1 ⋯, (t.1.erase t.2, t.2).2) = t

Tactic:
simp [insert_erase h1]

Result:
no goals

Proof state:
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ (if h :
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2 ∈
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1 then
      ((if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1.erase
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)
    else
      (cons (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1 h,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)) =
    t

Tactic:
split_ifs with h1 h2 h3

Result:
case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h2 : (t.1.erase t.2, t.2).2 ∈ (t.1.erase t.2, t.2).1
⊢ ((t.1.erase t.2, t.2).1.erase (t.1.erase t.2, t.2).2, (t.1.erase t.2, t.2).2) = t

case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∈ t.1
h2 : (t.1.erase t.2, t.2).2 ∉ (t.1.erase t.2, t.2).1
⊢ (cons (t.1.erase t.2, t.2).2 (t.1.erase t.2, t.2).1 ⋯, (t.1.erase t.2, t.2).2) = t

case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h3 : (cons t.2 t.1 h1, t.2).2 ∈ (cons t.2 t.1 h1, t.2).1
⊢ ((cons t.2 t.1 h1, t.2).1.erase (cons t.2 t.1 h1, t.2).2, (cons t.2 t.1 h1, t.2).2) = t

case neg
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h3 : (cons t.2 t.1 h1, t.2).2 ∉ (cons t.2 t.1 h1, t.2).1
⊢ (cons (cons t.2 t.1 h1, t.2).2 (cons t.2 t.1 h1, t.2).1 ⋯, (cons t.2 t.1 h1, t.2).2) = t

Proof state:
case pos
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
h1 : t.2 ∉ t.1
h3 : (cons t.2 t.1 h1, t.2).2 ∈ (cons t.2 t.1 h1, t.2).1
⊢ ((cons t.2 t.1 h1, t.2).1.erase (cons t.2 t.1 h1, t.2).2, (cons t.2 t.1 h1, t.2).2) = t

Tactic:
simp_all

Result:
no goals

Proof state:
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ MvPolynomial.NewtonIdentities.pairMap σ (MvPolynomial.NewtonIdentities.pairMap σ t) = t

Tactic:
rw [pairMap, pairMap]

Result:
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ (if h :
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2 ∈
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1 then
      ((if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1.erase
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)
    else
      (cons (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2
          (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).1 h,
        (if h : t.2 ∈ t.1 then (t.1.erase t.2, t.2) else (cons t.2 t.1 h, t.2)).2)) =
    t

Proof state:
σ : Type u_1
inst✝ : DecidableEq σ
⊢ Function.Involutive (MvPolynomial.NewtonIdentities.pairMap σ)

Tactic:
intro t

Result:
σ : Type u_1
inst✝ : DecidableEq σ
t : Finset σ × σ
⊢ MvPolynomial.NewtonIdentities.pairMap σ (MvPolynomial.NewtonIdentities.pairMap σ t) = t