[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
hs : IsSubgroup s
x y : G
hx : x ∈ s
hy : y ∈ s
⊢ x / y ∈ s
[PROOFSTEP]
simpa only [div_eq_mul_inv] using hs.mul_mem hx (hs.inv_mem hy)
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
⊢ IsAddSubgroup s → IsSubgroup s
[PROOFSTEP]
rintro ⟨⟨h₁, h₂⟩, h₃⟩
[GOAL]
case mk.mk
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
h₃ : ∀ {a : Additive G}, a ∈ s → -a ∈ s
h₁ : 0 ∈ s
h₂ : ∀ {a b : Additive G}, a ∈ s → b ∈ s → a + b ∈ s
⊢ IsSubgroup s
[PROOFSTEP]
exact @IsSubgroup.mk G _ _ ⟨h₁, @h₂⟩ @h₃
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set A
⊢ IsSubgroup s → IsAddSubgroup s
[PROOFSTEP]
rintro ⟨⟨h₁, h₂⟩, h₃⟩
[GOAL]
case mk.mk
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set A
h₃ : ∀ {a : Multiplicative A}, a ∈ s → a⁻¹ ∈ s
h₁ : 1 ∈ s
h₂ : ∀ {a b : Multiplicative A}, a ∈ s → b ∈ s → a * b ∈ s
⊢ IsAddSubgroup s
[PROOFSTEP]
exact @IsAddSubgroup.mk A _ _ ⟨h₁, @h₂⟩ @h₃
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
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
[PROOFSTEP]
have : 1 * a⁻¹ ∈ s := div_mem one_mem ha
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
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
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_4
G : Type u_1
H : Type u_2
A : Type u_3
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⁻¹
[PROOFSTEP]
rw [one_mul]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
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
[PROOFSTEP]
have : a * b⁻¹⁻¹ ∈ s := div_mem ha (inv_mem b hb)
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
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
[PROOFSTEP]
convert this
[GOAL]
case h.e'_4.h.e'_6
G : Type u_1
H : Type u_2
A : Type u_3
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⁻¹⁻¹
[PROOFSTEP]
rw [inv_inv]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set A
zero_mem : 0 ∈ s
sub_mem : ∀ {a b : A}, a ∈ s → b ∈ s → a - b ∈ s
x y : A
hx : x ∈ s
hy : y ∈ s
⊢ x + -y ∈ s
[PROOFSTEP]
simpa only [sub_eq_add_neg] using sub_mem hx hy
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
s : Set G
hs : IsSubgroup s
h : a⁻¹ ∈ s
⊢ a ∈ s
[PROOFSTEP]
simpa using hs.inv_mem h
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
s : Set G
hs : IsSubgroup s
h : a ∈ s
hba : b * a ∈ s
⊢ b ∈ s
[PROOFSTEP]
simpa using hs.mul_mem hba (hs.inv_mem h)
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
s : Set G
hs : IsSubgroup s
h : a ∈ s
hab : a * b ∈ s
⊢ b ∈ s
[PROOFSTEP]
simpa using hs.mul_mem (hs.inv_mem h) hab
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : CommGroup G
s : Set G
hs : IsSubgroup s
n : G
hn : n ∈ s
g : G
⊢ g * n * g⁻¹ ∈ s
[PROOFSTEP]
rwa [mul_right_comm, mul_right_inv, one_mul]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
s : Set G
⊢ IsNormalAddSubgroup s → IsNormalSubgroup s
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case mk
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
s : Set G
h₁ : IsAddSubgroup s
h₂ : ∀ (n : Additive G), n ∈ s → ∀ (g : Additive G), g + n + -g ∈ s
⊢ IsNormalSubgroup s
[PROOFSTEP]
exact @IsNormalSubgroup.mk G _ _ (Additive.isAddSubgroup_iff.1 h₁) @h₂
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : AddGroup A
s : Set A
⊢ IsNormalSubgroup s → IsNormalAddSubgroup s
[PROOFSTEP]
rintro ⟨h₁, h₂⟩
[GOAL]
case mk
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : AddGroup A
s : Set A
h₁ : IsSubgroup s
h₂ : ∀ (n : Multiplicative A), n ∈ s → ∀ (g : Multiplicative A), g * n * g⁻¹ ∈ s
⊢ IsNormalAddSubgroup s
[PROOFSTEP]
exact @IsNormalAddSubgroup.mk A _ _ (Multiplicative.isSubgroup_iff.1 h₁) @h₂
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝ : Group G
s : Set G
hs : IsNormalSubgroup s
a b : G
hab : a * b ∈ s
⊢ b * a ∈ s
[PROOFSTEP]
have h : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ s := hs.normal (a * b) hab a⁻¹
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝ : Group G
s : Set G
hs : IsNormalSubgroup s
a b : G
hab : a * b ∈ s
h : a⁻¹ * (a * b) * a⁻¹⁻¹ ∈ s
⊢ b * a ∈ s
[PROOFSTEP]
simp at h 
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝ : Group G
s : Set G
hs : IsNormalSubgroup s
a b : G
hab : a * b ∈ s
h : b * a ∈ s
⊢ b * a ∈ s
[PROOFSTEP]
exact h
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
⊢ IsNormalSubgroup (trivial G)
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
⊢ 1 ∈ trivial G
[PROOFSTEP]
simp (config := { contextual := true }) [trivial]
[GOAL]
case refine'_2
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
⊢ ∀ {a b : G}, a ∈ trivial G → b ∈ trivial G → a * b ∈ trivial G
[PROOFSTEP]
simp (config := { contextual := true }) [trivial]
[GOAL]
case refine'_3
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
⊢ ∀ {a : G}, a ∈ trivial G → a⁻¹ ∈ trivial G
[PROOFSTEP]
simp (config := { contextual := true }) [trivial]
[GOAL]
case refine'_4
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
⊢ ∀ (n : G), n ∈ trivial G → ∀ (g : G), g * n * g⁻¹ ∈ trivial G
[PROOFSTEP]
simp (config := { contextual := true }) [trivial]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
s : Set G
hs : IsSubgroup s
⊢ s = trivial G ↔ ∀ (x : G), x ∈ s → x = 1
[PROOFSTEP]
simp only [Set.ext_iff, IsSubgroup.mem_trivial]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
s : Set G
hs : IsSubgroup s
⊢ (∀ (x : G), x ∈ s ↔ x = 1) ↔ ∀ (x : G), x ∈ s → x = 1
[PROOFSTEP]
exact ⟨fun h x => (h x).1, fun h x => ⟨h x, fun hx => hx.symm ▸ hs.toIsSubmonoid.one_mem⟩⟩
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
⊢ IsNormalSubgroup univ
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
⊢ 1 ∈ univ
[PROOFSTEP]
simp
[GOAL]
case refine'_2
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
⊢ ∀ {a b : G}, a ∈ univ → b ∈ univ → a * b ∈ univ
[PROOFSTEP]
simp
[GOAL]
case refine'_3
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
⊢ ∀ {a : G}, a ∈ univ → a⁻¹ ∈ univ
[PROOFSTEP]
simp
[GOAL]
case refine'_4
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
⊢ ∀ (n : G), n ∈ univ → ∀ (g : G), g * n * g⁻¹ ∈ univ
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
⊢ 1 ∈ center G
[PROOFSTEP]
simp [center]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
a✝ b✝ : G
ha : a✝ ∈ center G
hb : b✝ ∈ center G
g : G
⊢ g * (a✝ * b✝) = a✝ * b✝ * g
[PROOFSTEP]
rw [← mul_assoc, mem_center.2 ha g, mul_assoc, mem_center.2 hb g, ← mul_assoc]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b c : G
inst✝ : Group G
a : G
ha : a ∈ center G
g : G
⊢ g * a⁻¹ = a⁻¹ * (g * a) * a⁻¹
[PROOFSTEP]
simp [ha g]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b c : G
inst✝ : Group G
a : G
ha : a ∈ center G
g : G
⊢ a⁻¹ * (g * a) * a⁻¹ = a⁻¹ * g
[PROOFSTEP]
rw [← mul_assoc, mul_assoc]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b c : G
inst✝ : Group G
a : G
ha : a ∈ center G
g : G
⊢ a⁻¹ * g * (a * a⁻¹) = a⁻¹ * g
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
n : G
ha : n ∈ center G
g h : G
⊢ h * (g * n * g⁻¹) = h * n
[PROOFSTEP]
simp [ha g, mul_assoc]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
n : G
ha : n ∈ center G
g h : G
⊢ h * n = g * g⁻¹ * n * h
[PROOFSTEP]
rw [ha h]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
n : G
ha : n ∈ center G
g h : G
⊢ n * h = g * g⁻¹ * n * h
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
n : G
ha : n ∈ center G
g h : G
⊢ g * g⁻¹ * n * h = g * n * g⁻¹ * h
[PROOFSTEP]
rw [mul_assoc g, ha g⁻¹, ← mul_assoc]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
s : Set G
⊢ 1 ∈ normalizer s
[PROOFSTEP]
simp [normalizer]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝ : Group G
s : Set G
a b : G
ha : ∀ (n : G), n ∈ s ↔ a * n * a⁻¹ ∈ s
hb : ∀ (n : G), n ∈ s ↔ b * n * b⁻¹ ∈ s
n : G
⊢ n ∈ s ↔ a * b * n * (a * b)⁻¹ ∈ s
[PROOFSTEP]
rw [mul_inv_rev, ← mul_assoc, mul_assoc a, mul_assoc a, ← ha, ← hb]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b c : G
inst✝ : Group G
s : Set G
a : G
ha : ∀ (n : G), n ∈ s ↔ a * n * a⁻¹ ∈ s
n : G
⊢ n ∈ s ↔ a⁻¹ * n * a⁻¹⁻¹ ∈ s
[PROOFSTEP]
rw [ha (a⁻¹ * n * a⁻¹⁻¹)]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b c : G
inst✝ : Group G
s : Set G
a : G
ha : ∀ (n : G), n ∈ s ↔ a * n * a⁻¹ ∈ s
n : G
⊢ n ∈ s ↔ a * (a⁻¹ * n * a⁻¹⁻¹) * a⁻¹ ∈ s
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
s : Set G
hs : IsSubgroup s
g : G
hg : g ∈ s
n : G
⊢ n ∈ s ↔ g * n * g⁻¹ ∈ s
[PROOFSTEP]
rw [IsSubgroup.mul_mem_cancel_right hs ((IsSubgroup.inv_mem_iff hs).2 hg), IsSubgroup.mul_mem_cancel_left hs hg]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
h : f (a * b⁻¹) = 1
⊢ f a = f b
[PROOFSTEP]
rw [hf.map_mul, hf.map_inv] at h 
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
h : f a * (f b)⁻¹ = 1
⊢ f a = f b
[PROOFSTEP]
rw [← inv_inv (f b), eq_inv_of_mul_eq_one_left h]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
h : f (a⁻¹ * b) = 1
⊢ f a = f b
[PROOFSTEP]
rw [hf.map_mul, hf.map_inv] at h 
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
h : (f a)⁻¹ * f b = 1
⊢ f a = f b
[PROOFSTEP]
apply inv_injective
[GOAL]
case a
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
h : (f a)⁻¹ * f b = 1
⊢ (f a)⁻¹ = (f b)⁻¹
[PROOFSTEP]
rw [eq_inv_of_mul_eq_one_left h]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
h : f a = f b
⊢ f (a * b⁻¹) = 1
[PROOFSTEP]
have : f a * (f b)⁻¹ = 1 := by rw [h, mul_right_inv]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
h : f a = f b
⊢ f a * (f b)⁻¹ = 1
[PROOFSTEP]
rw [h, mul_right_inv]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
h : f a = f b
this : f a * (f b)⁻¹ = 1
⊢ f (a * b⁻¹) = 1
[PROOFSTEP]
rwa [← hf.map_inv, ← hf.map_mul] at this 
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
h : f a = f b
⊢ f (a⁻¹ * b) = 1
[PROOFSTEP]
have : (f a)⁻¹ * f b = 1 := by rw [h, mul_left_inv]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
h : f a = f b
⊢ (f a)⁻¹ * f b = 1
[PROOFSTEP]
rw [h, mul_left_inv]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
h : f a = f b
this : (f a)⁻¹ * f b = 1
⊢ f (a⁻¹ * b) = 1
[PROOFSTEP]
rwa [← hf.map_inv, ← hf.map_mul] at this 
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
⊢ f a = f b ↔ a * b⁻¹ ∈ ker f
[PROOFSTEP]
rw [mem_ker]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
⊢ f a = f b ↔ f (a * b⁻¹) = 1
[PROOFSTEP]
exact one_iff_ker_inv hf _ _
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
⊢ f a = f b ↔ a⁻¹ * b ∈ ker f
[PROOFSTEP]
rw [mem_ker]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a b : G
⊢ f a = f b ↔ f (a⁻¹ * b) = 1
[PROOFSTEP]
exact one_iff_ker_inv' hf _ _
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁✝ a₂✝ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
hs : IsSubgroup s
a₁ a₂ : H
x✝¹ : a₁ ∈ f '' s
x✝ : a₂ ∈ f '' s
b₁ : G
hb₁ : b₁ ∈ s
eq₁ : f b₁ = a₁
b₂ : G
hb₂ : b₂ ∈ s
eq₂ : f b₂ = a₂
⊢ f (b₁ * b₂) = a₁ * a₂
[PROOFSTEP]
simp [eq₁, eq₂, hf.map_mul]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
hs : IsSubgroup s
a : H
x✝ : a ∈ f '' s
b : G
hb : b ∈ s
Eq : f b = a
⊢ f b⁻¹ = a⁻¹
[PROOFSTEP]
rw [hf.map_inv]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b✝ c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
hs : IsSubgroup s
a : H
x✝ : a ∈ f '' s
b : G
hb : b ∈ s
Eq : f b = a
⊢ (f b)⁻¹ = a⁻¹
[PROOFSTEP]
simp [*]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set H
hs : IsSubgroup s
⊢ IsSubgroup (f ⁻¹' s)
[PROOFSTEP]
refine' { .. }
[GOAL]
case refine'_1
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set H
hs : IsSubgroup s
⊢ 1 ∈ f ⁻¹' s
[PROOFSTEP]
simp (config := { contextual := true }) [hs.one_mem, hs.mul_mem, hs.inv_mem, hf.map_mul, hf.map_one, hf.map_inv,
  InvMemClass.inv_mem]
[GOAL]
case refine'_2
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set H
hs : IsSubgroup s
⊢ ∀ {a b : G}, a ∈ f ⁻¹' s → b ∈ f ⁻¹' s → a * b ∈ f ⁻¹' s
[PROOFSTEP]
simp (config := { contextual := true }) [hs.one_mem, hs.mul_mem, hs.inv_mem, hf.map_mul, hf.map_one, hf.map_inv,
  InvMemClass.inv_mem]
[GOAL]
case refine'_3
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set H
hs : IsSubgroup s
⊢ ∀ {a : G}, a ∈ f ⁻¹' s → a⁻¹ ∈ f ⁻¹' s
[PROOFSTEP]
simp (config := { contextual := true }) [hs.one_mem, hs.mul_mem, hs.inv_mem, hf.map_mul, hf.map_one, hf.map_inv,
  InvMemClass.inv_mem]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set H
hs : IsNormalSubgroup s
⊢ 1 ∈ f ⁻¹' s
[PROOFSTEP]
simp [hf.map_one, hs.toIsSubgroup.one_mem]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set H
hs : IsNormalSubgroup s
⊢ ∀ {a b : G}, a ∈ f ⁻¹' s → b ∈ f ⁻¹' s → a * b ∈ f ⁻¹' s
[PROOFSTEP]
simp (config := { contextual := true }) [hf.map_mul, hs.toIsSubgroup.mul_mem]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set H
hs : IsNormalSubgroup s
⊢ ∀ {a : G}, a ∈ f ⁻¹' s → a⁻¹ ∈ f ⁻¹' s
[PROOFSTEP]
simp (config := { contextual := true }) [hf.map_inv, hs.toIsSubgroup.inv_mem]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set H
hs : IsNormalSubgroup s
⊢ ∀ (n : G), n ∈ f ⁻¹' s → ∀ (g : G), g * n * g⁻¹ ∈ f ⁻¹' s
[PROOFSTEP]
simp (config := { contextual := true }) [hs.normal, hf.map_mul, hf.map_inv]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
h : ker f = IsSubgroup.trivial G
⊢ Injective f
[PROOFSTEP]
intro a₁ a₂ hfa
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁✝ a₂✝ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
h : ker f = IsSubgroup.trivial G
a₁ a₂ : G
hfa : f a₁ = f a₂
⊢ a₁ = a₂
[PROOFSTEP]
simp [ext_iff, ker, IsSubgroup.trivial] at h 
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁✝ a₂✝ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a₁ a₂ : G
hfa : f a₁ = f a₂
h : ∀ (x : G), f x = 1 ↔ x = 1
⊢ a₁ = a₂
[PROOFSTEP]
have ha : a₁ * a₂⁻¹ = 1 := by rw [← h]; exact hf.inv_ker_one hfa
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁✝ a₂✝ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a₁ a₂ : G
hfa : f a₁ = f a₂
h : ∀ (x : G), f x = 1 ↔ x = 1
⊢ a₁ * a₂⁻¹ = 1
[PROOFSTEP]
rw [← h]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁✝ a₂✝ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a₁ a₂ : G
hfa : f a₁ = f a₂
h : ∀ (x : G), f x = 1 ↔ x = 1
⊢ f (a₁ * a₂⁻¹) = 1
[PROOFSTEP]
exact hf.inv_ker_one hfa
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁✝ a₂✝ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
a₁ a₂ : G
hfa : f a₁ = f a₂
h : ∀ (x : G), f x = 1 ↔ x = 1
ha : a₁ * a₂⁻¹ = 1
⊢ a₁ = a₂
[PROOFSTEP]
rw [eq_inv_of_mul_eq_one_left ha, inv_inv a₂]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
h : Injective f
x : G
hx : x ∈ ker f
⊢ x ∈ IsSubgroup.trivial G
[PROOFSTEP]
suffices f x = f 1 by simpa using h this
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
h : Injective f
x : G
hx : x ∈ ker f
this : f x = f 1
⊢ x ∈ IsSubgroup.trivial G
[PROOFSTEP]
simpa using h this
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
h : Injective f
x : G
hx : x ∈ ker f
⊢ f x = f 1
[PROOFSTEP]
simp [hf.map_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
h : Injective f
x : G
hx : x ∈ ker f
⊢ f x = 1
[PROOFSTEP]
rwa [mem_ker] at hx 
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
h : Injective f
x : G
⊢ x ∈ IsSubgroup.trivial G → x ∈ ker f
[PROOFSTEP]
simp (config := { contextual := true }) [mem_ker, hf.map_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
⊢ ker f = IsSubgroup.trivial G ↔ ∀ (x : G), f x = 1 → x = 1
[PROOFSTEP]
rw [Set.ext_iff]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
⊢ (∀ (x : G), x ∈ ker f ↔ x ∈ IsSubgroup.trivial G) ↔ ∀ (x : G), f x = 1 → x = 1
[PROOFSTEP]
simp [ker]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
⊢ (∀ (x : G), f x = 1 ↔ x = 1) ↔ ∀ (x : G), f x = 1 → x = 1
[PROOFSTEP]
exact ⟨fun h x hx => (h x).1 hx, fun h x => ⟨h x, fun hx => by rw [hx, hf.map_one]⟩⟩
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
h : ∀ (x : G), f x = 1 → x = 1
x : G
hx : x = 1
⊢ f x = 1
[PROOFSTEP]
rw [hx, hf.map_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b c : G
inst✝ : Group G
s✝ s t : Set G
ht : IsSubgroup t
h : s ⊆ t
a : G
ha : a ∈ closure s
⊢ a ∈ t
[PROOFSTEP]
induction ha
[GOAL]
case basic
G : Type u_1
H : Type u_2
A : Type u_3
a✝² a₁ a₂ b c : G
inst✝ : Group G
s✝ s t : Set G
ht : IsSubgroup t
h : s ⊆ t
a a✝¹ : G
a✝ : a✝¹ ∈ s
⊢ a✝¹ ∈ t
[PROOFSTEP]
simp [h _, *, ht.one_mem, ht.mul_mem, IsSubgroup.inv_mem_iff]
[GOAL]
case one
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b c : G
inst✝ : Group G
s✝ s t : Set G
ht : IsSubgroup t
h : s ⊆ t
a : G
⊢ 1 ∈ t
[PROOFSTEP]
simp [h _, *, ht.one_mem, ht.mul_mem, IsSubgroup.inv_mem_iff]
[GOAL]
case inv
G : Type u_1
H : Type u_2
A : Type u_3
a✝² a₁ a₂ b c : G
inst✝ : Group G
s✝ s t : Set G
ht : IsSubgroup t
h : s ⊆ t
a a✝¹ : G
a✝ : InClosure s a✝¹
a_ih✝ : a✝¹ ∈ t
⊢ a✝¹⁻¹ ∈ t
[PROOFSTEP]
simp [h _, *, ht.one_mem, ht.mul_mem, IsSubgroup.inv_mem_iff]
[GOAL]
case mul
G : Type u_1
H : Type u_2
A : Type u_3
a✝³ a₁ a₂ b c : G
inst✝ : Group G
s✝ s t : Set G
ht : IsSubgroup t
h : s ⊆ t
a a✝² b✝ : G
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
a_ih✝¹ : a✝² ∈ t
a_ih✝ : b✝ ∈ t
⊢ a✝² * b✝ ∈ t
[PROOFSTEP]
simp [h _, *, ht.one_mem, ht.mul_mem, IsSubgroup.inv_mem_iff]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b c : G
inst✝ : Group G
s✝ s : Set G
a : G
h : a ∈ closure s
x✝² : G
x✝¹ : InClosure s x✝²
x✝ : ∃ l, (∀ (x : G), x ∈ l → x ∈ s ∨ x⁻¹ ∈ s) ∧ List.prod l = x✝²
L : List G
HL1 : ∀ (x : G), x ∈ L → x ∈ s ∨ x⁻¹ ∈ s
HL2 : List.prod L = x✝²
x : G
hx : x ∈ List.map Inv.inv (List.reverse L)
y : G
hy1 : y ∈ List.reverse L
hy2 : y⁻¹ = x
⊢ y ∈ s → y⁻¹⁻¹ ∈ s
[PROOFSTEP]
rw [inv_inv]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b c : G
inst✝ : Group G
s✝ s : Set G
a : G
h : a ∈ closure s
x✝² : G
x✝¹ : InClosure s x✝²
x✝ : ∃ l, (∀ (x : G), x ∈ l → x ∈ s ∨ x⁻¹ ∈ s) ∧ List.prod l = x✝²
L : List G
HL1 : ∀ (x : G), x ∈ L → x ∈ s ∨ x⁻¹ ∈ s
HL2 : List.prod L = x✝²
x : G
hx : x ∈ List.map Inv.inv (List.reverse L)
y : G
hy1 : y ∈ List.reverse L
hy2 : y⁻¹ = x
⊢ y ∈ s → y ∈ s
[PROOFSTEP]
exact id
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b c : G
inst✝ : Group G
s✝ s : Set G
a : G
h : a ∈ closure s
x : G
x✝¹ : InClosure s x
x✝ : ∃ l, (∀ (x : G), x ∈ l → x ∈ s ∨ x⁻¹ ∈ s) ∧ List.prod l = x
L : List G
HL1 : ∀ (x : G), x ∈ L → x ∈ s ∨ x⁻¹ ∈ s
HL2 : List.prod L = x
hd : G
tl : List G
ih : List.prod (List.map Inv.inv (List.reverse tl)) = (List.prod tl)⁻¹
⊢ List.prod (List.map Inv.inv (List.reverse (hd :: tl))) = (List.prod (hd :: tl))⁻¹
[PROOFSTEP]
rw [List.reverse_cons, List.map_append, List.prod_append, ih, List.map_singleton, List.prod_cons, List.prod_nil,
  mul_one, List.prod_cons, mul_inv_rev]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b c : G
inst✝ : Group G
s✝ s : Set G
a : G
h : a ∈ closure s
x y : G
x✝³ : InClosure s x
x✝² : InClosure s y
x✝¹ : ∃ l, (∀ (x : G), x ∈ l → x ∈ s ∨ x⁻¹ ∈ s) ∧ List.prod l = x
x✝ : ∃ l, (∀ (x : G), x ∈ l → x ∈ s ∨ x⁻¹ ∈ s) ∧ List.prod l = y
L1 : List G
HL1 : ∀ (x : G), x ∈ L1 → x ∈ s ∨ x⁻¹ ∈ s
HL2 : List.prod L1 = x
L2 : List G
HL3 : ∀ (x : G), x ∈ L2 → x ∈ s ∨ x⁻¹ ∈ s
HL4 : List.prod L2 = y
⊢ List.prod (L1 ++ L2) = x * y
[PROOFSTEP]
rw [List.prod_append, HL2, HL4]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
⊢ f '' closure s ≤ closure (f '' s)
[PROOFSTEP]
rintro _ ⟨x, hx, rfl⟩
[GOAL]
case intro.intro
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
⊢ f x ∈ closure (f '' s)
[PROOFSTEP]
exact
  InClosure.recOn hx (by intros _ ha; exact subset_closure (mem_image_of_mem f ha))
    (by
      rw [hf.map_one]
      apply IsSubmonoid.one_mem (closure.isSubgroup _).toIsSubmonoid)
    (by
      intros _ _
      rw [hf.map_inv]
      apply IsSubgroup.inv_mem (closure.isSubgroup _))
    (by
      intros _ _ _ _ ha hb
      rw [hf.map_mul]
      exact (closure.isSubgroup (f '' s)).toIsSubmonoid.mul_mem ha hb)
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
⊢ ∀ {a : G}, a ∈ s → f a ∈ closure (f '' s)
[PROOFSTEP]
intros _ ha
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
a✝ : G
ha : a✝ ∈ s
⊢ f a✝ ∈ closure (f '' s)
[PROOFSTEP]
exact subset_closure (mem_image_of_mem f ha)
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
⊢ f 1 ∈ closure (f '' s)
[PROOFSTEP]
rw [hf.map_one]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
⊢ 1 ∈ closure (f '' s)
[PROOFSTEP]
apply IsSubmonoid.one_mem (closure.isSubgroup _).toIsSubmonoid
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
⊢ ∀ {a : G}, InClosure s a → f a ∈ closure (f '' s) → f a⁻¹ ∈ closure (f '' s)
[PROOFSTEP]
intros _ _
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
a✝¹ : G
a✝ : InClosure s a✝¹
⊢ f a✝¹ ∈ closure (f '' s) → f a✝¹⁻¹ ∈ closure (f '' s)
[PROOFSTEP]
rw [hf.map_inv]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
a✝¹ : G
a✝ : InClosure s a✝¹
⊢ f a✝¹ ∈ closure (f '' s) → (f a✝¹)⁻¹ ∈ closure (f '' s)
[PROOFSTEP]
apply IsSubgroup.inv_mem (closure.isSubgroup _)
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
⊢ ∀ {a b : G},
    InClosure s a → InClosure s b → f a ∈ closure (f '' s) → f b ∈ closure (f '' s) → f (a * b) ∈ closure (f '' s)
[PROOFSTEP]
intros _ _ _ _ ha hb
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
a✝² b✝ : G
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
ha : f a✝² ∈ closure (f '' s)
hb : f b✝ ∈ closure (f '' s)
⊢ f (a✝² * b✝) ∈ closure (f '' s)
[PROOFSTEP]
rw [hf.map_mul]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝¹ : Group G
s✝ : Set G
inst✝ : Group H
f : G → H
hf : IsGroupHom f
s : Set G
x : G
hx : x ∈ closure s
a✝² b✝ : G
a✝¹ : InClosure s a✝²
a✝ : InClosure s b✝
ha : f a✝² ∈ closure (f '' s)
hb : f b✝ ∈ closure (f '' s)
⊢ f a✝² * f b✝ ∈ closure (f '' s)
[PROOFSTEP]
exact (closure.isSubgroup (f '' s)).toIsSubmonoid.mul_mem ha hb
[GOAL]
G✝ : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G✝
inst✝¹ : Group G✝
s✝ : Set G✝
G : Type u_4
inst✝ : CommGroup G
s t : Set G
x : G
⊢ x ∈ closure (s ∪ t) ↔ ∃ y, y ∈ closure s ∧ ∃ z, z ∈ closure t ∧ y * z = x
[PROOFSTEP]
simp only [closure_eq_mclosure, Monoid.mem_closure_union_iff, exists_prop, preimage_union]
[GOAL]
G✝ : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G✝
inst✝¹ : Group G✝
s✝ : Set G✝
G : Type u_4
inst✝ : CommGroup G
s t : Set G
x : G
⊢ (∃ y,
      (∃ y_1, y_1 ∈ Monoid.Closure s ∧ ∃ z, z ∈ Monoid.Closure t ∧ y_1 * z = y) ∧
        ∃ z,
          (∃ y, y ∈ Monoid.Closure (Inv.inv ⁻¹' s) ∧ ∃ z_1, z_1 ∈ Monoid.Closure (Inv.inv ⁻¹' t) ∧ y * z_1 = z) ∧
            y * z = x) ↔
    ∃ y,
      (∃ y_1, y_1 ∈ Monoid.Closure s ∧ ∃ z, z ∈ Monoid.Closure (Inv.inv ⁻¹' s) ∧ y_1 * z = y) ∧
        ∃ z, (∃ y, y ∈ Monoid.Closure t ∧ ∃ z_1, z_1 ∈ Monoid.Closure (Inv.inv ⁻¹' t) ∧ y * z_1 = z) ∧ y * z = x
[PROOFSTEP]
constructor
[GOAL]
case mp
G✝ : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G✝
inst✝¹ : Group G✝
s✝ : Set G✝
G : Type u_4
inst✝ : CommGroup G
s t : Set G
x : G
⊢ (∃ y,
      (∃ y_1, y_1 ∈ Monoid.Closure s ∧ ∃ z, z ∈ Monoid.Closure t ∧ y_1 * z = y) ∧
        ∃ z,
          (∃ y, y ∈ Monoid.Closure (Inv.inv ⁻¹' s) ∧ ∃ z_1, z_1 ∈ Monoid.Closure (Inv.inv ⁻¹' t) ∧ y * z_1 = z) ∧
            y * z = x) →
    ∃ y,
      (∃ y_1, y_1 ∈ Monoid.Closure s ∧ ∃ z, z ∈ Monoid.Closure (Inv.inv ⁻¹' s) ∧ y_1 * z = y) ∧
        ∃ z, (∃ y, y ∈ Monoid.Closure t ∧ ∃ z_1, z_1 ∈ Monoid.Closure (Inv.inv ⁻¹' t) ∧ y * z_1 = z) ∧ y * z = x
[PROOFSTEP]
rintro ⟨_, ⟨ys, hys, yt, hyt, rfl⟩, _, ⟨zs, hzs, zt, hzt, rfl⟩, rfl⟩
[GOAL]
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G✝ : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G✝
inst✝¹ : Group G✝
s✝ : Set G✝
G : Type u_4
inst✝ : CommGroup G
s t : Set G
ys : G
hys : ys ∈ Monoid.Closure s
yt : G
hyt : yt ∈ Monoid.Closure t
zs : G
hzs : zs ∈ Monoid.Closure (Inv.inv ⁻¹' s)
zt : G
hzt : zt ∈ Monoid.Closure (Inv.inv ⁻¹' t)
⊢ ∃ y,
    (∃ y_1, y_1 ∈ Monoid.Closure s ∧ ∃ z, z ∈ Monoid.Closure (Inv.inv ⁻¹' s) ∧ y_1 * z = y) ∧
      ∃ z,
        (∃ y, y ∈ Monoid.Closure t ∧ ∃ z_1, z_1 ∈ Monoid.Closure (Inv.inv ⁻¹' t) ∧ y * z_1 = z) ∧
          y * z = ys * yt * (zs * zt)
[PROOFSTEP]
refine' ⟨_, ⟨_, hys, _, hzs, rfl⟩, _, ⟨_, hyt, _, hzt, rfl⟩, _⟩
[GOAL]
case mp.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G✝ : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G✝
inst✝¹ : Group G✝
s✝ : Set G✝
G : Type u_4
inst✝ : CommGroup G
s t : Set G
ys : G
hys : ys ∈ Monoid.Closure s
yt : G
hyt : yt ∈ Monoid.Closure t
zs : G
hzs : zs ∈ Monoid.Closure (Inv.inv ⁻¹' s)
zt : G
hzt : zt ∈ Monoid.Closure (Inv.inv ⁻¹' t)
⊢ ys * zs * (yt * zt) = ys * yt * (zs * zt)
[PROOFSTEP]
rw [mul_assoc, mul_assoc, mul_left_comm zs]
[GOAL]
case mpr
G✝ : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G✝
inst✝¹ : Group G✝
s✝ : Set G✝
G : Type u_4
inst✝ : CommGroup G
s t : Set G
x : G
⊢ (∃ y,
      (∃ y_1, y_1 ∈ Monoid.Closure s ∧ ∃ z, z ∈ Monoid.Closure (Inv.inv ⁻¹' s) ∧ y_1 * z = y) ∧
        ∃ z, (∃ y, y ∈ Monoid.Closure t ∧ ∃ z_1, z_1 ∈ Monoid.Closure (Inv.inv ⁻¹' t) ∧ y * z_1 = z) ∧ y * z = x) →
    ∃ y,
      (∃ y_1, y_1 ∈ Monoid.Closure s ∧ ∃ z, z ∈ Monoid.Closure t ∧ y_1 * z = y) ∧
        ∃ z,
          (∃ y, y ∈ Monoid.Closure (Inv.inv ⁻¹' s) ∧ ∃ z_1, z_1 ∈ Monoid.Closure (Inv.inv ⁻¹' t) ∧ y * z_1 = z) ∧
            y * z = x
[PROOFSTEP]
rintro ⟨_, ⟨ys, hys, zs, hzs, rfl⟩, _, ⟨yt, hyt, zt, hzt, rfl⟩, rfl⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G✝ : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G✝
inst✝¹ : Group G✝
s✝ : Set G✝
G : Type u_4
inst✝ : CommGroup G
s t : Set G
ys : G
hys : ys ∈ Monoid.Closure s
zs : G
hzs : zs ∈ Monoid.Closure (Inv.inv ⁻¹' s)
yt : G
hyt : yt ∈ Monoid.Closure t
zt : G
hzt : zt ∈ Monoid.Closure (Inv.inv ⁻¹' t)
⊢ ∃ y,
    (∃ y_1, y_1 ∈ Monoid.Closure s ∧ ∃ z, z ∈ Monoid.Closure t ∧ y_1 * z = y) ∧
      ∃ z,
        (∃ y, y ∈ Monoid.Closure (Inv.inv ⁻¹' s) ∧ ∃ z_1, z_1 ∈ Monoid.Closure (Inv.inv ⁻¹' t) ∧ y * z_1 = z) ∧
          y * z = ys * zs * (yt * zt)
[PROOFSTEP]
refine' ⟨_, ⟨ys, hys, yt, hyt, rfl⟩, _, ⟨zs, hzs, zt, hzt, rfl⟩, _⟩
[GOAL]
case mpr.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro.intro
G✝ : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G✝
inst✝¹ : Group G✝
s✝ : Set G✝
G : Type u_4
inst✝ : CommGroup G
s t : Set G
ys : G
hys : ys ∈ Monoid.Closure s
zs : G
hzs : zs ∈ Monoid.Closure (Inv.inv ⁻¹' s)
yt : G
hyt : yt ∈ Monoid.Closure t
zt : G
hzt : zt ∈ Monoid.Closure (Inv.inv ⁻¹' t)
⊢ ys * yt * (zs * zt) = ys * zs * (yt * zt)
[PROOFSTEP]
rw [mul_assoc, mul_assoc, mul_left_comm yt]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
⊢ trivial G ⊆ Group.closure ∅
[PROOFSTEP]
simp [Set.subset_def, (Group.closure.isSubgroup _).one_mem]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
inst✝ : Group G
⊢ ∅ ⊆ trivial G
[PROOFSTEP]
simp
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b c : G
s : Set G
inst✝ : Group G
t : Set G
ht : IsNormalSubgroup t
a : G
h : a ∈ t
x : G
hc : x ∈ conjugatesOf a
⊢ x ∈ t
[PROOFSTEP]
obtain ⟨c, w⟩ := isConj_iff.1 hc
[GOAL]
case intro
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b c✝ : G
s : Set G
inst✝ : Group G
t : Set G
ht : IsNormalSubgroup t
a : G
h : a ∈ t
x : G
hc : x ∈ conjugatesOf a
c : G
w : c * a * c⁻¹ = x
⊢ x ∈ t
[PROOFSTEP]
have H := IsNormalSubgroup.normal ht a h c
[GOAL]
case intro
G : Type u_1
H✝ : Type u_2
A : Type u_3
a✝ a₁ a₂ b c✝ : G
s : Set G
inst✝ : Group G
t : Set G
ht : IsNormalSubgroup t
a : G
h : a ∈ t
x : G
hc : x ∈ conjugatesOf a
c : G
w : c * a * c⁻¹ = x
H : c * a * c⁻¹ ∈ t
⊢ x ∈ t
[PROOFSTEP]
rwa [← w]
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n : G
h : n ∈ normalClosure s
g : G
⊢ g * n * g⁻¹ ∈ normalClosure s
[PROOFSTEP]
induction' h with x hx x hx ihx x y hx hy ihx ihy
[GOAL]
case basic
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g x : G
hx : x ∈ conjugatesOfSet s
⊢ g * x * g⁻¹ ∈ normalClosure s
[PROOFSTEP]
exact conjugatesOfSet_subset_normalClosure (conj_mem_conjugatesOfSet hx)
[GOAL]
case one
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g : G
⊢ g * 1 * g⁻¹ ∈ normalClosure s
[PROOFSTEP]
simpa using (normalClosure.isSubgroup s).one_mem
[GOAL]
case inv
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g x : G
hx : InClosure (conjugatesOfSet s) x
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ g * x⁻¹ * g⁻¹ ∈ normalClosure s
[PROOFSTEP]
rw [← conj_inv]
[GOAL]
case inv
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g x : G
hx : InClosure (conjugatesOfSet s) x
ihx : g * x * g⁻¹ ∈ normalClosure s
⊢ (g * x * g⁻¹)⁻¹ ∈ normalClosure s
[PROOFSTEP]
exact (normalClosure.isSubgroup _).inv_mem ihx
[GOAL]
case mul
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g x y : G
hx : InClosure (conjugatesOfSet s) x
hy : InClosure (conjugatesOfSet s) y
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * (x * y) * g⁻¹ ∈ normalClosure s
[PROOFSTEP]
rw [← conj_mul]
[GOAL]
case mul
G : Type u_1
H : Type u_2
A : Type u_3
a a₁ a₂ b c : G
s : Set G
inst✝ : Group G
src✝ : IsSubgroup (normalClosure s) := isSubgroup s
n g x y : G
hx : InClosure (conjugatesOfSet s) x
hy : InClosure (conjugatesOfSet s) y
ihx : g * x * g⁻¹ ∈ normalClosure s
ihy : g * y * g⁻¹ ∈ normalClosure s
⊢ g * x * g⁻¹ * (g * y * g⁻¹) ∈ normalClosure s
[PROOFSTEP]
exact (normalClosure.isSubgroup _).toIsSubmonoid.mul_mem ihx ihy
[GOAL]
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b c : G
s✝ : Set G
inst✝ : Group G
s t : Set G
ht : IsNormalSubgroup t
h : s ⊆ t
a : G
w : a ∈ normalClosure s
⊢ a ∈ t
[PROOFSTEP]
induction' w with x hx x _ ihx x y _ _ ihx ihy
[GOAL]
case basic
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b c : G
s✝ : Set G
inst✝ : Group G
s t : Set G
ht : IsNormalSubgroup t
h : s ⊆ t
a x : G
hx : x ∈ conjugatesOfSet s
⊢ x ∈ t
[PROOFSTEP]
exact conjugatesOfSet_subset' ht h <| hx
[GOAL]
case one
G : Type u_1
H : Type u_2
A : Type u_3
a✝ a₁ a₂ b c : G
s✝ : Set G
inst✝ : Group G
s t : Set G
ht : IsNormalSubgroup t
h : s ⊆ t
a : G
⊢ 1 ∈ t
[PROOFSTEP]
exact ht.toIsSubgroup.toIsSubmonoid.one_mem
[GOAL]
case inv
G : Type u_1
H : Type u_2
A : Type u_3
a✝¹ a₁ a₂ b c : G
s✝ : Set G
inst✝ : Group G
s t : Set G
ht : IsNormalSubgroup t
h : s ⊆ t
a x : G
a✝ : InClosure (conjugatesOfSet s) x
ihx : x ∈ t
⊢ x⁻¹ ∈ t
[PROOFSTEP]
exact ht.toIsSubgroup.inv_mem ihx
[GOAL]
case mul
G : Type u_1
H : Type u_2
A : Type u_3
a✝² a₁ a₂ b c : G
s✝ : Set G
inst✝ : Group G
s t : Set G
ht : IsNormalSubgroup t
h : s ⊆ t
a x y : G
a✝¹ : InClosure (conjugatesOfSet s) x
a✝ : InClosure (conjugatesOfSet s) y
ihx : x ∈ t
ihy : y ∈ t
⊢ x * y ∈ t
[PROOFSTEP]
exact ht.toIsSubgroup.toIsSubmonoid.mul_mem ihx ihy
