awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
j : J
⊢ Eq.{v + 1} (α := (F ⋙ Functor.obj coyoneda (op s.pt)).obj j)
    ((↑((Types.isLimitEquivSections (hc (op s.pt)) :
              (a : ((coyoneda.obj (op s.pt)).mapCone c).pt) → (↑(F ⋙ coyoneda.obj (op s.pt)).sections : Type (max v w)))
            m) :
        (j : J) → (F ⋙ coyoneda.obj (op s.pt)).obj j)
      j)
    ((↑((Types.isLimitEquivSections (hc (op s.pt)) :
              (a : ((coyoneda.obj (op s.pt)).mapCone c).pt) → (↑(F ⋙ coyoneda.obj (op s.pt)).sections : Type (max v w)))
            ((hom (FC := TypeCat.Fun)
                  (IsLimit.lift (hc (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s)) :
                (a : (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone s).pt) →
                  (fun (X : Type v) ↦ X) ((coyoneda.obj (op s.pt)).mapCone c).pt)
              (𝟙 (unop (op s.pt))))) :
        (j : J) → (F ⋙ coyoneda.obj (op s.pt)).obj j)
      j)
have a : m ≫ c.π.app j =
  (@hom _ types TypeCat.Fun _ _ _ _ _
          (IsLimit.lift (hc (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s)) :
        (a : s.pt ⟶ s.pt) → s.pt ⟶ c.pt)
      (𝟙 s.pt) ≫
    c.π.app j
Tactic: dsimp [Types.isLimitEquivSections, Types.sectionOfCone]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
c : Cone F
hc : (X : Cᵒᵖ) → IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c)
s : Cone F
m : s.pt ⟶ c.pt
hm : ∀ (j : J), m ≫ c.π.app j = s.π.app j
j : J
⊢ m ≫ c.π.app j =
    (@hom _ types TypeCat.Fun _ _ _ _ _
            (IsLimit.lift (hc (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s)) :
          (a : s.pt ⟶ s.pt) → s.pt ⟶ c.pt)
        (𝟙 s.pt) ≫
      c.π.app j
have eq : Eq (α := (F ⋙ Functor.obj coyoneda (op s.pt)).obj j)
  ((hom (FC := TypeCat.Fun)
          (IsLimit.lift (hc (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s) ≫
            NatTrans.app (Cone.π (Functor.mapCone (Functor.obj coyoneda (op s.pt)) c)) j) :
        (a : ((coyoneda.obj (op s.pt)).mapCone s).pt) → (F ⋙ coyoneda.obj (op s.pt)).obj j)
      (𝟙 s.pt) :
    (F ⋙ Functor.obj coyoneda (op s.pt)).obj j)
  (((@hom _ types TypeCat.Fun _ _ _ _ _ (NatTrans.app (Cone.π (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s)) j) :
          TypeCat.Fun
            (Cone.pt (F := F ⋙ Functor.obj coyoneda (op s.pt)) (Functor.mapCone (Functor.obj coyoneda (op s.pt)) s))
            ((F ⋙ Functor.obj coyoneda (op s.pt)).obj j)) :
        (a : ((coyoneda.obj (op s.pt)).mapCone s).pt) → (F ⋙ coyoneda.obj (op s.pt)).obj j)
      (𝟙 s.pt) :
    (F ⋙ Functor.obj coyoneda (op s.pt)).obj j)
Tactic: have eq := congr_hom ((hc (op s.pt)).fac ((coyoneda.obj (op s.pt)).mapCone s) j) (𝟙 s.pt)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
J : Type w
inst_1 : Category.{t, w} J
F : Functor.{t, v, w, u} J C
c : Cone F
x : (X : Cᵒᵖ) → IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c)
⊢ (fun (h : IsLimit c) (x : Cᵒᵖ) ↦
        (isLimitOfPreserves (Functor.obj coyoneda x) h :
          IsLimit (F := F ⋙ Functor.obj coyoneda x) (Functor.mapCone (Functor.obj coyoneda x) c)))
      ((fun (h : (X : Cᵒᵖ) → IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c)) ↦
          coyonedaJointlyReflectsLimits F c h)
        x) =
    x
have h : ∀ (x_1 : Cᵒᵖ),
  (fun (h : IsLimit c) (x : Cᵒᵖ) ↦
        (isLimitOfPreserves (Functor.obj coyoneda x) h :
          IsLimit (F := F ⋙ Functor.obj coyoneda x) (Functor.mapCone (Functor.obj coyoneda x) c)))
      ((fun (h : (X : Cᵒᵖ) → IsLimit (F := F ⋙ Functor.obj coyoneda X) (Functor.mapCone (Functor.obj coyoneda X) c)) ↦
          coyonedaJointlyReflectsLimits F c h)
        x)
      x_1 =
    x x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ PreservesLimitsOfSize.{t, w, v, max u v, u, max u (v + 1)} (C := C) yoneda
have x : ∀ (k : Cᵒᵖ), PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (yoneda ⋙ Functor.obj (evaluation Cᵒᵖ (Type v)) k)
Tactic: apply preservesLimits_of_evaluation
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Cᵒᵖ
⊢ PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (yoneda ⋙ Functor.obj (evaluation Cᵒᵖ (Type v)) K)
have x : PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (Functor.obj coyoneda K)
Tactic: change PreservesLimitsOfSize (coyoneda.obj K)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ PreservesLimitsOfSize.{t, w, v, max u v, u, max u (v + 1)} (C := Cᵒᵖ) coyoneda
have x : ∀ (k : C), PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (coyoneda ⋙ Functor.obj (evaluation C (Type v)) k)
Tactic: apply preservesLimits_of_evaluation
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : C
⊢ PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (coyoneda ⋙ Functor.obj (evaluation C (Type v)) K)
have x : PreservesLimitsOfSize.{t, w, v, v, u, v + 1} (Functor.obj yoneda K)
Tactic: change PreservesLimitsOfSize (yoneda.obj K)
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ PreservesLimitsOfSize.{t, w, v, max (max u v) w', u, max (max u (v + 1)) (w' + 1)} (C := C) uliftYoneda.{w', v, u}
have x : ∀ (k : Cᵒᵖ),
  PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
    (uliftYoneda.{w', v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type (max w' v))) k)
Tactic: apply preservesLimits_of_evaluation
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : Cᵒᵖ
⊢ PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
    (uliftYoneda.{w', v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type (max w' v))) K)
have x : PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)} (Functor.obj coyoneda K ⋙ uliftFunctor.{w', v})
Tactic: change PreservesLimitsOfSize.{t, w} (coyoneda.obj K ⋙ uliftFunctor.{w'})
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
⊢ PreservesLimitsOfSize.{t, w, v, max (max u v) w', u, max (max u (v + 1)) (w' + 1)} (C := Cᵒᵖ) uliftCoyoneda.{w', v, u}
have x : ∀ (k : C),
  PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
    (uliftCoyoneda.{w', v, u} ⋙ Functor.obj (evaluation C (Type (max w' v))) k)
Tactic: apply preservesLimits_of_evaluation
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
K : C
⊢ PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
    (uliftCoyoneda.{w', v, u} ⋙ Functor.obj (evaluation C (Type (max w' v))) K)
have x : PreservesLimitsOfSize.{t, w, v, max w' v, u, max (w' + 1) (v + 1)} (Functor.obj yoneda K ⋙ uliftFunctor.{w', v})
Tactic: change PreservesLimitsOfSize.{t, w} (yoneda.obj _ ⋙ uliftFunctor.{w'})
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : LocallySmall.{w', v, u} C
K : Cᵒᵖ
J : Type w
x : Category.{t, w} J
⊢ PreservesLimitsOfShape.{t, w, v, w', u, w' + 1} J (shrinkYoneda.{w', v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w')) K)
have this : PreservesLimitsOfShape J ((shrinkYoneda.{w', v, u} ⋙ Functor.obj (evaluation Cᵒᵖ (Type w')) K) ⋙ uliftFunctor.{v, w'})
Tactic: have := preservesLimitsOfShape_of_natIso (J := J) (Functor.associator _ _ _ ≪≫
      shrinkYonedaCompEvaluationCompUliftFunctorIsoUliftFunctor.{w'} K).symm
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w', u, w' + 1} Cᵒᵖ (Type w')
inst_1 : F.IsRepresentable
⊢ PreservesLimitsOfSize.{t, w, v, w', u, w' + 1} F
have suffices : PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)} (F ⋙ uliftFunctor.{v, w'})
Tactic: suffices PreservesLimitsOfSize (F ⋙ uliftFunctor.{v}) from
    preservesLimits_of_reflects_of_preserves _ (uliftFunctor.{v})
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, w', u, w' + 1} Cᵒᵖ (Type w')
inst_1 : F.IsRepresentable
⊢ PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)} (F ⋙ uliftFunctor.{v, w'})
have rw : PreservesLimitsOfSize.{t, w, v, max v w', u, max (v + 1) (w' + 1)}
  (obj uliftYoneda.{w', v, u} (F ⋙ uliftFunctor.{v, w'}).reprX)
Tactic: rw [preservesLimitsOfSize_iff_of_natIso (F ⋙ uliftFunctor.{v}).uliftYonedaReprXIso.symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} C (Type u_1)
inst_1 : F.IsCorepresentable
⊢ PreservesLimitsOfSize.{t, w, v, u_1, u, u_1 + 1} F
have suffices : PreservesLimitsOfSize.{t, w, v, max u_1 v, u, max (u_1 + 1) (v + 1)} (F ⋙ uliftFunctor.{v, u_1})
Tactic: suffices PreservesLimitsOfSize (F ⋙ uliftFunctor.{v}) from
    preservesLimits_of_reflects_of_preserves _ (uliftFunctor.{v})
-- Lean 4 proof step from Mathlib.CategoryTheory.Limits.Yoneda (goal)
Goal:
C : Type u
inst : Category.{v, u} C
F : Functor.{v, u_1, u, u_1 + 1} C (Type u_1)
inst_1 : F.IsCorepresentable
⊢ PreservesLimitsOfSize.{t, w, v, max u_1 v, u, max (u_1 + 1) (v + 1)} (F ⋙ uliftFunctor.{v, u_1})
have rw : PreservesLimitsOfSize.{t, w, v, max u_1 v, u, max (u_1 + 1) (v + 1)}
  (obj uliftCoyoneda.{u_1, v, u} (op (F ⋙ uliftFunctor.{v, u_1}).coreprX))
Tactic: rw [preservesLimitsOfSize_iff_of_natIso (F ⋙ uliftFunctor.{v}).uliftCoyonedaCoreprXIso.symm]
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
D : Type u'
F : D → C
x x_1 x_2 : InducedCategory C F
x_3 : R
x_4 : x ⟶ x_1
x_5 : x_1 ⟶ x_2
⊢ (x_3 • x_4) ≫ x_5 = x_3 • x_4 ≫ x_5
have h : ((x_3 • x_4) ≫ x_5).hom = (x_3 • x_4 ≫ x_5).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
D : Type u'
F : D → C
x x_1 x_2 : InducedCategory C F
x_3 : x ⟶ x_1
x_4 : R
x_5 : x_1 ⟶ x_2
⊢ x_3 ≫ (x_4 • x_5) = x_4 • x_3 ≫ x_5
have h : (x_3 ≫ (x_4 • x_5)).hom = (x_4 • x_3 ≫ x_5).hom
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
X Y : C
f : X ⟶ Y
inst_4 : Epi f
r : R
inst_5 : Invertible r
Z : C
g g' : Y ⟶ Z
H : (r • f) ≫ g = (r • f) ≫ g'
⊢ g = g'
have H₁ : r • g = r • g'
Tactic: rw [smul_comp, smul_comp, ← comp_smul, ← comp_smul, cancel_epi] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.Basic (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
R : Type w
inst_2 : Semiring R
inst_3 : Linear.{w, v, u} R C
X Y : C
f : X ⟶ Y
inst_4 : Mono f
r : R
inst_5 : Invertible r
Z : C
g g' : Z ⟶ X
H : g ≫ (r • f) = g' ≫ (r • f)
⊢ g = g'
have H₁ : r • g = r • g'
Tactic: rw [comp_smul, comp_smul, ← smul_comp, ← smul_comp, cancel_mono] at H
Cleared hypotheses: H
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
S : Type w
inst_2 : CommSemiring S
inst_3 : Linear.{w, v, u} S C
X Y Z : C
x y : X ⟶ Y
⊢ leftComp S Z (x + y) = HAdd.hAdd (α := (Y ⟶ Z) →ₗ[S] X ⟶ Z) (leftComp S Z x) (leftComp S Z y)
have h : ∀ (x_1 : Y ⟶ Z),
  Eq (α := X ⟶ Z) ((leftComp S Z (x + y) : (a : Y ⟶ Z) → X ⟶ Z) x_1 : X ⟶ Z)
    ((HAdd.hAdd (α := (Y ⟶ Z) →ₗ[S] X ⟶ Z) (leftComp S Z x) (leftComp S Z y) : (a : Y ⟶ Z) → X ⟶ Z) x_1 : X ⟶ Z)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
S : Type w
inst_2 : CommSemiring S
inst_3 : Linear.{w, v, u} S C
X Y Z : C
m : S
x : X ⟶ Y
⊢ leftComp S Z (m • x) =
    HSMul.hSMul (α := S) (β := (Y ⟶ Z) →ₗ[S] X ⟶ Z) ((RingHom.id S : (a : S) → S) m : S) (leftComp S Z x)
have h : ∀ (x_1 : Y ⟶ Z),
  Eq (α := X ⟶ Z) ((leftComp S Z (m • x) : (a : Y ⟶ Z) → X ⟶ Z) x_1 : X ⟶ Z)
    ((HSMul.hSMul (α := S) (β := (Y ⟶ Z) →ₗ[S] X ⟶ Z) ((RingHom.id S : (a : S) → S) m : S) (leftComp S Z x) :
          (a : Y ⟶ Z) → X ⟶ Z)
        x_1 :
      X ⟶ Z)
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.FunctorCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
r : R
α : F ⟶ G
X Y : C
f : X ⟶ Y
⊢ F.map f ≫ (r • α.app Y) = (r • α.app X) ≫ G.map f
have rw : r • F.map f ≫ α.app Y = (r • α.app X) ≫ G.map f
Tactic: rw [comp_smul, smul_comp, α.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.FunctorCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
r : R
α : F ⟶ G
X Y : C
f : X ⟶ Y
rw : r • F.map f ≫ α.app Y = (r • α.app X) ≫ G.map f
⊢ F.map f ≫ (r • α.app Y) = (r • α.app X) ≫ G.map f
have rw₁ : r • F.map f ≫ α.app Y = r • α.app X ≫ G.map f
Tactic: rw [comp_smul, smul_comp, α.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.FunctorCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
r : R
α : F ⟶ G
X Y : C
f : X ⟶ Y
rw : r • F.map f ≫ α.app Y = (r • α.app X) ≫ G.map f
rw₁ : r • F.map f ≫ α.app Y = r • α.app X ≫ G.map f
⊢ F.map f ≫ (r • α.app Y) = (r • α.app X) ≫ G.map f
have rw₂ : r • α.app X ≫ G.map f = r • α.app X ≫ G.map f
Tactic: rw [comp_smul, smul_comp, α.naturality]
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.FunctorCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
x y : R
b : F ⟶ G
⊢ (x * y) • b = x • y • b
have w : ∀ (x_1 : C), ((x * y) • b).app x_1 = (x • y • b).app x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.FunctorCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
b : F ⟶ G
⊢ HSMul.hSMul (α := R) 1 b = b
have w : ∀ (x : C), (HSMul.hSMul (α := R) 1 b).app x = b.app x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.FunctorCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
a : R
⊢ HSMul.hSMul (β := F ⟶ G) a 0 = 0
have w : ∀ (x : C), (HSMul.hSMul (β := F ⟶ G) a 0).app x = NatTrans.app 0 x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.FunctorCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
a : R
x y : F ⟶ G
⊢ a • (x + y) = a • x + a • y
have w : ∀ (x_1 : C), (a • (x + y)).app x_1 = (a • x + a • y).app x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.FunctorCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
r s : R
x : F ⟶ G
⊢ (r + s) • x = r • x + s • x
have w : ∀ (x_1 : C), ((r + s) • x).app x_1 = (r • x + s • x).app x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.FunctorCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
F G : Functor.{v_1, v_2, u_2, u_3} C D
x : F ⟶ G
⊢ HSMul.hSMul (α := R) 0 x = 0
have w : ∀ (x_1 : C), (HSMul.hSMul (α := R) 0 x).app x_1 = NatTrans.app 0 x_1
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.FunctorCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
X Y Z : Functor.{v_1, v_2, u_2, u_3} C D
r : R
f : X ⟶ Y
g : Y ⟶ Z
⊢ (r • f) ≫ g = r • f ≫ g
have w : ∀ (x : C), ((r • f) ≫ g).app x = (r • f ≫ g).app x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.FunctorCategory (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_2, u_3} D
inst_4 : Linear.{u_1, v_2, u_3} R D
X Y Z : Functor.{v_1, v_2, u_2, u_3} C D
f : X ⟶ Y
r : R
g : Y ⟶ Z
⊢ f ≫ (r • g) = r • f ≫ g
have w : ∀ (x : C), (f ≫ (r • g)).app x = (r • f ≫ g).app x
Tactic: ext
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.LinearFunctor (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
⊢ Linear R F ↔
    ∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
have mp : Linear R F →
  ∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.LinearFunctor (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
mp :
  Linear R F →
    ∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
⊢ Linear R F ↔
    ∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
have mpr : (∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))) →
  Linear R F
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.LinearFunctor (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
h : Linear R F
X : C
r : R
⊢ F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
have mp : r • F.map (𝟙 X) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
Tactic: rw [h.map_smul, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.LinearFunctor (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
h : Linear R F
X : C
r : R
mp : r • F.map (𝟙 X) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
⊢ F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
have mp₁ : HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
Tactic: rw [h.map_smul, F.map_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.LinearFunctor (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
⊢ (∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))) →
    Linear R F
have mpr : ∀
  (h :
    ∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X)))
  {X Y : C} (f : X ⟶ Y) (r : R), F.map (r • f) = r • F.map f
Tactic: refine fun h => ⟨fun {X Y} f r => ?_⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.LinearFunctor (hypothesis)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
h : ∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
X Y : C
f : X ⟶ Y
r : R
⊢ F.map (r • f) = r • F.map f
have this : r • f = HSMul.hSMul (β := X ⟶ X) r (𝟙 X) ≫ f
Tactic: have : r • f = (r • 𝟙 X) ≫ f := by simp
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.LinearFunctor (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
h : ∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
X Y : C
f : X ⟶ Y
r : R
this : r • f = HSMul.hSMul (β := X ⟶ X) r (𝟙 X) ≫ f
⊢ F.map (r • f) = r • F.map f
have mpr : F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X) ≫ f) = r • F.map f
Tactic: rw [this, F.map_comp, h, Linear.smul_comp, Category.id_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Linear.LinearFunctor (goal)
Goal:
R : Type u_1
inst : Semiring R
C : Type u_2
D : Type u_3
inst_1 : Category.{v_1, u_2} C
inst_2 : Category.{v_2, u_3} D
inst_3 : Preadditive.{v_1, u_2} C
inst_4 : Preadditive.{v_2, u_3} D
inst_5 : CategoryTheory.Linear.{u_1, v_1, u_2} R C
inst_6 : CategoryTheory.Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
h : ∀ (X : C) (r : R), F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) = HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X))
X Y : C
f : X ⟶ Y
r : R
this : r • f = HSMul.hSMul (β := X ⟶ X) r (𝟙 X) ≫ f
mpr : F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X) ≫ f) = r • F.map f
⊢ F.map (r • f) = r • F.map f
have mpr₁ : F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) ≫ F.map f = r • F.map f
Tactic: rw [this, F.map_comp, h, Linear.smul_comp, Category.id_comp]