awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
f : G ≃* N
⊢ map f.toMonoidHom (normalizer (↑H : Set G)) = normalizer (↑(map f.toMonoidHom H) : Set N)
have h : ∀ (x : N),
  x ∈ map f.toMonoidHom (normalizer (↑H : Set G)) ↔
    Membership.mem (γ := Subgroup N) (normalizer (↑(map f.toMonoidHom H) : Set N)) x
Tactic: ext x
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
f : G ≃* N
x : N
⊢ x ∈ map f.toMonoidHom (normalizer (↑H : Set G)) ↔
    Membership.mem (γ := Subgroup N) (normalizer (↑(map f.toMonoidHom H) : Set N)) x
have h : (∀ (h : G),
    h ∈ H ↔
      HMul.hMul (β := G) (HMul.hMul (α := G) ((f.symm : (a : N) → G) x : G) h) (((f.symm : (a : N) → G) x)⁻¹ : G) ∈ H) ↔
  ∀ (h : N),
    Membership.mem (α := G) H ((f.symm : (a : N) → G) h : G) ↔
      Membership.mem (α := G) H ((f.symm : (a : N) → G) (x * h * x⁻¹) : G)
Tactic: simp only [mem_normalizer_iff, mem_map_equiv]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
H : Subgroup G
f : G ≃* N
x : N
⊢ (∀ (h : G),
      h ∈ H ↔
        HMul.hMul (β := G) (HMul.hMul (α := G) ((f.symm : (a : N) → G) x : G) h) (((f.symm : (a : N) → G) x)⁻¹ : G) ∈
          H) ↔
    ∀ (h : N),
      Membership.mem (α := G) H ((f.symm : (a : N) → G) h : G) ↔
        Membership.mem (α := G) H ((f.symm : (a : N) → G) (x * h * x⁻¹) : G)
have h : ∀ (a : G),
  (a ∈ H ↔
      HMul.hMul (β := G) (HMul.hMul (α := G) ((f.symm : (a : N) → G) x : G) a) (((f.symm : (a : N) → G) x)⁻¹ : G) ∈ H) ↔
    (Membership.mem (α := G) H ((f.symm : (a : N) → G) ((f.toEquiv : (a : G) → N) a : N) : G) ↔
      Membership.mem (α := G) H
        ((f.symm : (a : N) → G) (HMul.hMul (β := N) x ((f.toEquiv : (a : G) → N) a : N) * x⁻¹) : G))
Tactic: rw [f.toEquiv.forall_congr]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst_4 : Group G₁
inst_5 : Group G₂
inst_6 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ (g : (a : G₁) → G₃) (f_inv (x * y)) =
    HMul.hMul (α := G₃) (β := G₃) ((g : (a : G₁) → G₃) (f_inv x) : G₃) ((g : (a : G₁) → G₃) (f_inv y) : G₃)
have rw : f_inv (x * y) * (f_inv x * f_inv y)⁻¹ ∈ g.ker
Tactic: rw [← g.map_mul, ← mul_inv_eq_one, ← g.map_inv, ← g.map_mul, ← g.mem_ker]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst_4 : Group G₁
inst_5 : Group G₂
inst_6 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ f_inv (x * y) * (f_inv x * f_inv y)⁻¹ ∈ g.ker
have a : f_inv (x * y) * (f_inv x * f_inv y)⁻¹ ∈ f.ker
Tactic: apply hg
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst_4 : Group G₁
inst_5 : Group G₂
inst_6 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x y : G₂
⊢ f_inv (x * y) * (f_inv x * f_inv y)⁻¹ ∈ f.ker
have a : (f : (a : G₁) → G₂) (f_inv (x * y)) =
  HMul.hMul (α := G₂) (β := G₂) ((f : (a : G₁) → G₂) (f_inv x) : G₂) ((f : (a : G₁) → G₂) (f_inv y) : G₂)
Tactic: rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one, f.map_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst : Group G₁
inst_1 : Group G₂
inst_2 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ Eq.{u_7 + 1} (α := G₃) ((f.liftOfRightInverseAux f_inv hf g hg : (a : G₂) → G₃) ((f : (a : G₁) → G₂) x : G₂) : G₃)
    ((g : (a : G₁) → G₃) x : G₃)
have dsimp : Eq.{u_7 + 1} (α := G₃) ((g : (a : G₁) → G₃) (f_inv ((f : (a : G₁) → G₂) x)) : G₃) ((g : (a : G₁) → G₃) x : G₃)
Tactic: dsimp [liftOfRightInverseAux]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst : Group G₁
inst_1 : Group G₂
inst_2 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ Eq.{u_7 + 1} (α := G₃) ((g : (a : G₁) → G₃) (f_inv ((f : (a : G₁) → G₂) x)) : G₃) ((g : (a : G₁) → G₃) x : G₃)
have rw : f_inv ((f : (a : G₁) → G₂) x) * x⁻¹ ∈ g.ker
Tactic: rw [← mul_inv_eq_one, ← g.map_inv, ← g.map_mul, ← g.mem_ker]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst : Group G₁
inst_1 : Group G₂
inst_2 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f_inv ((f : (a : G₁) → G₂) x) * x⁻¹ ∈ g.ker
have a : f_inv ((f : (a : G₁) → G₂) x) * x⁻¹ ∈ f.ker
Tactic: apply hg
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst : Group G₁
inst_1 : Group G₂
inst_2 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
x : G₁
⊢ f_inv ((f : (a : G₁) → G₂) x) * x⁻¹ ∈ f.ker
have a : Eq.{u_6 + 1} (α := G₂) ((f : (a : G₁) → G₂) (f_inv ((f : (a : G₁) → G₂) x)) : G₂) ((f : (a : G₁) → G₂) x : G₂)
Tactic: rw [f.mem_ker, f.map_mul, f.map_inv, mul_inv_eq_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst_4 : Group G₁
inst_5 : Group G₂
inst_6 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : { g : G₁ →* G₃ // f.ker ≤ g.ker }
⊢ (fun (φ : G₂ →* G₃) ↦
        (Subtype.mk (p := fun (g : G₁ →* G₃) ↦ f.ker ≤ g.ker) (φ.comp f) ⋯ : { g : G₁ →* G₃ // f.ker ≤ g.ker }))
      ((fun (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) ↦ f.liftOfRightInverseAux f_inv hf (↑g : G₁ →* G₃) ⋯) g) =
    g
have a : ∀ (x : G₁),
  Eq.{u_7 + 1} (α := G₃)
    (((↑((fun (φ : G₂ →* G₃) ↦
                  (Subtype.mk (p := fun (g : G₁ →* G₃) ↦ f.ker ≤ g.ker) (φ.comp f) sorry :
                    { g : G₁ →* G₃ // f.ker ≤ g.ker }))
                ((fun (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) ↦ f.liftOfRightInverseAux f_inv hf (↑g : G₁ →* G₃) sorry)
                  g)) :
            G₁ →* G₃) :
          (a : G₁) → G₃)
        x :
      G₃)
    (((↑g : G₁ →* G₃) : (a : G₁) → G₃) x : G₃)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
G'' : Type u_3
inst : Group G
inst_1 : Group G'
inst_2 : Group G''
A : Type u_4
inst_3 : AddGroup A
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst_4 : Group G₁
inst_5 : Group G₂
inst_6 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
φ : G₂ →* G₃
⊢ (fun (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) ↦ f.liftOfRightInverseAux f_inv hf (↑g : G₁ →* G₃) ⋯)
      ((fun (φ : G₂ →* G₃) ↦
          (Subtype.mk (p := fun (g : G₁ →* G₃) ↦ f.ker ≤ g.ker) (φ.comp f) ⋯ : { g : G₁ →* G₃ // f.ker ≤ g.ker }))
        φ) =
    φ
have h : ∀ (b : G₂),
  Eq.{u_7 + 1} (α := G₃)
    (((fun (g : { g : G₁ →* G₃ // f.ker ≤ g.ker }) ↦ f.liftOfRightInverseAux f_inv hf (↑g : G₁ →* G₃) sorry)
            ((fun (φ : G₂ →* G₃) ↦
                (Subtype.mk (p := fun (g : G₁ →* G₃) ↦ f.ker ≤ g.ker) (φ.comp f) sorry : { g : G₁ →* G₃ // f.ker ≤ g.ker }))
              φ) :
          (a : G₂) → G₃)
        b :
      G₃)
    ((φ : (a : G₂) → G₃) b : G₃)
Tactic: ext b
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G₁ : Type u_5
G₂ : Type u_6
G₃ : Type u_7
inst : Group G₁
inst_1 : Group G₂
inst_2 : Group G₃
f : G₁ →* G₂
f_inv : G₂ → G₁
hf : RightInverse f_inv (⇑f : (a : G₁) → G₂)
g : G₁ →* G₃
hg : f.ker ≤ g.ker
h : G₂ →* G₃
hh : h.comp f = g
⊢ h =
    (f.liftOfRightInverse f_inv hf : (a : { g : G₁ →* G₃ // f.ker ≤ g.ker }) → G₂ →* G₃)
      (Subtype.mk (p := fun (g : G₁ →* G₃) ↦ f.ker ≤ g.ker) g hg)
have simp_rw : h =
  (f.liftOfRightInverse f_inv hf : (a : { g : G₁ →* G₃ // f.ker ≤ g.ker }) → G₂ →* G₃)
    (Subtype.mk (p := fun (g : G₁ →* G₃) ↦ f.ker ≤ g.ker) (h.comp f) sorry)
Tactic: simp_rw [← hh]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
s : Set G
f : G →* N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
⊢ map f (normalClosure s) = normalClosure ((⇑f : (a : G) → N) '' s)
have this : (map f (normalClosure s)).Normal
Tactic: have : Normal (map f (normalClosure s)) := Normal.map inferInstance f hf
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
s : Set G
f : G →* N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
this : (map f (normalClosure s)).Normal
⊢ map f (normalClosure s) = normalClosure ((⇑f : (a : G) → N) '' s)
have a : map f (normalClosure s) ≤ normalClosure ((⇑f : (a : G) → N) '' s)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
s : Set G
f : G →* N
hf : Surjective.{u_1 + 1, u_5 + 1} (α := G) (β := N) (⇑f : (a : G) → N)
this : (map f (normalClosure s)).Normal
a : map f (normalClosure s) ≤ normalClosure ((⇑f : (a : G) → N) '' s)
⊢ map f (normalClosure s) = normalClosure ((⇑f : (a : G) → N) '' s)
have a₁ : normalClosure ((⇑f : (a : G) → N) '' s) ≤ map f (normalClosure s)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
N : Type u_5
inst_1 : Group N
s : Set N
f : G ≃* N
⊢ Eq (α := Subgroup G) (normalClosure ((⇑f : (a : G) → N) ⁻¹' s)) (comap (↑f : G →* N) (normalClosure s))
have this : Eq.{u_1 + 1} (α := Set G) ((⇑f.symm : (a : N) → G) '' s) ((⇑f.toEquiv : (a : G) → N) ⁻¹' s)
Tactic: have := f.toEquiv.image_symm_eq_preimage s
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
A B' B : Subgroup G
hN : (B'.subgroupOf B).Normal
⊢ Normal (G := ↥(A ⊓ B)) ((A ⊓ B').subgroupOf (A ⊓ B))
have rw : ∀ (hN : B ≤ normalizer (↑(B' ⊓ B) : Set G)), A ⊓ B ≤ normalizer (↑(A ⊓ B' ⊓ (A ⊓ B)) : Set G)
Tactic: rw [normal_subgroupOf_iff_le_normalizer_inf] at hN ⊢
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
A B' B : Subgroup G
hN : B ≤ normalizer (↑(B' ⊓ B) : Set G)
⊢ A ⊓ B ≤ normalizer (↑(A ⊓ B' ⊓ (A ⊓ B)) : Set G)
have rw : A ⊓ B ≤ normalizer (↑(A ⊓ (B' ⊓ B)) : Set G)
Tactic: rw [inf_inf_inf_comm, inf_idem]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
A' A B : Subgroup G
hN : (A'.subgroupOf A).Normal
⊢ Normal (G := ↥(A ⊓ B)) ((A' ⊓ B).subgroupOf (A ⊓ B))
have rw : ∀ (hN : A ≤ normalizer (↑(A' ⊓ A) : Set G)), A ⊓ B ≤ normalizer (↑(A' ⊓ B ⊓ (A ⊓ B)) : Set G)
Tactic: rw [normal_subgroupOf_iff_le_normalizer_inf] at hN ⊢
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
A' A B : Subgroup G
hN : A ≤ normalizer (↑(A' ⊓ A) : Set G)
⊢ A ⊓ B ≤ normalizer (↑(A' ⊓ B ⊓ (A ⊓ B)) : Set G)
have rw : A ⊓ B ≤ normalizer (↑(A' ⊓ A ⊓ B) : Set G)
Tactic: rw [inf_inf_inf_comm, inf_idem]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
⊢ (iInf a).Normal
have conj_mem : ∀ n ∈ iInf a, ∀ (g : G), g * n * g⁻¹ ∈ iInf a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
ι : Sort u_6
a : ι → Subgroup G
norm : ∀ (i : ι), (a i).Normal
g : G
g_in_iInf : g ∈ iInf a
h : G
⊢ h * g * h⁻¹ ∈ iInf a
have conj_mem : ∀ (g_in_iInf : ∀ (i : ι), g ∈ a i) (h : G) (i : ι), h * g * h⁻¹ ∈ a i
Tactic: rw [Subgroup.mem_iInf] at g_in_iInf ⊢
Cleared hypotheses: g_in_iInf, h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hK : H ≤ K
hN : (H.subgroupOf K).Normal
a b : G
hb : b ∈ K
h : a * b ∈ H
⊢ b * a ∈ H
have this : b * (a * b) * b⁻¹ ∈ H
Tactic: have := (normal_subgroupOf_iff hK).mp hN (a * b) b h hb
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hK : H ≤ K
hN : (H.subgroupOf K).Normal
a b : G
hb : b ∈ K
h : a * b ∈ H
this : b * (a * b) * b⁻¹ ∈ H
⊢ b * a ∈ H
have rwa : ∀ (this : b * (a * b * b⁻¹) ∈ H), b * a ∈ H
Tactic: rwa [mul_assoc, mul_assoc, mul_inv_cancel, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hK : H ≤ K
hN : (H.subgroupOf K).Normal
a b : G
hb : b ∈ K
h : a * b ∈ H
this : b * (a * b) * b⁻¹ ∈ H
rwa : ∀ (this : b * (a * b * b⁻¹) ∈ H), b * a ∈ H
⊢ b * a ∈ H
have rwa₁ : ∀ (this : b * (a * (b * b⁻¹)) ∈ H), b * a ∈ H
Tactic: rwa [mul_assoc, mul_assoc, mul_inv_cancel, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hK : H ≤ K
hN : (H.subgroupOf K).Normal
a b : G
hb : b ∈ K
h : a * b ∈ H
this : b * (a * b) * b⁻¹ ∈ H
rwa : ∀ (this : b * (a * b * b⁻¹) ∈ H), b * a ∈ H
rwa₁ : ∀ (this : b * (a * (b * b⁻¹)) ∈ H), b * a ∈ H
⊢ b * a ∈ H
have rwa₂ : ∀ (this : b * (a * 1) ∈ H), b * a ∈ H
Tactic: rwa [mul_assoc, mul_assoc, mul_inv_cancel, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H K : Subgroup G
hK : H ≤ K
hN : (H.subgroupOf K).Normal
a b : G
hb : b ∈ K
h : a * b ∈ H
this : b * (a * b) * b⁻¹ ∈ H
rwa : ∀ (this : b * (a * b * b⁻¹) ∈ H), b * a ∈ H
rwa₁ : ∀ (this : b * (a * (b * b⁻¹)) ∈ H), b * a ∈ H
rwa₂ : ∀ (this : b * (a * 1) ∈ H), b * a ∈ H
⊢ b * a ∈ H
have rwa₃ : ∀ (this : b * a ∈ H), b * a ∈ H
Tactic: rwa [mul_assoc, mul_assoc, mul_inv_cancel, mul_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
this : x * y * x⁻¹ * y⁻¹ = 1
⊢ x * y = y * x
have this₁ : x * y = (x⁻¹ * y⁻¹)⁻¹
Tactic: rw [mul_assoc, mul_eq_one_iff_eq_inv] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ Commute x y
have suffices : x * y * x⁻¹ * y⁻¹ = 1
Tactic: suffices x * y * x⁻¹ * y⁻¹ = 1 by
    change x * y = y * x
    · rw [mul_assoc, mul_eq_one_iff_eq_inv] at this
      simpa
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ = 1
have a : x * y * x⁻¹ * y⁻¹ ∈ H₁ ⊓ H₂
Tactic: apply hdis.le_bot
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ H₁ ⊓ H₂
have a : x * y * x⁻¹ * y⁻¹ ∈ (↑H₁.toSubmonoid : Set G)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
a : x * y * x⁻¹ * y⁻¹ ∈ (↑H₁.toSubmonoid : Set G)
⊢ x * y * x⁻¹ * y⁻¹ ∈ H₁ ⊓ H₂
have a₁ : x * y * x⁻¹ * y⁻¹ ∈ (↑H₂.toSubmonoid : Set G)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ (↑H₁.toSubmonoid : Set G)
have a : x * (y * x⁻¹ * y⁻¹) ∈ H₁
Tactic: suffices x * (y * x⁻¹ * y⁻¹) ∈ H₁ by simpa [mul_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H₁ H₂ : Subgroup G
hH₁ : H₁.Normal
hH₂ : H₂.Normal
hdis : Disjoint H₁ H₂
x y : G
hx : x ∈ H₁
hy : y ∈ H₂
⊢ x * y * x⁻¹ * y⁻¹ ∈ H₂
have apply : x * y * x⁻¹ ∈ H₂
Tactic: apply H₂.mul_mem _ (H₂.inv_mem hy)
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
⊢ (N.subgroupOf H).Normal
have rw : H ≤ normalizer (↑(N ⊓ H) : Set G)
Tactic: rw [normal_subgroupOf_iff_le_normalizer_inf]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H N : Subgroup G
hLE : H ≤ normalizer (↑N : Set G)
⊢ Normal (G := ↥(H ⊔ N)) (N.subgroupOf (H ⊔ N))
have rw : H ⊔ N ≤ normalizer (↑N : Set G)
Tactic: rw [normal_subgroupOf_iff_le_normalizer le_sup_right]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g g' : G
hg : g ∈ N
hg' : g' ∈ N
hc : IsConj g g'
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
⊢ Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g' hg'}) ⊤
have obtain : ∀ (c : G) {hg' : c * g * c⁻¹ ∈ N} (hc : IsConj g (c * g * c⁻¹)),
  Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'}) ⊤
Tactic: obtain ⟨c, rfl⟩ := isConj_iff.1 hc
Cleared hypotheses: g', hg', hc
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
⊢ Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c * g * c⁻¹) hg'}) ⊤
have h : ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
Tactic: have h : ∀ x : N, (MulAut.conj c) x ∈ N := by
    rintro ⟨x, hx⟩
    exact hn.conj_mem _ hx c
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
x : G
hx : x ∈ N
⊢ ∃ (a : ↥N),
    (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h :
          (a : ↥N) → ↥N)
        a =
      Subtype.mk (p := fun (x : G) ↦ x ∈ N) x hx
have refine_1 : c⁻¹ * x * c ∈ N
Tactic: refine ⟨⟨c⁻¹ * x * c, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
x : G
hx : x ∈ N
refine_1 : c⁻¹ * x * c ∈ N
⊢ ∃ (a : ↥N),
    (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h :
          (a : ↥N) → ↥N)
        a =
      Subtype.mk (p := fun (x : G) ↦ x ∈ N) x hx
have refine_2 : (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h :
      (a : ↥N) → ↥N)
    (Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c⁻¹ * x * c) sorry) =
  Subtype.mk (p := fun (x : G) ↦ x ∈ N) x hx
Tactic: refine ⟨⟨c⁻¹ * x * c, ?_⟩, ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
x : G
hx : x ∈ N
⊢ c⁻¹ * x * c ∈ N
have h₁ : c⁻¹ * x * c⁻¹⁻¹ ∈ N
Tactic: have h := hn.conj_mem _ hx c⁻¹
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h_1 :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
x : G
hx : x ∈ N
h : c⁻¹ * x * c⁻¹⁻¹ ∈ N
⊢ c⁻¹ * x * c ∈ N
have refine_1 : ∀ (h : c⁻¹ * x * c ∈ N), c⁻¹ * x * c ∈ N
Tactic: rwa [inv_inv] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
x : G
hx : x ∈ N
⊢ (MonoidHom.codRestrict (MonoidHom.restrict (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) c)) N) N h :
        (a : ↥N) → ↥N)
      (Subtype.mk (p := fun (x : G) ↦ x ∈ N) (c⁻¹ * x * c) ⋯) =
    Subtype.mk (p := fun (x : G) ↦ x ∈ N) x hx
have refine_2 : x * c * c⁻¹ = x
Tactic: simp only [MonoidHom.codRestrict_apply, MulEquiv.coe_toMonoidHom, MulAut.conj_apply,
      MonoidHom.restrict_apply, Subtype.mk_eq_mk, ← mul_assoc, mul_inv_cancel, one_mul]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
x : G
hx : x ∈ N
⊢ x * c * c⁻¹ = x
have refine_2 : x * (c * c⁻¹) = x
Tactic: rw [mul_assoc, mul_inv_cancel, mul_one]
-- Lean 4 proof step from Mathlib.Algebra.Group.Subgroup.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
hn : N.Normal
g : G
hg : g ∈ N
ht : Eq (α := Subgroup ↥N) (normalClosure {Subtype.mk (p := fun (x : G) ↦ x ∈ N) g hg}) ⊤
c : G
hg' : c * g * c⁻¹ ∈ N
hc : IsConj g (c * g * c⁻¹)
h :
  ∀ (x : ↥N), Membership.mem (α := G) N ((((MulAut.conj : (a : G) → MulAut G) c : MulAut G) : (a : G) → G) (↑x : G) : G)
x : G
hx : x ∈ N
refine_2 : x * (c * c⁻¹) = x
⊢ x * c * c⁻¹ = x
have refine_2₁ : x * 1 = x
Tactic: rw [mul_assoc, mul_inv_cancel, mul_one]