α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ diag s = image (fun a => (a, a)) s
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ card (diag s) = card s
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
case a.mk
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
⊢ (a₁, a₂) ∈ diag s ↔ (a₁, a₂) ∈ image (fun a => (a, a)) s
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
⊢ diag s = image (fun a => (a, a)) s
ext ⟨a₁, a₂⟩
case a.mk
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd ↔ (a₁, a₂) ∈ image (fun a => (a, a)) s
case a.mk
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
⊢ (a₁, a₂) ∈ diag s ↔ (a₁, a₂) ∈ image (fun a => (a, a)) s
rw [mem_diag]
case a.mk.mp
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
h : (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
⊢ ∃ a, a ∈ s ∧ (a, a) = (a₁, a₂)

case a.mk.mpr
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
h : ∃ a, a ∈ s ∧ (a, a) = (a₁, a₂)
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
case a.mk
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd ↔ (a₁, a₂) ∈ image (fun a => (a, a)) s
constructor <;> intro h <;> rw [Finset.mem_image] at *
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : diag s = image (fun a => (a, a)) s
⊢ card (image (fun a => (a, a)) s) = card s
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : diag s = image (fun a => (a, a)) s
⊢ card (diag s) = card s
rw [this]
case H
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : diag s = image (fun a => (a, a)) s
⊢ Set.InjOn (fun a => (a, a)) ↑s
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : diag s = image (fun a => (a, a)) s
⊢ card (image (fun a => (a, a)) s) = card s
apply card_image_of_injOn
no goals
case H
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
this : diag s = image (fun a => (a, a)) s
⊢ Set.InjOn (fun a => (a, a)) ↑s
exact fun x1 _ x2 _ h3 => (Prod.mk.inj h3).1
case a.mk.mp
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
h : (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
⊢ a₁ ∈ s ∧ (a₁, a₁) = (a₁, a₂)
case a.mk.mp
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
h : (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
⊢ ∃ a, a ∈ s ∧ (a, a) = (a₁, a₂)
use a₁
no goals
case a.mk.mp
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
h : (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
⊢ a₁ ∈ s ∧ (a₁, a₁) = (a₁, a₂)
simpa using h
case a.mk.mpr.intro.intro
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
case a.mk.mpr
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ : α
h : ∃ a, a ∈ s ∧ (a, a) = (a₁, a₂)
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
rcases h with ⟨a, h1, h2⟩
case a.mk.mpr.intro.intro
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
h : a = a₁ ∧ a = a₂
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
case a.mk.mpr.intro.intro
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
have h := Prod.mk.inj h2
case a.mk.mpr.intro.intro
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
h : a = a₁ ∧ a = a₂
⊢ (a, a).fst ∈ s ∧ (a, a).fst = (a, a).snd
case a.mk.mpr.intro.intro
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
h : a = a₁ ∧ a = a₂
⊢ (a₁, a₂).fst ∈ s ∧ (a₁, a₂).fst = (a₁, a₂).snd
rw [← h.1, ← h.2]
no goals
case a.mk.mpr.intro.intro
α : Type u_1
β : Type ?u.109406
γ : Type ?u.109409
inst✝ : DecidableEq α
s t : Finset α
x : α × α
a₁ a₂ a : α
h1 : a ∈ s
h2 : (a, a) = (a₁, a₂)
h : a = a₁ ∧ a = a₂
⊢ (a, a).fst ∈ s ∧ (a, a).fst = (a, a).snd
use h1