-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem monoidalPreadditive_of_faithful {D} [Category D] [Preadditive D] [MonoidalCategory D]
    (F : D ⥤ C) [F.Monoidal] [F.Faithful] [F.Additive] :
    MonoidalPreadditive D :=
  { whiskerLeft_zero

Proof state:
case a
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
f✝ g✝ : Y✝ ⟶ Z✝
⊢ F.map (X✝ ◁ (f✝ + g✝)) = F.map (X✝ ◁ f✝ + X✝ ◁ g✝)

Tactic:
simp only [Functor.Monoidal.map_whiskerLeft, Functor.map_add, Preadditive.comp_add,
  Preadditive.add_comp, MonoidalPreadditive.whiskerLeft_add]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
⊢ ∀ {X Y Z : D}, 0 ▷ X = 0

Tactic:
intros

Result:
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
⊢ 0 ▷ X✝ = 0

Proof state:
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
⊢ ∀ {X Y Z : D}, X ◁ 0 = 0

Tactic:
intros

Result:
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
⊢ X✝ ◁ 0 = 0

Proof state:
case a
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
⊢ F.map (0 ▷ X✝) = F.map 0

Tactic:
simp [Functor.Monoidal.map_whiskerRight]

Result:
no goals

Proof state:
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
⊢ ∀ {X Y Z : D} (f g : Y ⟶ Z), (f + g) ▷ X = f ▷ X + g ▷ X

Tactic:
intros

Result:
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
f✝ g✝ : Y✝ ⟶ Z✝
⊢ (f✝ + g✝) ▷ X✝ = f✝ ▷ X✝ + g✝ ▷ X✝

Proof state:
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
⊢ X✝ ◁ 0 = 0

Tactic:
apply F.map_injective

Result:
case a
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
⊢ F.map (X✝ ◁ 0) = F.map 0

Proof state:
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
⊢ 0 ▷ X✝ = 0

Tactic:
apply F.map_injective

Result:
case a
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
⊢ F.map (0 ▷ X✝) = F.map 0

Proof state:
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
f✝ g✝ : Y✝ ⟶ Z✝
⊢ X✝ ◁ (f✝ + g✝) = X✝ ◁ f✝ + X✝ ◁ g✝

Tactic:
apply F.map_injective

Result:
case a
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
f✝ g✝ : Y✝ ⟶ Z✝
⊢ F.map (X✝ ◁ (f✝ + g✝)) = F.map (X✝ ◁ f✝ + X✝ ◁ g✝)

Proof state:
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
f✝ g✝ : Y✝ ⟶ Z✝
⊢ (f✝ + g✝) ▷ X✝ = f✝ ▷ X✝ + g✝ ▷ X✝

Tactic:
apply F.map_injective

Result:
case a
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
f✝ g✝ : Y✝ ⟶ Z✝
⊢ F.map ((f✝ + g✝) ▷ X✝) = F.map (f✝ ▷ X✝ + g✝ ▷ X✝)

Proof state:
case a
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
⊢ F.map (X✝ ◁ 0) = F.map 0

Tactic:
simp [Functor.Monoidal.map_whiskerLeft]

Result:
no goals

Proof state:
case a
C : Type u_1
inst✝⁹ : Category.{u_4, u_1} C
inst✝⁸ : Preadditive C
inst✝⁷ : MonoidalCategory C
inst✝⁶ : MonoidalPreadditive C
D : Type u_2
inst✝⁵ : Category.{u_3, u_2} D
inst✝⁴ : Preadditive D
inst✝³ : MonoidalCategory D
F : D ⥤ C
inst✝² : F.Monoidal
inst✝¹ : F.Faithful
inst✝ : F.Additive
X✝ Y✝ Z✝ : D
f✝ g✝ : Y✝ ⟶ Z✝
⊢ F.map ((f✝ + g✝) ▷ X✝) = F.map (f✝ ▷ X✝ + g✝ ▷ X✝)

Tactic:
simp only [Functor.Monoidal.map_whiskerRight, Functor.map_add, Preadditive.comp_add,
  Preadditive.add_comp, MonoidalPreadditive.add_whiskerRight]

Result:
no goals