-- Mathlib/RingTheory/MvPolynomial/Symmetric/NewtonIdentities.lean
theorem disjUnion_filter_pairs_eq_pairs (k : ℕ) :
    disjUnion {t ∈ pairs σ k | #t.1 < k} {t ∈ pairs σ k | #t.1 = k}
      (disjoint_filter_pairs_lt_filter_pairs_eq σ k) = pairs σ k

Proof state:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a : Finset σ × σ
⊢ a ∈ univ ∧ ((#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 < k ∨ (#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 = k) ↔
    a ∈ univ ∧ #a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)

Tactic:
refine ⟨fun ha ↦ by tauto, fun ha ↦ ?_⟩

Result:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a : Finset σ × σ
ha : a ∈ univ ∧ #a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)
⊢ a ∈ univ ∧ ((#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 < k ∨ (#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 = k)

Proof state:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a : Finset σ × σ
ha : a ∈ univ ∧ #a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)
⊢ a ∈ univ ∧ ((#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 < k ∨ (#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 = k)

Tactic:
have hacard := le_iff_lt_or_eq.mp ha.2.1

Result:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a : Finset σ × σ
ha : a ∈ univ ∧ #a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)
hacard : #a.1 < k ∨ #a.1 = k
⊢ a ∈ univ ∧ ((#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 < k ∨ (#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 = k)

Proof state:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
⊢ ∀ (a : Finset σ × σ),
    a ∈
        filter (fun a => (#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 < k) univ ∪
          filter (fun a => (#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 = k) univ ↔
      a ∈ univ ∧ #a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)

Tactic:
intro a

Result:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a : Finset σ × σ
⊢ a ∈
      filter (fun a => (#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 < k) univ ∪
        filter (fun a => (#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 = k) univ ↔
    a ∈ univ ∧ #a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)

Proof state:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a : Finset σ × σ
ha : a ∈ univ ∧ #a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)
hacard : #a.1 < k ∨ #a.1 = k
⊢ a ∈ univ ∧ ((#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 < k ∨ (#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 = k)

Tactic:
tauto

Result:
no goals

Proof state:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
⊢ (filter (fun t => #t.1 < k) (MvPolynomial.NewtonIdentities.pairs σ k)).disjUnion
      (filter (fun t => #t.1 = k) (MvPolynomial.NewtonIdentities.pairs σ k)) ⋯ =
    MvPolynomial.NewtonIdentities.pairs σ k

Tactic:
simp only [disjUnion_eq_union, Finset.ext_iff, pairs, filter_filter, mem_filter]

Result:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
⊢ ∀ (a : Finset σ × σ),
    a ∈
        filter (fun a => (#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 < k) univ ∪
          filter (fun a => (#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 = k) univ ↔
      a ∈ univ ∧ #a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)

Proof state:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a : Finset σ × σ
⊢ a ∈
      filter (fun a => (#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 < k) univ ∪
        filter (fun a => (#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 = k) univ ↔
    a ∈ univ ∧ #a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)

Tactic:
rw [← filter_or, mem_filter]

Result:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a : Finset σ × σ
⊢ a ∈ univ ∧ ((#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 < k ∨ (#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 = k) ↔
    a ∈ univ ∧ #a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)

Proof state:
σ : Type u_1
inst✝¹ : DecidableEq σ
inst✝ : Fintype σ
k : ℕ
a : Finset σ × σ
ha : a ∈ univ ∧ ((#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 < k ∨ (#a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)) ∧ #a.1 = k)
⊢ a ∈ univ ∧ #a.1 ≤ k ∧ (#a.1 = k → a.2 ∈ a.1)

Tactic:
tauto

Result:
no goals