awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.GroupTheory.SchurZassenhaus
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
hN3 : Finite G
⊢ ∃ (H : Subgroup G), N.IsComplement' H

Tactic:
exact exists_right_complement'_of_coprime_aux' rfl hN

Premises used: _private.0.Subgroup.exists_right_complement'_of_coprime_aux', rfl
-- Module: Mathlib.GroupTheory.SchurZassenhaus
Goal:
G : Type u
inst : Group G
N : Subgroup G
inst_1 : N.Normal
hN : (Nat.card.{u} ↥N).Coprime N.index
⊢ ∃ (H : Subgroup G), H.IsComplement' N

Tactic:
Exists.imp (fun _ => IsComplement'.symm) (exists_right_complement'_of_coprime hN)

Premises used: Exists.imp, Subgroup.exists_right_complement'_of_coprime, Subgroup.IsComplement'.symm
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
a b : N ⋊[φ] G
⊢ a * b =
    ⟨HMul.hMul (β := N) a.left ((((φ : (a : G) → MulAut N) a.right : MulAut N) : (a : N) → N) b.left : N),
      a.right * b.right⟩

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
a b : N ⋊[φ] G
⊢ (a * b).left = HMul.hMul (β := N) a.left ((((φ : (a : G) → MulAut N) a.right : MulAut N) : (a : N) → N) b.left : N)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
a b : N ⋊[φ] G
⊢ (a * b).right = a.right * b.right

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.SemidirectProduct
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.{u_1 + 1} (α := N) (left.{u_1, u_2} (G := G) (φ := φ) 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.SemidirectProduct
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.{u_2 + 1} (α := G) (right.{u_1, u_2} (N := N) (φ := φ) 1) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
a : N ⋊[φ] G
⊢ a⁻¹.left = (((φ : (a : G) → MulAut N) a.right⁻¹ : MulAut N) : (a : N) → N) a.left⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
a : N ⋊[φ] G
⊢ a⁻¹.right = a.right⁻¹

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.SemidirectProduct
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)
a b c : N ⋊[φ] G
⊢ (a * b * c).left = (a * (b * c)).left

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.SemidirectProduct
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)
a b c : N ⋊[φ] G
⊢ (a * b * c).right = (a * (b * c)).right

Tactic:
simp [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.GroupTheory.SemidirectProduct
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)
a : N ⋊[φ] G
⊢ (1 * a).left = a.left

Tactic:
simp
-- Module: Mathlib.GroupTheory.SemidirectProduct
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)
a : N ⋊[φ] G
⊢ (a * 1).left = a.left

Tactic:
simp
-- Module: Mathlib.GroupTheory.SemidirectProduct
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)
a : N ⋊[φ] G
⊢ (a⁻¹ * a).left = left.{u_1, u_2} (G := G) (φ := φ) 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.SemidirectProduct
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)
a : N ⋊[φ] G
⊢ (a⁻¹ * a).right = right.{u_1, u_2} (N := N) (φ := φ) 1

Tactic:
simp
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
right :
  SemidirectProduct.right (φ := φ) ⟨x * y, 1⟩ =
    (HMul.hMul (α := N ⋊[φ] G) (⟨x, 1⟩ : N ⋊[φ] G) (⟨y, 1⟩ : N ⋊[φ] G)).right
⊢ ⟨x * y, 1⟩ = HMul.hMul (α := N ⋊[φ] G) (⟨x, 1⟩ : N ⋊[φ] G) (⟨y, 1⟩ : N ⋊[φ] G)

Tactic:
ext
-- Module: Mathlib.GroupTheory.SemidirectProduct
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.{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:
simp only [mul_left, map_one, MulAut.one_apply, mul_right, mul_one]

Premises used: MulAut.one_apply, map_one, SemidirectProduct.mul_right, mul_one, SemidirectProduct.mul_left
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
⊢ right (φ := φ) ⟨x * y, 1⟩ = (HMul.hMul (α := N ⋊[φ] G) (⟨x, 1⟩ : N ⋊[φ] G) (⟨y, 1⟩ : N ⋊[φ] G)).right

Tactic:
simp only [mul_left, map_one, MulAut.one_apply, mul_right, mul_one]

Premises used: MulAut.one_apply, map_one, SemidirectProduct.mul_right, mul_one, SemidirectProduct.mul_left
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
n : N
⊢ left.{u_1, u_2} (G := G) (φ := φ) ((inl : (a : N) → N ⋊[φ] G) n) = n

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
n : N
⊢ Eq.{u_2 + 1} (α := G) (right.{u_1, u_2} (N := N) (φ := φ) ((inl : (a : N) → N ⋊[φ] G) n)) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
⊢ Function.Injective (α := N) (β := N ⋊[φ] G) (⇑inl : (a : N) → N ⋊[φ] G)

Tactic:
Function.injective_iff_hasLeftInverse.2 ⟨left, left_inl⟩

Premises used: Iff.mpr, Function.injective_iff_hasLeftInverse, SemidirectProduct.left_inl, SemidirectProduct.left, Exists.intro
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
n₁ n₂ : N
⊢ Eq (α := N ⋊[φ] G) ((inl : (a : N) → N ⋊[φ] G) n₁ : N ⋊[φ] G) ((inl : (a : N) → N ⋊[φ] G) n₂ : N ⋊[φ] G) ↔ n₁ = n₂

Tactic:
inl_injective.eq_iff

Premises used: Function.Injective.eq_iff, SemidirectProduct.inl_injective
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
right :
  SemidirectProduct.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
⊢ ⟨1, x * y⟩ = HMul.hMul (α := N ⋊[φ] G) (⟨1, x⟩ : N ⋊[φ] G) (⟨1, y⟩ : N ⋊[φ] G)

Tactic:
ext
-- Module: Mathlib.GroupTheory.SemidirectProduct
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 (φ := φ) ⟨1, x * y⟩ = (HMul.hMul (α := N ⋊[φ] G) (⟨1, x⟩ : N ⋊[φ] G) (⟨1, y⟩ : N ⋊[φ] G)).left

Tactic:
simp
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
⊢ 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:
simp
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
⊢ Eq.{u_1 + 1} (α := N) (left.{u_1, u_2} (G := G) (φ := φ) ((inr : (a : G) → N ⋊[φ] G) g)) 1

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
⊢ right.{u_1, u_2} (N := N) (φ := φ) ((inr : (a : G) → N ⋊[φ] G) g) = g

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
⊢ Function.Injective (α := G) (β := N ⋊[φ] G) (⇑inr : (a : G) → N ⋊[φ] G)

Tactic:
Function.injective_iff_hasLeftInverse.2 ⟨right, right_inr⟩

Premises used: Iff.mpr, SemidirectProduct.right, Function.injective_iff_hasLeftInverse, SemidirectProduct.right_inr, Exists.intro
-- Module: Mathlib.GroupTheory.SemidirectProduct
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₂ : G
⊢ Eq (α := N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g₁ : N ⋊[φ] G) ((inr : (a : G) → N ⋊[φ] G) g₂ : N ⋊[φ] G) ↔ g₁ = g₂

Tactic:
inr_injective.eq_iff

Premises used: SemidirectProduct.inr_injective, Function.Injective.eq_iff
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
right :
  SemidirectProduct.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
⊢ (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:
ext
-- Module: Mathlib.GroupTheory.SemidirectProduct
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.{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:
simp
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
⊢ 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:
simp
-- Module: Mathlib.GroupTheory.SemidirectProduct
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)
rw₂ 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)

Tactic:
rw [← map_inv, inl_aut, inv_inv]

Premises used: SemidirectProduct.inl_aut, map_inv, inv_inv
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
right :
  SemidirectProduct.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
⊢ ⟨n, g⟩ =
    HMul.hMul (α := N ⋊[φ] G) (β := N ⋊[φ] G) ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G)
      ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G)

Tactic:
ext
-- Module: Mathlib.GroupTheory.SemidirectProduct
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 (φ := φ) (⟨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:
simp
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
⊢ 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:
simp
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
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
⊢ 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

Tactic:
ext
-- Module: Mathlib.GroupTheory.SemidirectProduct
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)).left =
    x.left

Tactic:
simp
-- Module: Mathlib.GroupTheory.SemidirectProduct
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)).right =
    x.right

Tactic:
simp
-- Module: Mathlib.GroupTheory.SemidirectProduct
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 (α := (a : N ⋊[φ] G) → G) (⇑rightHom : (a : N ⋊[φ] G) → G) right

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
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)
⊢ Eq (α := N →* G) (MonoidHom.comp (N := N ⋊[φ] G) rightHom inl) 1

Tactic:
ext
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
⊢ Eq.{u_2 + 1} (α := G) ((MonoidHom.comp (N := N ⋊[φ] G) rightHom inl : (a : N) → G) x : G) ((1 : (a : N) → G) x : G)

Tactic:
simp [rightHom]

Premises used: SemidirectProduct.rightHom
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
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)
⊢ Eq (α := G →* G) (MonoidHom.comp (N := N ⋊[φ] G) rightHom inr) (MonoidHom.id G)

Tactic:
ext
-- Module: Mathlib.GroupTheory.SemidirectProduct
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 : G
⊢ Eq (α := G) ((MonoidHom.comp (N := N ⋊[φ] G) rightHom inr : (a : G) → G) x : G) ((MonoidHom.id G : (a : G) → G) x : G)

Tactic:
simp [rightHom]

Premises used: SemidirectProduct.rightHom
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
n : N
⊢ Eq.{u_2 + 1} (α := G) ((rightHom : (a : N ⋊[φ] G) → G) ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G) : G) (1 : G)

Tactic:
simp [rightHom]

Premises used: SemidirectProduct.rightHom
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
⊢ (rightHom : (a : N ⋊[φ] G) → G) ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G) = g

Tactic:
simp [rightHom]

Premises used: SemidirectProduct.rightHom
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
inst : Group N
inst_1 : Group G
φ : MonoidHom.{u_2, u_1} G (MulAut N)
⊢ Function.Surjective (α := N ⋊[φ] G) (β := G) (⇑rightHom : (a : N ⋊[φ] G) → G)

Tactic:
Function.surjective_iff_hasRightInverse.2 ⟨inr, rightHom_inr⟩

Premises used: Iff.mpr, Function.surjective_iff_hasRightInverse, SemidirectProduct.inr, SemidirectProduct.rightHom_inr, Exists.intro, DFunLike.coe
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
⊢ Membership.mem (γ := Subgroup (N ⋊[φ] G)) (MonoidHom.range inl) x →
    Membership.mem (γ := Subgroup (N ⋊[φ] G)) (MonoidHom.ker rightHom) x

Tactic:
simp +contextual [MonoidHom.mem_ker, eq_comm]

Premises used: MonoidHom.mem_ker, eq_comm
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
right : SemidirectProduct.right.{u_1, u_2} (N := N) (φ := φ) ((inl : (a : N) → N ⋊[φ] G) x.left) = x.right
⊢ (inl : (a : N) → N ⋊[φ] G) x.left = x

Tactic:
ext
-- Module: Mathlib.GroupTheory.SemidirectProduct
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.{u_1, u_2} (G := G) (φ := φ) ((inl : (a : N) → N ⋊[φ] G) x.left) = x.left

Tactic:
simp_all [MonoidHom.mem_ker]

Premises used: MonoidHom.mem_ker
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
⊢ right.{u_1, u_2} (N := N) (φ := φ) ((inl : (a : N) → N ⋊[φ] G) x.left) = x.right

Tactic:
simp_all [MonoidHom.mem_ker]

Premises used: MonoidHom.mem_ker
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
⊢ HMul.hMul (α := H) (β := H) ((fn : (a : N) → H) (left.{u_1, u_2} (G := G) (φ := φ) 1) : H)
      ((fg : (a : G) → H) (right.{u_1, u_2} (N := N) (φ := φ) 1) : H) =
    1

Tactic:
simp
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
⊢ ∀ (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
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
this :
  ∀ (n : G) (g : N),
    (fn : (a : N) → H) ((((φ : (a : G) → MulAut N) n : MulAut N) : (a : N) → N) g : N) =
      HMul.hMul (β := H) (HMul.hMul (α := H) (β := H) ((fg : (a : G) → H) n : H) ((fn : (a : N) → H) g : H))
        (((fg : (a : G) → H) n)⁻¹ : H)
⊢ 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)

Tactic:
simp only [mul_left, mul_right, map_mul, this, mul_assoc, inv_mul_cancel_left]

Premises used: inv_mul_cancel_left, mul_assoc, map_mul, SemidirectProduct.mul_right, SemidirectProduct.mul_left
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
n : N
⊢ Eq.{u_3 + 1} (α := H) ((lift fn fg h : (a : N ⋊[φ] G) → H) ((inl : (a : N) → N ⋊[φ] G) n : N ⋊[φ] G) : H)
    ((fn : (a : N) → H) n : H)

Tactic:
simp [lift]

Premises used: SemidirectProduct.lift