awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : Subsingleton.{u + 1} ↥N ∧ Nonempty.{u + 1} ↥N
hN1 : ¬Nat.card.{u} ↥N = 0
hN2 : N.index = 0
this : Subsingleton.{u + 1} ↥N
⊢ ∃ (H : Subgroup G), N.IsComplement' H
have pos : ∃ (H : Subgroup G), IsComplement' ⊥ H
Tactic: rw [N.eq_bot_of_subsingleton]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
hN1 : ¬Nat.card.{u} ↥N = 0
hN2 : ¬N.index = 0
⊢ Finite G
have h : Nat.card G ≠ 0
Tactic: apply Nat.finite_of_card_ne_zero
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (goal)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
hN1 : ¬Nat.card.{u} ↥N = 0
hN2 : ¬N.index = 0
⊢ Nat.card G ≠ 0
have h : Nat.card.{u} ↥N * N.index ≠ 0
Tactic: rw [← N.card_mul_index]
-- Lean 4 proof step from Mathlib.GroupTheory.SchurZassenhaus (hypothesis)
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
hN1 : ¬Nat.card.{u} ↥N = 0
hN2 : ¬N.index = 0
⊢ ∃ (H : Subgroup G), N.IsComplement' H
have hN3 : Finite G
Tactic: have hN3 : Finite G := by
    apply Nat.finite_of_card_ne_zero
    rw [← N.card_mul_index]
    exact mul_ne_zero hN1 hN2
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
x y : N
⊢ ⟨x * y, 1⟩ = HMul.hMul (α := N ⋊[φ] G) (⟨x, 1⟩ : N ⋊[φ] G) (⟨y, 1⟩ : N ⋊[φ] G)
have left : left.{u_1, u_2} (G := G) (φ := φ) (⟨x * y, 1⟩ : N ⋊[φ] G) =
  (HMul.hMul (α := N ⋊[φ] G) (⟨x, 1⟩ : N ⋊[φ] G) (⟨y, 1⟩ : N ⋊[φ] G)).left
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
x y : N
left :
  SemidirectProduct.left.{u_1, u_2} (G := G) (φ := φ) (⟨x * y, 1⟩ : N ⋊[φ] G) =
    (HMul.hMul (α := N ⋊[φ] G) (⟨x, 1⟩ : N ⋊[φ] G) (⟨y, 1⟩ : N ⋊[φ] G)).left
⊢ ⟨x * y, 1⟩ = HMul.hMul (α := N ⋊[φ] G) (⟨x, 1⟩ : N ⋊[φ] G) (⟨y, 1⟩ : N ⋊[φ] G)
have right : right (φ := φ) ⟨x * y, 1⟩ = (HMul.hMul (α := N ⋊[φ] G) (⟨x, 1⟩ : N ⋊[φ] G) (⟨y, 1⟩ : N ⋊[φ] G)).right
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
x y : G
⊢ ⟨1, x * y⟩ = HMul.hMul (α := N ⋊[φ] G) (⟨1, x⟩ : N ⋊[φ] G) (⟨1, y⟩ : N ⋊[φ] G)
have left : left (φ := φ) ⟨1, x * y⟩ = (HMul.hMul (α := N ⋊[φ] G) (⟨1, x⟩ : N ⋊[φ] G) (⟨1, y⟩ : N ⋊[φ] G)).left
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
x y : G
left :
  SemidirectProduct.left (φ := φ) ⟨1, x * y⟩ = (HMul.hMul (α := N ⋊[φ] G) (⟨1, x⟩ : N ⋊[φ] G) (⟨1, y⟩ : N ⋊[φ] G)).left
⊢ ⟨1, x * y⟩ = HMul.hMul (α := N ⋊[φ] G) (⟨1, x⟩ : N ⋊[φ] G) (⟨1, y⟩ : N ⋊[φ] G)
have right : right.{u_1, u_2} (N := N) (φ := φ) (⟨1, x * y⟩ : N ⋊[φ] G) =
  (HMul.hMul (α := N ⋊[φ] G) (⟨1, x⟩ : N ⋊[φ] G) (⟨1, y⟩ : N ⋊[φ] G)).right
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
g : G
n : N
⊢ (inl : (a : N) → N ⋊[φ] G) ((((φ : (a : G) → MulAut N) g : MulAut N) : (a : N) → N) n) =
    HMul.hMul (β := N ⋊[φ] G)
      (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)
        ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G))
      ((inr : (a : G) → N ⋊[φ] G) g⁻¹ : N ⋊[φ] G)
have left : left.{u_1, u_2} (G := G) (φ := φ)
    ((inl : (a : N) → N ⋊[φ] G) ((((φ : (a : G) → MulAut N) g : MulAut N) : (a : N) → N) n)) =
  (HMul.hMul (β := N ⋊[φ] G)
      (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)
        ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G))
      ((inr : (a : G) → N ⋊[φ] G) g⁻¹ : N ⋊[φ] G)).left
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
g : G
n : N
left :
  SemidirectProduct.left.{u_1, u_2} (G := G) (φ := φ)
      ((inl : (a : N) → N ⋊[φ] G) ((((φ : (a : G) → MulAut N) g : MulAut N) : (a : N) → N) n)) =
    (HMul.hMul (β := N ⋊[φ] G)
        (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)
          ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G))
        ((inr : (a : G) → N ⋊[φ] G) g⁻¹ : N ⋊[φ] G)).left
⊢ (inl : (a : N) → N ⋊[φ] G) ((((φ : (a : G) → MulAut N) g : MulAut N) : (a : N) → N) n) =
    HMul.hMul (β := N ⋊[φ] G)
      (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)
        ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G))
      ((inr : (a : G) → N ⋊[φ] G) g⁻¹ : N ⋊[φ] G)
have right : right.{u_1, u_2} (N := N) (φ := φ)
    ((inl : (a : N) → N ⋊[φ] G) ((((φ : (a : G) → MulAut N) g : MulAut N) : (a : N) → N) n)) =
  (HMul.hMul (β := N ⋊[φ] G)
      (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)
        ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G))
      ((inr : (a : G) → N ⋊[φ] G) g⁻¹ : N ⋊[φ] G)).right
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
g : G
n : N
⊢ (inl : (a : N) → N ⋊[φ] G) (((((φ : (a : G) → MulAut N) g)⁻¹ : MulAut N) : (a : N) → N) n) =
    HMul.hMul (β := N ⋊[φ] G)
      (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g⁻¹ : N ⋊[φ] G)
        ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G))
      ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)
have rw : (inl : (a : N) → N ⋊[φ] G) ((((φ : (a : G) → MulAut N) g⁻¹ : MulAut N) : (a : N) → N) n) =
  HMul.hMul (β := N ⋊[φ] G)
    (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g⁻¹ : N ⋊[φ] G)
      ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G))
    ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)
Tactic: rw [← map_inv, inl_aut, inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
g : G
n : N
rw :
  (inl : (a : N) → N ⋊[φ] G) ((((φ : (a : G) → MulAut N) g⁻¹ : MulAut N) : (a : N) → N) n) =
    HMul.hMul (β := N ⋊[φ] G)
      (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g⁻¹ : N ⋊[φ] G)
        ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G))
      ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)
⊢ (inl : (a : N) → N ⋊[φ] G) (((((φ : (a : G) → MulAut N) g)⁻¹ : MulAut N) : (a : N) → N) n) =
    HMul.hMul (β := N ⋊[φ] G)
      (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g⁻¹ : N ⋊[φ] G)
        ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G))
      ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)
have rw₁ : HMul.hMul (β := N ⋊[φ] G)
    (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g⁻¹ : N ⋊[φ] G)
      ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G))
    ((inr : (a : G) → N ⋊[φ] G) g⁻¹⁻¹ : N ⋊[φ] G) =
  HMul.hMul (β := N ⋊[φ] G)
    (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g⁻¹ : N ⋊[φ] G)
      ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G))
    ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)
Tactic: rw [← map_inv, inl_aut, inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
g : G
n : N
rw :
  (inl : (a : N) → N ⋊[φ] G) ((((φ : (a : G) → MulAut N) g⁻¹ : MulAut N) : (a : N) → N) n) =
    HMul.hMul (β := N ⋊[φ] G)
      (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g⁻¹ : N ⋊[φ] G)
        ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G))
      ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)
rw₁ :
  HMul.hMul (β := N ⋊[φ] G)
      (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g⁻¹ : N ⋊[φ] G)
        ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G))
      ((inr : (a : G) → N ⋊[φ] G) g⁻¹⁻¹ : N ⋊[φ] G) =
    HMul.hMul (β := N ⋊[φ] G)
      (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g⁻¹ : N ⋊[φ] G)
        ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G))
      ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)
⊢ (inl : (a : N) → N ⋊[φ] G) (((((φ : (a : G) → MulAut N) g)⁻¹ : MulAut N) : (a : N) → N) n) =
    HMul.hMul (β := N ⋊[φ] G)
      (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g⁻¹ : N ⋊[φ] G)
        ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G))
      ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)
have rw₂ : HMul.hMul (β := N ⋊[φ] G)
    (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g⁻¹ : N ⋊[φ] G)
      ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G))
    ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G) =
  HMul.hMul (β := N ⋊[φ] G)
    (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g⁻¹ : N ⋊[φ] G)
      ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G))
    ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)
Tactic: rw [← map_inv, inl_aut, inv_inv]
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
g : G
n : N
⊢ ⟨n, g⟩ =
    HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G)
      ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)
have left : left (φ := φ) (⟨n, g⟩ : N ⋊[φ] G) =
  (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G)
      ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)).left
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
g : G
n : N
left :
  SemidirectProduct.left (φ := φ) (⟨n, g⟩ : N ⋊[φ] G) =
    (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G)
        ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)).left
⊢ ⟨n, g⟩ =
    HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G)
      ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)
have right : right (φ := φ) (⟨n, g⟩ : N ⋊[φ] G) =
  (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G)
      ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)).right
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
x : N ⋊[φ] G
⊢ HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inl : (a : N) → N ⋊[φ] G) x.left : N ⋊[φ] G)
      ((inr : (a : G) → N ⋊[φ] G) x.right : N ⋊[φ] G) =
    x
have left : (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inl : (a : N) → N ⋊[φ] G) x.left : N ⋊[φ] G)
      ((inr : (a : G) → N ⋊[φ] G) x.right : N ⋊[φ] G)).left =
  x.left
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
x : N ⋊[φ] G
left :
  (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inl : (a : N) → N ⋊[φ] G) x.left : N ⋊[φ] G)
        ((inr : (a : G) → N ⋊[φ] G) x.right : N ⋊[φ] G)).left =
    x.left
⊢ HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inl : (a : N) → N ⋊[φ] G) x.left : N ⋊[φ] G)
      ((inr : (a : G) → N ⋊[φ] G) x.right : N ⋊[φ] G) =
    x
have right : (HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inl : (a : N) → N ⋊[φ] G) x.left : N ⋊[φ] G)
      ((inr : (a : G) → N ⋊[φ] G) x.right : N ⋊[φ] G)).right =
  x.right
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
⊢ Eq (α := N →* G) (MonoidHom.comp (N := N ⋊[φ] G) rightHom inl) 1
have h : ∀ (x : N),
  Eq.{u_2 + 1} (α := G) ((MonoidHom.comp (N := N ⋊[φ] G) rightHom inl : (a : N) → G) x : G) ((1 : (a : N) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
⊢ Eq (α := G →* G) (MonoidHom.comp (N := N ⋊[φ] G) rightHom inr) (MonoidHom.id G)
have h : ∀ (x : G),
  Eq (α := G) ((MonoidHom.comp (N := N ⋊[φ] G) rightHom inr : (a : G) → G) x : G) ((MonoidHom.id G : (a : G) → G) x : G)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
x : N ⋊[φ] G
hx : Membership.mem (γ := Subgroup (N ⋊[φ] G)) (MonoidHom.ker rightHom) x
⊢ (inl : (a : N) → N ⋊[φ] G) x.left = x
have left : left.{u_1, u_2} (G := G) (φ := φ) ((inl : (a : N) → N ⋊[φ] G) x.left) = x.left
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
x : N ⋊[φ] G
hx : Membership.mem (γ := Subgroup (N ⋊[φ] G)) (MonoidHom.ker rightHom) x
left : SemidirectProduct.left.{u_1, u_2} (G := G) (φ := φ) ((inl : (a : N) → N ⋊[φ] G) x.left) = x.left
⊢ (inl : (a : N) → N ⋊[φ] G) x.left = x
have right : right.{u_1, u_2} (N := N) (φ := φ) ((inl : (a : N) → N ⋊[φ] G) x.left) = x.right
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (hypothesis)
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
fn : N →* H
fg : G →* H
h :
  ∀ (g : G),
    fn.comp (MulEquiv.toMonoidHom ((φ : (a : G) → MulAut N) g)) =
      MonoidHom.comp (MulEquiv.toMonoidHom ((MulAut.conj : (a : H) → MulAut H) ((fg : (a : G) → H) g))) fn
a b : N ⋊[φ] G
⊢ HMul.hMul (α := H) (β := H) ((fn : (a : N) → H) (a * b).left : H) ((fg : (a : G) → H) (a * b).right : H) =
    HMul.hMul (α := H) (β := H) ((fn : (a : N) → H) a.left : H) ((fg : (a : G) → H) a.right : H) *
      HMul.hMul (α := H) (β := H) ((fn : (a : N) → H) b.left : H) ((fg : (a : G) → H) b.right : H)
have this : ∀ (n : G) (g : N),
  Eq.{u_3 + 1} (α := H) ((fn.comp (MulEquiv.toMonoidHom ((φ : (a : G) → MulAut N) n)) : (a : N) → H) g : H)
    ((MonoidHom.comp (MulEquiv.toMonoidHom ((MulAut.conj : (a : H) → MulAut H) ((fg : (a : G) → H) n))) fn :
          (a : N) → H)
        g :
      H)
Tactic: have := fun n g ↦ DFunLike.ext_iff.1 (h n) g
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
fn : N →* H
fg : G →* H
h :
  ∀ (g : G),
    fn.comp (MulEquiv.toMonoidHom ((φ : (a : G) → MulAut N) g)) =
      MonoidHom.comp (MulEquiv.toMonoidHom ((MulAut.conj : (a : H) → MulAut H) ((fg : (a : G) → H) g))) fn
⊢ (lift fn fg h).comp inl = fn
have h₁ : ∀ (x : N), Eq.{u_3 + 1} (α := H) (((lift fn fg h).comp inl : (a : N) → H) x : H) ((fn : (a : N) → H) x : H)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
fn : N →* H
fg : G →* H
h :
  ∀ (g : G),
    fn.comp (MulEquiv.toMonoidHom ((φ : (a : G) → MulAut N) g)) =
      MonoidHom.comp (MulEquiv.toMonoidHom ((MulAut.conj : (a : H) → MulAut H) ((fg : (a : G) → H) g))) fn
⊢ (lift fn fg h).comp inr = fg
have h₁ : ∀ (x : G), Eq.{u_3 + 1} (α := H) (((lift fn fg h).comp inr : (a : G) → H) x : H) ((fg : (a : G) → H) x : H)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
fn : N →* H
fg : G →* H
h :
  ∀ (g : G),
    fn.comp (MulEquiv.toMonoidHom ((φ : (a : G) → MulAut N) g)) =
      MonoidHom.comp (MulEquiv.toMonoidHom ((MulAut.conj : (a : H) → MulAut H) ((fg : (a : G) → H) g))) fn
F : N ⋊[φ] G →* H
x : G
⊢ (F.comp inl).comp (MulEquiv.toMonoidHom ((φ : (a : G) → MulAut N) x)) =
    MonoidHom.comp (MulEquiv.toMonoidHom ((MulAut.conj : (a : H) → MulAut H) ((F.comp inr : (a : G) → H) x)))
      (F.comp inl)
have h₁ : ∀ (x_1 : N),
  Eq.{u_3 + 1} (α := H) (((F.comp inl).comp (MulEquiv.toMonoidHom ((φ : (a : G) → MulAut N) x)) : (a : N) → H) x_1 : H)
    ((MonoidHom.comp (MulEquiv.toMonoidHom ((MulAut.conj : (a : H) → MulAut H) ((F.comp inr : (a : G) → H) x)))
            (F.comp inl) :
          (a : N) → H)
        x_1 :
      H)
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
F : N ⋊[φ] G →* H
⊢ F = lift (F.comp inl) (F.comp inr) ⋯
have rw : ∀ (x : N ⋊[φ] G),
  Eq.{u_3 + 1} (α := H) ((F : (a : N ⋊[φ] G) → H) x : H) ((lift (F.comp inl) (F.comp inr) sorry : (a : N ⋊[φ] G) → H) x : H)
Tactic: rw [DFunLike.ext_iff]
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
f g : N ⋊[φ] G →* H
hl : f.comp inl = g.comp inl
hr : f.comp inr = g.comp inr
⊢ f = g
have rw : Eq (α := N ⋊[φ] G →* H) (lift (f.comp inl) (f.comp inr) sorry) (lift (g.comp inl) (g.comp inr) sorry)
Tactic: rw [lift_unique f, lift_unique g]
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (hypothesis)
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst_3 : Group N₁
inst_4 : Group G₁
inst_5 : Group N₂
inst_6 : Group G₂
φ₁ : MonoidHom.{u_5, u_4} G₁ (MulAut N₁)
φ₂ : MonoidHom.{u_7, u_6} G₂ (MulAut N₂)
fn : N₁ →* N₂
fg : G₁ →* G₂
h :
  ∀ (g : G₁),
    fn.comp (MulEquiv.toMonoidHom ((φ₁ : (a : G₁) → MulAut N₁) g)) =
      MonoidHom.comp (MulEquiv.toMonoidHom ((φ₂ : (a : G₂) → MulAut N₂) ((fg : (a : G₁) → G₂) g))) fn
x y : N₁ ⋊[φ₁] G₁
⊢ ⟨(fn : (a : N₁) → N₂) (x * y).left, (fg : (a : G₁) → G₂) (x * y).right⟩ =
    HMul.hMul (α := N₂ ⋊[φ₂] G₂) (β := N₂ ⋊[φ₂] G₂)
      (⟨(fn : (a : N₁) → N₂) x.left, (fg : (a : G₁) → G₂) x.right⟩ : N₂ ⋊[φ₂] G₂)
      (⟨(fn : (a : N₁) → N₂) y.left, (fg : (a : G₁) → G₂) y.right⟩ : N₂ ⋊[φ₂] G₂)
have h₁ : Eq.{u_6 + 1} (α := N₂)
  ((fn.comp (MulEquiv.toMonoidHom ((φ₁ : (a : G₁) → MulAut N₁) x.right)) : (a : N₁) → N₂) y.left : N₂)
  ((MonoidHom.comp (MulEquiv.toMonoidHom ((φ₂ : (a : G₂) → MulAut N₂) ((fg : (a : G₁) → G₂) x.right))) fn :
        (a : N₁) → N₂)
      y.left :
    N₂)
Tactic: replace h := DFunLike.ext_iff.1 (h x.right) y.left
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst_3 : Group N₁
inst_4 : Group G₁
inst_5 : Group N₂
inst_6 : Group G₂
φ₁ : MonoidHom.{u_5, u_4} G₁ (MulAut N₁)
φ₂ : MonoidHom.{u_7, u_6} G₂ (MulAut N₂)
fn : N₁ →* N₂
fg : G₁ →* G₂
x y : N₁ ⋊[φ₁] G₁
h :
  Eq.{u_6 + 1} (α := N₂)
    ((fn.comp (MulEquiv.toMonoidHom ((φ₁ : (a : G₁) → MulAut N₁) x.right)) : (a : N₁) → N₂) y.left : N₂)
    ((MonoidHom.comp (MulEquiv.toMonoidHom ((φ₂ : (a : G₂) → MulAut N₂) ((fg : (a : G₁) → G₂) x.right))) fn :
          (a : N₁) → N₂)
        y.left :
      N₂)
⊢ ⟨(fn : (a : N₁) → N₂) (x * y).left, (fg : (a : G₁) → G₂) (x * y).right⟩ =
    HMul.hMul (α := N₂ ⋊[φ₂] G₂) (β := N₂ ⋊[φ₂] G₂)
      (⟨(fn : (a : N₁) → N₂) x.left, (fg : (a : G₁) → G₂) x.right⟩ : N₂ ⋊[φ₂] G₂)
      (⟨(fn : (a : N₁) → N₂) y.left, (fg : (a : G₁) → G₂) y.right⟩ : N₂ ⋊[φ₂] G₂)
have left : left.{u_6, u_7} (G := G₂) (φ := φ₂) ⟨(fn : (a : N₁) → N₂) (x * y).left, (fg : (a : G₁) → G₂) (x * y).right⟩ =
  (HMul.hMul (α := N₂ ⋊[φ₂] G₂) (β := N₂ ⋊[φ₂] G₂)
      (⟨(fn : (a : N₁) → N₂) x.left, (fg : (a : G₁) → G₂) x.right⟩ : N₂ ⋊[φ₂] G₂)
      (⟨(fn : (a : N₁) → N₂) y.left, (fg : (a : G₁) → G₂) y.right⟩ : N₂ ⋊[φ₂] G₂)).left
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N : Type u_1
G : Type u_2
H : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H
φ : MonoidHom.{u_2, u_1} G (MulAut N)
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst_3 : Group N₁
inst_4 : Group G₁
inst_5 : Group N₂
inst_6 : Group G₂
φ₁ : MonoidHom.{u_5, u_4} G₁ (MulAut N₁)
φ₂ : MonoidHom.{u_7, u_6} G₂ (MulAut N₂)
fn : N₁ →* N₂
fg : G₁ →* G₂
x y : N₁ ⋊[φ₁] G₁
h :
  Eq.{u_6 + 1} (α := N₂)
    ((fn.comp (MulEquiv.toMonoidHom ((φ₁ : (a : G₁) → MulAut N₁) x.right)) : (a : N₁) → N₂) y.left : N₂)
    ((MonoidHom.comp (MulEquiv.toMonoidHom ((φ₂ : (a : G₂) → MulAut N₂) ((fg : (a : G₁) → G₂) x.right))) fn :
          (a : N₁) → N₂)
        y.left :
      N₂)
left :
  SemidirectProduct.left.{u_6, u_7} (G := G₂) (φ := φ₂)
      ⟨(fn : (a : N₁) → N₂) (x * y).left, (fg : (a : G₁) → G₂) (x * y).right⟩ =
    (HMul.hMul (α := N₂ ⋊[φ₂] G₂) (β := N₂ ⋊[φ₂] G₂)
        (⟨(fn : (a : N₁) → N₂) x.left, (fg : (a : G₁) → G₂) x.right⟩ : N₂ ⋊[φ₂] G₂)
        (⟨(fn : (a : N₁) → N₂) y.left, (fg : (a : G₁) → G₂) y.right⟩ : N₂ ⋊[φ₂] G₂)).left
⊢ ⟨(fn : (a : N₁) → N₂) (x * y).left, (fg : (a : G₁) → G₂) (x * y).right⟩ =
    HMul.hMul (α := N₂ ⋊[φ₂] G₂) (β := N₂ ⋊[φ₂] G₂)
      (⟨(fn : (a : N₁) → N₂) x.left, (fg : (a : G₁) → G₂) x.right⟩ : N₂ ⋊[φ₂] G₂)
      (⟨(fn : (a : N₁) → N₂) y.left, (fg : (a : G₁) → G₂) y.right⟩ : N₂ ⋊[φ₂] G₂)
have right : right.{u_6, u_7} (N := N₂) (φ := φ₂) ⟨(fn : (a : N₁) → N₂) (x * y).left, (fg : (a : G₁) → G₂) (x * y).right⟩ =
  (HMul.hMul (α := N₂ ⋊[φ₂] G₂) (β := N₂ ⋊[φ₂] G₂)
      (⟨(fn : (a : N₁) → N₂) x.left, (fg : (a : G₁) → G₂) x.right⟩ : N₂ ⋊[φ₂] G₂)
      (⟨(fn : (a : N₁) → N₂) y.left, (fg : (a : G₁) → G₂) y.right⟩ : N₂ ⋊[φ₂] G₂)).right
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst : Group N₁
inst_1 : Group G₁
inst_2 : Group N₂
inst_3 : Group G₂
φ₁ : MonoidHom.{u_5, u_4} G₁ (MulAut N₁)
φ₂ : MonoidHom.{u_7, u_6} G₂ (MulAut N₂)
fn : N₁ →* N₂
fg : G₁ →* G₂
h :
  ∀ (g : G₁),
    fn.comp (MulEquiv.toMonoidHom ((φ₁ : (a : G₁) → MulAut N₁) g)) =
      MonoidHom.comp (MulEquiv.toMonoidHom ((φ₂ : (a : G₂) → MulAut N₂) ((fg : (a : G₁) → G₂) g))) fn
⊢ (map fn fg h).comp inl = MonoidHom.comp inl fn
have h₁ : ∀ (x : N₁),
  Eq.{u_6 + 1} (α := N₂) (left.{u_6, u_7} (G := G₂) (φ := φ₂) (((map fn fg h).comp inl : (a : N₁) → N₂ ⋊[φ₂] G₂) x))
    (left.{u_6, u_7} (G := G₂) (φ := φ₂) ((MonoidHom.comp inl fn : (a : N₁) → N₂ ⋊[φ₂] G₂) x))
Tactic: ext
-- Lean 4 proof step from Mathlib.GroupTheory.SemidirectProduct (goal)
Goal:
N₁ : Type u_4
G₁ : Type u_5
N₂ : Type u_6
G₂ : Type u_7
inst : Group N₁
inst_1 : Group G₁
inst_2 : Group N₂
inst_3 : Group G₂
φ₁ : MonoidHom.{u_5, u_4} G₁ (MulAut N₁)
φ₂ : MonoidHom.{u_7, u_6} G₂ (MulAut N₂)
fn : N₁ →* N₂
fg : G₁ →* G₂
h :
  ∀ (g : G₁),
    fn.comp (MulEquiv.toMonoidHom ((φ₁ : (a : G₁) → MulAut N₁) g)) =
      MonoidHom.comp (MulEquiv.toMonoidHom ((φ₂ : (a : G₂) → MulAut N₂) ((fg : (a : G₁) → G₂) g))) fn
h₁ :
  ∀ (x : N₁),
    Eq.{u_6 + 1} (α := N₂) (left.{u_6, u_7} (G := G₂) (φ := φ₂) (((map fn fg h).comp inl : (a : N₁) → N₂ ⋊[φ₂] G₂) x))
      (left.{u_6, u_7} (G := G₂) (φ := φ₂) ((MonoidHom.comp inl fn : (a : N₁) → N₂ ⋊[φ₂] G₂) x))
⊢ (map fn fg h).comp inl = MonoidHom.comp inl fn
have h₂ : ∀ (x : N₁),
  Eq.{u_7 + 1} (α := G₂) (right.{u_6, u_7} (N := N₂) (φ := φ₂) (((map fn fg h).comp inl : (a : N₁) → N₂ ⋊[φ₂] G₂) x))
    (right.{u_6, u_7} (N := N₂) (φ := φ₂) ((MonoidHom.comp inl fn : (a : N₁) → N₂ ⋊[φ₂] G₂) x))
Tactic: ext