Theorem: compat_myMap (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:
⊢ myMap () ^ 3 = 1

State before:
⊢ myMap () ^ 3 = 1
Tactic:
decide
State after:
no goals