α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
⊢ ↑(closure (↑H * ↑N)) = ↑H * ↑N
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
⊢ ↑(H ⊔ N) = ↑H * ↑N
rw [sup_eq_closure]
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ x ∈ ↑H * ↑N
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
⊢ ↑(closure (↑H * ↑N)) = ↑H * ↑N
refine Set.Subset.antisymm (fun x hx => ?_) subset_closure
case refine_1
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ ∀ (x : G), x ∈ ↑H * ↑N → (fun x => x ∈ ↑H * ↑N) x

case refine_2
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ ∀ (x : G), x ∈ ↑H * ↑N → (fun x => x ∈ ↑H * ↑N) x⁻¹

case refine_3
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ (fun x => x ∈ ↑H * ↑N) 1

case refine_4
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ ∀ (x y : G), (fun x => x ∈ ↑H * ↑N) x → (fun x => x ∈ ↑H * ↑N) y → (fun x => x ∈ ↑H * ↑N) (x * y)
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ x ∈ ↑H * ↑N
refine closure_induction'' (p := fun x => x ∈ (H : Set G) * (N : Set G)) hx ?_ ?_ ?_ ?_
case refine_1.intro.intro.intro.intro
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
⊢ (fun x x_1 => x * x_1) x y ∈ ↑H * ↑N
case refine_1
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ ∀ (x : G), x ∈ ↑H * ↑N → (fun x => x ∈ ↑H * ↑N) x
rintro _ ⟨x, y, hx, hy, rfl⟩
no goals
case refine_1.intro.intro.intro.intro
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
⊢ (fun x x_1 => x * x_1) x y ∈ ↑H * ↑N
exact mul_mem_mul hx hy
case refine_2.intro.intro.intro.intro
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
⊢ ((fun x x_1 => x * x_1) x y)⁻¹ ∈ ↑H * ↑N
case refine_2
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ ∀ (x : G), x ∈ ↑H * ↑N → (fun x => x ∈ ↑H * ↑N) x⁻¹
rintro _ ⟨x, y, hx, hy, rfl⟩
no goals
case refine_2.intro.intro.intro.intro
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
⊢ ((fun x x_1 => x * x_1) x y)⁻¹ ∈ ↑H * ↑N
simpa only [mul_inv_rev, mul_assoc, inv_inv, inv_mul_cancel_left]
  using mul_mem_mul (inv_mem hx) (hN.conj_mem _ (inv_mem hy) x)
no goals
case refine_3
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ (fun x => x ∈ ↑H * ↑N) 1
exact ⟨1, 1, one_mem _, one_mem _, mul_one 1⟩
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
x' y' : G
hx' : x' ∈ ↑H
hy' : y' ∈ ↑N
⊢ (fun x x_1 => x * x_1) x y * (fun x x_1 => x * x_1) x' y' ∈ ↑H * ↑N
case refine_4
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ ∀ (x y : G), (fun x => x ∈ ↑H * ↑N) x → (fun x => x ∈ ↑H * ↑N) y → (fun x => x ∈ ↑H * ↑N) (x * y)
rintro _ _ ⟨x, y, hx, hy, rfl⟩ ⟨x', y', hx', hy', rfl⟩
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
x' y' : G
hx' : x' ∈ ↑H
hy' : y' ∈ ↑N
⊢ x'⁻¹ * y * x' ∈ N

case refine_4.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
x' y' : G
hx' : x' ∈ ↑H
hy' : y' ∈ ↑N
⊢ (fun x x_1 => x * x_1) (x * x') (x'⁻¹ * y * x' * y') = (fun x x_1 => x * x_1) x y * (fun x x_1 => x * x_1) x' y'
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
x' y' : G
hx' : x' ∈ ↑H
hy' : y' ∈ ↑N
⊢ (fun x x_1 => x * x_1) x y * (fun x x_1 => x * x_1) x' y' ∈ ↑H * ↑N
refine ⟨x * x', x'⁻¹ * y * x' * y', mul_mem hx hx', mul_mem ?_ hy', ?_⟩
no goals
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
x' y' : G
hx' : x' ∈ ↑H
hy' : y' ∈ ↑N
⊢ x'⁻¹ * y * x' ∈ N
simpa using hN.conj_mem _ hy x'⁻¹
no goals
case refine_4.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type ?u.23973
G : Type u_1
A : Type ?u.23979
S : Type ?u.23982
inst✝¹ : Group G
inst✝ : AddGroup A
s : Set G
H N : Subgroup G
hN : Normal N
x✝ : G
hx✝ : x✝ ∈ ↑(closure (↑H * ↑N))
x y : G
hx : x ∈ ↑H
hy : y ∈ ↑N
x' y' : G
hx' : x' ∈ ↑H
hy' : y' ∈ ↑N
⊢ (fun x x_1 => x * x_1) (x * x') (x'⁻¹ * y * x' * y') = (fun x x_1 => x * x_1) x y * (fun x x_1 => x * x_1) x' y'
simp only [mul_assoc, mul_inv_cancel_left]