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

State before:
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : ι
⊢ toFin i = toFin j ↔ i = j
Tactic:
constructor
State after:
case mp
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : ι
⊢ toFin i = toFin j → i = j

case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : ι
⊢ i = j → toFin i = toFin j

State before:
case mp
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : ι
⊢ toFin i = toFin j → i = j
Tactic:
apply LawfulIndexType.leftInv.injective
State after:
no goals

State before:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i j : ι
⊢ i = j → toFin i = toFin j
Tactic:
rintro rfl
State after:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i : ι
⊢ toFin i = toFin i

State before:
case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
i : ι
⊢ toFin i = toFin i
Tactic:
rfl
State after:
no goals