[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
α β : A₁ ⟶ A₂
⊢ F.map (α.f + β.f) ≫ A₂.str = A₁.str ≫ (α.f + β.f)
[PROOFSTEP]
simp only [Functor.map_add, add_comp, Endofunctor.Algebra.Hom.h, comp_add]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
⊢ ∀ (a b c : A₁ ⟶ A₂), a + b + c = a + (b + c)
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
a✝ b✝ c✝ : A₁ ⟶ A₂
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
[PROOFSTEP]
apply Algebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
a✝ b✝ c✝ : A₁ ⟶ A₂
⊢ (a✝ + b✝ + c✝).f = (a✝ + (b✝ + c✝)).f
[PROOFSTEP]
apply add_assoc
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
⊢ F.map 0 ≫ A₂.str = A₁.str ≫ 0
[PROOFSTEP]
simp only [Functor.map_zero, zero_comp, comp_zero]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
⊢ ∀ (a : A₁ ⟶ A₂), 0 + a = a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
a✝ : A₁ ⟶ A₂
⊢ 0 + a✝ = a✝
[PROOFSTEP]
apply Algebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
a✝ : A₁ ⟶ A₂
⊢ (0 + a✝).f = a✝.f
[PROOFSTEP]
apply zero_add
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
⊢ ∀ (a : A₁ ⟶ A₂), a + 0 = a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
a✝ : A₁ ⟶ A₂
⊢ a✝ + 0 = a✝
[PROOFSTEP]
apply Algebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
a✝ : A₁ ⟶ A₂
⊢ (a✝ + 0).f = a✝.f
[PROOFSTEP]
apply add_zero
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
n : ℕ
α : A₁ ⟶ A₂
⊢ F.map (n • α.f) ≫ A₂.str = A₁.str ≫ (n • α.f)
[PROOFSTEP]
rw [comp_nsmul, Functor.map_nsmul, nsmul_comp, Endofunctor.Algebra.Hom.h]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
⊢ ∀ (x : A₁ ⟶ A₂), (fun n α => Algebra.Hom.mk (n • α.f)) 0 x = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
x✝ : A₁ ⟶ A₂
⊢ (fun n α => Algebra.Hom.mk (n • α.f)) 0 x✝ = 0
[PROOFSTEP]
apply Algebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
x✝ : A₁ ⟶ A₂
⊢ ((fun n α => Algebra.Hom.mk (n • α.f)) 0 x✝).f = 0.f
[PROOFSTEP]
apply zero_smul
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
⊢ ∀ (n : ℕ) (x : A₁ ⟶ A₂),
    (fun n α => Algebra.Hom.mk (n • α.f)) (n + 1) x = x + (fun n α => Algebra.Hom.mk (n • α.f)) n x
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
n✝ : ℕ
x✝ : A₁ ⟶ A₂
⊢ (fun n α => Algebra.Hom.mk (n • α.f)) (n✝ + 1) x✝ = x✝ + (fun n α => Algebra.Hom.mk (n • α.f)) n✝ x✝
[PROOFSTEP]
apply Algebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
n✝ : ℕ
x✝ : A₁ ⟶ A₂
⊢ ((fun n α => Algebra.Hom.mk (n • α.f)) (n✝ + 1) x✝).f = (x✝ + (fun n α => Algebra.Hom.mk (n • α.f)) n✝ x✝).f
[PROOFSTEP]
apply succ_nsmul
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
α : A₁ ⟶ A₂
⊢ F.map (-α.f) ≫ A₂.str = A₁.str ≫ (-α.f)
[PROOFSTEP]
simp only [Functor.map_neg, neg_comp, Endofunctor.Algebra.Hom.h, comp_neg]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
α β : A₁ ⟶ A₂
⊢ F.map (α.f - β.f) ≫ A₂.str = A₁.str ≫ (α.f - β.f)
[PROOFSTEP]
simp only [Functor.map_sub, sub_comp, Endofunctor.Algebra.Hom.h, comp_sub]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
⊢ ∀ (a b : A₁ ⟶ A₂), a - b = a + -b
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
a✝ b✝ : A₁ ⟶ A₂
⊢ a✝ - b✝ = a✝ + -b✝
[PROOFSTEP]
apply Algebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
a✝ b✝ : A₁ ⟶ A₂
⊢ (a✝ - b✝).f = (a✝ + -b✝).f
[PROOFSTEP]
apply sub_eq_add_neg
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
r : ℤ
α : A₁ ⟶ A₂
⊢ F.map (r • α.f) ≫ A₂.str = A₁.str ≫ (r • α.f)
[PROOFSTEP]
rw [comp_zsmul, Functor.map_zsmul, zsmul_comp, Endofunctor.Algebra.Hom.h]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
⊢ ∀ (a : A₁ ⟶ A₂), (fun r α => Algebra.Hom.mk (r • α.f)) 0 a = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
a✝ : A₁ ⟶ A₂
⊢ (fun r α => Algebra.Hom.mk (r • α.f)) 0 a✝ = 0
[PROOFSTEP]
apply Algebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
a✝ : A₁ ⟶ A₂
⊢ ((fun r α => Algebra.Hom.mk (r • α.f)) 0 a✝).f = 0.f
[PROOFSTEP]
apply zero_smul
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
⊢ ∀ (n : ℕ) (a : A₁ ⟶ A₂),
    (fun r α => Algebra.Hom.mk (r • α.f)) (Int.ofNat (Nat.succ n)) a =
      a + (fun r α => Algebra.Hom.mk (r • α.f)) (Int.ofNat n) a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
n✝ : ℕ
a✝ : A₁ ⟶ A₂
⊢ (fun r α => Algebra.Hom.mk (r • α.f)) (Int.ofNat (Nat.succ n✝)) a✝ =
    a✝ + (fun r α => Algebra.Hom.mk (r • α.f)) (Int.ofNat n✝) a✝
[PROOFSTEP]
apply Algebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
n✝ : ℕ
a✝ : A₁ ⟶ A₂
⊢ ((fun r α => Algebra.Hom.mk (r • α.f)) (Int.ofNat (Nat.succ n✝)) a✝).f =
    (a✝ + (fun r α => Algebra.Hom.mk (r • α.f)) (Int.ofNat n✝) a✝).f
[PROOFSTEP]
dsimp
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
n✝ : ℕ
a✝ : A₁ ⟶ A₂
⊢ ↑(Nat.succ n✝) • a✝.f = (a✝ + Algebra.Hom.mk (↑n✝ • a✝.f)).f
[PROOFSTEP]
simp only [coe_nat_zsmul, succ_nsmul]
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
n✝ : ℕ
a✝ : A₁ ⟶ A₂
⊢ a✝.f + n✝ • a✝.f = (a✝ + Algebra.Hom.mk (n✝ • a✝.f)).f
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
⊢ ∀ (n : ℕ) (a : A₁ ⟶ A₂),
    (fun r α => Algebra.Hom.mk (r • α.f)) (Int.negSucc n) a = -(fun r α => Algebra.Hom.mk (r • α.f)) (↑(Nat.succ n)) a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
n✝ : ℕ
a✝ : A₁ ⟶ A₂
⊢ (fun r α => Algebra.Hom.mk (r • α.f)) (Int.negSucc n✝) a✝ = -(fun r α => Algebra.Hom.mk (r • α.f)) (↑(Nat.succ n✝)) a✝
[PROOFSTEP]
apply Algebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
n✝ : ℕ
a✝ : A₁ ⟶ A₂
⊢ ((fun r α => Algebra.Hom.mk (r • α.f)) (Int.negSucc n✝) a✝).f =
    (-(fun r α => Algebra.Hom.mk (r • α.f)) (↑(Nat.succ n✝)) a✝).f
[PROOFSTEP]
simp only [negSucc_zsmul, neg_inj, nsmul_eq_smul_cast ℤ]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
⊢ ∀ (a : A₁ ⟶ A₂), -a + a = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
a✝ : A₁ ⟶ A₂
⊢ -a✝ + a✝ = 0
[PROOFSTEP]
apply Algebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
a✝ : A₁ ⟶ A₂
⊢ (-a✝ + a✝).f = 0.f
[PROOFSTEP]
apply add_left_neg
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
⊢ ∀ (a b : A₁ ⟶ A₂), a + b = b + a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
a✝ b✝ : A₁ ⟶ A₂
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
apply Algebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Algebra F
a✝ b✝ : A₁ ⟶ A₂
⊢ (a✝ + b✝).f = (b✝ + a✝).f
[PROOFSTEP]
apply add_comm
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
⊢ ∀ (P Q R : Algebra F) (f f' : P ⟶ Q) (g : Q ⟶ R), (f + f') ≫ g = f ≫ g + f' ≫ g
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
P✝ Q✝ R✝ : Algebra F
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ (f✝ + f'✝) ≫ g✝ = f✝ ≫ g✝ + f'✝ ≫ g✝
[PROOFSTEP]
apply Algebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
P✝ Q✝ R✝ : Algebra F
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ ((f✝ + f'✝) ≫ g✝).f = (f✝ ≫ g✝ + f'✝ ≫ g✝).f
[PROOFSTEP]
apply add_comp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
⊢ ∀ (P Q R : Algebra F) (f : P ⟶ Q) (g g' : Q ⟶ R), f ≫ (g + g') = f ≫ g + f ≫ g'
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
P✝ Q✝ R✝ : Algebra F
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ f✝ ≫ (g✝ + g'✝) = f✝ ≫ g✝ + f✝ ≫ g'✝
[PROOFSTEP]
apply Algebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
P✝ Q✝ R✝ : Algebra F
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ (f✝ ≫ (g✝ + g'✝)).f = (f✝ ≫ g✝ + f✝ ≫ g'✝).f
[PROOFSTEP]
apply comp_add
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
α β : A₁ ⟶ A₂
⊢ A₁.str ≫ F.map (α.f + β.f) = (α.f + β.f) ≫ A₂.str
[PROOFSTEP]
simp only [Functor.map_add, comp_add, Endofunctor.Coalgebra.Hom.h, add_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
⊢ ∀ (a b c : A₁ ⟶ A₂), a + b + c = a + (b + c)
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
a✝ b✝ c✝ : A₁ ⟶ A₂
⊢ a✝ + b✝ + c✝ = a✝ + (b✝ + c✝)
[PROOFSTEP]
apply Coalgebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
a✝ b✝ c✝ : A₁ ⟶ A₂
⊢ (a✝ + b✝ + c✝).f = (a✝ + (b✝ + c✝)).f
[PROOFSTEP]
apply add_assoc
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
⊢ A₁.str ≫ F.map 0 = 0 ≫ A₂.str
[PROOFSTEP]
simp only [Functor.map_zero, zero_comp, comp_zero]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
⊢ ∀ (a : A₁ ⟶ A₂), 0 + a = a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
a✝ : A₁ ⟶ A₂
⊢ 0 + a✝ = a✝
[PROOFSTEP]
apply Coalgebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
a✝ : A₁ ⟶ A₂
⊢ (0 + a✝).f = a✝.f
[PROOFSTEP]
apply zero_add
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
⊢ ∀ (a : A₁ ⟶ A₂), a + 0 = a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
a✝ : A₁ ⟶ A₂
⊢ a✝ + 0 = a✝
[PROOFSTEP]
apply Coalgebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
a✝ : A₁ ⟶ A₂
⊢ (a✝ + 0).f = a✝.f
[PROOFSTEP]
apply add_zero
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
n : ℕ
α : A₁ ⟶ A₂
⊢ A₁.str ≫ F.map (n • α.f) = (n • α.f) ≫ A₂.str
[PROOFSTEP]
rw [Functor.map_nsmul, comp_nsmul, Endofunctor.Coalgebra.Hom.h, nsmul_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
⊢ ∀ (x : A₁ ⟶ A₂), (fun n α => Coalgebra.Hom.mk (n • α.f)) 0 x = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
x✝ : A₁ ⟶ A₂
⊢ (fun n α => Coalgebra.Hom.mk (n • α.f)) 0 x✝ = 0
[PROOFSTEP]
apply Coalgebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
x✝ : A₁ ⟶ A₂
⊢ ((fun n α => Coalgebra.Hom.mk (n • α.f)) 0 x✝).f = 0.f
[PROOFSTEP]
apply zero_smul
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
⊢ ∀ (n : ℕ) (x : A₁ ⟶ A₂),
    (fun n α => Coalgebra.Hom.mk (n • α.f)) (n + 1) x = x + (fun n α => Coalgebra.Hom.mk (n • α.f)) n x
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
n✝ : ℕ
x✝ : A₁ ⟶ A₂
⊢ (fun n α => Coalgebra.Hom.mk (n • α.f)) (n✝ + 1) x✝ = x✝ + (fun n α => Coalgebra.Hom.mk (n • α.f)) n✝ x✝
[PROOFSTEP]
apply Coalgebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
n✝ : ℕ
x✝ : A₁ ⟶ A₂
⊢ ((fun n α => Coalgebra.Hom.mk (n • α.f)) (n✝ + 1) x✝).f = (x✝ + (fun n α => Coalgebra.Hom.mk (n • α.f)) n✝ x✝).f
[PROOFSTEP]
apply succ_nsmul
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
α : A₁ ⟶ A₂
⊢ A₁.str ≫ F.map (-α.f) = (-α.f) ≫ A₂.str
[PROOFSTEP]
simp only [Functor.map_neg, comp_neg, Endofunctor.Coalgebra.Hom.h, neg_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
α β : A₁ ⟶ A₂
⊢ A₁.str ≫ F.map (α.f - β.f) = (α.f - β.f) ≫ A₂.str
[PROOFSTEP]
simp only [Functor.map_sub, comp_sub, Endofunctor.Coalgebra.Hom.h, sub_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
⊢ ∀ (a b : A₁ ⟶ A₂), a - b = a + -b
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
a✝ b✝ : A₁ ⟶ A₂
⊢ a✝ - b✝ = a✝ + -b✝
[PROOFSTEP]
apply Coalgebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
a✝ b✝ : A₁ ⟶ A₂
⊢ (a✝ - b✝).f = (a✝ + -b✝).f
[PROOFSTEP]
apply sub_eq_add_neg
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
r : ℤ
α : A₁ ⟶ A₂
⊢ A₁.str ≫ F.map (r • α.f) = (r • α.f) ≫ A₂.str
[PROOFSTEP]
rw [Functor.map_zsmul, comp_zsmul, Endofunctor.Coalgebra.Hom.h, zsmul_comp]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
⊢ ∀ (a : A₁ ⟶ A₂), (fun r α => Coalgebra.Hom.mk (r • α.f)) 0 a = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
a✝ : A₁ ⟶ A₂
⊢ (fun r α => Coalgebra.Hom.mk (r • α.f)) 0 a✝ = 0
[PROOFSTEP]
apply Coalgebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
a✝ : A₁ ⟶ A₂
⊢ ((fun r α => Coalgebra.Hom.mk (r • α.f)) 0 a✝).f = 0.f
[PROOFSTEP]
apply zero_smul
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
⊢ ∀ (n : ℕ) (a : A₁ ⟶ A₂),
    (fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.ofNat (Nat.succ n)) a =
      a + (fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.ofNat n) a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
n✝ : ℕ
a✝ : A₁ ⟶ A₂
⊢ (fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.ofNat (Nat.succ n✝)) a✝ =
    a✝ + (fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.ofNat n✝) a✝
[PROOFSTEP]
apply Coalgebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
n✝ : ℕ
a✝ : A₁ ⟶ A₂
⊢ ((fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.ofNat (Nat.succ n✝)) a✝).f =
    (a✝ + (fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.ofNat n✝) a✝).f
[PROOFSTEP]
dsimp
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
n✝ : ℕ
a✝ : A₁ ⟶ A₂
⊢ ↑(Nat.succ n✝) • a✝.f = (a✝ + Coalgebra.Hom.mk (↑n✝ • a✝.f)).f
[PROOFSTEP]
simp only [coe_nat_zsmul, succ_nsmul]
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
n✝ : ℕ
a✝ : A₁ ⟶ A₂
⊢ a✝.f + n✝ • a✝.f = (a✝ + Coalgebra.Hom.mk (n✝ • a✝.f)).f
[PROOFSTEP]
rfl
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
⊢ ∀ (n : ℕ) (a : A₁ ⟶ A₂),
    (fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.negSucc n) a =
      -(fun r α => Coalgebra.Hom.mk (r • α.f)) (↑(Nat.succ n)) a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
n✝ : ℕ
a✝ : A₁ ⟶ A₂
⊢ (fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.negSucc n✝) a✝ =
    -(fun r α => Coalgebra.Hom.mk (r • α.f)) (↑(Nat.succ n✝)) a✝
[PROOFSTEP]
apply Coalgebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
n✝ : ℕ
a✝ : A₁ ⟶ A₂
⊢ ((fun r α => Coalgebra.Hom.mk (r • α.f)) (Int.negSucc n✝) a✝).f =
    (-(fun r α => Coalgebra.Hom.mk (r • α.f)) (↑(Nat.succ n✝)) a✝).f
[PROOFSTEP]
simp only [negSucc_zsmul, neg_inj, nsmul_eq_smul_cast ℤ]
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
⊢ ∀ (a : A₁ ⟶ A₂), -a + a = 0
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
a✝ : A₁ ⟶ A₂
⊢ -a✝ + a✝ = 0
[PROOFSTEP]
apply Coalgebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
a✝ : A₁ ⟶ A₂
⊢ (-a✝ + a✝).f = 0.f
[PROOFSTEP]
apply add_left_neg
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
⊢ ∀ (a b : A₁ ⟶ A₂), a + b = b + a
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
a✝ b✝ : A₁ ⟶ A₂
⊢ a✝ + b✝ = b✝ + a✝
[PROOFSTEP]
apply Coalgebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
A₁ A₂ : Coalgebra F
a✝ b✝ : A₁ ⟶ A₂
⊢ (a✝ + b✝).f = (b✝ + a✝).f
[PROOFSTEP]
apply add_comm
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
⊢ ∀ (P Q R : Coalgebra F) (f f' : P ⟶ Q) (g : Q ⟶ R), (f + f') ≫ g = f ≫ g + f' ≫ g
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
P✝ Q✝ R✝ : Coalgebra F
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ (f✝ + f'✝) ≫ g✝ = f✝ ≫ g✝ + f'✝ ≫ g✝
[PROOFSTEP]
apply Coalgebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
P✝ Q✝ R✝ : Coalgebra F
f✝ f'✝ : P✝ ⟶ Q✝
g✝ : Q✝ ⟶ R✝
⊢ ((f✝ + f'✝) ≫ g✝).f = (f✝ ≫ g✝ + f'✝ ≫ g✝).f
[PROOFSTEP]
apply add_comp
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
⊢ ∀ (P Q R : Coalgebra F) (f : P ⟶ Q) (g g' : Q ⟶ R), f ≫ (g + g') = f ≫ g + f ≫ g'
[PROOFSTEP]
intros
[GOAL]
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
P✝ Q✝ R✝ : Coalgebra F
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ f✝ ≫ (g✝ + g'✝) = f✝ ≫ g✝ + f✝ ≫ g'✝
[PROOFSTEP]
apply Coalgebra.Hom.ext
[GOAL]
case f
C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : Preadditive C
F : C ⥤ C
inst✝ : Functor.Additive F
P✝ Q✝ R✝ : Coalgebra F
f✝ : P✝ ⟶ Q✝
g✝ g'✝ : Q✝ ⟶ R✝
⊢ (f✝ ≫ (g✝ + g'✝)).f = (f✝ ≫ g✝ + f✝ ≫ g'✝).f
[PROOFSTEP]
apply comp_add
