Theorem: Tutorial.homToPerm_injective (Solution/Advanced/Algebra/Lecture2.lean)

State before:
G : Type
inst✝ : Group G
⊢ Function.Injective ⇑(homToPerm G)
Tactic:
rw [injective_iff_map_eq_one]
State after:
G : Type
inst✝ : Group G
⊢ ∀ (a : G), (homToPerm G) a = 1 → a = 1

State before:
G : Type
inst✝ : Group G
⊢ ∀ (a : G), (homToPerm G) a = 1 → a = 1
Tactic:
intro a h
State after:
G : Type
inst✝ : Group G
a : G
h : (homToPerm G) a = 1
⊢ a = 1

State before:
G : Type
inst✝ : Group G
a : G
h : (homToPerm G) a = 1
⊢ a = 1
Tactic:
calc
  a = a * 1 := by simp
  _ = (homToPerm G a) 1 := by
    rfl
    _ = 1 := by
    simp [h]
State after:
no goals

State before:
G : Type
inst✝ : Group G
a : G
h : (homToPerm G) a = 1
⊢ a = a * 1
Tactic:
simp
State after:
no goals

State before:
G : Type
inst✝ : Group G
a : G
h : (homToPerm G) a = 1
⊢ a * 1 = ((homToPerm G) a) 1
Tactic:
rfl
State after:
no goals

State before:
G : Type
inst✝ : Group G
a : G
h : (homToPerm G) a = 1
⊢ ((homToPerm G) a) 1 = 1
Tactic:
simp [h]
State after:
no goals