awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
left :
  ∀ g₁ ∈ H₁,
    ∀ g₂ ∈ H₂,
      Membership.mem (α := G') ⁅map f H₁, map f H₂⁆
        (Bracket.bracket (L := G') ((f : (a : G) → G') g₁ : G') ((f : (a : G) → G') g₂) : G')
⊢ (∀ g₁ ∈ H₁,
      ∀ g₂ ∈ H₂,
        Membership.mem (α := G') ⁅map f H₁, map f H₂⁆
          (Bracket.bracket (L := G') ((f : (a : G) → G') g₁ : G') ((f : (a : G) → G') g₂) : G')) ∧
    ∀ g₁ ∈ map f H₁, ∀ g₂ ∈ map f H₂, ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆
have right : ∀ g₁ ∈ map f H₁, ∀ g₂ ∈ map f H₂, ⁅g₁, g₂⁆ ∈ map f ⁅H₁, H₂⁆
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
f : G →* G'
p : G
hp : p ∈ (↑H₁ : Set G)
q : G
hq : q ∈ (↑H₂ : Set G)
⊢ Membership.mem (α := G') (map f ⁅H₁, H₂⁆)
    (Bracket.bracket (L := G') ((f : (a : G) → G') p : G') ((f : (a : G) → G') q) : G')
have right : Membership.mem (α := G') (map f ⁅H₁, H₂⁆) ((f : (a : G) → G') ⁅p, q⁆ : G')
Tactic: rw [← map_commutatorElement]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
have a : ⁅H₁.prod K₁, H₂.prod K₂⁆ ≤ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
a : ⁅H₁.prod K₁, H₂.prod K₂⁆ ≤ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
⊢ ⁅H₁.prod K₁, H₂.prod K₂⁆ = ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
have a₁ : ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁.prod K₁, H₂.prod K₂⁆ ≤ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
have a : ∀ g₁ ∈ H₁.prod K₁, ∀ g₂ ∈ H₂.prod K₂, ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆
Tactic: rw [commutator_le]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ ⁅H₁, H₂⁆.prod ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
have a : map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆ ∧
  map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
Tactic: rw [prod_le_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆ ∧
    map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
have a : map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
a : map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆ ∧
    map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
have a₁ : map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
Tactic: constructor
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inl G G') ⁅H₁, H₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
have a : Bracket.bracket (L := Subgroup (G × G')) (map (MonoidHom.inl G G') H₁) (map (MonoidHom.inl G G') H₂) ≤
  ⁅H₁.prod K₁, H₂.prod K₂⁆
Tactic: rw [map_commutator]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ Bracket.bracket (L := Subgroup (G × G')) (map (MonoidHom.inl G G') H₁) (map (MonoidHom.inl G G') H₂) ≤
    ⁅H₁.prod K₁, H₂.prod K₂⁆
have a : map (MonoidHom.inl G G') H₁ ≤ H₁.prod K₁
Tactic: apply commutator_mono
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
a : map (MonoidHom.inl G G') H₁ ≤ H₁.prod K₁
⊢ Bracket.bracket (L := Subgroup (G × G')) (map (MonoidHom.inl G G') H₁) (map (MonoidHom.inl G G') H₂) ≤
    ⁅H₁.prod K₁, H₂.prod K₂⁆
have a₁ : map (MonoidHom.inl G G') H₂ ≤ H₂.prod K₂
Tactic: apply commutator_mono
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ map (MonoidHom.inr G G') ⁅K₁, K₂⁆ ≤ ⁅H₁.prod K₁, H₂.prod K₂⁆
have a : Bracket.bracket (L := Subgroup (G × G')) (map (MonoidHom.inr G G') K₁) (map (MonoidHom.inr G G') K₂) ≤
  ⁅H₁.prod K₁, H₂.prod K₂⁆
Tactic: rw [map_commutator]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
⊢ Bracket.bracket (L := Subgroup (G × G')) (map (MonoidHom.inr G G') K₁) (map (MonoidHom.inr G G') K₂) ≤
    ⁅H₁.prod K₁, H₂.prod K₂⁆
have a : map (MonoidHom.inr G G') K₁ ≤ H₁.prod K₁
Tactic: apply commutator_mono
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
G' : Type u_2
inst : Group G
inst_1 : Group G'
H₁ H₂ : Subgroup G
K₁ K₂ : Subgroup G'
a : map (MonoidHom.inr G G') K₁ ≤ H₁.prod K₁
⊢ Bracket.bracket (L := Subgroup (G × G')) (map (MonoidHom.inr G G') K₁) (map (MonoidHom.inr G G') K₂) ≤
    ⁅H₁.prod K₁, H₂.prod K₂⁆
have a₁ : map (MonoidHom.inr G G') K₂ ≤ H₂.prod K₂
Tactic: apply commutator_mono
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
⊢ map H.subtype (_root_.commutator ↥H) = ⁅H, H⁆
have rw : map H.subtype (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) = ⁅H, H⁆
Tactic: rw [_root_.commutator_def, map_commutator, ← MonoidHom.range_eq_map, H.range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : map H.subtype (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) = ⁅H, H⁆
⊢ map H.subtype (_root_.commutator ↥H) = ⁅H, H⁆
have rw₁ : ⁅map H.subtype ⊤, map H.subtype ⊤⁆ = ⁅H, H⁆
Tactic: rw [_root_.commutator_def, map_commutator, ← MonoidHom.range_eq_map, H.range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : map H.subtype (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) = ⁅H, H⁆
rw₁ : ⁅map H.subtype ⊤, map H.subtype ⊤⁆ = ⁅H, H⁆
⊢ map H.subtype (_root_.commutator ↥H) = ⁅H, H⁆
have rw₂ : ⁅H.subtype.range, H.subtype.range⁆ = ⁅H, H⁆
Tactic: rw [_root_.commutator_def, map_commutator, ← MonoidHom.range_eq_map, H.range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Subgroup G
rw : map H.subtype (Bracket.bracket (L := Subgroup ↥H) ⊤ ⊤) = ⁅H, H⁆
rw₁ : ⁅map H.subtype ⊤, map H.subtype ⊤⁆ = ⁅H, H⁆
rw₂ : ⁅H.subtype.range, H.subtype.range⁆ = ⁅H, H⁆
⊢ map H.subtype (_root_.commutator ↥H) = ⁅H, H⁆
have rw₃ : ⁅H, H⁆ = ⁅H, H⁆
Tactic: rw [_root_.commutator_def, map_commutator, ← MonoidHom.range_eq_map, H.range_subtype]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G) (commutator G) ⊥ ↔ IsMulCommutative G
have rw : Eq (α := Subgroup G) (center G) ⊤ ↔ IsMulCommutative G
Tactic: rw [commutator_eq_bot_iff_center_eq_top, center_eq_top_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
rw : Eq (α := Subgroup G) (center G) ⊤ ↔ IsMulCommutative G
⊢ Eq (α := Subgroup G) (commutator G) ⊥ ↔ IsMulCommutative G
have rw₁ : IsMulCommutative G ↔ IsMulCommutative G
Tactic: rw [commutator_eq_bot_iff_center_eq_top, center_eq_top_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
⊢ LE.le (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (centralizer (↑(commutator G) : Set G)) (centralizer (↑(commutator G) : Set G)))
    (center G)
have rw : Eq (α := Subgroup G)
  (Bracket.bracket (L := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (centralizer (↑(commutator G) : Set G)) (centralizer (↑(commutator G) : Set G)))
    ⊤)
  ⊥
Tactic: rw [← Subgroup.centralizer_univ, ← Subgroup.coe_top, ←
    Subgroup.commutator_eq_bot_iff_le_centralizer]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
this :
  Eq (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ (centralizer (↑(commutator G) : Set G)))
      (centralizer (↑(commutator G) : Set G)))
    ⊥
⊢ Eq (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G)
      (Bracket.bracket (L := Subgroup G) (centralizer (↑(commutator G) : Set G))
        (centralizer (↑(commutator G) : Set G)))
      ⊤)
    ⊥
have refine : Eq (α := Subgroup G)
  (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) (centralizer (↑(commutator G) : Set G)) ⊤)
    (centralizer (↑(commutator G) : Set G)))
  ⊥
Tactic: refine Subgroup.commutator_commutator_eq_bot_of_rotate ?_ this
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G)
      (Bracket.bracket (L := Subgroup G) (centralizer (↑(commutator G) : Set G))
        (centralizer (↑(commutator G) : Set G)))
      ⊤)
    ⊥
have suffices : Eq (α := Subgroup G)
  (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ (centralizer (↑(commutator G) : Set G)))
    (centralizer (↑(commutator G) : Set G)))
  ⊥
Tactic: suffices ⁅⁅⊤, centralizer (commutator G : Set G)⁆, centralizer (commutator G : Set G)⁆ = ⊥ by
    refine Subgroup.commutator_commutator_eq_bot_of_rotate ?_ this
    rwa [Subgroup.commutator_comm (centralizer (commutator G : Set G))]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
⊢ Eq (α := Subgroup G)
    (Bracket.bracket (L := Subgroup G) (Bracket.bracket (L := Subgroup G) ⊤ (centralizer (↑(commutator G) : Set G)))
      (centralizer (↑(commutator G) : Set G)))
    ⊥
have rw : LE.le (α := Subgroup G) (centralizer (↑(commutator G) : Set G))
  (centralizer (↑(Bracket.bracket (L := Subgroup G) ⊤ (centralizer (↑(commutator G) : Set G))) : Set G))
Tactic: rw [Subgroup.commutator_comm, Subgroup.commutator_eq_bot_iff_le_centralizer]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
g : G
hg : IsConj g (HPow.hPow (β := ℕ) g 2)
⊢ g ∈ commutatorSet G
have obtain : ∀ (h : Gˣ) (hg : SemiconjBy (↑h : G) g (HPow.hPow (β := ℕ) g 2)), g ∈ commutatorSet G
Tactic: obtain ⟨h, hg⟩ := hg
Cleared hypotheses: hg
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h : G) g (HPow.hPow (β := ℕ) g 2)
⊢ g ∈ commutatorSet G
have h₁ : ⁅(↑h : G), g⁆ = g
Tactic: use h, g
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
g : G
h : Gˣ
hg : SemiconjBy (↑h : G) g (HPow.hPow (β := ℕ) g 2)
⊢ ⁅(↑h : G), g⁆ = g
have h₁ : HPow.hPow (β := ℕ) g 2 * (↑h : G) * (↑h : G)⁻¹ * g⁻¹ = g
Tactic: rw [commutatorElement_def, hg]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_4
inst_1 : Group H
f : G →* H
⊢ map f (commutator G) = ⁅f.range, f.range⁆
have rw : ⁅map f ⊤, map f ⊤⁆ = ⁅f.range, f.range⁆
Tactic: rw [_root_.commutator_def, Subgroup.map_commutator]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_4
inst_1 : Group H
f : G →* H
⊢ ⁅map f ⊤, map f ⊤⁆ = ⁅f.range, f.range⁆
have hx : map f ⊤ = f.range
Tactic: apply congr_arg₂
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_4
inst_1 : Group H
f : G →* H
⊢ map f ⊤ = f.range
have hx : Codisjoint ⊤ f.ker
Tactic: rw [Subgroup.map_eq_range_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_4
inst_1 : Group H
f : G →* H
⊢ Codisjoint ⊤ f.ker
have hx : ⊤ ⊔ f.ker = ⊤
Tactic: rw [codisjoint_iff, top_sup_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_4
inst_1 : Group H
f : G →* H
hx : ⊤ ⊔ f.ker = ⊤
⊢ Codisjoint ⊤ f.ker
have hx₁ : Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤
Tactic: rw [codisjoint_iff, top_sup_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_4
inst_1 : Group H
f : G →* H
⊢ map f ⊤ = f.range
have hy : Codisjoint ⊤ f.ker
Tactic: rw [Subgroup.map_eq_range_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_4
inst_1 : Group H
f : G →* H
⊢ Codisjoint ⊤ f.ker
have hy : ⊤ ⊔ f.ker = ⊤
Tactic: rw [codisjoint_iff, top_sup_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
H : Type u_4
inst_1 : Group H
f : G →* H
hy : ⊤ ⊔ f.ker = ⊤
⊢ Codisjoint ⊤ f.ker
have hy₁ : Eq.{u_1 + 1} (α := Subgroup G) ⊤ ⊤
Tactic: rw [codisjoint_iff, top_sup_eq]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
⊢ Set.image (α := ↥(closureCommutatorRepresentatives G))
      (⇑(Subgroup.subtype (closureCommutatorRepresentatives G)) : (a : ↥(closureCommutatorRepresentatives G)) → G)
      (commutatorSet ↥(closureCommutatorRepresentatives G)) =
    commutatorSet G
have h₁ : Set.image (α := ↥(closureCommutatorRepresentatives G))
    (⇑(Subgroup.subtype (closureCommutatorRepresentatives G)) : (a : ↥(closureCommutatorRepresentatives G)) → G)
    (commutatorSet ↥(closureCommutatorRepresentatives G)) ⊆
  commutatorSet G
Tactic: apply Set.Subset.antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
h₁ :
  Set.image (α := ↥(closureCommutatorRepresentatives G))
      (⇑(Subgroup.subtype (closureCommutatorRepresentatives G)) : (a : ↥(closureCommutatorRepresentatives G)) → G)
      (commutatorSet ↥(closureCommutatorRepresentatives G)) ⊆
    commutatorSet G
⊢ Set.image (α := ↥(closureCommutatorRepresentatives G))
      (⇑(Subgroup.subtype (closureCommutatorRepresentatives G)) : (a : ↥(closureCommutatorRepresentatives G)) → G)
      (commutatorSet ↥(closureCommutatorRepresentatives G)) =
    commutatorSet G
have h₂ : commutatorSet G ⊆
  Set.image (α := ↥(closureCommutatorRepresentatives G))
    (⇑(Subgroup.subtype (closureCommutatorRepresentatives G)) : (a : ↥(closureCommutatorRepresentatives G)) → G)
    (commutatorSet ↥(closureCommutatorRepresentatives G))
Tactic: apply Set.Subset.antisymm
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
⊢ IsMulCommutative.{u_1} (G ⧸ N) ↔ _root_.commutator G ≤ N
have refine_1 : ∀ (hcomm : IsMulCommutative.{u_1} (G ⧸ N)), _root_.commutator G ≤ N
Tactic: refine ⟨fun hcomm ↦ ?_, fun hGN ↦ ⟨⟨fun x' y' ↦ ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
refine_1 : ∀ (hcomm : IsMulCommutative.{u_1} (G ⧸ N)), _root_.commutator G ≤ N
⊢ IsMulCommutative.{u_1} (G ⧸ N) ↔ _root_.commutator G ≤ N
have refine_2 : ∀ (hGN : _root_.commutator G ≤ N) (x' y' : G ⧸ N), x' * y' = y' * x'
Tactic: refine ⟨fun hcomm ↦ ?_, fun hGN ↦ ⟨⟨fun x' y' ↦ ?_⟩⟩⟩
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hcomm : IsMulCommutative.{u_1} (G ⧸ N)
⊢ _root_.commutator G ≤ N
have refine_1 : commutatorSet G ⊆ (↑N : Set G)
Tactic: rw [commutator_eq_normalClosure, ← Subgroup.normalClosure_subset_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hcomm : IsMulCommutative.{u_1} (G ⧸ N)
p q : G
⊢ ⁅p, q⁆ ∈ (↑N : Set G)
have refine_1 : Eq (α := G ⧸ N) (↑(p * q * p⁻¹ * q⁻¹) : G ⧸ N) 1
Tactic: rw [SetLike.mem_coe, ← QuotientGroup.eq_one_iff, commutatorElement_def]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hcomm : IsMulCommutative.{u_1} (G ⧸ N)
p q : G
⊢ Eq (α := G ⧸ N) (↑(p * q * p⁻¹ * q⁻¹) : G ⧸ N) 1
have refine_1 : HMul.hMul (α := G ⧸ N) (↑p : G ⧸ N) (↑q : G ⧸ N) * (↑p : G ⧸ N)⁻¹ * (↑q : G ⧸ N)⁻¹ = 1
Tactic: simp only [QuotientGroup.mk_mul, QuotientGroup.mk_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hcomm : IsMulCommutative.{u_1} (G ⧸ N)
p q : G
⊢ HMul.hMul (α := G ⧸ N) (↑p : G ⧸ N) (↑q : G ⧸ N) * (↑p : G ⧸ N)⁻¹ * (↑q : G ⧸ N)⁻¹ = 1
have refine_1 : Eq (α := G ⧸ N) (Bracket.bracket (L := G ⧸ N) (↑p : G ⧸ N) (↑q : G ⧸ N)) 1
Tactic: rw [← commutatorElement_def, commutatorElement_eq_one_iff_mul_comm, mul_comm']
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hcomm : IsMulCommutative.{u_1} (G ⧸ N)
p q : G
refine_1 : Eq (α := G ⧸ N) (Bracket.bracket (L := G ⧸ N) (↑p : G ⧸ N) (↑q : G ⧸ N)) 1
⊢ HMul.hMul (α := G ⧸ N) (↑p : G ⧸ N) (↑q : G ⧸ N) * (↑p : G ⧸ N)⁻¹ * (↑q : G ⧸ N)⁻¹ = 1
have refine_1₁ : HMul.hMul (α := G ⧸ N) (↑p : G ⧸ N) (↑q : G ⧸ N) = HMul.hMul (α := G ⧸ N) (↑q : G ⧸ N) (↑p : G ⧸ N)
Tactic: rw [← commutatorElement_def, commutatorElement_eq_one_iff_mul_comm, mul_comm']
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hcomm : IsMulCommutative.{u_1} (G ⧸ N)
p q : G
refine_1 : Eq (α := G ⧸ N) (Bracket.bracket (L := G ⧸ N) (↑p : G ⧸ N) (↑q : G ⧸ N)) 1
refine_1₁ : HMul.hMul (α := G ⧸ N) (↑p : G ⧸ N) (↑q : G ⧸ N) = HMul.hMul (α := G ⧸ N) (↑q : G ⧸ N) (↑p : G ⧸ N)
⊢ HMul.hMul (α := G ⧸ N) (↑p : G ⧸ N) (↑q : G ⧸ N) * (↑p : G ⧸ N)⁻¹ * (↑q : G ⧸ N)⁻¹ = 1
have refine_1₂ : HMul.hMul (α := G ⧸ N) (↑q : G ⧸ N) (↑p : G ⧸ N) = HMul.hMul (α := G ⧸ N) (↑q : G ⧸ N) (↑p : G ⧸ N)
Tactic: rw [← commutatorElement_def, commutatorElement_eq_one_iff_mul_comm, mul_comm']
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hGN : _root_.commutator G ≤ N
x' y' : G ⧸ N
⊢ x' * y' = y' * x'
have refine_2 : ∀ (x : G),
  HMul.hMul (α := G ⧸ N) ((QuotientGroup.mk' N : (a : G) → G ⧸ N) x : G ⧸ N) y' =
    HMul.hMul (β := G ⧸ N) y' ((QuotientGroup.mk' N : (a : G) → G ⧸ N) x : G ⧸ N)
Tactic: obtain ⟨x, rfl⟩ := QuotientGroup.mk'_surjective N x'
Cleared hypotheses: x'
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hGN : _root_.commutator G ≤ N
y' : G ⧸ N
x : G
⊢ HMul.hMul (α := G ⧸ N) ((QuotientGroup.mk' N : (a : G) → G ⧸ N) x : G ⧸ N) y' =
    HMul.hMul (β := G ⧸ N) y' ((QuotientGroup.mk' N : (a : G) → G ⧸ N) x : G ⧸ N)
have refine_2 : ∀ (y : G),
  HMul.hMul (α := G ⧸ N) (β := G ⧸ N) ((QuotientGroup.mk' N : (a : G) → G ⧸ N) x : G ⧸ N)
      ((QuotientGroup.mk' N : (a : G) → G ⧸ N) y : G ⧸ N) =
    HMul.hMul (α := G ⧸ N) (β := G ⧸ N) ((QuotientGroup.mk' N : (a : G) → G ⧸ N) y : G ⧸ N)
      ((QuotientGroup.mk' N : (a : G) → G ⧸ N) x : G ⧸ N)
Tactic: obtain ⟨y, rfl⟩ := QuotientGroup.mk'_surjective N y'
Cleared hypotheses: y'
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ HMul.hMul (α := G ⧸ N) (β := G ⧸ N) ((QuotientGroup.mk' N : (a : G) → G ⧸ N) x : G ⧸ N)
      ((QuotientGroup.mk' N : (a : G) → G ⧸ N) y : G ⧸ N) =
    HMul.hMul (α := G ⧸ N) (β := G ⧸ N) ((QuotientGroup.mk' N : (a : G) → G ⧸ N) y : G ⧸ N)
      ((QuotientGroup.mk' N : (a : G) → G ⧸ N) x : G ⧸ N)
have refine_2 : ⁅x, y⁆ ∈ N
Tactic: rw [← commutatorElement_eq_one_iff_mul_comm, ← map_commutatorElement, QuotientGroup.mk'_apply,
      QuotientGroup.eq_one_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ ⁅x, y⁆ ∈ N
have refine_2 : Membership.mem (γ := Subgroup G) (_root_.commutator G) ⁅x, y⁆
Tactic: apply hGN
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hGN : _root_.commutator G ≤ N
x y : G
⊢ Membership.mem (γ := Subgroup G) (_root_.commutator G) ⁅x, y⁆
have refine_2 : Membership.mem (γ := Subgroup G) (closure (commutatorSet G)) ⁅x, y⁆
Tactic: rw [commutator_eq_closure]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative.{u_1} ↥H
⊢ _root_.commutator G ≤ N
have apply : IsMulCommutative.{u_1} (G ⧸ N)
Tactic: apply quotient_commutative_iff_commutator_le.mp
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative.{u_1} ↥H
φ : ↥H →ₙ* G ⧸ N := (↑(MonoidHom.comp (QuotientGroup.mk' N) H.subtype) : ↥H →ₙ* G ⧸ N)
⊢ IsMulCommutative.{u_1} (G ⧸ N)
have apply : Function.Surjective (α := ↥H) (β := G ⧸ N) (⇑φ : (a : ↥H) → G ⧸ N)
Tactic: apply Function.Surjective.mul_comm (f := φ) _ hH
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative.{u_1} ↥H
φ : ↥H →ₙ* G ⧸ N := (↑(MonoidHom.comp (QuotientGroup.mk' N) H.subtype) : ↥H →ₙ* G ⧸ N)
⊢ Eq (α := Subgroup (G ⧸ N)) (Subgroup.map (QuotientGroup.mk' N) ⊤) ⊤
have rw : Function.Surjective (α := G) (β := G ⧸ N) (⇑(QuotientGroup.mk' N) : (a : G) → G ⧸ N)
Tactic: rw [← MonoidHom.range_eq_map, MonoidHom.range_eq_top]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (hypothesis)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative.{u_1} ↥H
φ : ↥H →ₙ* G ⧸ N := (↑(MonoidHom.comp (QuotientGroup.mk' N) H.subtype) : ↥H →ₙ* G ⧸ N)
⊢ Function.Surjective (α := ↥H) (β := G ⧸ N) (⇑φ : (a : ↥H) → G ⧸ N)
have this : Eq (α := Subgroup (G ⧸ N)) (Subgroup.map (QuotientGroup.mk' N) ⊤) ⊤
Tactic: have : Subgroup.map (QuotientGroup.mk' N) ⊤ = ⊤ := by
    rw [← MonoidHom.range_eq_map, MonoidHom.range_eq_top]
    exact QuotientGroup.mk'_surjective N
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Basic (goal)
Goal:
G : Type u_1
inst : Group G
N : Subgroup G
inst_1 : N.Normal
H : Subgroup G
hHN : N ⊔ H = ⊤
hH : IsMulCommutative.{u_1} ↥H
φ : ↥H →ₙ* G ⧸ N := (↑(MonoidHom.comp (QuotientGroup.mk' N) H.subtype) : ↥H →ₙ* G ⧸ N)
this : Eq (α := Subgroup (G ⧸ N)) (Subgroup.map (QuotientGroup.mk' N) ⊤) ⊤
⊢ Function.Surjective (α := ↥H) (β := G ⧸ N) (⇑φ : (a : ↥H) → G ⧸ N)
have rw : N ⊔ H.subtype.range = N ⊔ H ⊔ N
Tactic: rw [MulHom.coe_coe, ← MonoidHom.range_eq_top, MonoidHom.range_eq_map, ← Subgroup.map_map, ← this,
    Subgroup.map_eq_map_iff, QuotientGroup.ker_mk', sup_comm, ← hHN, ← MonoidHom.range_eq_map]
-- Lean 4 proof step from Mathlib.GroupTheory.Commutator.Finite (goal)
Goal:
η : Type u_2
inst : Finite η
Gs : η → Type u_3
inst_1 : (i : η) → Group (Gs i)
H K : (i : η) → Subgroup (Gs i)
⊢ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆ = pi (f := Gs) Set.univ fun (i : η) ↦ ⁅H i, K i⁆
have apply : (pi (f := Gs) Set.univ fun (i : η) ↦ ⁅H i, K i⁆) ≤ ⁅pi (f := Gs) Set.univ H, pi (f := Gs) Set.univ K⁆
Tactic: apply le_antisymm (commutator_pi_pi_le H K)