Theorem: compat_myMap (LeanCourse/MIL/C08_Groups_and_Rings/S01_Groups.lean)

State before:
⊢ ∀ r ∈ {FreeGroup.of () ^ 3}, ↑(↑FreeGroup.lift myMap) r = 1
Tactic:
rintro _ rfl
State after:
⊢ ↑(↑FreeGroup.lift myMap) (FreeGroup.of () ^ 3) = 1

State before:
⊢ ↑(↑FreeGroup.lift myMap) (FreeGroup.of () ^ 3) = 1
Tactic:
simp
State after:
no goals