awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Subgroup G) (closure s) y), p y hy → p (x * y) ⋯
inv_mul_cancel :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Subgroup G) (closure s) y), p y hy → p (x⁻¹ * y) ⋯
x : G
h : Membership.mem (γ := Subgroup G) (closure s) x
⊢ p x h
have revert : ∀ (h : Membership.mem (γ := Subgroup G) (closure s) x), p x h
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
mul_left : ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Subgroup G) (closure s) y), p y hy → p (x * y) ⋯
inv_mul_cancel :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Subgroup G) (closure s) y), p y hy → p (x⁻¹ * y) ⋯
x : G
⊢ ∀ (h : Membership.mem (γ := Subgroup G) (closure s) x), p x h
have simp_rw : ∀
  (mul_left :
    ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
      p y sorry → p (x * y) sorry)
  (inv_mul_cancel :
    ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
      p y sorry → p (x⁻¹ * y) sorry)
  (h : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) x), p x sorry
Tactic: simp_rw [← mem_toSubmonoid, closure_toSubmonoid] at *
Cleared hypotheses: mul_left, inv_mul_cancel
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
x_1 : G
mul_left :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x * y) ⋯
inv_mul_cancel :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x⁻¹ * y) ⋯
x : G
hx : x ∈ s ∪ s⁻¹
y : G
hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y
ih : p y ⋯
⊢ p (x * y) ⋯
have mul_left₁ : ∀ (hx : x ∈ s), p (x * y) sorry
Tactic: cases hx with
    | inl hx => exact mul_left _ hx _ hy ih
    | inr hx => simpa only [inv_inv] using inv_mul_cancel _ hx _ hy ih
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
x_1 : G
mul_left :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x * y) ⋯
inv_mul_cancel :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x⁻¹ * y) ⋯
x : G
hx : x ∈ s ∪ s⁻¹
y : G
hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y
ih : p y ⋯
mul_left₁ : ∀ (hx : x ∈ s), p (x * y) ⋯
⊢ p (x * y) ⋯
have mul_left₂ : ∀ (hx : x ∈ s⁻¹), p (x * y) sorry
Tactic: cases hx with
    | inl hx => exact mul_left _ hx _ hy ih
    | inr hx => simpa only [inv_inv] using inv_mul_cancel _ hx _ hy ih
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
x : G
mul_left :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x * y) ⋯
inv_mul_cancel :
  ∀ (x : G) (hx : x ∈ s) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y),
    p y ⋯ → p (x⁻¹ * y) ⋯
h : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) x
one₁ : p 1 ⋯
⊢ p x ⋯
have mul_left₁ : ∀ (x : G) (hx : x ∈ s ∪ s⁻¹) (y : G) (hy : Membership.mem (γ := Submonoid G) (Submonoid.closure (s ∪ s⁻¹)) y)
  (ih : p y sorry), p (x * y) sorry
Tactic: induction h using Submonoid.closure_induction_left with
  | one => exact one
  | mul_left x hx y hy ih =>
    cases hx with
    | inl hx => exact mul_left _ hx _ hy ih
    | inr hx => simpa only [inv_inv] using inv_mul_cancel _ hx _ hy ih
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
mul_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure s) x) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯
mul_inv_cancel :
  ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure s) x) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯
x : G
h : Membership.mem (γ := Subgroup G) (closure s) x
m : Gᵐᵒᵖ
hm : Membership.mem (γ := Subgroup Gᵐᵒᵖ) (closure (MulOpposite.unop ⁻¹' s)) m
⊢ Membership.mem (γ := Subgroup G) (closure s) (MulOpposite.unop m)
have rwa : ∀ (hm : Membership.mem (γ := Subgroup Gᵐᵒᵖ) (Subgroup.op (closure s)) m),
  Membership.mem (γ := Subgroup G) (closure s) (MulOpposite.unop m)
Tactic: rwa [← op_closure] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
p : (x : G) → Membership.mem (γ := Subgroup G) (closure s) x → Prop
one : p 1 ⋯
mul_right : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure s) x) (y : G) (hy : y ∈ s), p x hx → p (x * y) ⋯
mul_inv_cancel :
  ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure s) x) (y : G) (hy : y ∈ s), p x hx → p (x * y⁻¹) ⋯
x : G
h : Membership.mem (γ := Subgroup G) (closure s) x
⊢ Membership.mem (γ := Subgroup Gᵐᵒᵖ) (closure (MulOpposite.unop ⁻¹' s)) { unop' := x : PreOpposite G }
have rwa : Membership.mem (γ := Subgroup Gᵐᵒᵖ) (Subgroup.op (closure s)) { unop' := x : PreOpposite G }
Tactic: rwa [← op_closure]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
x : G
⊢ Eq (α := Subgroup G) (closure {x⁻¹}) (closure {x})
have rw : Eq (α := Subgroup G) (closure {x}⁻¹) (closure {x})
Tactic: rw [← Set.inv_singleton, closure_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
x : G
rw : Eq (α := Subgroup G) (closure {x}⁻¹) (closure {x})
⊢ Eq (α := Subgroup G) (closure {x⁻¹}) (closure {x})
have rw₁ : Eq (α := Subgroup G) (closure {x}) (closure {x})
Tactic: rw [← Set.inv_singleton, closure_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (hypothesis)
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
⊢ C x
have hx₁ : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), (↑(S i) : Set G))) x
Tactic: rw [iSup_eq_closure] at hx
Cleared hypotheses: hx, mem, one, mul
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x_1 : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : Membership.mem (γ := Set G) (⋃ (i : ι), (↑(S i) : Set G)) x
⊢ C x
have mem₁ : ∀ (i : ι) (hi : x ∈ (↑(S i) : Set G)), C x
Tactic: obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x_1 : G
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
x : G
hx : Membership.mem (γ := Set G) (⋃ (i : ι), (↑(S i) : Set G)) x
⊢ C x⁻¹
have inv_mem : ∀ (i : ι) (hi : x ∈ (↑(S i) : Set G)), C x⁻¹
Tactic: obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), (↑(S i) : Set G))) x
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
one₁ : C 1
⊢ C x
have mem₁ : ∀ (x : G) (hx : Membership.mem (γ := Set G) (⋃ (i : ι), (↑(S i) : Set G)) x), C x
Tactic: induction hx using closure_induction'' with
  | one => exact one
  | mem x hx =>
    obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
    exact mem _ _ hi
  | inv_mem x hx =>
    obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
    exact mem _ _ (inv_mem hi)
  | mul x y _ _ ihx ihy => exact mul x y ihx ihy
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), (↑(S i) : Set G))) x
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
one₁ : C 1
mem₁ : ∀ (x : G) (hx : Membership.mem (γ := Set G) (⋃ (i : ι), (↑(S i) : Set G)) x), C x
⊢ C x
have inv_mem : ∀ (x : G) (hx : Membership.mem (γ := Set G) (⋃ (i : ι), (↑(S i) : Set G)) x), C x⁻¹
Tactic: induction hx using closure_induction'' with
  | one => exact one
  | mem x hx =>
    obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
    exact mem _ _ hi
  | inv_mem x hx =>
    obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
    exact mem _ _ (inv_mem hi)
  | mul x y _ _ ihx ihy => exact mul x y ihx ihy
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
ι : Sort u_5
S : ι → Subgroup G
C : G → Prop
x : G
hx : Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), (↑(S i) : Set G))) x
mem : ∀ (i : ι), ∀ x ∈ S i, C x
one : C 1
mul : ∀ (x y : G), C x → C y → C (x * y)
one₁ : C 1
mem₁ : ∀ (x : G) (hx : Membership.mem (γ := Set G) (⋃ (i : ι), (↑(S i) : Set G)) x), C x
inv_mem : ∀ (x : G) (hx : Membership.mem (γ := Set G) (⋃ (i : ι), (↑(S i) : Set G)) x), C x⁻¹
⊢ C x
have mul₁ : ∀ (x y : G),
  Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), (↑(S i) : Set G))) x →
    Membership.mem (γ := Subgroup G) (closure (⋃ (i : ι), (↑(S i) : Set G))) y → ∀ (ihx : C x) (ihy : C y), C (x * y)
Tactic: induction hx using closure_induction'' with
  | one => exact one
  | mem x hx =>
    obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
    exact mem _ _ hi
  | inv_mem x hx =>
    obtain ⟨i, hi⟩ := Set.mem_iUnion.mp hx
    exact mem _ _ (inv_mem hi)
  | mul x y _ _ ihx ihy => exact mul x y ihx ihy
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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 : G
hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x
⊢ C x hx
have suffices : ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h
Tactic: suffices ∃ h, C x h from this.snd
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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 : G
hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x
⊢ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h
have refine_1 : ∀ (i : ι) (x : G) (hx : x ∈ S i), (fun (x : G) ↦ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h) x
Tactic: refine iSup_induction S (C := fun x => ∃ h, C x h) hx (fun i x hx => ?_) ?_ fun x y => ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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 : G
hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x
refine_1 :
  ∀ (i : ι) (x : G) (hx : x ∈ S i), (fun (x : G) ↦ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h) x
⊢ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h
have refine_2 : (fun (x : G) ↦ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h) 1
Tactic: refine iSup_induction S (C := fun x => ∃ h, C x h) hx (fun i x hx => ?_) ?_ fun x y => ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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 : G
hx : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x
refine_1 :
  ∀ (i : ι) (x : G) (hx : x ∈ S i), (fun (x : G) ↦ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h) x
refine_2 : ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) 1), C 1 h
⊢ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h
have refine_3 : ∀ (x y : G),
  (fun (x : G) ↦ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h) x →
    (fun (x : G) ↦ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h) y →
      (fun (x : G) ↦ ∃ (h : Membership.mem (γ := Subgroup G) (⨆ (i : ι), S i) x), C x h) (x * y)
Tactic: refine iSup_induction S (C := fun x => ∃ h, C x h) hx (fun i x hx => ?_) ?_ fun x y => ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
H : Subgroup G
n : ℕ
hs : s ⊆ (↑H : Set G)
⊢ s ^ n ⊆ (↑H : Set G)
have zero : HPow.hPow (β := ℕ) s 0 ⊆ (↑H : Set G)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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)
⊢ s ^ n ⊆ (↑H : Set G)
have succ : ∀ (n : ℕ), s ^ n ⊆ (↑H : Set G) → s ^ (n + 1) ⊆ (↑H : Set G)
Tactic: induction n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
m n : ℕ
hmn : m ∣ n
⊢ LE.le (α := Subgroup G) (closure (s ^ n)) (closure (s ^ m))
have obtain : ∀ (k : ℕ), LE.le (α := Subgroup G) (closure (s ^ (m * k))) (closure (s ^ m))
Tactic: obtain ⟨k, rfl⟩ := hmn
Cleared hypotheses: n, hmn
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
s : Set G
n : ℕ
hs : 1 ∈ s
hn : n ≠ 0
⊢ LE.le (α := Subgroup G) (closure s) (closure (s ^ n))
have grw : LE.le (α := Subgroup G) (closure s) (closure s)
Tactic: grw [← subset_pow hs hn]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
⊢ closure (↑H : Set G) ⊔ closure (↑K : Set G) ≤ H ⊔ K
have rw : H ⊔ closure (↑K : Set G) ≤ H ⊔ K
Tactic: rw [closure_eq, closure_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
rw : H ⊔ closure (↑K : Set G) ≤ H ⊔ K
⊢ closure (↑H : Set G) ⊔ closure (↑K : Set G) ≤ H ⊔ K
have rw₁ : H ⊔ K ≤ H ⊔ K
Tactic: rw [closure_eq, closure_eq]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ (↑(normalizer (↑N : Set G)) : Set G)
⊢ S * (↑N : Set G) = (↑N : Set G) * S
have 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))
Tactic: rw [← iUnion_mul_left_image, ← iUnion_mul_right_image]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ (↑(normalizer (↑N : Set G)) : 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))
have 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)})
Tactic: simp only [image_mul_left, image_mul_right, Set.preimage]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
S : Set G
N : Subgroup G
hLE : S ⊆ (↑(normalizer (↑N : Set G)) : 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)})
have h : ∀ (s : G) (hs : s ∈ S) (x : G), s⁻¹ * x ∈ (↑N : Set G) ↔ x * s⁻¹ ∈ (↑N : Set G)
Tactic: congr! 5 with s hs x
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
⊢ (↑(H ⊔ N) : Set G) = (↑H : Set G) * (↑N : Set G)
have rw : (↑(closure ((↑H : Set G) * (↑N : Set G))) : Set G) = (↑H : Set G) * (↑N : Set G)
Tactic: rw [sup_eq_closure_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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)
have refine : ∀ (x : G) (hx : x ∈ (↑(closure ((↑H : Set G) * (↑N : Set G))) : Set G)), x ∈ (↑H : Set G) * (↑N : Set G)
Tactic: refine Set.Subset.antisymm (fun x hx => ?_) subset_closure
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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)
⊢ x⁻¹ ∈ (↑H : Set G) * (↑N : Set G)
have 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)
Tactic: obtain ⟨x, hx, y, hy, rfl⟩ := hx
Cleared hypotheses: x, hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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)
⊢ x'_1 * x' ∈ (↑H : Set G) * (↑N : Set G)
have 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)
Tactic: obtain ⟨x, hx, y, hy, rfl⟩ := hx
Cleared hypotheses: x'_1, hx_1, hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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)
⊢ (fun (x1 x2 : G) ↦ x1 * x2) x y * x' ∈ (↑H : Set G) * (↑N : Set G)
have 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)
Tactic: obtain ⟨x', hx', y', hy', rfl⟩ := hx'
Cleared hypotheses: x', hy_1, hx'
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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)
have mul : x'⁻¹ * y * x' ∈ N
Tactic: refine ⟨x * x', mul_mem hx hx', x'⁻¹ * y * x' * y', mul_mem ?_ hy', ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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
⊢ 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)
have 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')
Tactic: refine ⟨x * x', mul_mem hx hx', x'⁻¹ * y * x' * y', mul_mem ?_ hy', ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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)
⊢ x ∈ (↑H : Set G) * (↑N : Set G)
have one : 1 ∈ (↑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]
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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)
⊢ x ∈ (↑H : Set G) * (↑N : Set G)
have mem : ∀ (x : G) (hx : x ∈ (↑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]
Cleared hypotheses: hx