Theorem: Tutorial.Subgroup.inv_mem_iff (Solution/Advanced/Algebra/Lecture1.lean)

State before:
G : Type
inst✝ : Group G
H : Subgroup G
a : G
⊢ a⁻¹ ∈ H ↔ a ∈ H
Tactic:
constructor
State after:
case mp
G : Type
inst✝ : Group G
H : Subgroup G
a : G
⊢ a⁻¹ ∈ H → a ∈ H

case mpr
G : Type
inst✝ : Group G
H : Subgroup G
a : G
⊢ a ∈ H → a⁻¹ ∈ H

State before:
case mp
G : Type
inst✝ : Group G
H : Subgroup G
a : G
⊢ a⁻¹ ∈ H → a ∈ H
Tactic:
intro h
State after:
case mp
G : Type
inst✝ : Group G
H : Subgroup G
a : G
h : a⁻¹ ∈ H
⊢ a ∈ H

State before:
case mp
G : Type
inst✝ : Group G
H : Subgroup G
a : G
h : a⁻¹ ∈ H
⊢ a ∈ H
Tactic:
have h := inv_mem h
State after:
case mp
G : Type
inst✝ : Group G
H : Subgroup G
a : G
h✝ : a⁻¹ ∈ H
h : a⁻¹⁻¹ ∈ H
⊢ a ∈ H

State before:
case mp
G : Type
inst✝ : Group G
H : Subgroup G
a : G
h✝ : a⁻¹ ∈ H
h : a⁻¹⁻¹ ∈ H
⊢ a ∈ H
Tactic:
simpa using h
State after:
no goals

State before:
case mpr
G : Type
inst✝ : Group G
H : Subgroup G
a : G
⊢ a ∈ H → a⁻¹ ∈ H
Tactic:
exact inv_mem
State after:
no goals