-- Mathlib/Algebra/Group/Subgroup/Pointwise.lean
theorem mul_normal (H N : Subgroup G) [hN : N.Normal] : (↑(H ⊔ N) : Set G) = H * N

Proof state:
case mul.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 => x1 * x2) x y ∈ closure (↑H * ↑N)
x' : G
hx' : x' ∈ ↑H
y' : G
hy' : y' ∈ ↑N
hy✝ : (fun x1 x2 => x1 * x2) x' y' ∈ closure (↑H * ↑N)
⊢ (fun x1 x2 => x1 * x2) x y * (fun x1 x2 => x1 * x2) x' y' ∈ ↑H * ↑N

Tactic:
refine ⟨x * x', mul_mem hx hx', x'⁻¹ * y * x' * y', mul_mem ?_ hy', ?_⟩

Result:
case mul.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 => x1 * x2) x y ∈ closure (↑H * ↑N)
x' : G
hx' : x' ∈ ↑H
y' : G
hy' : y' ∈ ↑N
hy✝ : (fun x1 x2 => x1 * x2) x' y' ∈ closure (↑H * ↑N)
⊢ x'⁻¹ * y * x' ∈ N

case mul.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 => x1 * x2) x y ∈ closure (↑H * ↑N)
x' : G
hx' : x' ∈ ↑H
y' : G
hy' : y' ∈ ↑N
hy✝ : (fun x1 x2 => x1 * x2) x' y' ∈ closure (↑H * ↑N)
⊢ (fun x1 x2 => x1 * x2) (x * x') (x'⁻¹ * y * x' * y') = (fun x1 x2 => x1 * x2) x y * (fun x1 x2 => x1 * x2) x' y'

Proof state:
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
⊢ ↑(H ⊔ N) = ↑H * ↑N

Tactic:
rw [sup_eq_closure_mul]

Result:
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
⊢ ↑(closure (↑H * ↑N)) = ↑H * ↑N

Proof state:
case mem
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
x x✝ : G
hx : x✝ ∈ ↑H * ↑N
⊢ x✝ ∈ ↑H * ↑N

Tactic:
exact hx

Result:
no goals

Proof state:
case mul
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
x x'✝ x' : G
hx✝ : x'✝ ∈ closure (↑H * ↑N)
hy✝ : x' ∈ closure (↑H * ↑N)
hx : x'✝ ∈ ↑H * ↑N
hx' : x' ∈ ↑H * ↑N
⊢ x'✝ * x' ∈ ↑H * ↑N

Tactic:
obtain ⟨x, hx, y, hy, rfl⟩ := hx

Result:
case mul.intro.intro.intro.intro
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
x✝ x' : G
hy✝ : x' ∈ closure (↑H * ↑N)
hx' : x' ∈ ↑H * ↑N
x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 => x1 * x2) x y ∈ closure (↑H * ↑N)
⊢ (fun x1 x2 => x1 * x2) x y * x' ∈ ↑H * ↑N

Proof state:
case inv_mem.intro.intro.intro.intro
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
⊢ ((fun x1 x2 => x1 * x2) x y)⁻¹ ∈ ↑H * ↑N

Tactic:
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)

Result:
no goals

Proof state:
case mul.intro.intro.intro.intro.intro.intro.intro.intro.refine_1
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 => x1 * x2) x y ∈ closure (↑H * ↑N)
x' : G
hx' : x' ∈ ↑H
y' : G
hy' : y' ∈ ↑N
hy✝ : (fun x1 x2 => x1 * x2) x' y' ∈ closure (↑H * ↑N)
⊢ x'⁻¹ * y * x' ∈ N

Tactic:
simpa using hN.conj_mem _ hy x'⁻¹

Result:
no goals

Proof state:
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
⊢ ↑(closure (↑H * ↑N)) = ↑H * ↑N

Tactic:
refine Set.Subset.antisymm (fun x hx => ?_) subset_closure

Result:
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
x : G
hx : x ∈ ↑(closure (↑H * ↑N))
⊢ x ∈ ↑H * ↑N

Proof state:
case inv_mem
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
x✝ x : G
hx : x ∈ ↑H * ↑N
⊢ x⁻¹ ∈ ↑H * ↑N

Tactic:
obtain ⟨x, hx, y, hy, rfl⟩ := hx

Result:
case inv_mem.intro.intro.intro.intro
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
⊢ ((fun x1 x2 => x1 * x2) x y)⁻¹ ∈ ↑H * ↑N

Proof state:
case mul.intro.intro.intro.intro.intro.intro.intro.intro.refine_2
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 => x1 * x2) x y ∈ closure (↑H * ↑N)
x' : G
hx' : x' ∈ ↑H
y' : G
hy' : y' ∈ ↑N
hy✝ : (fun x1 x2 => x1 * x2) x' y' ∈ closure (↑H * ↑N)
⊢ (fun x1 x2 => x1 * x2) (x * x') (x'⁻¹ * y * x' * y') = (fun x1 x2 => x1 * x2) x y * (fun x1 x2 => x1 * x2) x' y'

Tactic:
simp only [mul_assoc, mul_inv_cancel_left]

Result:
no goals

Proof state:
case one
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
x : G
⊢ 1 ∈ ↑H * ↑N

Tactic:
exact ⟨1, one_mem _, 1, one_mem _, mul_one 1⟩

Result:
no goals

Proof state:
case mul.intro.intro.intro.intro
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
x✝ x' : G
hy✝ : x' ∈ closure (↑H * ↑N)
hx' : x' ∈ ↑H * ↑N
x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 => x1 * x2) x y ∈ closure (↑H * ↑N)
⊢ (fun x1 x2 => x1 * x2) x y * x' ∈ ↑H * ↑N

Tactic:
obtain ⟨x', hx', y', hy', rfl⟩ := hx'

Result:
case mul.intro.intro.intro.intro.intro.intro.intro.intro
G : Type u_2
inst✝ : Group G
H N : Subgroup G
hN : N.Normal
x✝ x : G
hx : x ∈ ↑H
y : G
hy : y ∈ ↑N
hx✝ : (fun x1 x2 => x1 * x2) x y ∈ closure (↑H * ↑N)
x' : G
hx' : x' ∈ ↑H
y' : G
hy' : y' ∈ ↑N
hy✝ : (fun x1 x2 => x1 * x2) x' y' ∈ closure (↑H * ↑N)
⊢ (fun x1 x2 => x1 * x2) x y * (fun x1 x2 => x1 * x2) x' y' ∈ ↑H * ↑N