[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Mul α
inst✝ : MulOneClass β
f : α →ₙ* β
x y : WithOne α
⊢ OneHom.toFun
      { toFun := fun x => Option.casesOn x 1 ↑f,
        map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
      (1 * y) =
    OneHom.toFun
        { toFun := fun x => Option.casesOn x 1 ↑f,
          map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
        1 *
      OneHom.toFun
        { toFun := fun x => Option.casesOn x 1 ↑f,
          map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
        y
[PROOFSTEP]
rw [one_mul]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Mul α
inst✝ : MulOneClass β
f : α →ₙ* β
x y : WithOne α
⊢ OneHom.toFun
      { toFun := fun x => Option.casesOn x 1 ↑f,
        map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
      y =
    OneHom.toFun
        { toFun := fun x => Option.casesOn x 1 ↑f,
          map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
        1 *
      OneHom.toFun
        { toFun := fun x => Option.casesOn x 1 ↑f,
          map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
        y
[PROOFSTEP]
exact (one_mul _).symm
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Mul α
inst✝ : MulOneClass β
f : α →ₙ* β
x✝ y : WithOne α
x : α
⊢ OneHom.toFun
      { toFun := fun x => Option.casesOn x 1 ↑f,
        map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
      (↑x * 1) =
    OneHom.toFun
        { toFun := fun x => Option.casesOn x 1 ↑f,
          map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
        ↑x *
      OneHom.toFun
        { toFun := fun x => Option.casesOn x 1 ↑f,
          map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
        1
[PROOFSTEP]
rw [mul_one]
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝¹ : Mul α
inst✝ : MulOneClass β
f : α →ₙ* β
x✝ y : WithOne α
x : α
⊢ OneHom.toFun
      { toFun := fun x => Option.casesOn x 1 ↑f,
        map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
      ↑x =
    OneHom.toFun
        { toFun := fun x => Option.casesOn x 1 ↑f,
          map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
        ↑x *
      OneHom.toFun
        { toFun := fun x => Option.casesOn x 1 ↑f,
          map_one' := (_ : (fun x => Option.casesOn x 1 ↑f) 1 = (fun x => Option.casesOn x 1 ↑f) 1) }
        1
[PROOFSTEP]
exact (mul_one _).symm
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
⊢ map (MulHom.id α) = MonoidHom.id (WithOne α)
[PROOFSTEP]
ext x
[GOAL]
case h
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
x : WithOne α
⊢ ↑(map (MulHom.id α)) x = ↑(MonoidHom.id (WithOne α)) x
[PROOFSTEP]
induction x using WithOne.cases_on
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
⊢ ↑(map (MulHom.id α)) 1 = ↑(MonoidHom.id (WithOne α)) 1
[PROOFSTEP]
rfl
[GOAL]
case h.a
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
a✝ : α
⊢ ↑(map (MulHom.id α)) ↑a✝ = ↑(MonoidHom.id (WithOne α)) ↑a✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
x : WithOne α
⊢ ↑(map g) (↑(map f) x) = ↑(map (MulHom.comp g f)) x
[PROOFSTEP]
induction x using WithOne.cases_on
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
⊢ ↑(map g) (↑(map f) 1) = ↑(map (MulHom.comp g f)) 1
[PROOFSTEP]
rfl
[GOAL]
case a
α : Type u
β : Type v
γ : Type w
inst✝² : Mul α
inst✝¹ : Mul β
inst✝ : Mul γ
f : α →ₙ* β
g : β →ₙ* γ
a✝ : α
⊢ ↑(map g) (↑(map f) ↑a✝) = ↑(map (MulHom.comp g f)) ↑a✝
[PROOFSTEP]
rfl
