G : Type u_1
H : Type ?u.4214
A : Type ?u.4217
a✝ a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
one_mem : 1 ∈ s
div_mem : ∀ {a b : G}, a ∈ s → b ∈ s → a * b⁻¹ ∈ s
a : G
ha : a ∈ s
this : 1 * a⁻¹ ∈ s
⊢ a⁻¹ ∈ s
G : Type u_1
H : Type ?u.4214
A : Type ?u.4217
a✝ a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
one_mem : 1 ∈ s
div_mem : ∀ {a b : G}, a ∈ s → b ∈ s → a * b⁻¹ ∈ s
a : G
ha : a ∈ s
⊢ a⁻¹ ∈ s
have : 1 * a⁻¹ ∈ s := div_mem one_mem ha
case h.e'_4
G : Type u_1
H : Type ?u.4214
A : Type ?u.4217
a✝ a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
one_mem : 1 ∈ s
div_mem : ∀ {a b : G}, a ∈ s → b ∈ s → a * b⁻¹ ∈ s
a : G
ha : a ∈ s
this : 1 * a⁻¹ ∈ s
⊢ a⁻¹ = 1 * a⁻¹
G : Type u_1
H : Type ?u.4214
A : Type ?u.4217
a✝ a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
one_mem : 1 ∈ s
div_mem : ∀ {a b : G}, a ∈ s → b ∈ s → a * b⁻¹ ∈ s
a : G
ha : a ∈ s
this : 1 * a⁻¹ ∈ s
⊢ a⁻¹ ∈ s
convert this using 1
no goals
case h.e'_4
G : Type u_1
H : Type ?u.4214
A : Type ?u.4217
a✝ a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
one_mem : 1 ∈ s
div_mem : ∀ {a b : G}, a ∈ s → b ∈ s → a * b⁻¹ ∈ s
a : G
ha : a ∈ s
this : 1 * a⁻¹ ∈ s
⊢ a⁻¹ = 1 * a⁻¹
rw [one_mul]
G : Type u_1
H : Type ?u.4214
A : Type ?u.4217
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
one_mem : 1 ∈ s
div_mem : ∀ {a b : G}, a ∈ s → b ∈ s → a * b⁻¹ ∈ s
inv_mem : ∀ (a : G), a ∈ s → a⁻¹ ∈ s
a b : G
ha : a ∈ s
hb : b ∈ s
this : a * b⁻¹⁻¹ ∈ s
⊢ a * b ∈ s
G : Type u_1
H : Type ?u.4214
A : Type ?u.4217
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
one_mem : 1 ∈ s
div_mem : ∀ {a b : G}, a ∈ s → b ∈ s → a * b⁻¹ ∈ s
inv_mem : ∀ (a : G), a ∈ s → a⁻¹ ∈ s
a b : G
ha : a ∈ s
hb : b ∈ s
⊢ a * b ∈ s
have : a * b⁻¹⁻¹ ∈ s := div_mem ha (inv_mem b hb)
case h.e'_4.h.e'_6
G : Type u_1
H : Type ?u.4214
A : Type ?u.4217
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
one_mem : 1 ∈ s
div_mem : ∀ {a b : G}, a ∈ s → b ∈ s → a * b⁻¹ ∈ s
inv_mem : ∀ (a : G), a ∈ s → a⁻¹ ∈ s
a b : G
ha : a ∈ s
hb : b ∈ s
this : a * b⁻¹⁻¹ ∈ s
⊢ b = b⁻¹⁻¹
G : Type u_1
H : Type ?u.4214
A : Type ?u.4217
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
one_mem : 1 ∈ s
div_mem : ∀ {a b : G}, a ∈ s → b ∈ s → a * b⁻¹ ∈ s
inv_mem : ∀ (a : G), a ∈ s → a⁻¹ ∈ s
a b : G
ha : a ∈ s
hb : b ∈ s
this : a * b⁻¹⁻¹ ∈ s
⊢ a * b ∈ s
convert this
no goals
case h.e'_4.h.e'_6
G : Type u_1
H : Type ?u.4214
A : Type ?u.4217
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
one_mem : 1 ∈ s
div_mem : ∀ {a b : G}, a ∈ s → b ∈ s → a * b⁻¹ ∈ s
inv_mem : ∀ (a : G), a ∈ s → a⁻¹ ∈ s
a b : G
ha : a ∈ s
hb : b ∈ s
this : a * b⁻¹⁻¹ ∈ s
⊢ b = b⁻¹⁻¹
rw [inv_inv]