[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f g : CentroidHom α
h : (fun f => f.toFun) f = (fun f => f.toFun) g
⊢ f = g
[PROOFSTEP]
cases f
[GOAL]
case mk
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
g : CentroidHom α
toAddMonoidHom✝ : α →+ α
map_mul_left'✝ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝) (a * b) = a * ZeroHom.toFun (↑toAddMonoidHom✝) b
map_mul_right'✝ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝) (a * b) = ZeroHom.toFun (↑toAddMonoidHom✝) a * b
h :
  (fun f => f.toFun)
      { toAddMonoidHom := toAddMonoidHom✝, map_mul_left' := map_mul_left'✝, map_mul_right' := map_mul_right'✝ } =
    (fun f => f.toFun) g
⊢ { toAddMonoidHom := toAddMonoidHom✝, map_mul_left' := map_mul_left'✝, map_mul_right' := map_mul_right'✝ } = g
[PROOFSTEP]
cases g
[GOAL]
case mk.mk
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
toAddMonoidHom✝¹ : α →+ α
map_mul_left'✝¹ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝¹) (a * b) = a * ZeroHom.toFun (↑toAddMonoidHom✝¹) b
map_mul_right'✝¹ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝¹) (a * b) = ZeroHom.toFun (↑toAddMonoidHom✝¹) a * b
toAddMonoidHom✝ : α →+ α
map_mul_left'✝ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝) (a * b) = a * ZeroHom.toFun (↑toAddMonoidHom✝) b
map_mul_right'✝ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝) (a * b) = ZeroHom.toFun (↑toAddMonoidHom✝) a * b
h :
  (fun f => f.toFun)
      { toAddMonoidHom := toAddMonoidHom✝¹, map_mul_left' := map_mul_left'✝¹, map_mul_right' := map_mul_right'✝¹ } =
    (fun f => f.toFun)
      { toAddMonoidHom := toAddMonoidHom✝, map_mul_left' := map_mul_left'✝, map_mul_right' := map_mul_right'✝ }
⊢ { toAddMonoidHom := toAddMonoidHom✝¹, map_mul_left' := map_mul_left'✝¹, map_mul_right' := map_mul_right'✝¹ } =
    { toAddMonoidHom := toAddMonoidHom✝, map_mul_left' := map_mul_left'✝, map_mul_right' := map_mul_right'✝ }
[PROOFSTEP]
congr with x
[GOAL]
case mk.mk.e_toAddMonoidHom.h
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
toAddMonoidHom✝¹ : α →+ α
map_mul_left'✝¹ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝¹) (a * b) = a * ZeroHom.toFun (↑toAddMonoidHom✝¹) b
map_mul_right'✝¹ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝¹) (a * b) = ZeroHom.toFun (↑toAddMonoidHom✝¹) a * b
toAddMonoidHom✝ : α →+ α
map_mul_left'✝ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝) (a * b) = a * ZeroHom.toFun (↑toAddMonoidHom✝) b
map_mul_right'✝ : ∀ (a b : α), ZeroHom.toFun (↑toAddMonoidHom✝) (a * b) = ZeroHom.toFun (↑toAddMonoidHom✝) a * b
h :
  (fun f => f.toFun)
      { toAddMonoidHom := toAddMonoidHom✝¹, map_mul_left' := map_mul_left'✝¹, map_mul_right' := map_mul_right'✝¹ } =
    (fun f => f.toFun)
      { toAddMonoidHom := toAddMonoidHom✝, map_mul_left' := map_mul_left'✝, map_mul_right' := map_mul_right'✝ }
x : α
⊢ ↑toAddMonoidHom✝¹ x = ↑toAddMonoidHom✝ x
[PROOFSTEP]
exact congrFun h x
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
f' : α → α
h : f' = ↑f
src✝ : α →+ α := AddMonoidHom.copy f.toAddMonoidHom f' h
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := { toFun := f', map_zero' := (_ : ZeroHom.toFun (↑src✝) 0 = 0) },
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := { toFun := f', map_zero' := (_ : ZeroHom.toFun (↑src✝) 0 = 0) },
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
simp_rw [h, map_mul_left]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
f' : α → α
h : f' = ↑f
src✝ : α →+ α := AddMonoidHom.copy f.toAddMonoidHom f' h
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := { toFun := f', map_zero' := (_ : ZeroHom.toFun (↑src✝) 0 = 0) },
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := { toFun := f', map_zero' := (_ : ZeroHom.toFun (↑src✝) 0 = 0) },
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
simp_rw [h, map_mul_right]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
g f₁ f₂ : CentroidHom α
hg : Injective ↑g
h : comp g f₁ = comp g f₂
a : α
⊢ ↑g (↑f₁ a) = ↑g (↑f₂ a)
[PROOFSTEP]
rw [← comp_apply, h, comp_apply]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f g : CentroidHom α
src✝ : α →+ α := ↑f + ↑g
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
show f (a * b) + g (a * b) = a * (f b + g b)
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f g : CentroidHom α
src✝ : α →+ α := ↑f + ↑g
a b : α
⊢ ↑f (a * b) + ↑g (a * b) = a * (↑f b + ↑g b)
[PROOFSTEP]
simp [map_mul_left, mul_add]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f g : CentroidHom α
src✝ : α →+ α := ↑f + ↑g
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
show f (a * b) + g (a * b) = (f a + g a) * b
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f g : CentroidHom α
src✝ : α →+ α := ↑f + ↑g
a b : α
⊢ ↑f (a * b) + ↑g (a * b) = (↑f a + ↑g a) * b
[PROOFSTEP]
simp [map_mul_right, add_mul]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
f : CentroidHom α
src✝ : α →+ α := SMul.smul n ↑f
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
change n • f (a * b) = a * n • f b
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
f : CentroidHom α
src✝ : α →+ α := SMul.smul n ↑f
a b : α
⊢ n • ↑f (a * b) = a * n • ↑f b
[PROOFSTEP]
rw [map_mul_left f, ← mul_smul_comm]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
f : CentroidHom α
src✝ : α →+ α := SMul.smul n ↑f
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
change n • f (a * b) = n • f a * b
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
n : ℕ
f : CentroidHom α
src✝ : α →+ α := SMul.smul n ↑f
a b : α
⊢ n • ↑f (a * b) = n • ↑f a * b
[PROOFSTEP]
rw [map_mul_right f, ← smul_mul_assoc]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n : ℕ
src✝ : AddMonoid.End α := toEnd f ^ n
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n : ℕ
src✝¹ : AddMonoid.End α := toEnd f ^ n
a b : α
src✝ : AddMonoid.End α := toEnd f ^ Nat.zero
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
exact rfl
[GOAL]
case succ
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n✝ : ℕ
src✝¹ : AddMonoid.End α := toEnd f ^ n✝
a b : α
n : ℕ
ih :
  let src := toEnd f ^ n;
  ZeroHom.toFun
      (↑{ toZeroHom := ↑src,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
        b
src✝ : AddMonoid.End α := toEnd f ^ Nat.succ n
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
simp
[GOAL]
case succ
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n✝ : ℕ
src✝¹ : AddMonoid.End α := toEnd f ^ n✝
a b : α
n : ℕ
ih :
  let src := toEnd f ^ n;
  ZeroHom.toFun
      (↑{ toZeroHom := ↑src,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
        b
src✝ : AddMonoid.End α := toEnd f ^ Nat.succ n
⊢ ↑(toEnd f ^ Nat.succ n) (a * b) = a * ↑(toEnd f ^ Nat.succ n) b
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case succ
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n✝ : ℕ
src✝¹ : AddMonoid.End α := toEnd f ^ n✝
a b : α
n : ℕ
ih :
  let src := toEnd f ^ n;
  ZeroHom.toFun
      (↑{ toZeroHom := ↑src,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
        b
src✝ : AddMonoid.End α := toEnd f ^ Nat.succ n
⊢ ↑(toEnd f * toEnd f ^ n) (a * b) = a * ↑(toEnd f * toEnd f ^ n) b
[PROOFSTEP]
exact (congr_arg f.toEnd ih).trans (f.map_mul_left' _ _)
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n : ℕ
src✝ : AddMonoid.End α := toEnd f ^ n
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
induction' n with n ih
[GOAL]
case zero
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n : ℕ
src✝¹ : AddMonoid.End α := toEnd f ^ n
a b : α
src✝ : AddMonoid.End α := toEnd f ^ Nat.zero
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
exact rfl
[GOAL]
case succ
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n✝ : ℕ
src✝¹ : AddMonoid.End α := toEnd f ^ n✝
a b : α
n : ℕ
ih :
  let src := toEnd f ^ n;
  ZeroHom.toFun
      (↑{ toZeroHom := ↑src,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
        a *
      b
src✝ : AddMonoid.End α := toEnd f ^ Nat.succ n
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
simp
[GOAL]
case succ
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n✝ : ℕ
src✝¹ : AddMonoid.End α := toEnd f ^ n✝
a b : α
n : ℕ
ih :
  let src := toEnd f ^ n;
  ZeroHom.toFun
      (↑{ toZeroHom := ↑src,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
        a *
      b
src✝ : AddMonoid.End α := toEnd f ^ Nat.succ n
⊢ ↑(toEnd f ^ Nat.succ n) (a * b) = ↑(toEnd f ^ Nat.succ n) a * b
[PROOFSTEP]
rw [pow_succ]
[GOAL]
case succ
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
f : CentroidHom α
n✝ : ℕ
src✝¹ : AddMonoid.End α := toEnd f ^ n✝
a b : α
n : ℕ
ih :
  let src := toEnd f ^ n;
  ZeroHom.toFun
      (↑{ toZeroHom := ↑src,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src) (x + y) = ZeroHom.toFun (↑src) x + ZeroHom.toFun (↑src) y) })
        a *
      b
src✝ : AddMonoid.End α := toEnd f ^ Nat.succ n
⊢ ↑(toEnd f * toEnd f ^ n) (a * b) = ↑(toEnd f * toEnd f ^ n) a * b
[PROOFSTEP]
exact (congr_arg f.toEnd ih).trans (f.map_mul_right' _ _)
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ (↑T ∘ ↑S) (a * b) = (↑S ∘ ↑T) (a * b)
[PROOFSTEP]
simp
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocSemiring α
T S : CentroidHom α
a b : α
⊢ ↑T (↑S (a * b)) = ↑S (↑T (a * b))
[PROOFSTEP]
rw [map_mul_right, map_mul_left, ← map_mul_right, ← map_mul_left]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
f : CentroidHom α
src✝ : α →+ α := -↑f
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
change -f (a * b) = a * (-f b)
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
f : CentroidHom α
src✝ : α →+ α := -↑f
a b : α
⊢ -↑f (a * b) = a * -↑f b
[PROOFSTEP]
simp [map_mul_left]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
f : CentroidHom α
src✝ : α →+ α := -↑f
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
change -f (a * b) = (-f a) * b
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
f : CentroidHom α
src✝ : α →+ α := -↑f
a b : α
⊢ -↑f (a * b) = -↑f a * b
[PROOFSTEP]
simp [map_mul_right]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
f g : CentroidHom α
src✝ : α →+ α := ↑f - ↑g
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
change (FunLike.coe f - FunLike.coe g) (a * b) = a * (FunLike.coe f - FunLike.coe g) b
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
f g : CentroidHom α
src✝ : α →+ α := ↑f - ↑g
a b : α
⊢ (↑f - ↑g) (a * b) = a * (↑f - ↑g) b
[PROOFSTEP]
simp [map_mul_left, mul_sub]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
f g : CentroidHom α
src✝ : α →+ α := ↑f - ↑g
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
change (FunLike.coe f - FunLike.coe g) (a * b) = ((FunLike.coe f - FunLike.coe g) a) * b
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
f g : CentroidHom α
src✝ : α →+ α := ↑f - ↑g
a b : α
⊢ (↑f - ↑g) (a * b) = (↑f - ↑g) a * b
[PROOFSTEP]
simp [map_mul_right, sub_mul]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
n : ℤ
f : CentroidHom α
src✝ : α →+ α := SMul.smul n ↑f
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    a *
      ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        b
[PROOFSTEP]
change n • f (a * b) = a * n • f b
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
n : ℤ
f : CentroidHom α
src✝ : α →+ α := SMul.smul n ↑f
a b : α
⊢ n • ↑f (a * b) = a * n • ↑f b
[PROOFSTEP]
rw [map_mul_left f, ← mul_smul_comm]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
n : ℤ
f : CentroidHom α
src✝ : α →+ α := SMul.smul n ↑f
a b : α
⊢ ZeroHom.toFun
      (↑{ toZeroHom := ↑src✝,
          map_add' :=
            (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
      (a * b) =
    ZeroHom.toFun
        (↑{ toZeroHom := ↑src✝,
            map_add' :=
              (_ : ∀ (x y : α), ZeroHom.toFun (↑src✝) (x + y) = ZeroHom.toFun (↑src✝) x + ZeroHom.toFun (↑src✝) y) })
        a *
      b
[PROOFSTEP]
change n • f (a * b) = n • f a * b
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalNonAssocRing α
n : ℤ
f : CentroidHom α
src✝ : α →+ α := SMul.smul n ↑f
a b : α
⊢ n • ↑f (a * b) = n • ↑f a * b
[PROOFSTEP]
rw [map_mul_right f, ← smul_mul_assoc]
[GOAL]
F : Type u_1
α : Type u_2
inst✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
src✝ : Ring (CentroidHom α) := instRing
f g : CentroidHom α
⊢ f * g = g * f
[PROOFSTEP]
ext
[GOAL]
case h
F : Type u_1
α : Type u_2
inst✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
src✝ : Ring (CentroidHom α) := instRing
f g : CentroidHom α
a✝ : α
⊢ ↑(f * g) a✝ = ↑(g * f) a✝
[PROOFSTEP]
refine' sub_eq_zero.1 ((or_self_iff _).1 <| (h _ _) fun r ↦ _)
[GOAL]
case h
F : Type u_1
α : Type u_2
inst✝ : NonUnitalRing α
h : ∀ (a b : α), (∀ (r : α), a * r * b = 0) → a = 0 ∨ b = 0
src✝ : Ring (CentroidHom α) := instRing
f g : CentroidHom α
a✝ r : α
⊢ (↑(f * g) a✝ - ↑(g * f) a✝) * r * (↑(f * g) a✝ - ↑(g * f) a✝) = 0
[PROOFSTEP]
rw [mul_assoc, sub_mul, sub_eq_zero, ← map_mul_right, ← map_mul_right, coe_mul, coe_mul, comp_mul_comm]
