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
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)
⊢ x ∈ (↑H : Set G) * (↑N : Set G)
have inv_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
-- 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)
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)
⊢ x ∈ (↑H : Set G) * (↑N : Set G)
have 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)
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
N H : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
⊢ (↑(N ⊔ H) : Set G) = (↑N : Set G) * (↑H : Set G)
have rw : (↑(N ⊔ H) : Set G) = (↑H : Set G) * (↑N : Set G)
Tactic: rw [← set_mul_normalizer_comm _ _ hLE, sup_comm, coe_mul_of_left_le_normalizer_right _ _ hLE]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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)
⊢ (↑(N ⊔ H) : Set G) = (↑N : Set G) * (↑H : Set G)
have rw₁ : (↑(H ⊔ N) : Set G) = (↑H : Set G) * (↑N : Set G)
Tactic: rw [← set_mul_normalizer_comm _ _ hLE, sup_comm, coe_mul_of_left_le_normalizer_right _ _ hLE]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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)
⊢ (↑(N ⊔ H) : Set G) = (↑N : Set G) * (↑H : Set G)
have rw₂ : (↑H : Set G) * (↑N : Set G) = (↑H : Set G) * (↑N : Set G)
Tactic: rw [← set_mul_normalizer_comm _ _ hLE, sup_comm, coe_mul_of_left_le_normalizer_right _ _ hLE]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : A ≤ C
⊢ (↑A : Set G) * (↑(B ⊓ C) : Set G) = (↑A : Set G) * (↑B : Set G) ∩ (↑C : Set G)
have h₁ : ∀ (x : G), x ∈ (↑A : Set G) * (↑(B ⊓ C) : Set G) ↔ x ∈ (↑A : Set G) * (↑B : Set G) ∩ (↑C : Set G)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : A ≤ C
x : 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 ∈ (↑B : Set G), x_1 * y = x) ∧ x ∈ (↑C : Set G)
have 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)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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)
⊢ (∃ 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)
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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)
have h₁ : ∃ x ∈ (↑A : Set G), ∃ y_1 ∈ (↑B : Set G), x * y_1 = y * z
Tactic: refine ⟨?_, mul_mem (h hy) hzC⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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
have h₁ : z ∈ (↑C : Set G)
Tactic: refine ⟨y, hy, z, ⟨hz, ?_⟩, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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)
⊢ z ∈ (↑C : Set G)
have h₁ : y⁻¹ * (y * z) ∈ C
Tactic: suffices y⁻¹ * (y * z) ∈ C by simpa
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : C ≤ A
⊢ (↑(A ⊓ B) : Set G) * (↑C : Set G) = (↑A : Set G) ∩ ((↑B : Set G) * (↑C : Set G))
have h₁ : ∀ (x : G), x ∈ (↑(A ⊓ B) : Set G) * (↑C : Set G) ↔ x ∈ (↑A : Set G) ∩ ((↑B : Set G) * (↑C : Set G))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : C ≤ A
x : G
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
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
have h₁ : ∃ x ∈ (↑B : Set G), ∃ y_1 ∈ (↑C : Set G), x * y_1 = y * z
Tactic: refine ⟨A.mul_mem hyA (h hz), ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hy : y ∈ (↑B : Set G)
z : G
hz : z ∈ (↑C : Set G)
hyz : y * z ∈ (↑A : Set G)
⊢ ∃ (x : G), (x ∈ (↑A : Set G) ∧ x ∈ (↑B : Set G)) ∧ ∃ y_1 ∈ (↑C : Set G), x * y_1 = y * z
have h₁ : y ∈ (↑A : Set G)
Tactic: refine ⟨y, ⟨?_, hy⟩, z, hz, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
A B C : Subgroup G
h : C ≤ A
y : G
hy : y ∈ (↑B : Set G)
z : G
hz : z ∈ (↑C : Set G)
hyz : y * z ∈ (↑A : Set G)
⊢ y ∈ (↑A : Set G)
have h₁ : y * z * z⁻¹ ∈ A
Tactic: suffices y * z * z⁻¹ ∈ A by simpa
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (hypothesis)
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s : G
hs : Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G) ⊓ normalizer (↑K : Set G)) s
g : G
hg : g ∈ H ⊔ K
⊢ s * g * s⁻¹ ∈ H ⊔ K
have hs₁ : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
Tactic: simp only [mem_inf, mem_normalizer_iff] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (hypothesis)
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : g ∈ H ⊔ K
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
⊢ s * g * s⁻¹ ∈ H ⊔ K
have hg₁ : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
Tactic: rw [sup_eq_closure] at hg
Cleared hypotheses: hg, hs
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
⊢ s * g * s⁻¹ ∈ H ⊔ K
have refine_1 : ∀ (x : G) (hx : x ∈ (↑H : Set G) ∪ (↑K : Set G)), s * x * s⁻¹ ∈ H ⊔ K
Tactic: refine closure_induction ?_ ?_ ?_ ?_ hg
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
refine_1 : ∀ (x : G) (hx : x ∈ (↑H : Set G) ∪ (↑K : Set G)), s * x * s⁻¹ ∈ H ⊔ K
⊢ s * g * s⁻¹ ∈ H ⊔ K
have refine_2 : s * 1 * s⁻¹ ∈ H ⊔ K
Tactic: refine closure_induction ?_ ?_ ?_ ?_ hg
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
refine_1 : ∀ (x : G) (hx : x ∈ (↑H : Set G) ∪ (↑K : Set G)), s * x * s⁻¹ ∈ H ⊔ K
refine_2 : s * 1 * s⁻¹ ∈ H ⊔ K
⊢ s * g * s⁻¹ ∈ H ⊔ K
have refine_3 : ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) x)
  (hy : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) y),
  s * x * s⁻¹ ∈ H ⊔ K → s * y * s⁻¹ ∈ H ⊔ K → s * (x * y) * s⁻¹ ∈ H ⊔ K
Tactic: refine closure_induction ?_ ?_ ?_ ?_ hg
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
refine_1 : ∀ (x : G) (hx : x ∈ (↑H : Set G) ∪ (↑K : Set G)), s * x * s⁻¹ ∈ H ⊔ K
refine_2 : s * 1 * s⁻¹ ∈ H ⊔ K
refine_3 :
  ∀ (x y : G) (hx : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) x)
    (hy : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) y),
    s * x * s⁻¹ ∈ H ⊔ K → s * y * s⁻¹ ∈ H ⊔ K → s * (x * y) * s⁻¹ ∈ H ⊔ K
⊢ s * g * s⁻¹ ∈ H ⊔ K
have refine_4 : ∀ (x : G) (hx : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) x),
  s * x * s⁻¹ ∈ H ⊔ K → s * x⁻¹ * s⁻¹ ∈ H ⊔ K
Tactic: refine closure_induction ?_ ?_ ?_ ?_ hg
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
x : G
hx : x ∈ (↑H : Set G) ∪ (↑K : Set G)
⊢ s * x * s⁻¹ ∈ H ⊔ K
have refine_1 : ∀ (hl : x ∈ (↑H : Set G)), s * x * s⁻¹ ∈ H ⊔ K
Tactic: obtain hl | hr := (mem_union x _ _).mpr hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
x : G
hx : x ∈ (↑H : Set G) ∪ (↑K : Set G)
refine_1 : ∀ (hl : x ∈ (↑H : Set G)), s * x * s⁻¹ ∈ H ⊔ K
⊢ s * x * s⁻¹ ∈ H ⊔ K
have refine_1₁ : ∀ (hr : x ∈ (↑K : Set G)), s * x * s⁻¹ ∈ H ⊔ K
Tactic: obtain hl | hr := (mem_union x _ _).mpr hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
x : G
hx : x ∈ (↑H : Set G) ∪ (↑K : Set G)
hl : x ∈ (↑H : Set G)
⊢ s * x * s⁻¹ ∈ H
have rwa : x ∈ H
Tactic: rwa [← hs.1]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
x : G
hx : x ∈ (↑H : Set G) ∪ (↑K : Set G)
hr : x ∈ (↑K : Set G)
⊢ s * x * s⁻¹ ∈ K
have rwa : x ∈ K
Tactic: rwa [← hs.2]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s g : G
hg : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) g
hs : (∀ (h : G), h ∈ H ↔ s * h * s⁻¹ ∈ H) ∧ ∀ (h : G), h ∈ K ↔ s * h * s⁻¹ ∈ K
x y : G
hx : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) x
hy : Membership.mem (γ := Subgroup G) (closure ((↑H : Set G) ∪ (↑K : Set G))) y
hsx : s * x * s⁻¹ ∈ H ⊔ K
hsy : s * y * s⁻¹ ∈ H ⊔ K
⊢ s * (x * y) * s⁻¹ ∈ H ⊔ K
have refine_3 : s * x * s⁻¹ * (s * y * s⁻¹) ∈ H ⊔ K
Tactic: rw [show s * (x * y) * s⁻¹ = (s * x * s⁻¹) * (s * y * s⁻¹) by simp]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
s : G
hs : Membership.mem (γ := Subgroup G) (normalizer (↑H : Set G) ⊓ normalizer (↑K : Set G)) s
g : G
⊢ g ∈ (↑(H ⊔ K) : Set G) ↔ s * g * s⁻¹ ∈ (↑(H ⊔ K) : Set G)
have refine : s * g * s⁻¹ ∈ (↑(H ⊔ K) : Set G) → g ∈ (↑(H ⊔ K) : Set G)
Tactic: refine ⟨conj_mem_sup_of_mem_inf_normalizer_of_mem_inf hs g, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H K : Subgroup G
hHnK : LE.le (α := Subgroup G) (normalizer (↑H : Set G)) (normalizer (↑K : Set G))
⊢ LE.le (α := Subgroup G) (normalizer (↑H : Set G)) (normalizer (↑(K ⊔ H) : Set G))
have rw : LE.le (α := Subgroup G) (normalizer (↑H : Set G)) (normalizer (↑(H ⊔ K) : Set G))
Tactic: rw [sup_comm]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst : Group G
inst_1 : AddGroup A
s : Set G
H K : Subgroup G
hH : H.Normal
hK : K.Normal
n : G
hmem : n ∈ H ⊔ K
g : G
⊢ g * n * g⁻¹ ∈ H ⊔ K
have rw : ∀ (hmem : n ∈ (↑H : Set G) * (↑K : Set G)) (g : G), g * n * g⁻¹ ∈ (↑H : Set G) * (↑K : Set G)
Tactic: rw [← SetLike.mem_coe, normal_mul] at hmem ⊢
Cleared hypotheses: hmem, g
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst : Group G
inst_1 : AddGroup A
s : Set G
H K : Subgroup G
hH : H.Normal
hK : K.Normal
n : G
hmem : n ∈ (↑H : Set G) * (↑K : Set G)
g : G
⊢ g * n * g⁻¹ ∈ (↑H : Set G) * (↑K : Set G)
have rcases : ∀ (h : G) (hh : h ∈ (↑H : Set G)) (k : G) (hk : k ∈ (↑K : Set G)),
  g * (fun (x1 x2 : G) ↦ x1 * x2) h k * g⁻¹ ∈ (↑H : Set G) * (↑K : Set G)
Tactic: rcases hmem with ⟨h, hh, k, hk, rfl⟩
Cleared hypotheses: n, hmem
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
α : Type u_1
G : Type u_2
A : Type u_3
S : Type u_4
inst : Group G
inst_1 : AddGroup A
s : Set G
H K : Subgroup G
hH : H.Normal
hK : K.Normal
g h : G
hh : h ∈ (↑H : Set G)
k : G
hk : k ∈ (↑K : Set G)
⊢ g * (fun (x1 x2 : G) ↦ x1 * x2) h k * g⁻¹ ∈ (↑H : Set G) * (↑K : Set G)
have refine : (fun (x1 x2 : G) ↦ x1 * x2) (g * h * g⁻¹) (g * k * g⁻¹) = g * (fun (x1 x2 : G) ↦ x1 * x2) h k * g⁻¹
Tactic: refine ⟨g * h * g⁻¹, hH.conj_mem h hh g, g * k * g⁻¹, hK.conj_mem k hk g, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
X : Type u_5
inst_1 : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g x_1 y : G
hx_1 : Membership.mem (γ := Subgroup G) (closure s) x_1
hy : Membership.mem (γ := Subgroup G) (closure s) y
h₁ : ∀ {x : X} (hx : x ∈ t), x_1 • x ∈ t
h₂ : ∀ {x : X} (hx : x ∈ t), y • x ∈ t
x : X
hx : x ∈ t
⊢ (x_1 * y) • x ∈ t
have mul : x_1 • y • x ∈ t
Tactic: rw [mul_smul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
X : Type u_5
inst_1 : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g : G
hg : Membership.mem (γ := Subgroup G) (closure s) g
x : X
hx : x ∈ t
⊢ g • x ∈ t
have one : ∀ {x : X} (hx : x ∈ t), HSMul.hSMul.{u_2, u_5, u_5} (α := G) 1 x ∈ t
Tactic: induction hg using Subgroup.closure_induction'' generalizing x with
  | one => simpa
  | mem g' hg' => exact hst g' hg' x hx
  | inv_mem g' hg' => exact hst g'⁻¹ (hs g' hg') x hx
  | mul _ _ _ _ h₁ h₂ => rw [mul_smul]; exact h₁ (h₂ hx)
Cleared hypotheses: hg, x, hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
X : Type u_5
inst_1 : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g : G
hg : Membership.mem (γ := Subgroup G) (closure s) g
x : X
hx : x ∈ t
one : ∀ {x : X} (hx : x ∈ t), HSMul.hSMul.{u_2, u_5, u_5} (α := G) 1 x ∈ t
mem : ∀ (g' : G) (hg' : g' ∈ s) {x : X} (hx : x ∈ t), g' • x ∈ t
⊢ g • x ∈ t
have inv_mem : ∀ (g' : G) (hg' : g' ∈ s) {x : X} (hx : x ∈ t), g'⁻¹ • x ∈ t
Tactic: induction hg using Subgroup.closure_induction'' generalizing x with
  | one => simpa
  | mem g' hg' => exact hst g' hg' x hx
  | inv_mem g' hg' => exact hst g'⁻¹ (hs g' hg') x hx
  | mul _ _ _ _ h₁ h₂ => rw [mul_smul]; exact h₁ (h₂ hx)
Cleared hypotheses: hg, x, hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
X : Type u_5
inst_1 : MulAction G X
s : Set G
t : Set X
hs : ∀ g ∈ s, g⁻¹ ∈ s
hst : ∀ g ∈ s, ∀ x ∈ t, g • x ∈ t
g : G
hg : Membership.mem (γ := Subgroup G) (closure s) g
x : X
hx : x ∈ t
one : ∀ {x : X} (hx : x ∈ t), HSMul.hSMul.{u_2, u_5, u_5} (α := G) 1 x ∈ t
mem : ∀ (g' : G) (hg' : g' ∈ s) {x : X} (hx : x ∈ t), g' • x ∈ t
inv_mem : ∀ (g' : G) (hg' : g' ∈ s) {x : X} (hx : x ∈ t), g'⁻¹ • x ∈ t
⊢ g • x ∈ t
have mul : ∀ (x y : G),
  Membership.mem (γ := Subgroup G) (closure s) x →
    Membership.mem (γ := Subgroup G) (closure s) y →
      ∀ (h₁ : ∀ {x_1 : X} (hx : x_1 ∈ t), x • x_1 ∈ t) (h₂ : ∀ {x : X} (hx : x ∈ t), y • x ∈ t) {x_1 : X}
        (hx : x_1 ∈ t), (x * y) • x_1 ∈ t
Tactic: induction hg using Subgroup.closure_induction'' generalizing x with
  | one => simpa
  | mem g' hg' => exact hst g' hg' x hx
  | inv_mem g' hg' => exact hst g'⁻¹ (hs g' hg') x hx
  | mul _ _ _ _ h₁ h₂ => rw [mul_smul]; exact h₁ (h₂ hx)
Cleared hypotheses: hg, x, hx
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) h : MulAut G) H = H
have refine_1 : HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) h : MulAut G) H ≤ H
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
refine_1 : HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) h : MulAut G) H ≤ H
⊢ HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) h : MulAut G) H = H
have refine_2 : H ≤ HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) h : MulAut G) H
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : G
hh : h ∈ H
⊢ H ≤ HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) h : MulAut G) H
have refine_2 : HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) h⁻¹ : MulAut G) H ≤ H
Tactic: rw [subset_pointwise_smul_iff, ← map_inv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
⊢ HSMul.hSMul (α := MulAut ↥H) ((MulAut.conj : (a : ↥H) → MulAut ↥H) h : MulAut ↥H) (P.subgroupOf H) =
    (HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) (↑h : G) : MulAut G) P).subgroupOf H
have refine_1 : HSMul.hSMul (α := MulAut ↥H) ((MulAut.conj : (a : ↥H) → MulAut ↥H) h : MulAut ↥H) (P.subgroupOf H) ≤
  (HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) (↑h : G) : MulAut G) P).subgroupOf H
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
P H : Subgroup G
hP : P ≤ H
h : ↥H
refine_1 :
  HSMul.hSMul (α := MulAut ↥H) ((MulAut.conj : (a : ↥H) → MulAut ↥H) h : MulAut ↥H) (P.subgroupOf H) ≤
    (HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) (↑h : G) : MulAut G) P).subgroupOf H
⊢ HSMul.hSMul (α := MulAut ↥H) ((MulAut.conj : (a : ↥H) → MulAut ↥H) h : MulAut ↥H) (P.subgroupOf H) =
    (HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) (↑h : G) : MulAut G) P).subgroupOf H
have refine_2 : (HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) (↑h : G) : MulAut G) P).subgroupOf H ≤
  HSMul.hSMul (α := MulAut ↥H) ((MulAut.conj : (a : ↥H) → MulAut ↥H) h : MulAut ↥H) (P.subgroupOf H)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
h : ∀ (g : G), HSMul.hSMul (α := MulAut G) ((MulAut.conj : (a : G) → MulAut G) g : MulAut G) H = H
⊢ H.Normal
have conj_mem : ∀ n ∈ H, ∀ (g : G), g * n * g⁻¹ ∈ H
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
⊢ H.normalCore = ⨅ (g : ConjAct G), g • H
have h : ∀ (g : G), g ∈ H.normalCore ↔ Membership.mem (γ := Subgroup G) (⨅ (g : ConjAct G), g • H) g
Tactic: ext g
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Pointwise (goal)
Goal:
G : Type u_2
inst : Group G
H : Subgroup G
g : G
⊢ g ∈ H.normalCore ↔ Membership.mem (γ := Subgroup G) (⨅ (g : ConjAct G), g • H) g
have h : g ∈ { carrier := {a : G | ∀ (b : G), b * a * b⁻¹ ∈ H}, mul_mem' := sorry, one_mem' := sorry, inv_mem' := sorry : Subgroup G } ↔
  ∀ (i : ConjAct G), i⁻¹ • g ∈ H
Tactic: simp only [Subgroup.normalCore, Subgroup.mem_iInf, Subgroup.mem_pointwise_smul_iff_inv_smul_mem]