-- Mathlib/Data/Sym/Sym2.lean
theorem filter_image_mk_not_isDiag [DecidableEq α] (s : Finset α) :
    {a ∈ (s ×ˢ s).image Sym2.mk | ¬a.IsDiag} = s.offDiag.image Sym2.mk

Proof state:
case h.h.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
h : s(a, b) = s(x✝, y✝)
ha : a ∈ s
hb : b ∈ s
hab : ¬s(x✝, y✝).IsDiag
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ s(a, b) = s(x✝, y✝)) ∧ ¬s(x✝, y✝).IsDiag

Tactic:
exact ⟨⟨a, b, ⟨ha, hb⟩, h⟩, hab⟩

Result:
no goals

Proof state:
case h.h.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
h : s(a, b) = s(x✝, y✝)
ha : a ∈ s
hb : b ∈ s
hab : a ≠ b
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ s(a, b) = s(x✝, y✝)) ∧ ¬s(x✝, y✝).IsDiag

Tactic:
rw [Ne, ← Sym2.mk_isDiag_iff, h] at hab

Result:
case h.h.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
h : s(a, b) = s(x✝, y✝)
ha : a ∈ s
hb : b ∈ s
hab : ¬s(x✝, y✝).IsDiag
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ s(a, b) = s(x✝, y✝)) ∧ ¬s(x✝, y✝).IsDiag

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ filter (fun a => ¬a.IsDiag) (image Sym2.mk (s ×ˢ s)) = image Sym2.mk s.offDiag

Tactic:
ext z

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
z : Sym2 α
⊢ z ∈ filter (fun a => ¬a.IsDiag) (image Sym2.mk (s ×ˢ s)) ↔ z ∈ image Sym2.mk s.offDiag

Proof state:
case h.h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ s(a, b) = s(x✝, y✝)) ∧ ¬s(x✝, y✝).IsDiag ↔
    ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ s(a, b) = s(x✝, y✝)

Tactic:
constructor

Result:
case h.h.mp
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ s(a, b) = s(x✝, y✝)) ∧ ¬s(x✝, y✝).IsDiag →
    ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ s(a, b) = s(x✝, y✝)

case h.h.mpr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ s(a, b) = s(x✝, y✝)) →
    (∃ a b, (a ∈ s ∧ b ∈ s) ∧ s(a, b) = s(x✝, y✝)) ∧ ¬s(x✝, y✝).IsDiag

Proof state:
case h.h.mpr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ s(a, b) = s(x✝, y✝)) →
    (∃ a b, (a ∈ s ∧ b ∈ s) ∧ s(a, b) = s(x✝, y✝)) ∧ ¬s(x✝, y✝).IsDiag

Tactic:
rintro ⟨a, b, ⟨ha, hb, hab⟩, h⟩

Result:
case h.h.mpr.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
h : s(a, b) = s(x✝, y✝)
ha : a ∈ s
hb : b ∈ s
hab : a ≠ b
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ s(a, b) = s(x✝, y✝)) ∧ ¬s(x✝, y✝).IsDiag

Proof state:
case h.h.mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
hab : ¬s(x✝, y✝).IsDiag
a b : α
h : s(a, b) = s(x✝, y✝)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ s(a, b) = s(x✝, y✝)

Tactic:
rw [← h, Sym2.mk_isDiag_iff] at hab

Result:
case h.h.mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
hab : ¬a = b
h : s(a, b) = s(x✝, y✝)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ s(a, b) = s(x✝, y✝)

Proof state:
case h.h.mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ a b : α
hab : ¬a = b
h : s(a, b) = s(x✝, y✝)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ s(a, b) = s(x✝, y✝)

Tactic:
exact ⟨a, b, ⟨ha, hb, hab⟩, h⟩

Result:
no goals

Proof state:
case h.h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ s(x✝, y✝) ∈ filter (fun a => ¬a.IsDiag) (image Sym2.mk (s ×ˢ s)) ↔ s(x✝, y✝) ∈ image Sym2.mk s.offDiag

Tactic:
simp only [mem_image, mem_offDiag, mem_filter, Prod.exists, mem_product]

Result:
case h.h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ s(a, b) = s(x✝, y✝)) ∧ ¬s(x✝, y✝).IsDiag ↔
    ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ s(a, b) = s(x✝, y✝)

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
z : Sym2 α
⊢ z ∈ filter (fun a => ¬a.IsDiag) (image Sym2.mk (s ×ˢ s)) ↔ z ∈ image Sym2.mk s.offDiag

Tactic:
induction z

Result:
case h.h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ s(x✝, y✝) ∈ filter (fun a => ¬a.IsDiag) (image Sym2.mk (s ×ˢ s)) ↔ s(x✝, y✝) ∈ image Sym2.mk s.offDiag

Proof state:
case h.h.mp
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
⊢ (∃ a b, (a ∈ s ∧ b ∈ s) ∧ s(a, b) = s(x✝, y✝)) ∧ ¬s(x✝, y✝).IsDiag →
    ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ s(a, b) = s(x✝, y✝)

Tactic:
rintro ⟨⟨a, b, ⟨ha, hb⟩, h⟩, hab⟩

Result:
case h.h.mp.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x✝ y✝ : α
hab : ¬s(x✝, y✝).IsDiag
a b : α
h : s(a, b) = s(x✝, y✝)
ha : a ∈ s
hb : b ∈ s
⊢ ∃ a b, (a ∈ s ∧ b ∈ s ∧ a ≠ b) ∧ s(a, b) = s(x✝, y✝)