-- Mathlib/Data/Sym/Card.lean
lemma two_mul_card_image_offDiag (s : Finset α) : 2 * #(s.offDiag.image Sym2.mk) = #s.offDiag

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Sym2.mk z = s(x, y)) s.offDiag = {(x, y), (y, x)}
⊢ x = y → ¬y = x

Tactic:
exact fun _ => hxy'

Result:
no goals

Proof state:
case h.mk
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
x₁ y₁ : α
⊢ (x₁, y₁) ∈ filter (fun z => Sym2.mk z = s(x, y)) s.offDiag ↔ (x₁, y₁) ∈ {(x, y), (y, x)}

Tactic:
rw [mem_filter, mem_insert, mem_singleton, Sym2.eq_iff, Prod.mk.inj_iff, Prod.mk.inj_iff,
  and_iff_right_iff_imp]

Result:
case h.mk
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
x₁ y₁ : α
⊢ x₁ = x ∧ y₁ = y ∨ x₁ = y ∧ y₁ = x → (x₁, y₁) ∈ s.offDiag

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
hxy : s(x, y) ∈ image Sym2.mk s.offDiag
⊢ #(filter (fun a => Sym2.mk a = s(x, y)) s.offDiag) = 2

Tactic:
simp_rw [mem_image, mem_offDiag] at hxy

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
hxy : ∃ a, (a.1 ∈ s ∧ a.2 ∈ s ∧ a.1 ≠ a.2) ∧ Sym2.mk a = s(x, y)
⊢ #(filter (fun a => Sym2.mk a = s(x, y)) s.offDiag) = 2

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
h : Sym2.mk a = s(x, y)
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
⊢ #(filter (fun a => Sym2.mk a = s(x, y)) s.offDiag) = 2

Tactic:
replace h := Sym2.eq.1 h

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
⊢ #(filter (fun a => Sym2.mk a = s(x, y)) s.offDiag) = 2

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
⊢ x ∈ s ∧ y ∈ s ∧ x ≠ y

Tactic:
cases h <;> refine ⟨‹_›, ‹_›, ?_⟩ <;> [exact ha; exact ha.symm]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ ∀ (x y : α), s(x, y) ∈ image Sym2.mk s.offDiag → #(filter (fun a => Sym2.mk a = s(x, y)) s.offDiag) = 2

Tactic:
rintro x y hxy

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
hxy : s(x, y) ∈ image Sym2.mk s.offDiag
⊢ #(filter (fun a => Sym2.mk a = s(x, y)) s.offDiag) = 2

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ 2 * #(image Sym2.mk s.offDiag) = #s.offDiag

Tactic:
rw [card_eq_sum_card_image (Sym2.mk : α × α → _), sum_const_nat (Sym2.ind _), mul_comm]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ ∀ (x y : α), s(x, y) ∈ image Sym2.mk s.offDiag → #(filter (fun a => Sym2.mk a = s(x, y)) s.offDiag) = 2

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
⊢ #(filter (fun a => Sym2.mk a = s(x, y)) s.offDiag) = 2

Tactic:
obtain ⟨hx, hy, hxy⟩ : x ∈ s ∧ y ∈ s ∧ x ≠ y := by
  cases h <;> refine ⟨‹_›, ‹_›, ?_⟩ <;> [exact ha; exact ha.symm]

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
⊢ #(filter (fun a => Sym2.mk a = s(x, y)) s.offDiag) = 2

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Sym2.mk z = s(x, y)) s.offDiag = {(x, y), (y, x)}
⊢ #(filter (fun a => Sym2.mk a = s(x, y)) s.offDiag) = 2

Tactic:
rw [this, card_insert_of_not_mem, card_singleton]

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Sym2.mk z = s(x, y)) s.offDiag = {(x, y), (y, x)}
⊢ (x, y) ∉ {(y, x)}

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
⊢ #(filter (fun a => Sym2.mk a = s(x, y)) s.offDiag) = 2

Tactic:
have hxy' : y ≠ x := hxy.symm

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
⊢ #(filter (fun a => Sym2.mk a = s(x, y)) s.offDiag) = 2

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Sym2.mk z = s(x, y)) s.offDiag = {(x, y), (y, x)}
⊢ (x, y) ∉ {(y, x)}

Tactic:
simp only [not_and, Prod.mk.inj_iff, mem_singleton]

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
this : filter (fun z => Sym2.mk z = s(x, y)) s.offDiag = {(x, y), (y, x)}
⊢ x = y → ¬y = x

Proof state:
case h.mk
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
x₁ y₁ : α
⊢ x₁ = x ∧ y₁ = y ∨ x₁ = y ∧ y₁ = x → (x₁, y₁) ∈ s.offDiag

Tactic:
rintro (⟨rfl, rfl⟩ | ⟨rfl, rfl⟩) <;> rw [mem_offDiag] <;> exact ⟨‹_›, ‹_›, ‹_›⟩

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
hxy : ∃ a, (a.1 ∈ s ∧ a.2 ∈ s ∧ a.1 ≠ a.2) ∧ Sym2.mk a = s(x, y)
⊢ #(filter (fun a => Sym2.mk a = s(x, y)) s.offDiag) = 2

Tactic:
obtain ⟨a, ⟨ha₁, ha₂, ha⟩, h⟩ := hxy

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
h : Sym2.mk a = s(x, y)
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
⊢ #(filter (fun a => Sym2.mk a = s(x, y)) s.offDiag) = 2

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
⊢ filter (fun z => Sym2.mk z = s(x, y)) s.offDiag = {(x, y), (y, x)}

Tactic:
ext ⟨x₁, y₁⟩

Result:
case h.mk
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
x y : α
a : α × α
ha₁ : a.1 ∈ s
ha₂ : a.2 ∈ s
ha : a.1 ≠ a.2
h : Rel α a (x, y)
hx : x ∈ s
hy : y ∈ s
hxy : x ≠ y
hxy' : y ≠ x
x₁ y₁ : α
⊢ (x₁, y₁) ∈ filter (fun z => Sym2.mk z = s(x, y)) s.offDiag ↔ (x₁, y₁) ∈ {(x, y), (y, x)}