-- Mathlib/Data/Finset/Prod.lean
theorem diag_card : (diag s).card = s.card

Proof state:
case h.mk.mpr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a₁ a₂ : α
h : ∃ a ∈ s, (a, a) = (a₁, a₂)
⊢ (a₁, a₂).1 ∈ s ∧ (a₁, a₂).1 = (a₁, a₂).2

Tactic:
rcases h with ⟨a, h1, h2⟩

Result:
case h.mk.mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
⊢ (a₁, a₂).1 ∈ s ∧ (a₁, a₂).1 = (a₁, a₂).2

Proof state:
case h.mk.mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
h : a = a₁ ∧ a = a₂
⊢ (a₁, a₂).1 ∈ s ∧ (a₁, a₂).1 = (a₁, a₂).2

Tactic:
rw [← h.1, ← h.2]

Result:
case h.mk.mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
h : a = a₁ ∧ a = a₂
⊢ (a, a).1 ∈ s ∧ (a, a).1 = (a, a).2

Proof state:
case H
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
this : s.diag = image (fun a => (a, a)) s
⊢ Set.InjOn (fun a => (a, a)) ↑s

Tactic:
exact fun x1 _ x2 _ h3 => (Prod.mk.inj h3).1

Result:
no goals

Proof state:
case h.mk
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a₁ a₂ : α
⊢ (a₁, a₂).1 ∈ s ∧ (a₁, a₂).1 = (a₁, a₂).2 ↔ (a₁, a₂) ∈ image (fun a => (a, a)) s

Tactic:
constructor <;> intro h <;> rw [Finset.mem_image] at *

Result:
case h.mk.mp
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a₁ a₂ : α
h : (a₁, a₂).1 ∈ s ∧ (a₁, a₂).1 = (a₁, a₂).2
⊢ ∃ a ∈ s, (a, a) = (a₁, a₂)

case h.mk.mpr
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a₁ a₂ : α
h : ∃ a ∈ s, (a, a) = (a₁, a₂)
⊢ (a₁, a₂).1 ∈ s ∧ (a₁, a₂).1 = (a₁, a₂).2

Proof state:
case h.mk.mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
h : a = a₁ ∧ a = a₂
⊢ (a, a).1 ∈ s ∧ (a, a).1 = (a, a).2

Tactic:
use h1

Result:
no goals

Proof state:
case h.mk
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a₁ a₂ : α
⊢ (a₁, a₂) ∈ s.diag ↔ (a₁, a₂) ∈ image (fun a => (a, a)) s

Tactic:
rw [mem_diag]

Result:
case h.mk
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a₁ a₂ : α
⊢ (a₁, a₂).1 ∈ s ∧ (a₁, a₂).1 = (a₁, a₂).2 ↔ (a₁, a₂) ∈ image (fun a => (a, a)) s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ #s.diag = #s

Tactic:
suffices diag s = s.image fun a => (a, a) by
  rw [this]
  apply card_image_of_injOn
  exact fun x1 _ x2 _ h3 => (Prod.mk.inj h3).1

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s.diag = image (fun a => (a, a)) s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
⊢ s.diag = image (fun a => (a, a)) s

Tactic:
ext ⟨a₁, a₂⟩

Result:
case h.mk
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a₁ a₂ : α
⊢ (a₁, a₂) ∈ s.diag ↔ (a₁, a₂) ∈ image (fun a => (a, a)) s

Proof state:
case h.mk.mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
⊢ (a₁, a₂).1 ∈ s ∧ (a₁, a₂).1 = (a₁, a₂).2

Tactic:
have h := Prod.mk.inj h2

Result:
case h.mk.mpr.intro.intro
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
h : a = a₁ ∧ a = a₂
⊢ (a₁, a₂).1 ∈ s ∧ (a₁, a₂).1 = (a₁, a₂).2

Proof state:
case h.mk.mp
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a₁ a₂ : α
h : (a₁, a₂).1 ∈ s ∧ (a₁, a₂).1 = (a₁, a₂).2
⊢ ∃ a ∈ s, (a, a) = (a₁, a₂)

Tactic:
use a₁

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a₁ a₂ : α
h : (a₁, a₂).1 ∈ s ∧ (a₁, a₂).1 = (a₁, a₂).2
⊢ a₁ ∈ s ∧ (a₁, a₁) = (a₁, a₂)

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
this : s.diag = image (fun a => (a, a)) s
⊢ #(image (fun a => (a, a)) s) = #s

Tactic:
apply card_image_of_injOn

Result:
case H
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
this : s.diag = image (fun a => (a, a)) s
⊢ Set.InjOn (fun a => (a, a)) ↑s

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a₁ a₂ : α
h : (a₁, a₂).1 ∈ s ∧ (a₁, a₂).1 = (a₁, a₂).2
⊢ a₁ ∈ s ∧ (a₁, a₁) = (a₁, a₂)

Tactic:
simpa using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
this : s.diag = image (fun a => (a, a)) s
⊢ #s.diag = #s

Tactic:
rw [this]

Result:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
this : s.diag = image (fun a => (a, a)) s
⊢ #(image (fun a => (a, a)) s) = #s