Theorem: self_inv_of_squares_id (Lectures/GroupSquaresId.lean)

State before:
G : Type u_1
inst✝ : Group G
⊢ (∀ (x : G), x * x = 1) → ∀ (x : G), x⁻¹ = x
Tactic:
intro h
State after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
⊢ ∀ (x : G), x⁻¹ = x

State before:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
⊢ ∀ (x : G), x⁻¹ = x
Tactic:
intro x
State after:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x : G
⊢ x⁻¹ = x

State before:
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x : G
⊢ x⁻¹ = x
Tactic:
apply inv_eq_of_mul_eq_one_right
State after:
case a
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x : G
⊢ x * x = 1

State before:
case a
G : Type u_1
inst✝ : Group G
h : ∀ (x : G), x * x = 1
x : G
⊢ x * x = 1
Tactic:
apply h
State after:
no goals