awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : (x : G) → Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x → Prop
hp : ∀ (i : ι) (x : G) (hx : x ∈ S i), C x ⋯
h1 : C 1 ⋯
hmul :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x)
    (hy : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) y), C x hx → C y hy → C (x * y) ⋯
x_1 : G
hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x_1
x y : G
w : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x
Cx : C x w
w_1 : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) y
Cy : C y w_1
⊢ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) (x * y)), C (x * y) h

Tactic:
exact ⟨_, hmul _ _ _ _ Cx Cy⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s t : Set G
H : Subgroup G
hs : s ⊆ (↑H : Set G)
ht : t ⊆ (↑H : Set G)
⊢ s * t ⊆ (↑H : Set G)

Tactic:
Submonoid.mul_subset hs ht

Premises used: Submonoid.mul_subset
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
H : Subgroup G
n : ℕ
hs : s ⊆ (↑H : Set G)
zero : HPow.hPow (β := ℕ) s 0 ⊆ (↑H : Set G)
succ : ∀ (n : ℕ), s ^ n ⊆ (↑H : Set G) → s ^ (n + 1) ⊆ (↑H : Set G)
⊢ s ^ n ⊆ (↑H : Set G)

Tactic:
induction n
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
H : Subgroup G
hs : s ⊆ (↑H : Set G)
⊢ HPow.hPow (β := ℕ) s 0 ⊆ (↑H : Set G)

Tactic:
simp [pow_succ, *]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
H : Subgroup G
hs : s ⊆ (↑H : Set G)
n : ℕ
h : s ^ n ⊆ (↑H : Set G)
⊢ s ^ (n + 1) ⊆ (↑H : Set G)

Tactic:
simp [pow_succ, *]

Premises used: pow_succ
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
S T : Set G
⊢ LE.le (α := Subgroup G) (closure (S * T)) (closure S ⊔ closure T)

Tactic:
sInf_le fun _x ⟨_s, hs, _t, ht, hx⟩ => hx ▸
    (closure S ⊔ closure T).mul_mem (SetLike.le_def.mp le_sup_left <| subset_closure hs)
      (SetLike.le_def.mp le_sup_right <| subset_closure ht)

Premises used: Subgroup.closure, le_sup_left, Set.Mem, SetLike.le_def, Membership.mem, Eq.rec, le_sup_right, Subgroup.subset_closure, _private.0.Subgroup.closure_mul_le.match_1, SetLike.coe, Max.max, sInf_le, Iff.mp, Subgroup.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
n : ℕ
⊢ LE.le (α := Subgroup G) (closure (s ^ n)) (closure s)

Tactic:
simp
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
m n : ℕ
hmn : m ∣ n
obtain : ∀ (k : ℕ), LE.le (α := Subgroup G) (closure (s ^ (m * k))) (closure (s ^ m))
⊢ LE.le (α := Subgroup G) (closure (s ^ n)) (closure (s ^ m))

Tactic:
obtain ⟨k, rfl⟩ := hmn

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
m k : ℕ
⊢ LE.le (α := Subgroup G) (closure (s ^ (m * k))) (closure (s ^ m))

Tactic:
simp [pow_mul]

Premises used: pow_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
s : Set G
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
grw grw₁ : LE.le (α := Subgroup G) (closure s) (closure s)
⊢ LE.le (α := Subgroup G) (closure s) (closure (s ^ n))

Tactic:
grw [← subset_pow hs hn]

Premises used: Set.subset_pow
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
rw : H ⊔ closure (↑K : Set G) ≤ H ⊔ K
rw₁ rw₂ : H ⊔ K ≤ H ⊔ K
⊢ closure (↑H : Set G) ⊔ closure (↑K : Set G) ≤ H ⊔ K

Tactic:
rw [closure_eq, closure_eq]

Premises used: Subgroup.closure_eq
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ (↑(normalizer (↑N : Set G)) : Set G)
rw :
  Eq.{u_2 + 1} (α := Set G) (⋃ a ∈ S, (fun (x : G) ↦ a * x) '' (↑N : Set G))
    (⋃ a ∈ S, (fun (x : G) ↦ x * a) '' (↑N : Set G))
⊢ S * (↑N : Set G) = (↑N : Set G) * S

Tactic:
rw [← iUnion_mul_left_image, ← iUnion_mul_right_image]

Premises used: Set.iUnion_mul_left_image, Set.iUnion_mul_right_image
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ (↑(normalizer (↑N : Set G)) : Set G)
simp : Eq.{u_2 + 1} (α := Set G) (⋃ a ∈ S, {x : G | a⁻¹ * x ∈ (↑N : Set G)}) (⋃ a ∈ S, {x : G | x * a⁻¹ ∈ (↑N : Set G)})
⊢ Eq.{u_2 + 1} (α := Set G) (⋃ a ∈ S, (fun (x : G) ↦ a * x) '' (↑N : Set G))
    (⋃ a ∈ S, (fun (x : G) ↦ x * a) '' (↑N : Set G))

Tactic:
simp only [image_mul_left, image_mul_right, Set.preimage]

Premises used: Set.image_mul_right, Set.preimage, Set.image_mul_left
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ (↑(normalizer (↑N : Set G)) : Set G)
h : ∀ (s : G) (hs : s ∈ S) (x : G), s⁻¹ * x ∈ (↑N : Set G) ↔ x * s⁻¹ ∈ (↑N : Set G)
⊢ Eq.{u_2 + 1} (α := Set G) (⋃ a ∈ S, {x : G | a⁻¹ * x ∈ (↑N : Set G)}) (⋃ a ∈ S, {x : G | x * a⁻¹ ∈ (↑N : Set G)})

Tactic:
congr! 5 with s hs x
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ (↑(normalizer (↑N : Set G)) : Set G)
s : G
hs : s ∈ S
x : G
⊢ s⁻¹ * x ∈ (↑N : Set G) ↔ x * s⁻¹ ∈ (↑N : Set G)

Tactic:
(mem_normalizer_iff'.mp (inv_mem (hLE hs)) x).symm

Premises used: Set.Mem, InvMemClass.inv_mem, Iff.mp, Subgroup.mem_normalizer_iff', Iff.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ (↑(normalizer (↑N : Set G)) : Set G)
s : G
hs : s ∈ S
x : G
⊢ s⁻¹ * x ∈ (↑N : Set G) ↔ x * s⁻¹ ∈ (↑N : Set G)

Tactic:
exact (mem_normalizer_iff'.mp (inv_mem (hLE hs)) x).symm

Premises used: InvMemClass.inv_mem, Iff.mp, Subgroup.mem_normalizer_iff', Iff.symm
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
S : Set G
N : Subgroup G
hN : N.Normal
⊢ S * (↑N : Set G) = (↑N : Set G) * S

Tactic:
set_mul_normalizer_comm S N subset_normalizer_of_normal

Premises used: Subgroup.set_mul_normalizer_comm, Subgroup.subset_normalizer_of_normal
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
rw : (↑(closure ((↑H : Set G) * (↑N : Set G))) : Set G) = (↑H : Set G) * (↑N : Set G)
⊢ (↑(H ⊔ N) : Set G) = (↑H : Set G) * (↑N : Set G)

Tactic:
rw [sup_eq_closure_mul]

Premises used: Subgroup.sup_eq_closure_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
⊢ (↑(closure ((↑H : Set G) * (↑N : Set G))) : Set G) = (↑H : Set G) * (↑N : Set G)

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

Premises used: Set.Subset.antisymm, Subgroup.subset_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
refine : ∀ (x : G) (hx : x ∈ (↑(closure ((↑H : Set G) * (↑N : Set G))) : Set G)), x ∈ (↑H : Set G) * (↑N : Set G)
⊢ (↑(closure ((↑H : Set G) * (↑N : Set G))) : Set G) = (↑H : Set G) * (↑N : Set G)

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

Premises used: Set.Subset.antisymm, Subgroup.subset_closure
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
x : G
⊢ 1 ∈ (↑H : Set G) * (↑N : Set G)

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

Premises used: Set.Mem, setOf, Set.image2, And.intro, Exists.intro, OneMemClass.one_mem, mul_one, OfNat.ofNat
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
x : G
⊢ 1 ∈ (↑H : Set G) * (↑N : Set G)

Tactic:
exact ⟨1, one_mem _, 1, one_mem _, mul_one 1⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
x x_1 : G
hx : x_1 ∈ (↑H : Set G) * (↑N : Set G)
⊢ x_1 ∈ (↑H : Set G) * (↑N : Set G)

Tactic:
hx
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
x x_1 : G
hx : x_1 ∈ (↑H : Set G) * (↑N : Set G)
⊢ x_1 ∈ (↑H : Set G) * (↑N : Set G)

Tactic:
exact hx
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
x_1 x : G
hx : x ∈ (↑H : Set G) * (↑N : Set G)
inv_mem :
  ∀ (x : G) (hx : x ∈ (↑H : Set G)) (y : G) (hy : y ∈ (↑N : Set G)),
    ((fun (x1 x2 : G) ↦ x1 * x2) x y)⁻¹ ∈ (↑H : Set G) * (↑N : Set G)
⊢ x⁻¹ ∈ (↑H : Set G) * (↑N : Set G)

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

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
x_1 x : G
hx : x ∈ (↑H : Set G)
y : G
hy : y ∈ (↑N : Set G)
⊢ ((fun (x1 x2 : G) ↦ x1 * x2) x y)⁻¹ ∈ (↑H : Set G) * (↑N : Set G)

Tactic:
simpa only [mul_inv_rev, mul_assoc, inv_inv, inv_mul_cancel_left]
      using mul_mem_mul (inv_mem hx) ((mem_normalizer_iff.mp (hLE hx) y⁻¹).mp (inv_mem hy))

Premises used: inv_mul_cancel_left, mul_assoc, InvMemClass.inv_mem, Inv.inv, Subgroup.mem_normalizer_iff, inv_inv, Iff.mp, mul_inv_rev, Set.mul_mem_mul
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
x x'_1 x' : G
hx_1 : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) x'_1
hy : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) x'
hx : x'_1 ∈ (↑H : Set G) * (↑N : Set G)
hx' : x' ∈ (↑H : Set G) * (↑N : Set G)
mul :
  ∀ (x : G) (hx : x ∈ (↑H : Set G)) (y : G) (hy : y ∈ (↑N : Set G)),
    Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) ((fun (x1 x2 : G) ↦ x1 * x2) x y) →
      (fun (x1 x2 : G) ↦ x1 * x2) x y * x' ∈ (↑H : Set G) * (↑N : Set G)
⊢ x'_1 * x' ∈ (↑H : Set G) * (↑N : Set G)

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

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
x_1 x' : G
hy_1 : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) x'
hx' : x' ∈ (↑H : Set G) * (↑N : Set G)
x : G
hx : x ∈ (↑H : Set G)
y : G
hy : y ∈ (↑N : Set G)
hx_1 : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) ((fun (x1 x2 : G) ↦ x1 * x2) x y)
mul :
  ∀ (x' : G) (hx' : x' ∈ (↑H : Set G)) (y' : G) (hy' : y' ∈ (↑N : Set G)),
    Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) ((fun (x1 x2 : G) ↦ x1 * x2) x' y') →
      HMul.hMul (α := G) ((fun (x1 x2 : G) ↦ x1 * x2) x y) ((fun (x1 x2 : G) ↦ x1 * x2) x' y') ∈
        (↑H : Set G) * (↑N : Set G)
⊢ (fun (x1 x2 : G) ↦ x1 * x2) x y * x' ∈ (↑H : Set G) * (↑N : Set G)

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

Premises used: rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
x_1 x : G
hx : x ∈ (↑H : Set G)
y : G
hy : y ∈ (↑N : Set G)
hx_1 : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) ((fun (x1 x2 : G) ↦ x1 * x2) x y)
x' : G
hx' : x' ∈ (↑H : Set G)
y' : G
hy' : y' ∈ (↑N : Set G)
hy_1 : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) ((fun (x1 x2 : G) ↦ x1 * x2) x' y')
⊢ HMul.hMul (α := G) ((fun (x1 x2 : G) ↦ x1 * x2) x y) ((fun (x1 x2 : G) ↦ x1 * x2) x' y') ∈ (↑H : Set G) * (↑N : Set G)

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

Premises used: HMul.hMul, Set.Mem, setOf, Inv.inv, Set.image2, And.intro, Exists.intro, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
x_1 x : G
hx : x ∈ (↑H : Set G)
y : G
hy : y ∈ (↑N : Set G)
hx_1 : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) ((fun (x1 x2 : G) ↦ x1 * x2) x y)
x' : G
hx' : x' ∈ (↑H : Set G)
y' : G
hy' : y' ∈ (↑N : Set G)
hy_1 : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) ((fun (x1 x2 : G) ↦ x1 * x2) x' y')
mul : x'⁻¹ * y * x' ∈ N
mul₁ :
  (fun (x1 x2 : G) ↦ x1 * x2) (x * x') (x'⁻¹ * y * x' * y') =
    HMul.hMul (α := G) ((fun (x1 x2 : G) ↦ x1 * x2) x y) ((fun (x1 x2 : G) ↦ x1 * x2) x' y')
⊢ HMul.hMul (α := G) ((fun (x1 x2 : G) ↦ x1 * x2) x y) ((fun (x1 x2 : G) ↦ x1 * x2) x' y') ∈ (↑H : Set G) * (↑N : Set G)

Tactic:
refine ⟨x * x', mul_mem hx hx', x'⁻¹ * y * x' * y', mul_mem ?_ hy', ?_⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
x_1 x : G
hx : x ∈ (↑H : Set G)
y : G
hy : y ∈ (↑N : Set G)
hx_1 : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) ((fun (x1 x2 : G) ↦ x1 * x2) x y)
x' : G
hx' : x' ∈ (↑H : Set G)
y' : G
hy' : y' ∈ (↑N : Set G)
hy_1 : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) ((fun (x1 x2 : G) ↦ x1 * x2) x' y')
⊢ x'⁻¹ * y * x' ∈ N

Tactic:
(mem_normalizer_iff''.mp (hLE hx') y).mp hy

Premises used: Subgroup.mem_normalizer_iff'', Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
x_1 x : G
hx : x ∈ (↑H : Set G)
y : G
hy : y ∈ (↑N : Set G)
hx_1 : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) ((fun (x1 x2 : G) ↦ x1 * x2) x y)
x' : G
hx' : x' ∈ (↑H : Set G)
y' : G
hy' : y' ∈ (↑N : Set G)
hy_1 : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) ((fun (x1 x2 : G) ↦ x1 * x2) x' y')
⊢ x'⁻¹ * y * x' ∈ N

Tactic:
exact (mem_normalizer_iff''.mp (hLE hx') y).mp hy

Premises used: Subgroup.mem_normalizer_iff'', Iff.mp
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
x_1 x : G
hx : x ∈ (↑H : Set G)
y : G
hy : y ∈ (↑N : Set G)
hx_1 : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) ((fun (x1 x2 : G) ↦ x1 * x2) x y)
x' : G
hx' : x' ∈ (↑H : Set G)
y' : G
hy' : y' ∈ (↑N : Set G)
hy_1 : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) ((fun (x1 x2 : G) ↦ x1 * x2) x' y')
⊢ (fun (x1 x2 : G) ↦ x1 * x2) (x * x') (x'⁻¹ * y * x' * y') =
    HMul.hMul (α := G) ((fun (x1 x2 : G) ↦ x1 * x2) x y) ((fun (x1 x2 : G) ↦ x1 * x2) x' y')

Tactic:
simp only [mul_assoc, mul_inv_cancel_left]

Premises used: mul_assoc, mul_inv_cancel_left
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
x : G
hx : x ∈ (↑(closure ((↑H : Set G) * (↑N : Set G))) : Set G)
one : 1 ∈ (↑H : Set G) * (↑N : Set G)
mem : ∀ (x : G) (hx : x ∈ (↑H : Set G) * (↑N : Set G)), x ∈ (↑H : Set G) * (↑N : Set G)
inv_mem : ∀ (x : G) (hx : x ∈ (↑H : Set G) * (↑N : Set G)), x⁻¹ ∈ (↑H : Set G) * (↑N : Set G)
mul :
  ∀ (x' x'_1 : G),
    Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) x' →
      Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) * (↑N : Set G))) x'_1 →
        ∀ (hx : x' ∈ (↑H : Set G) * (↑N : Set G)) (hx' : x'_1 ∈ (↑H : Set G) * (↑N : Set G)),
          x' * x'_1 ∈ (↑H : Set G) * (↑N : Set G)
⊢ x ∈ (↑H : Set G) * (↑N : Set G)

Tactic:
induction hx using closure_induction'' with
  | one => exact ⟨1, one_mem _, 1, one_mem _, mul_one 1⟩
  | mem _ hx => exact hx
  | inv_mem x hx =>
    obtain ⟨x, hx, y, hy, rfl⟩ := hx
    simpa only [mul_inv_rev, mul_assoc, inv_inv, inv_mul_cancel_left]
      using mul_mem_mul (inv_mem hx) ((mem_normalizer_iff.mp (hLE hx) y⁻¹).mp (inv_mem hy))
  | mul x' x' _ _ hx hx' =>
    obtain ⟨x, hx, y, hy, rfl⟩ := hx
    obtain ⟨x', hx', y', hy', rfl⟩ := hx'
    refine ⟨x * x', mul_mem hx hx', x'⁻¹ * y * x' * y', mul_mem ?_ hy', ?_⟩
    · exact (mem_normalizer_iff''.mp (hLE hx') y).mp hy
    · simp only [mul_assoc, mul_inv_cancel_left]

Premises used: inv_mul_cancel_left, mul_assoc, Subgroup.mul, InvMemClass.inv_mem, Subgroup.one, inv_inv, mul_inv_rev, mul_inv_cancel_left, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
N H : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
rw : (↑(N ⊔ H) : Set G) = (↑H : Set G) * (↑N : Set G)
rw₁ : (↑(H ⊔ N) : Set G) = (↑H : Set G) * (↑N : Set G)
rw₂ rw₃ : (↑H : Set G) * (↑N : Set G) = (↑H : Set G) * (↑N : Set G)
⊢ (↑(N ⊔ H) : Set G) = (↑N : Set G) * (↑H : Set G)

Tactic:
rw [← set_mul_normalizer_comm _ _ hLE, sup_comm, coe_mul_of_left_le_normalizer_right _ _ hLE]

Premises used: Subgroup.coe_mul_of_left_le_normalizer_right, Subgroup.set_mul_normalizer_comm, sup_comm
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hN : N.Normal
⊢ (↑(H ⊔ N) : Set G) = (↑H : Set G) * (↑N : Set G)

Tactic:
coe_mul_of_left_le_normalizer_right H N le_normalizer_of_normal

Premises used: Subgroup.coe_mul_of_left_le_normalizer_right, Subgroup.le_normalizer_of_normal
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
N H : Subgroup G
inst_1 : N.Normal
⊢ (↑(N ⊔ H) : Set G) = (↑N : Set G) * (↑H : Set G)

Tactic:
coe_mul_of_right_le_normalizer_left N H le_normalizer_of_normal

Premises used: Subgroup.le_normalizer_of_normal, Subgroup.coe_mul_of_right_le_normalizer_left
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : A ≤ C
h₁ : ∀ (x : G), x ∈ (↑A : Set G) * (↑(B ⊓ C) : Set G) ↔ x ∈ (↑A : Set G) * (↑B : Set G) ∩ (↑C : Set G)
⊢ (↑A : Set G) * (↑(B ⊓ C) : Set G) = (↑A : Set G) * (↑B : Set G) ∩ (↑C : Set G)

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : A ≤ C
x : G
h₁ :
  (∃ x_1 ∈ (↑A : Set G), ∃ (y : G), (y ∈ (↑B : Set G) ∧ y ∈ (↑C : Set G)) ∧ x_1 * y = x) →
    (∃ x_1 ∈ (↑A : Set G), ∃ y ∈ (↑B : Set G), x_1 * y = x) ∧ x ∈ (↑C : Set G)
h₂ :
  (∃ x_1 ∈ (↑A : Set G), ∃ y ∈ (↑B : Set G), x_1 * y = x) ∧ x ∈ (↑C : Set G) →
    ∃ x_1 ∈ (↑A : Set G), ∃ (y : G), (y ∈ (↑B : Set G) ∧ y ∈ (↑C : Set G)) ∧ x_1 * y = x
⊢ (∃ x_1 ∈ (↑A : Set G), ∃ (y : G), (y ∈ (↑B : Set G) ∧ y ∈ (↑C : Set G)) ∧ x_1 * y = x) ↔
    (∃ x_1 ∈ (↑A : Set G), ∃ y ∈ (↑B : Set G), x_1 * y = x) ∧ x ∈ (↑C : Set G)

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ (↑A : Set G)
z : G
hzB : z ∈ (↑B : Set G)
hzC : z ∈ (↑C : Set G)
⊢ (∃ x ∈ (↑A : Set G), ∃ y_1 ∈ (↑B : Set G), x * y_1 = y * z) ∧ y * z ∈ (↑C : Set G)

Tactic:
⟨?_, mul_mem (h hy) hzC⟩

Premises used: And.intro, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ (↑A : Set G)
z : G
hzB : z ∈ (↑B : Set G)
hzC : z ∈ (↑C : Set G)
h₁ : ∃ x ∈ (↑A : Set G), ∃ y_1 ∈ (↑B : Set G), x * y_1 = y * z
⊢ (∃ x ∈ (↑A : Set G), ∃ y_1 ∈ (↑B : Set G), x * y_1 = y * z) ∧ y * z ∈ (↑C : Set G)

Tactic:
refine ⟨?_, mul_mem (h hy) hzC⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ (↑A : Set G)
z : G
hzB : z ∈ (↑B : Set G)
hzC : z ∈ (↑C : Set G)
⊢ ∃ x ∈ (↑A : Set G), ∃ y_1 ∈ (↑B : Set G), x * y_1 = y * z

Tactic:
⟨y, hy, z, hzB, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ (↑A : Set G)
z : G
hzB : z ∈ (↑B : Set G)
hzC : z ∈ (↑C : Set G)
⊢ ∃ x ∈ (↑A : Set G), ∃ y_1 ∈ (↑B : Set G), x * y_1 = y * z

Tactic:
exact ⟨y, hy, z, hzB, rfl⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ (↑A : Set G)
z : G
hz : z ∈ (↑B : Set G)
hyz : y * z ∈ (↑C : Set G)
⊢ ∃ x ∈ (↑A : Set G), ∃ (y_1 : G), (y_1 ∈ (↑B : Set G) ∧ y_1 ∈ (↑C : Set G)) ∧ x * y_1 = y * z

Tactic:
⟨y, hy, z, ⟨hz, ?_⟩, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ (↑A : Set G)
z : G
hz : z ∈ (↑B : Set G)
hyz : y * z ∈ (↑C : Set G)
h₁ : z ∈ (↑C : Set G)
⊢ ∃ x ∈ (↑A : Set G), ∃ (y_1 : G), (y_1 ∈ (↑B : Set G) ∧ y_1 ∈ (↑C : Set G)) ∧ x * y_1 = y * z

Tactic:
refine ⟨y, hy, z, ⟨hz, ?_⟩, rfl⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ (↑A : Set G)
z : G
hz : z ∈ (↑B : Set G)
hyz : y * z ∈ (↑C : Set G)
this : y⁻¹ * (y * z) ∈ C
⊢ z ∈ (↑C : Set G)

Tactic:
simpa
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ (↑A : Set G)
z : G
hz : z ∈ (↑B : Set G)
hyz : y * z ∈ (↑C : Set G)
h₁ : y⁻¹ * (y * z) ∈ C
⊢ z ∈ (↑C : Set G)

Tactic:
suffices y⁻¹ * (y * z) ∈ C by simpa
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ (↑A : Set G)
z : G
hz : z ∈ (↑B : Set G)
hyz : y * z ∈ (↑C : Set G)
⊢ y⁻¹ * (y * z) ∈ C

Tactic:
mul_mem (inv_mem (h hy)) hyz

Premises used: InvMemClass.inv_mem, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : A ≤ C
y : G
hy : y ∈ (↑A : Set G)
z : G
hz : z ∈ (↑B : Set G)
hyz : y * z ∈ (↑C : Set G)
⊢ y⁻¹ * (y * z) ∈ C

Tactic:
exact mul_mem (inv_mem (h hy)) hyz

Premises used: InvMemClass.inv_mem, MulMemClass.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : C ≤ A
h₁ : ∀ (x : G), x ∈ (↑(A ⊓ B) : Set G) * (↑C : Set G) ↔ x ∈ (↑A : Set G) ∩ ((↑B : Set G) * (↑C : Set G))
⊢ (↑(A ⊓ B) : Set G) * (↑C : Set G) = (↑A : Set G) ∩ ((↑B : Set G) * (↑C : Set G))

Tactic:
ext
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : C ≤ A
x : G
h₁ :
  (∃ (x_1 : G), (x_1 ∈ (↑A : Set G) ∧ x_1 ∈ (↑B : Set G)) ∧ ∃ y ∈ (↑C : Set G), x_1 * y = x) →
    x ∈ (↑A : Set G) ∧ ∃ x_1 ∈ (↑B : Set G), ∃ y ∈ (↑C : Set G), x_1 * y = x
h₂ :
  (x ∈ (↑A : Set G) ∧ ∃ x_1 ∈ (↑B : Set G), ∃ y ∈ (↑C : Set G), x_1 * y = x) →
    ∃ (x_1 : G), (x_1 ∈ (↑A : Set G) ∧ x_1 ∈ (↑B : Set G)) ∧ ∃ y ∈ (↑C : Set G), x_1 * y = x
⊢ (∃ (x_1 : G), (x_1 ∈ (↑A : Set G) ∧ x_1 ∈ (↑B : Set G)) ∧ ∃ y ∈ (↑C : Set G), x_1 * y = x) ↔
    x ∈ (↑A : Set G) ∧ ∃ x_1 ∈ (↑B : Set G), ∃ y ∈ (↑C : Set G), x_1 * y = x

Tactic:
constructor
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hyA : y ∈ (↑A : Set G)
hyB : y ∈ (↑B : Set G)
z : G
hz : z ∈ (↑C : Set G)
⊢ y * z ∈ (↑A : Set G) ∧ ∃ x ∈ (↑B : Set G), ∃ y_1 ∈ (↑C : Set G), x * y_1 = y * z

Tactic:
⟨A.mul_mem hyA (h hz), ?_⟩

Premises used: And.intro, Subgroup.mul_mem
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hyA : y ∈ (↑A : Set G)
hyB : y ∈ (↑B : Set G)
z : G
hz : z ∈ (↑C : Set G)
h₁ : ∃ x ∈ (↑B : Set G), ∃ y_1 ∈ (↑C : Set G), x * y_1 = y * z
⊢ y * z ∈ (↑A : Set G) ∧ ∃ x ∈ (↑B : Set G), ∃ y_1 ∈ (↑C : Set G), x * y_1 = y * z

Tactic:
refine ⟨A.mul_mem hyA (h hz), ?_⟩
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hyA : y ∈ (↑A : Set G)
hyB : y ∈ (↑B : Set G)
z : G
hz : z ∈ (↑C : Set G)
⊢ ∃ x ∈ (↑B : Set G), ∃ y_1 ∈ (↑C : Set G), x * y_1 = y * z

Tactic:
⟨y, hyB, z, hz, rfl⟩

Premises used: And.intro, Exists.intro, rfl
-- Module: Mathlib.Algebra.Group.Subgroup.Pointwise
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hyA : y ∈ (↑A : Set G)
hyB : y ∈ (↑B : Set G)
z : G
hz : z ∈ (↑C : Set G)
⊢ ∃ x ∈ (↑B : Set G), ∃ y_1 ∈ (↑C : Set G), x * y_1 = y * z

Tactic:
exact ⟨y, hyB, z, hz, rfl⟩