n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Finset.card Finset.univ = n

case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Function.Injective fun i => (f i, i)
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Finset.card (graph f) = n
rw [graph, Finset.card_image_of_injective]
no goals
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Finset.card Finset.univ = n
exact Finset.card_fin _
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (fun i => (f i, i)) a₁✝ = (fun i => (f i, i)) a₂✝ → a₁✝ = a₂✝
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Function.Injective fun i => (f i, i)
intro _ _
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (f a₁✝, a₁✝) = (f a₂✝, a₂✝) → a₁✝ = a₂✝
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (fun i => (f i, i)) a₁✝ = (fun i => (f i, i)) a₂✝ → a₁✝ = a₂✝
dsimp only
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (f a₁✝, a₁✝).fst = (f a₂✝, a₂✝).fst ∧ (f a₁✝, a₁✝).snd = (f a₂✝, a₂✝).snd → a₁✝ = a₂✝
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (f a₁✝, a₁✝) = (f a₂✝, a₂✝) → a₁✝ = a₂✝
rw [Prod.ext_iff]
no goals
case H
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
a₁✝ a₂✝ : Fin n
⊢ (f a₁✝, a₁✝).fst = (f a₂✝, a₂✝).fst ∧ (f a₁✝, a₁✝).snd = (f a₂✝, a₂✝).snd → a₁✝ = a₂✝
simp