α : Type u_1
β : Type ?u.72186
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn Quotient.mk' ↑(Finset.diag s)
α : Type u_1
β : Type ?u.72186
inst✝ : DecidableEq α
s : Finset α
⊢ Finset.card (image Quotient.mk' (Finset.diag s)) = Finset.card s
rw [card_image_of_injOn, diag_card]
case mk
α : Type u_1
β : Type ?u.72186
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx : (x₀, x₁) ∈ ↑(Finset.diag s)
x₂✝ : α × α
a✝ : x₂✝ ∈ ↑(Finset.diag s)
h : Quotient.mk' (x₀, x₁) = Quotient.mk' x₂✝
⊢ (x₀, x₁) = x₂✝
α : Type u_1
β : Type ?u.72186
inst✝ : DecidableEq α
s : Finset α
⊢ Set.InjOn Quotient.mk' ↑(Finset.diag s)
rintro ⟨x₀, x₁⟩ hx _ _ h
case mk.refl
α : Type u_1
β : Type ?u.72186
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx a✝ : (x₀, x₁) ∈ ↑(Finset.diag s)
h : Quotient.mk' (x₀, x₁) = Quotient.mk' (x₀, x₁)
⊢ (x₀, x₁) = (x₀, x₁)

case mk.swap
α : Type u_1
β : Type ?u.72186
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx : (x₀, x₁) ∈ ↑(Finset.diag s)
a✝ : (x₁, x₀) ∈ ↑(Finset.diag s)
h : Quotient.mk' (x₀, x₁) = Quotient.mk' (x₁, x₀)
⊢ (x₀, x₁) = (x₁, x₀)
case mk
α : Type u_1
β : Type ?u.72186
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx : (x₀, x₁) ∈ ↑(Finset.diag s)
x₂✝ : α × α
a✝ : x₂✝ ∈ ↑(Finset.diag s)
h : Quotient.mk' (x₀, x₁) = Quotient.mk' x₂✝
⊢ (x₀, x₁) = x₂✝
cases Quotient.eq'.1 h
no goals
case mk.refl
α : Type u_1
β : Type ?u.72186
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx a✝ : (x₀, x₁) ∈ ↑(Finset.diag s)
h : Quotient.mk' (x₀, x₁) = Quotient.mk' (x₀, x₁)
⊢ (x₀, x₁) = (x₀, x₁)
rfl
case mk.swap
α : Type u_1
β : Type ?u.72186
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
a✝ : (x₁, x₀) ∈ ↑(Finset.diag s)
h : Quotient.mk' (x₀, x₁) = Quotient.mk' (x₁, x₀)
hx : x₀ ∈ s ∧ x₀ = x₁
⊢ (x₀, x₁) = (x₁, x₀)
case mk.swap
α : Type u_1
β : Type ?u.72186
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
hx : (x₀, x₁) ∈ ↑(Finset.diag s)
a✝ : (x₁, x₀) ∈ ↑(Finset.diag s)
h : Quotient.mk' (x₀, x₁) = Quotient.mk' (x₁, x₀)
⊢ (x₀, x₁) = (x₁, x₀)
simp only [mem_coe, mem_diag] at hx
no goals
case mk.swap
α : Type u_1
β : Type ?u.72186
inst✝ : DecidableEq α
s : Finset α
x₀ x₁ : α
a✝ : (x₁, x₀) ∈ ↑(Finset.diag s)
h : Quotient.mk' (x₀, x₁) = Quotient.mk' (x₁, x₀)
hx : x₀ ∈ s ∧ x₀ = x₁
⊢ (x₀, x₁) = (x₁, x₀)
rw [hx.2]