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

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

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

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

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

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