Theorem: LeanColls.IndexType.fromFin_inj (LeanColls/Classes/IndexType/Basic.lean)

State before:
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : Fin (card ι)
⊢ fromFin i = fromFin j ↔ i = j
Tactic:
constructor
State after:
case mp
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : Fin (card ι)
⊢ fromFin i = fromFin j → i = j

case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : Fin (card ι)
⊢ i = j → fromFin i = fromFin j

State before:
case mp
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : Fin (card ι)
⊢ fromFin i = fromFin j → i = j
Tactic:
apply LawfulIndexType.rightInv.injective
State after:
no goals

State before:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : Fin (card ι)
⊢ i = j → fromFin i = fromFin j
Tactic:
rintro rfl
State after:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i : Fin (card ι)
⊢ fromFin i = fromFin i

State before:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i : Fin (card ι)
⊢ fromFin i = fromFin i
Tactic:
rfl
State after:
no goals