awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
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
⊢ r • f = HSMul.hSMul (β := X ⟶ X) r (𝟙 X) ≫ f

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
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
⊢ r • f = HSMul.hSMul (β := X ⟶ X) r (𝟙 X) ≫ f

Tactic:
have : r • f = (r • 𝟙 X) ≫ f := by simp
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
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
mpr₁ : F.map (HSMul.hSMul (β := X ⟶ X) r (𝟙 X)) ≫ F.map f = r • F.map f
mpr₂ : HSMul.hSMul (β := F.obj X ⟶ F.obj X) r (𝟙 (F.obj X)) ≫ F.map f = r • F.map f
mpr₃ : r • 𝟙 (F.obj X) ≫ F.map f = r • F.map f
mpr₄ mpr₅ : r • F.map f = r • F.map f
⊢ F.map (r • f) = r • F.map f

Tactic:
rw [this, F.map_comp, h, Linear.smul_comp, Category.id_comp]

Premises used: CategoryTheory.Functor.map_comp, CategoryTheory.Linear.smul_comp, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
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
inst_7 : Linear R F
X Y : C
r : R
f : X ⟶ Y
⊢ F.map (r • f) = r • F.map f

Tactic:
Functor.Linear.map_smul _ _

Premises used: CategoryTheory.Functor.Linear.map_smul
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
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
inst_7 : Linear R F
X Y : C
r : Rˣ
f : X ⟶ Y
⊢ F.map (r • f) = r • F.map f

Tactic:
apply map_smul

Premises used: CategoryTheory.Functor.map_smul
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
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
inst_7 : Linear R F
E : Type u_4
inst_8 : Category.{v_3, u_4} E
inst_9 : Preadditive.{v_3, u_4} E
inst_10 : CategoryTheory.Linear.{u_1, v_3, u_4} R E
G : Functor.{v_2, v_3, u_3, u_4} D E
inst_11 : F.Full
inst_12 : F.EssSurj
inst_13 : Linear R (F ⋙ G)
⊢ Linear R G

Tactic:
⟨fun {X Y} f r ↦ ?_⟩

Premises used: CategoryTheory.Functor.Linear.mk
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
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
inst_7 : Linear R F
E : Type u_4
inst_8 : Category.{v_3, u_4} E
inst_9 : Preadditive.{v_3, u_4} E
inst_10 : CategoryTheory.Linear.{u_1, v_3, u_4} R E
G : Functor.{v_2, v_3, u_3, u_4} D E
inst_11 : F.Full
inst_12 : F.EssSurj
inst_13 : Linear R (F ⋙ G)
refine : ∀ {X Y : D} (f : X ⟶ Y) (r : R), G.map (r • f) = r • G.map f
⊢ Linear R G

Tactic:
refine ⟨fun {X Y} f r ↦ ?_⟩
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
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
inst_7 : Linear R F
E : Type u_4
inst_8 : Category.{v_3, u_4} E
inst_9 : Preadditive.{v_3, u_4} E
inst_10 : CategoryTheory.Linear.{u_1, v_3, u_4} R E
G : Functor.{v_2, v_3, u_3, u_4} D E
inst_11 : F.Full
inst_12 : F.EssSurj
inst_13 : Linear R (F ⋙ G)
X Y : D
f : X ⟶ Y
r : R
obtain :
  ∀ (f' : F.objPreimage X ⟶ F.objPreimage Y)
    (hf' : F.map f' = Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y)),
    ∃ (X' : C) (Y' : C) (eX : F.obj X' ≅ X) (eY : F.obj Y' ≅ Y) (f' : X' ⟶ Y'), f = eX.inv ≫ F.map f' ≫ eY.hom
⊢ ∃ (X' : C) (Y' : C) (eX : F.obj X' ≅ X) (eY : F.obj Y' ≅ Y) (f' : X' ⟶ Y'), f = eX.inv ≫ F.map f' ≫ eY.hom

Tactic:
obtain ⟨f', hf'⟩ :=
      F.map_surjective ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)

Premises used: CategoryTheory.Functor.objObjPreimageIso, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.Functor.map_surjective
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
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
inst_7 : Linear R F
E : Type u_4
inst_8 : Category.{v_3, u_4} E
inst_9 : Preadditive.{v_3, u_4} E
inst_10 : CategoryTheory.Linear.{u_1, v_3, u_4} R E
G : Functor.{v_2, v_3, u_3, u_4} D E
inst_11 : F.Full
inst_12 : F.EssSurj
inst_13 : Linear R (F ⋙ G)
X Y : D
f : X ⟶ Y
r : R
f' : F.objPreimage X ⟶ F.objPreimage Y
hf' : F.map f' = Iso.hom (F.objObjPreimageIso X) ≫ f ≫ Iso.inv (F.objObjPreimageIso Y)
⊢ ∃ (X' : C) (Y' : C) (eX : F.obj X' ≅ X) (eY : F.obj Y' ≅ Y) (f' : X' ⟶ Y'), f = eX.inv ≫ F.map f' ≫ eY.hom

Tactic:
exact ⟨_, _, F.objObjPreimageIso X, F.objObjPreimageIso Y, f', by cat_disch⟩
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
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
inst_7 : Linear R F
E : Type u_4
inst_8 : Category.{v_3, u_4} E
inst_9 : Preadditive.{v_3, u_4} E
inst_10 : CategoryTheory.Linear.{u_1, v_3, u_4} R E
G : Functor.{v_2, v_3, u_3, u_4} D E
inst_11 : F.Full
inst_12 : F.EssSurj
inst_13 : Linear R (F ⋙ G)
X Y : D
f : X ⟶ Y
r : R
obtain :
  ∀ (X' Y' : C) (eX : F.obj X' ≅ X) (eY : F.obj Y' ≅ Y) (f' : X' ⟶ Y'),
    G.map (r • eX.inv ≫ F.map f' ≫ eY.hom) = r • G.map (eX.inv ≫ F.map f' ≫ eY.hom)
⊢ G.map (r • f) = r • G.map f

Tactic:
obtain ⟨X', Y', eX, eY, f', rfl⟩ :
      ∃ (X' Y' : C) (eX : F.obj X' ≅ X) (eY : F.obj Y' ≅ Y)
        (f' : X' ⟶ Y'), f = eX.inv ≫ F.map f' ≫ eY.hom := by
    obtain ⟨f', hf'⟩ :=
      F.map_surjective ((F.objObjPreimageIso X).hom ≫ f ≫ (F.objObjPreimageIso Y).inv)
    exact ⟨_, _, F.objObjPreimageIso X, F.objObjPreimageIso Y, f', by cat_disch⟩

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
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
inst_7 : Linear R F
E : Type u_4
inst_8 : Category.{v_3, u_4} E
inst_9 : Preadditive.{v_3, u_4} E
inst_10 : CategoryTheory.Linear.{u_1, v_3, u_4} R E
G : Functor.{v_2, v_3, u_3, u_4} D E
inst_11 : F.Full
inst_12 : F.EssSurj
inst_13 : Linear R (F ⋙ G)
X Y : D
r : R
X' Y' : C
eX : F.obj X' ≅ X
eY : F.obj Y' ≅ Y
f' : X' ⟶ Y'
⊢ G.map (r • eX.inv ≫ F.map f' ≫ eY.hom) = r • G.map (eX.inv ≫ F.map f' ≫ eY.hom)

Tactic:
simpa only [comp_map, map_smul, Linear.smul_comp, Linear.comp_smul, ← G.map_comp]
    using G.map eX.inv ≫= ((F ⋙ G).map_smul r f') =≫ G.map eY.hom

Premises used: CategoryTheory.Functor.comp, CategoryTheory.Functor.map_smul, CategoryTheory.Functor.map, CategoryTheory.Linear.comp_smul, CategoryTheory.Functor.map_comp, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv, CategoryTheory.Functor.comp_map, CategoryTheory.Linear.smul_comp
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
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
inst_7 : Linear R F
E : Type u_4
inst_8 : Category.{v_3, u_4} E
inst_9 : Preadditive.{v_3, u_4} E
inst_10 : CategoryTheory.Linear.{u_1, v_3, u_4} R E
G : Functor.{v_2, v_3, u_3, u_4} D E
inst_11 : F.Full
inst_12 : F.EssSurj
⊢ Linear R (F ⋙ G) ↔ Linear R G

Tactic:
⟨fun _ ↦ linear_of_full_essSurj_comp F G, fun _ ↦ inferInstance⟩

Premises used: inferInstance, Iff.intro, CategoryTheory.Functor.linear_of_full_essSurj_comp
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
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
inst_7 : Linear R F
inst_8 : F.Additive
X Y : C
⊢ Eq (α := (a : X ⟶ Y) → F.obj X ⟶ F.obj Y) (⇑(mapLinearMap R F) : (a : X ⟶ Y) → F.obj X ⟶ F.obj Y) F.map

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
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 G : Functor.{v_1, v_2, u_2, u_3} C D
e : F ≅ G
inst_7 : Linear R F
X Y : C
f : X ⟶ Y
r : R
⊢ G.map (r • f) = r • G.map f

Tactic:
simp only [← NatIso.naturality_1 e (r • f), F.map_smul, Linear.smul_comp,
          NatTrans.naturality, Linear.comp_smul, Iso.inv_hom_id_app_assoc]

Premises used: CategoryTheory.NatIso.naturality_1, CategoryTheory.Functor.map_smul, CategoryTheory.Linear.comp_smul, CategoryTheory.NatTrans.naturality, HSMul.hSMul, CategoryTheory.Iso.inv_hom_id_app_assoc, CategoryTheory.Linear.smul_comp
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
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 G : Functor.{v_1, v_2, u_2, u_3} C D
e : F ≅ G
inst_7 : Linear R F
⊢ Linear R G

Tactic:
exact
    { map_smul := fun f r => by
        simp only [← NatIso.naturality_1 e (r • f), F.map_smul, Linear.smul_comp,
          NatTrans.naturality, Linear.comp_smul, Iso.inv_hom_id_app_assoc] }
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
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 : Linear.{u_1, v_1, u_2} R C
inst_6 : Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
e : Equivalence.{v_1, v_2, u_2, u_3} C D
inst_7 : Functor.Linear R e.functor
X Y : D
r : X ⟶ Y
f : R
a : e.functor.map (e.inverse.map (f • r)) = e.functor.map (f • e.inverse.map r)
⊢ e.inverse.map (f • r) = f • e.inverse.map r

Tactic:
apply e.functor.map_injective

Premises used: CategoryTheory.Equivalence.functor, CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Linear.LinearFunctor
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 : Linear.{u_1, v_1, u_2} R C
inst_6 : Linear.{u_1, v_2, u_3} R D
F : Functor.{v_1, v_2, u_2, u_3} C D
e : Equivalence.{v_1, v_2, u_2, u_3} C D
inst_7 : Functor.Linear R e.functor
X Y : D
r : X ⟶ Y
f : R
⊢ e.functor.map (e.inverse.map (f • r)) = e.functor.map (f • e.inverse.map r)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Linear.Yoneda
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : Linear.{w, v, u} R C
⊢ Eq (α := C ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ (Type v))
    (linearYoneda R C ⋙
      obj (whiskeringRight Cᵒᵖ (ModuleCat.{v, w} R) (Type v))
        (forget (ModuleCat.{v, w} R) (FC := fun (x1 x2 : ModuleCat.{v, w} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
          (CC := ModuleCat.carrier)))
    yoneda

Tactic:
rfl

Premises used: CategoryTheory.Functor.comp, CategoryTheory.yoneda, CategoryTheory.Functor.whiskerRight, rfl
-- Module: Mathlib.CategoryTheory.Linear.Yoneda
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : Linear.{w, v, u} R C
⊢ Eq (α := C ⥤ Functor.{v, v, u, v + 1} Cᵒᵖ AddCommGrpCat)
    (linearYoneda R C ⋙
      obj (whiskeringRight Cᵒᵖ (ModuleCat.{v, w} R) AddCommGrpCat)
        (forget₂ (ModuleCat.{v, w} R) (FC := fun (x1 x2 : ModuleCat.{v, w} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
          (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
          (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier)))
    preadditiveYoneda

Tactic:
rfl

Premises used: LinearMap.toAddMonoidHom, CategoryTheory.preadditiveYoneda, CategoryTheory.Functor.comp, CategoryTheory.End, CategoryTheory.Functor.whiskerRight, CategoryTheory.Linear.leftComp, CategoryTheory.preadditiveYonedaObj, rfl
-- Module: Mathlib.CategoryTheory.Linear.Yoneda
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : Linear.{w, v, u} R C
⊢ Eq (α := Cᵒᵖ ⥤ C ⥤ Type v)
    (linearCoyoneda R C ⋙
      obj (whiskeringRight C (ModuleCat.{v, w} R) (Type v))
        (forget (ModuleCat.{v, w} R) (FC := fun (x1 x2 : ModuleCat.{v, w} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
          (CC := ModuleCat.carrier)))
    coyoneda

Tactic:
rfl

Premises used: CategoryTheory.Functor.flip, CategoryTheory.Functor.comp, CategoryTheory.Functor.whiskerRight, rfl
-- Module: Mathlib.CategoryTheory.Linear.Yoneda
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : Linear.{w, v, u} R C
⊢ Eq (α := Cᵒᵖ ⥤ C ⥤ AddCommGrpCat)
    (linearCoyoneda R C ⋙
      obj (whiskeringRight C (ModuleCat.{v, w} R) AddCommGrpCat)
        (forget₂ (ModuleCat.{v, w} R) (FC := fun (x1 x2 : ModuleCat.{v, w} R) ↦ (↑x1 : Type v) →ₗ[R] (↑x2 : Type v))
          (CC := ModuleCat.carrier) AddCommGrpCat (FD := fun (x1 x2 : AddCommGrpCat.{v}) ↦
          (↑x1 : Type v) →+ (↑x2 : Type v)) (CD := AddCommGrpCat.carrier)))
    preadditiveCoyoneda

Tactic:
rfl

Premises used: LinearMap.toAddMonoidHom, MulOpposite, CategoryTheory.Functor.comp, CategoryTheory.preadditiveCoyonedaObj, CategoryTheory.Functor.whiskerRight, CategoryTheory.Linear.rightComp, CategoryTheory.preadditiveCoyoneda, rfl
-- Module: Mathlib.CategoryTheory.Linear.Yoneda
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : Linear.{w, v, u} R C
⊢ Full (D := Cᵒᵖ ⥤ ModuleCat.{v, w} R) (linearYoneda R C)

Tactic:
let _ : Functor.Full (linearYoneda R C ⋙ (whiskeringRight _ _ _).obj
    (forget (ModuleCat.{v} R))) := Yoneda.yoneda_full
  Functor.Full.of_comp_faithful (linearYoneda R C)
    ((whiskeringRight _ _ _).obj (forget (ModuleCat.{v} R)))

Premises used: Opposite, ModuleCat, CategoryTheory.Functor.whiskeringRight, CategoryTheory.Yoneda.yoneda_full, CategoryTheory.forget, CategoryTheory.linearYoneda, CategoryTheory.Functor.Full.of_comp_faithful, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Linear.Yoneda
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : Linear.{w, v, u} R C
⊢ Full (D := C ⥤ ModuleCat.{v, w} R) (linearCoyoneda R C)

Tactic:
let _ : Functor.Full (linearCoyoneda R C ⋙ (whiskeringRight _ _ _).obj
    (forget (ModuleCat.{v} R))) := Coyoneda.coyoneda_full
  Functor.Full.of_comp_faithful (linearCoyoneda R C)
    ((whiskeringRight _ _ _).obj (forget (ModuleCat.{v} R)))

Premises used: ModuleCat, CategoryTheory.linearCoyoneda, CategoryTheory.Functor.whiskeringRight, CategoryTheory.forget, CategoryTheory.Coyoneda.coyoneda_full, CategoryTheory.Functor.Full.of_comp_faithful, CategoryTheory.Functor.obj
-- Module: Mathlib.CategoryTheory.Linear.Yoneda
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : Linear.{w, v, u} R C
⊢ Faithful (D := Cᵒᵖ ⥤ ModuleCat.{v, w} R) (linearYoneda R C)

Tactic:
Functor.Faithful.of_comp_eq (whiskering_linearYoneda R C)

Premises used: CategoryTheory.whiskering_linearYoneda, CategoryTheory.Functor.Faithful.of_comp_eq
-- Module: Mathlib.CategoryTheory.Linear.Yoneda
Goal:
R : Type w
inst : Ring R
C : Type u
inst_1 : Category.{v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : Linear.{w, v, u} R C
⊢ Faithful (D := C ⥤ ModuleCat.{v, w} R) (linearCoyoneda R C)

Tactic:
Functor.Faithful.of_comp_eq (whiskering_linearCoyoneda R C)

Premises used: CategoryTheory.whiskering_linearCoyoneda, CategoryTheory.Functor.Faithful.of_comp_eq
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
this : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') := Lifting.mk (W := W₁) (Iso.symm (CatCommSq.iso (G ⋙ F) L₁ L₁ (G' ⋙ F')))
⊢ 𝟭 D₁ ⟶ G' ⋙ F'

Tactic:
exact Localization.liftNatTrans L₁ W₁ L₁ ((G ⋙ F) ⋙ L₁) (𝟭 D₁) (G' ⋙ F')
    (whiskerRight adj.unit L₁)

Premises used: CategoryTheory.Localization.liftNatTrans, CategoryTheory.Functor.comp, CategoryTheory.Adjunction.unit, CategoryTheory.Functor.id, CategoryTheory.Functor.whiskerRight
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_5 : CatCommSq G L₁ L₂ G'
inst_6 : CatCommSq F L₂ L₁ F'
X₁ : C₁
this : Lifting L₁ W₁ ((G ⋙ F) ⋙ L₁) (G' ⋙ F') := Lifting.mk (W := W₁) (Iso.symm (CatCommSq.iso (G ⋙ F) L₁ L₁ (G' ⋙ F')))
⊢ (ε adj L₁ W₁ L₂ G' F').app (L₁.obj X₁) =
    L₁.map (adj.unit.app X₁) ≫
      (CatCommSq.iso F L₂ L₁ F').hom.app (G.obj X₁) ≫ F'.map ((CatCommSq.iso G L₁ L₂ G').hom.app X₁)

Tactic:
simp only [ε, liftNatTrans_app, Lifting.iso, Iso.symm,
    Functor.id_obj, Functor.comp_obj, Functor.rightUnitor_hom_app,
      whiskerRight_app, CatCommSq.hComp_iso_hom_app, id_comp]

Premises used: CategoryTheory.Functor.comp_obj, CategoryTheory.CatCommSq.hComp_iso_hom_app, CategoryTheory.Localization.Lifting.iso, CategoryTheory.Functor.rightUnitor_hom_app, CategoryTheory.Localization.liftNatTrans_app, CategoryTheory.Functor.id_obj, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Iso.symm, CategoryTheory.Adjunction.Localization.ε, CategoryTheory.Category.id_comp
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
W₁ : MorphismProperty.{v_1, u_1} C₁
inst_4 : L₁.IsLocalization W₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_5 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_6 : CatCommSq G L₁ L₂ G'
inst_7 : CatCommSq F L₂ L₁ F'
this : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') := Lifting.mk (W := W₂) (Iso.symm (CatCommSq.iso (F ⋙ G) L₂ L₂ (F' ⋙ G')))
⊢ F' ⋙ G' ⟶ 𝟭 D₂

Tactic:
exact liftNatTrans L₂ W₂ ((F ⋙ G) ⋙ L₂) L₂ (F' ⋙ G') (𝟭 D₂) (whiskerRight adj.counit L₂)

Premises used: CategoryTheory.Localization.liftNatTrans, CategoryTheory.Functor.comp, CategoryTheory.Functor.id, CategoryTheory.Adjunction.counit, CategoryTheory.Functor.whiskerRight
-- Module: Mathlib.CategoryTheory.Localization.Adjunction
Goal:
C₁ : Type u_1
C₂ : Type u_2
D₁ : Type u_3
D₂ : Type u_4
inst : Category.{v_1, u_1} C₁
inst_1 : Category.{v_2, u_2} C₂
inst_2 : Category.{v_3, u_3} D₁
inst_3 : Category.{v_4, u_4} D₂
G : Functor.{v_1, v_2, u_1, u_2} C₁ C₂
F : Functor.{v_2, v_1, u_2, u_1} C₂ C₁
adj : G ⊣ F
L₁ : Functor.{v_1, v_3, u_1, u_3} C₁ D₁
L₂ : Functor.{v_2, v_4, u_2, u_4} C₂ D₂
W₂ : MorphismProperty.{v_2, u_2} C₂
inst_4 : L₂.IsLocalization W₂
G' : Functor.{v_3, v_4, u_3, u_4} D₁ D₂
F' : Functor.{v_4, v_3, u_4, u_3} D₂ D₁
inst_5 : CatCommSq G L₁ L₂ G'
inst_6 : CatCommSq F L₂ L₁ F'
X₂ : C₂
this : Lifting L₂ W₂ ((F ⋙ G) ⋙ L₂) (F' ⋙ G') := Lifting.mk (W := W₂) (Iso.symm (CatCommSq.iso (F ⋙ G) L₂ L₂ (F' ⋙ G')))
⊢ (η adj L₁ L₂ W₂ G' F').app (L₂.obj X₂) =
    G'.map ((CatCommSq.iso F L₂ L₁ F').inv.app X₂) ≫
      (CatCommSq.iso G L₁ L₂ G').inv.app (F.obj X₂) ≫ L₂.map (adj.counit.app X₂)

Tactic:
simp only [η, liftNatTrans_app, Lifting.iso, Iso.symm, CatCommSq.hComp_iso_inv_app,
    whiskerRight_app, Functor.rightUnitor_inv_app, comp_id, assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.Localization.Lifting.iso, CategoryTheory.Category.comp_id, CategoryTheory.Localization.liftNatTrans_app, CategoryTheory.Adjunction.Localization.η, CategoryTheory.CatCommSq.hComp_iso_inv_app, CategoryTheory.Functor.whiskerRight_app, CategoryTheory.Iso.symm, CategoryTheory.Functor.rightUnitor_inv_app