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

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

case mpr
ι : Type u_1
inst✝¹ : IndexType ι
inst✝ : LawfulIndexType ι
x y : ι
⊢ x = y → toFin x = toFin y

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

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

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