awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
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)
⊢ (lift fn fg h).comp inl = fn

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)
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
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:
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
g : G
⊢ Eq.{u_3 + 1} (α := H) ((lift fn fg h : (a : N ⋊[φ] G) → H) ((inr : (a : G) → N ⋊[φ] G) g : N ⋊[φ] G) : H)
    ((fg : (a : G) → H) g : H)

Tactic:
simp [lift]

Premises used: SemidirectProduct.lift
-- 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
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)
⊢ (lift fn fg h).comp inr = fg

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)
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
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:
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
F : N ⋊[φ] G →* H
x : G
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)
⊢ (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)

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)
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
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:
simp [inl_aut]

Premises used: SemidirectProduct.inl_aut
-- 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)
F : N ⋊[φ] G →* H
rw :
  ∀ (x : N ⋊[φ] G),
    Eq.{u_3 + 1} (α := H) ((F : (a : N ⋊[φ] G) → H) x : H)
      ((lift (F.comp inl) (F.comp inr) ⋯ : (a : N ⋊[φ] G) → H) x : H)
⊢ F = lift (F.comp inl) (F.comp inr) ⋯

Tactic:
rw [DFunLike.ext_iff]

Premises used: DFunLike.ext_iff
-- 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)
F : N ⋊[φ] G →* H
⊢ ∀ (x : N ⋊[φ] G),
    Eq.{u_3 + 1} (α := H) ((F : (a : N ⋊[φ] G) → H) x : H)
      ((lift (F.comp inl) (F.comp inr) ⋯ : (a : N ⋊[φ] G) → H) x : H)

Tactic:
simp only [lift, MonoidHom.comp_apply, MonoidHom.coe_mk, OneHom.coe_mk, ← map_mul,
    inl_left_mul_inr_right, forall_const]

Premises used: SemidirectProduct.inl_left_mul_inr_right, OneHom.coe_mk, map_mul, SemidirectProduct.lift, MonoidHom.coe_mk, forall_const, MonoidHom.comp_apply
-- 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)
f g : N ⋊[φ] G →* H
hl : f.comp inl = g.comp inl
hr : f.comp inr = g.comp inr
rw : Eq (α := N ⋊[φ] G →* H) (lift (f.comp inl) (f.comp inr) ⋯) (lift (g.comp inl) (g.comp inr) ⋯)
⊢ f = g

Tactic:
rw [lift_unique f, lift_unique g]

Premises used: SemidirectProduct.lift_unique
-- 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)
f g : N ⋊[φ] G →* H
hl : f.comp inl = g.comp inl
hr : f.comp inr = g.comp inr
⊢ Eq (α := N ⋊[φ] G →* H) (lift (f.comp inl) (f.comp inr) ⋯) (lift (g.comp inl) (g.comp inr) ⋯)

Tactic:
simp only [*]
-- Module: Mathlib.GroupTheory.SemidirectProduct
Goal:
N : Type u_1
G : Type u_2
H_1 : Type u_3
inst : Group N
inst_1 : Group G
inst_2 : Group H_1
φ : MonoidHom.{u_2, u_1} G (MulAut N)
fn : N →* H_1
fg : G →* H_1
h_1 :
  ∀ (g : G),
    fn.comp (MulEquiv.toMonoidHom ((φ : (a : G) → MulAut N) g)) =
      MonoidHom.comp (MulEquiv.toMonoidHom ((MulAut.conj : (a : H_1) → MulAut H_1) ((fg : (a : G) → H_1) g))) fn
H K : Subgroup G
h : K ≤ normalizer (↑H : Set G)
⊢ ∀ (g : ↥K),
    H.subtype.comp (MulEquiv.toMonoidHom ((H.normalizerMonoidHom.comp (inclusion h) : (a : ↥K) → MulAut ↥H) g)) =
      MonoidHom.comp (MulEquiv.toMonoidHom ((MulAut.conj : (a : G) → MulAut G) ((K.subtype : (a : ↥K) → G) g)))
        H.subtype

Tactic:
simp [DFunLike.ext_iff]

Premises used: DFunLike.ext_iff
-- 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)
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
⊢ Eq (α := N₂ ⋊[φ₂] G₂)
    (⟨(fn : (a : N₁) → N₂) (left.{u_4, u_5} (G := G₁) (φ := φ₁) 1),
        (fg : (a : G₁) → G₂) (right.{u_4, u_5} (N := N₁) (φ := φ₁) 1)⟩ :
      N₂ ⋊[φ₂] G₂)
    (1 : N₂ ⋊[φ₂] G₂)

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)
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₁
⊢ 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
-- 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)
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
right :
  SemidirectProduct.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
⊢ ⟨(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₂)

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)
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.{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:
simp_all
-- 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)
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₂)
⊢ 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:
simp_all
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
g : N₁ ⋊[φ₁] G₁
⊢ Eq.{u_6 + 1} (α := N₂) (left.{u_6, u_7} (G := G₂) (φ := φ₂) ((map fn fg h : (a : N₁ ⋊[φ₁] G₁) → N₂ ⋊[φ₂] G₂) g) : N₂)
    ((fn : (a : N₁) → N₂) g.left : N₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
g : N₁ ⋊[φ₁] G₁
⊢ Eq.{u_7 + 1} (α := G₂) (right.{u_6, u_7} (N := N₂) (φ := φ₂) ((map fn fg h : (a : N₁ ⋊[φ₁] G₁) → N₂ ⋊[φ₂] G₂) g) : G₂)
    ((fg : (a : G₁) → G₂) g.right : G₂)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
⊢ MonoidHom.comp rightHom (map fn fg h) = fg.comp rightHom

Tactic:
rfl

Premises used: SemidirectProduct.rightHom, rfl
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
n : N₁
⊢ Eq (α := N₂ ⋊[φ₂] G₂)
    ((map fn fg h : (a : N₁ ⋊[φ₁] G₁) → N₂ ⋊[φ₂] G₂) ((inl : (a : N₁) → N₁ ⋊[φ₁] G₁) n) : N₂ ⋊[φ₂] G₂)
    ((inl : (a : N₂) → N₂ ⋊[φ₂] G₂) ((fn : (a : N₁) → N₂) n) : N₂ ⋊[φ₂] G₂)

Tactic:
simp [map]

Premises used: SemidirectProduct.map
-- Module: Mathlib.GroupTheory.SemidirectProduct
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))
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))
⊢ (map fn fg h).comp inl = MonoidHom.comp inl fn

Tactic:
ext
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
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:
simp
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
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:
simp
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
g : G₁
⊢ Eq (α := N₂ ⋊[φ₂] G₂)
    ((map fn fg h : (a : N₁ ⋊[φ₁] G₁) → N₂ ⋊[φ₂] G₂) ((inr : (a : G₁) → N₁ ⋊[φ₁] G₁) g) : N₂ ⋊[φ₂] G₂)
    ((inr : (a : G₂) → N₂ ⋊[φ₂] G₂) ((fg : (a : G₁) → G₂) g) : N₂ ⋊[φ₂] G₂)

Tactic:
simp [map]

Premises used: SemidirectProduct.map
-- Module: Mathlib.GroupTheory.SemidirectProduct
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 : G₁),
    Eq.{u_6 + 1} (α := N₂) (left.{u_6, u_7} (G := G₂) (φ := φ₂) (((map fn fg h).comp inr : (a : G₁) → N₂ ⋊[φ₂] G₂) x))
      (left.{u_6, u_7} (G := G₂) (φ := φ₂) ((MonoidHom.comp inr fg : (a : G₁) → N₂ ⋊[φ₂] G₂) x))
h₂ :
  ∀ (x : G₁),
    Eq.{u_7 + 1} (α := G₂) (right.{u_6, u_7} (N := N₂) (φ := φ₂) (((map fn fg h).comp inr : (a : G₁) → N₂ ⋊[φ₂] G₂) x))
      (right.{u_6, u_7} (N := N₂) (φ := φ₂) ((MonoidHom.comp inr fg : (a : G₁) → N₂ ⋊[φ₂] G₂) x))
⊢ (map fn fg h).comp inr = MonoidHom.comp inr fg

Tactic:
ext
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
x : G₁
⊢ Eq.{u_6 + 1} (α := N₂) (left.{u_6, u_7} (G := G₂) (φ := φ₂) (((map fn fg h).comp inr : (a : G₁) → N₂ ⋊[φ₂] G₂) x))
    (left.{u_6, u_7} (G := G₂) (φ := φ₂) ((MonoidHom.comp inr fg : (a : G₁) → N₂ ⋊[φ₂] G₂) x))

Tactic:
simp [map]

Premises used: SemidirectProduct.map
-- Module: Mathlib.GroupTheory.SemidirectProduct
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
x : G₁
⊢ Eq.{u_7 + 1} (α := G₂) (right.{u_6, u_7} (N := N₂) (φ := φ₂) (((map fn fg h).comp inr : (a : G₁) → N₂ ⋊[φ₂] G₂) x))
    (right.{u_6, u_7} (N := N₂) (φ := φ₂) ((MonoidHom.comp inr fg : (a : G₁) → N₂ ⋊[φ₂] G₂) x))

Tactic:
simp [map]

Premises used: SemidirectProduct.map
-- 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)
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₁),
    MulEquiv.trans ((φ₁ : (a : G₁) → MulAut N₁) g) fn = fn.trans ((φ₂ : (a : G₂) → MulAut N₂) ((fg : (a : G₁) → G₂) g))
x : N₁ ⋊[φ₁] G₁
⊢ (fun (x : N₂ ⋊[φ₂] G₂) ↦ (⟨(fn.symm : (a : N₂) → N₁) x.left, (fg.symm : (a : G₂) → G₁) x.right⟩ : N₁ ⋊[φ₁] G₁))
      ((fun (x : N₁ ⋊[φ₁] G₁) ↦ (⟨(fn : (a : N₁) → N₂) x.left, (fg : (a : G₁) → G₂) x.right⟩ : N₂ ⋊[φ₂] G₂)) x) =
    x

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)
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₁),
    MulEquiv.trans ((φ₁ : (a : G₁) → MulAut N₁) g) fn = fn.trans ((φ₂ : (a : G₂) → MulAut N₂) ((fg : (a : G₁) → G₂) g))
x : N₂ ⋊[φ₂] G₂
⊢ (fun (x : N₁ ⋊[φ₁] G₁) ↦ (⟨(fn : (a : N₁) → N₂) x.left, (fg : (a : G₁) → G₂) x.right⟩ : N₂ ⋊[φ₂] G₂))
      ((fun (x : N₂ ⋊[φ₂] G₂) ↦ (⟨(fn.symm : (a : N₂) → N₁) x.left, (fg.symm : (a : G₂) → G₁) x.right⟩ : N₁ ⋊[φ₁] G₁))
        x) =
    x

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)
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₁),
    MulEquiv.trans ((φ₁ : (a : G₁) → MulAut N₁) g) fn = fn.trans ((φ₂ : (a : G₂) → MulAut N₂) ((fg : (a : G₁) → G₂) g))
x y : N₁ ⋊[φ₁] G₁
⊢ Eq.{u_6 + 1} (α := N₂) ((MulEquiv.trans ((φ₁ : (a : G₁) → MulAut N₁) x.right) fn : (a : N₁) → N₂) y.left : N₂)
    ((fn.trans ((φ₂ : (a : G₂) → MulAut N₂) ((fg : (a : G₁) → G₂) x.right)) : (a : N₁) → N₂) y.left : N₂)

Tactic:
replace h := DFunLike.ext_iff.1 (h x.right) y.left