[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
a b c : N ⋊[φ] G
⊢ (a * b * c).left = (a * (b * c)).left
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
a b c : N ⋊[φ] G
⊢ (a * b * c).right = (a * (b * c)).right
[PROOFSTEP]
simp [mul_assoc]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
a : N ⋊[φ] G
⊢ (1 * a).left = a.left
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
a : N ⋊[φ] G
⊢ (a * 1).left = a.left
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
a : N ⋊[φ] G
⊢ (a⁻¹ * a).left = 1.left
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
a : N ⋊[φ] G
⊢ (a⁻¹ * a).right = 1.right
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
⊢ ∀ (x y : N),
    OneHom.toFun
        { toFun := fun n => { left := n, right := 1 },
          map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
        (x * y) =
      OneHom.toFun
          { toFun := fun n => { left := n, right := 1 },
            map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
          x *
        OneHom.toFun
          { toFun := fun n => { left := n, right := 1 },
            map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
          y
[PROOFSTEP]
intros
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : N
⊢ OneHom.toFun
      { toFun := fun n => { left := n, right := 1 },
        map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
      (x✝ * y✝) =
    OneHom.toFun
        { toFun := fun n => { left := n, right := 1 },
          map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
        x✝ *
      OneHom.toFun
        { toFun := fun n => { left := n, right := 1 },
          map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
        y✝
[PROOFSTEP]
ext
[GOAL]
case left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : N
⊢ (OneHom.toFun
        { toFun := fun n => { left := n, right := 1 },
          map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
        (x✝ * y✝)).left =
    (OneHom.toFun
          { toFun := fun n => { left := n, right := 1 },
            map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
          x✝ *
        OneHom.toFun
          { toFun := fun n => { left := n, right := 1 },
            map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
          y✝).left
[PROOFSTEP]
simp only [mul_left, map_one, MulAut.one_apply, mul_right, mul_one]
[GOAL]
case right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : N
⊢ (OneHom.toFun
        { toFun := fun n => { left := n, right := 1 },
          map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
        (x✝ * y✝)).right =
    (OneHom.toFun
          { toFun := fun n => { left := n, right := 1 },
            map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
          x✝ *
        OneHom.toFun
          { toFun := fun n => { left := n, right := 1 },
            map_one' := (_ : (fun n => { left := n, right := 1 }) 1 = (fun n => { left := n, right := 1 }) 1) }
          y✝).right
[PROOFSTEP]
simp only [mul_left, map_one, MulAut.one_apply, mul_right, mul_one]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
⊢ ∀ (x y : G),
    OneHom.toFun
        { toFun := fun g => { left := 1, right := g },
          map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
        (x * y) =
      OneHom.toFun
          { toFun := fun g => { left := 1, right := g },
            map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
          x *
        OneHom.toFun
          { toFun := fun g => { left := 1, right := g },
            map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
          y
[PROOFSTEP]
intros
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : G
⊢ OneHom.toFun
      { toFun := fun g => { left := 1, right := g },
        map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
      (x✝ * y✝) =
    OneHom.toFun
        { toFun := fun g => { left := 1, right := g },
          map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
        x✝ *
      OneHom.toFun
        { toFun := fun g => { left := 1, right := g },
          map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
        y✝
[PROOFSTEP]
ext
[GOAL]
case left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : G
⊢ (OneHom.toFun
        { toFun := fun g => { left := 1, right := g },
          map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
        (x✝ * y✝)).left =
    (OneHom.toFun
          { toFun := fun g => { left := 1, right := g },
            map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
          x✝ *
        OneHom.toFun
          { toFun := fun g => { left := 1, right := g },
            map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
          y✝).left
[PROOFSTEP]
simp
[GOAL]
case right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ y✝ : G
⊢ (OneHom.toFun
        { toFun := fun g => { left := 1, right := g },
          map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
        (x✝ * y✝)).right =
    (OneHom.toFun
          { toFun := fun g => { left := 1, right := g },
            map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
          x✝ *
        OneHom.toFun
          { toFun := fun g => { left := 1, right := g },
            map_one' := (_ : (fun g => { left := 1, right := g }) 1 = (fun g => { left := 1, right := g }) 1) }
          y✝).right
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
g : G
n : N
⊢ ↑inl (↑(↑φ g) n) = ↑inr g * ↑inl n * ↑inr g⁻¹
[PROOFSTEP]
ext
[GOAL]
case left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
g : G
n : N
⊢ (↑inl (↑(↑φ g) n)).left = (↑inr g * ↑inl n * ↑inr g⁻¹).left
[PROOFSTEP]
simp
[GOAL]
case right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
g : G
n : N
⊢ (↑inl (↑(↑φ g) n)).right = (↑inr g * ↑inl n * ↑inr g⁻¹).right
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
g : G
n : N
⊢ ↑inl (↑(↑φ g)⁻¹ n) = ↑inr g⁻¹ * ↑inl n * ↑inr g
[PROOFSTEP]
rw [← MonoidHom.map_inv, inl_aut, inv_inv]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
g : G
n : N
⊢ { left := n, right := g } = ↑inl n * ↑inr g
[PROOFSTEP]
ext
[GOAL]
case left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
g : G
n : N
⊢ { left := n, right := g }.left = (↑inl n * ↑inr g).left
[PROOFSTEP]
simp
[GOAL]
case right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
g : G
n : N
⊢ { left := n, right := g }.right = (↑inl n * ↑inr g).right
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x : N ⋊[φ] G
⊢ ↑inl x.left * ↑inr x.right = x
[PROOFSTEP]
ext
[GOAL]
case left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x : N ⋊[φ] G
⊢ (↑inl x.left * ↑inr x.right).left = x.left
[PROOFSTEP]
simp
[GOAL]
case right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x : N ⋊[φ] G
⊢ (↑inl x.left * ↑inr x.right).right = x.right
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
⊢ MonoidHom.comp rightHom inl = 1
[PROOFSTEP]
ext
[GOAL]
case h
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ : N
⊢ ↑(MonoidHom.comp rightHom inl) x✝ = ↑1 x✝
[PROOFSTEP]
simp [rightHom]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
⊢ MonoidHom.comp rightHom inr = MonoidHom.id G
[PROOFSTEP]
ext
[GOAL]
case h
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ : G
⊢ ↑(MonoidHom.comp rightHom inr) x✝ = ↑(MonoidHom.id G) x✝
[PROOFSTEP]
simp [rightHom]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
n : N
⊢ ↑rightHom (↑inl n) = 1
[PROOFSTEP]
simp [rightHom]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
g : G
⊢ ↑rightHom (↑inr g) = g
[PROOFSTEP]
simp [rightHom]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x✝ : N ⋊[φ] G
⊢ x✝ ∈ MonoidHom.range inl → x✝ ∈ MonoidHom.ker rightHom
[PROOFSTEP]
simp (config := { contextual := true }) [MonoidHom.mem_ker, eq_comm]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x : N ⋊[φ] G
hx : x ∈ MonoidHom.ker rightHom
⊢ ↑inl x.left = x
[PROOFSTEP]
ext
[GOAL]
case left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x : N ⋊[φ] G
hx : x ∈ MonoidHom.ker rightHom
⊢ (↑inl x.left).left = x.left
[PROOFSTEP]
simp_all [MonoidHom.mem_ker]
[GOAL]
case right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
x : N ⋊[φ] G
hx : x ∈ MonoidHom.ker rightHom
⊢ (↑inl x.left).right = x.right
[PROOFSTEP]
simp_all [MonoidHom.mem_ker]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁✝ : N →* H
f₂✝ : G →* H
h✝ :
  ∀ (g : G),
    MonoidHom.comp f₁✝ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂✝ g))) f₁✝
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
⊢ (fun a => ↑f₁ a.left * ↑f₂ a.right) 1 = 1
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁✝ : N →* H
f₂✝ : G →* H
h✝ :
  ∀ (g : G),
    MonoidHom.comp f₁✝ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂✝ g))) f₁✝
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
a b : N ⋊[φ] G
⊢ OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } (a * b) =
    OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } a *
      OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } b
[PROOFSTEP]
have := fun n g ↦ FunLike.ext_iff.1 (h n) g
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁✝ : N →* H
f₂✝ : G →* H
h✝ :
  ∀ (g : G),
    MonoidHom.comp f₁✝ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂✝ g))) f₁✝
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
a b : N ⋊[φ] G
this :
  ∀ (n : G) (g : N),
    ↑(MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ n))) g =
      ↑(MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ n))) f₁) g
⊢ OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } (a * b) =
    OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } a *
      OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } b
[PROOFSTEP]
simp only [MulAut.conj_apply, MonoidHom.comp_apply, MulEquiv.coe_toMonoidHom] at this 
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁✝ : N →* H
f₂✝ : G →* H
h✝ :
  ∀ (g : G),
    MonoidHom.comp f₁✝ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂✝ g))) f₁✝
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
a b : N ⋊[φ] G
this : ∀ (n : G) (g : N), ↑f₁ (↑(↑φ n) g) = ↑f₂ n * ↑f₁ g * (↑f₂ n)⁻¹
⊢ OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } (a * b) =
    OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } a *
      OneHom.toFun { toFun := fun a => ↑f₁ a.left * ↑f₂ a.right, map_one' := (_ : ↑f₁ 1 * ↑f₂ 1 = 1) } b
[PROOFSTEP]
simp only [mul_left, mul_right, map_mul, this, mul_assoc, inv_mul_cancel_left]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
n : N
⊢ ↑(lift f₁ f₂ h) (↑inl n) = ↑f₁ n
[PROOFSTEP]
simp [lift]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
⊢ MonoidHom.comp (lift f₁ f₂ h) inl = f₁
[PROOFSTEP]
ext
[GOAL]
case h
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
x✝ : N
⊢ ↑(MonoidHom.comp (lift f₁ f₂ h) inl) x✝ = ↑f₁ x✝
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
g : G
⊢ ↑(lift f₁ f₂ h) (↑inr g) = ↑f₂ g
[PROOFSTEP]
simp [lift]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
⊢ MonoidHom.comp (lift f₁ f₂ h) inr = f₂
[PROOFSTEP]
ext
[GOAL]
case h
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
x✝ : G
⊢ ↑(MonoidHom.comp (lift f₁ f₂ h) inr) x✝ = ↑f₂ x✝
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
F : N ⋊[φ] G →* H
x✝ : G
⊢ MonoidHom.comp (MonoidHom.comp F inl) (MulEquiv.toMonoidHom (↑φ x✝)) =
    MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp F inr) x✝))) (MonoidHom.comp F inl)
[PROOFSTEP]
ext
[GOAL]
case h
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
F : N ⋊[φ] G →* H
x✝¹ : G
x✝ : N
⊢ ↑(MonoidHom.comp (MonoidHom.comp F inl) (MulEquiv.toMonoidHom (↑φ x✝¹))) x✝ =
    ↑(MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp F inr) x✝¹))) (MonoidHom.comp F inl)) x✝
[PROOFSTEP]
simp [inl_aut]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
F : N ⋊[φ] G →* H
⊢ F =
    lift (MonoidHom.comp F inl) (MonoidHom.comp F inr)
      (_ :
        ∀ (x : G),
          MonoidHom.comp (MonoidHom.comp F inl) (MulEquiv.toMonoidHom (↑φ x)) =
            MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp F inr) x))) (MonoidHom.comp F inl))
[PROOFSTEP]
rw [FunLike.ext_iff]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
F : N ⋊[φ] G →* H
⊢ ∀ (x : N ⋊[φ] G),
    ↑F x =
      ↑(lift (MonoidHom.comp F inl) (MonoidHom.comp F inr)
            (_ :
              ∀ (x : G),
                MonoidHom.comp (MonoidHom.comp F inl) (MulEquiv.toMonoidHom (↑φ x)) =
                  MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp F inr) x)))
                    (MonoidHom.comp F inl)))
        x
[PROOFSTEP]
simp only [lift, MonoidHom.comp_apply, MonoidHom.coe_mk, OneHom.coe_mk, ← map_mul, inl_left_mul_inr_right, forall_const]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
f g : N ⋊[φ] G →* H
hl : MonoidHom.comp f inl = MonoidHom.comp g inl
hr : MonoidHom.comp f inr = MonoidHom.comp g inr
⊢ f = g
[PROOFSTEP]
rw [lift_unique f, lift_unique g]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
f₁ : N →* H
f₂ : G →* H
h :
  ∀ (g : G),
    MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑f₂ g))) f₁
f g : N ⋊[φ] G →* H
hl : MonoidHom.comp f inl = MonoidHom.comp g inl
hr : MonoidHom.comp f inr = MonoidHom.comp g inr
⊢ lift (MonoidHom.comp f inl) (MonoidHom.comp f inr)
      (_ :
        ∀ (x : G),
          MonoidHom.comp (MonoidHom.comp f inl) (MulEquiv.toMonoidHom (↑φ x)) =
            MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp f inr) x))) (MonoidHom.comp f inl)) =
    lift (MonoidHom.comp g inl) (MonoidHom.comp g inr)
      (_ :
        ∀ (x : G),
          MonoidHom.comp (MonoidHom.comp g inl) (MulEquiv.toMonoidHom (↑φ x)) =
            MonoidHom.comp (MulEquiv.toMonoidHom (↑MulAut.conj (↑(MonoidHom.comp g inr) x))) (MonoidHom.comp g inl))
[PROOFSTEP]
simp only [*]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
⊢ (fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right }) 1 = 1
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
x y : N ⋊[φ] G
⊢ OneHom.toFun
      { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
        map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
          map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
        x *
      OneHom.toFun
        { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
          map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
        y
[PROOFSTEP]
replace h := FunLike.ext_iff.1 (h x.right) y.left
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
x y : N ⋊[φ] G
h :
  ↑(MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ x.right))) y.left =
    ↑(MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ x.right))) f₁) y.left
⊢ OneHom.toFun
      { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
        map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
      (x * y) =
    OneHom.toFun
        { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
          map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
        x *
      OneHom.toFun
        { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
          map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
        y
[PROOFSTEP]
ext
[GOAL]
case left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
x y : N ⋊[φ] G
h :
  ↑(MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ x.right))) y.left =
    ↑(MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ x.right))) f₁) y.left
⊢ (OneHom.toFun
        { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
          map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
        (x * y)).left =
    (OneHom.toFun
          { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
            map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
          x *
        OneHom.toFun
          { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
            map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
          y).left
[PROOFSTEP]
simp_all
[GOAL]
case right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
x y : N ⋊[φ] G
h :
  ↑(MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ x.right))) y.left =
    ↑(MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ x.right))) f₁) y.left
⊢ (OneHom.toFun
        { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
          map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
        (x * y)).right =
    (OneHom.toFun
          { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
            map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
          x *
        OneHom.toFun
          { toFun := fun x => { left := ↑f₁ x.left, right := ↑f₂ x.right },
            map_one' := (_ : { left := ↑f₁ 1, right := ↑f₂ 1 } = 1) }
          y).right
[PROOFSTEP]
simp_all
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
n : N
⊢ ↑(map f₁ f₂ h) (↑inl n) = ↑inl (↑f₁ n)
[PROOFSTEP]
simp [map]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
⊢ MonoidHom.comp (map f₁ f₂ h) inl = MonoidHom.comp inl f₁
[PROOFSTEP]
ext
[GOAL]
case h.left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
x✝ : N
⊢ (↑(MonoidHom.comp (map f₁ f₂ h) inl) x✝).left = (↑(MonoidHom.comp inl f₁) x✝).left
[PROOFSTEP]
simp
[GOAL]
case h.right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
x✝ : N
⊢ (↑(MonoidHom.comp (map f₁ f₂ h) inl) x✝).right = (↑(MonoidHom.comp inl f₁) x✝).right
[PROOFSTEP]
simp
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
g : G
⊢ ↑(map f₁ f₂ h) (↑inr g) = ↑inr (↑f₂ g)
[PROOFSTEP]
simp [map]
[GOAL]
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
⊢ MonoidHom.comp (map f₁ f₂ h) inr = MonoidHom.comp inr f₂
[PROOFSTEP]
ext
[GOAL]
case h.left
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
x✝ : G
⊢ (↑(MonoidHom.comp (map f₁ f₂ h) inr) x✝).left = (↑(MonoidHom.comp inr f₂) x✝).left
[PROOFSTEP]
simp [map]
[GOAL]
case h.right
N : Type u_1
G : Type u_2
H : Type u_3
inst✝⁴ : Group N
inst✝³ : Group G
inst✝² : Group H
φ : G →* MulAut N
N₁ : Type u_4
G₁ : Type u_5
inst✝¹ : Group N₁
inst✝ : Group G₁
φ₁ : G₁ →* MulAut N₁
f₁ : N →* N₁
f₂ : G →* G₁
h : ∀ (g : G), MonoidHom.comp f₁ (MulEquiv.toMonoidHom (↑φ g)) = MonoidHom.comp (MulEquiv.toMonoidHom (↑φ₁ (↑f₂ g))) f₁
x✝ : G
⊢ (↑(MonoidHom.comp (map f₁ f₂ h) inr) x✝).right = (↑(MonoidHom.comp inr f₂) x✝).right
[PROOFSTEP]
simp [map]
