awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
M₁ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
X : Cᵒᵖ
⊢ Hom.app (Iso.inv (λ_ M₁)) X = Iso.inv (λ_ (M₁.obj X))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
M₁ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
X : Cᵒᵖ
⊢ Hom.app (Iso.hom (ρ_ M₁)) X = Iso.hom (ρ_ (M₁.obj X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
M₁ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
X : Cᵒᵖ
⊢ Hom.app (Iso.inv (ρ_ M₁)) X = Iso.inv (ρ_ (M₁.obj X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
M₁ M₂ M₃ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
X : Cᵒᵖ
⊢ Hom.app (Iso.hom (α_ M₁ M₂ M₃)) X = Iso.hom (α_ (M₁.obj X) (M₂.obj X) (M₃.obj X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
M₁ M₂ M₃ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
X : Cᵒᵖ
⊢ Hom.app (Iso.inv (α_ M₁ M₂ M₃)) X = Iso.inv (α_ (M₁.obj X) (M₂.obj X) (M₃.obj X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
M₁ M₂ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
X : Cᵒᵖ
⊢ Hom.app (Iso.hom (β_ M₁ M₂)) X = Iso.hom (β_ (M₁.obj X) (M₂.obj X))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
M₁ M₂ :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
X : Cᵒᵖ
⊢ Hom.app (Iso.inv (β_ M₁ M₂)) X = Iso.inv (β_ (M₁.obj X) (M₂.obj X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
R : CategoryTheory.Functor.{v_1, u, u_1, u + 1} Cᵒᵖ CommRingCat
F :
  PresheafOfModules
    (R ⋙
      forget₂ CommRingCat (FC := fun (R S : CommRingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CC :=
        CommRingCat.carrier) RingCat (FD := fun (R S : RingCat.{u}) ↦ (↑R : Type u) →+* (↑S : Type u)) (CD :=
        RingCat.carrier))
⊢ PreservesColimitsOfSize.{u, u, max u u_1, max u u_1, max (max (u + 1) u_1) v_1, max (max (u + 1) u_1) v_1}
    (tensorRight F)

Tactic:
preservesColimits_of_natIso (tensorLeftIsoTensorRight F)

Premises used: CategoryTheory.BraidedCategory.tensorLeftIsoTensorRight, CategoryTheory.Limits.preservesColimits_of_natIso
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
X : C
M N : PresheafOfModules R
g : M ⟶ N
f : (free R).obj (Functor.obj yoneda (F.obj X)) ⟶ M
erw :
  ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(S.obj (op X)) : Type u)) ↦
          LinearMap (R := (↑(S.obj (op X)) : Type u)) (RingHom.id (↑(S.obj (op X)) : Type u)) (↑x1 : Type u)
            (↑x2 : Type u))
          (CC := ModuleCat.carrier) (((pushforward φ).map g).app (op X)) :
        (a : (↑(((pushforward φ).obj M).obj (op X)) : Type u)) → (↑(((pushforward φ).obj N).obj (op X)) : Type u))
      ((freeYonedaEquiv :
            (a : (free S).obj (yoneda.obj X) ⟶ (pushforward φ).obj M) →
              (↑(((pushforward φ).obj M).obj (op X)) : Type u))
          (((Equiv.trans freeYonedaEquiv (Equiv.symm freeYonedaEquiv) :
                  (freeObj (Functor.obj yoneda (F.obj X)) ⟶ M) ≃
                    (freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj M)) :
                (a : freeObj (yoneda.obj (F.obj X)) ⟶ M) → freeObj (yoneda.obj X) ⟶ (pushforward φ).obj M)
              f :
            freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj M) :
        (↑(((pushforward φ).obj M).obj (op X)) : Type u)) :
    (↑(((pushforward φ).obj N).obj (op X)) : Type u))
| ((freeYonedaEquiv :
        (a : freeObj (yoneda.obj X) ⟶ (pushforward φ).obj N) →
          (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app (op X)))).obj ((pushforward₀Obj F R N).obj (op X))) :
            Type u))
      (({ toFun := fun (g_1 : freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj M) ↦ g_1 ≫ (pushforward φ).map g } :
            (a : freeObj (yoneda.obj X) ⟶ (pushforward φ).obj M) → freeObj (yoneda.obj X) ⟶ (pushforward φ).obj N)
          (((Equiv.trans freeYonedaEquiv (Equiv.symm freeYonedaEquiv) :
                  (freeObj (Functor.obj yoneda (F.obj X)) ⟶ M) ≃
                    (freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj M)) :
                (a : freeObj (yoneda.obj (F.obj X)) ⟶ M) → freeObj (yoneda.obj X) ⟶ (pushforward φ).obj M)
              f :
            freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj M) :
        freeObj (Functor.obj yoneda X) ⟶ (pushforward φ).obj N) :
    (↑(Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app (op X)))) ((pushforward₀Obj F R N).obj (op X))) :
      Type u))

Tactic:
erw [freeYonedaEquiv_comp]

Premises used: PresheafOfModules.freeYonedaEquiv_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
X : C
M N : PresheafOfModules R
g : M ⟶ N
f : (free R).obj (Functor.obj yoneda (F.obj X)) ⟶ M
⊢ Eq (α :=
    (↑(Functor.obj (ModuleCat.restrictScalars (RingCat.Hom.hom (φ.app (op X)))) ((pushforward₀Obj F R N).obj (op X))) :
      Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(R.obj (op (F.obj X))) : Type u)) ↦
            LinearMap (R := (↑(R.obj (op (F.obj X))) : Type u)) (RingHom.id (↑(R.obj (op (F.obj X))) : Type u))
              (↑x1 : Type u) (↑x2 : Type u))
            (CC := ModuleCat.carrier) (g.app (op (F.obj X))) :
          (a : (↑(M.obj (op (F.obj X))) : Type u)) → (↑(N.obj (op (F.obj X))) : Type u))
        ((freeYonedaEquiv : (a : (free R).obj (yoneda.obj (F.obj X)) ⟶ M) → (↑(M.obj (op (F.obj X))) : Type u)) f :
          (↑(M.obj (op (F.obj X))) : Type u)) :
      (↑(N.obj (op (F.obj X))) : Type u))
    ((ConcreteCategory.hom (FC := fun (x1 x2 : ModuleCat (↑(S.obj (op X)) : Type u)) ↦
            LinearMap (R := (↑(S.obj (op X)) : Type u)) (RingHom.id (↑(S.obj (op X)) : Type u)) (↑x1 : Type u)
              (↑x2 : Type u))
            (CC := ModuleCat.carrier) (((pushforward φ).map g).app (op X)) :
          (a : (↑(((pushforward φ).obj M).obj (op X)) : Type u)) → (↑(((pushforward φ).obj N).obj (op X)) : Type u))
        ((freeYonedaEquiv : (a : freeObj (yoneda.obj (F.obj X)) ⟶ M) → (↑(M.obj (op (F.obj X))) : Type u)) f :
          (↑(M.obj (op (F.obj X))) : Type u)) :
      (↑(((pushforward φ).obj N).obj (op X)) : Type u))

Tactic:
rfl
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
X : C
⊢ pullbackObjIsDefined φ ((free S).obj (Functor.obj yoneda X))

Tactic:
(pushforwardCompCoyonedaFreeYonedaCorepresentableBy φ X).isCorepresentable

Premises used: PresheafOfModules.pushforwardCompCoyonedaFreeYonedaCorepresentableBy, CategoryTheory.Functor.CorepresentableBy.isCorepresentable, CategoryTheory.Functor.leftAdjointObjIsDefined
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
h : ∀ (M : PresheafOfModules S), pullbackObjIsDefined φ M ↔ ⊤ M
⊢ pullbackObjIsDefined φ = ⊤

Tactic:
ext M
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
h : pullbackObjIsDefined φ M
⊢ pullbackObjIsDefined φ M ↔ ⊤ M

Tactic:
simp only [Pi.top_apply, Prop.top_eq_true, iff_true]

Premises used: iff_true, Pi.top_apply, Prop.top_eq_true
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
h :
  ∀ (j : WalkingParallelPair), (pushforward φ).leftAdjointObjIsDefined ((parallelPair M.toFreeYonedaCoproduct 0).obj j)
⊢ pullbackObjIsDefined φ M

Tactic:
apply leftAdjointObjIsDefined_of_isColimit
    M.isColimitFreeYonedaCoproductsCokernelCofork

Premises used: PresheafOfModules.isColimitFreeYonedaCoproductsCokernelCofork, CategoryTheory.Functor.leftAdjointObjIsDefined_of_isColimit
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ (pushforward φ).leftAdjointObjIsDefined ((parallelPair M.toFreeYonedaCoproduct 0).obj WalkingParallelPair.zero)

Tactic:
apply leftAdjointObjIsDefined_colimit _
      (fun _ ↦ pullbackObjIsDefined_free_yoneda _ _)

Premises used: CategoryTheory.Functor.leftAdjointObjIsDefined_colimit
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
M : PresheafOfModules S
⊢ (pushforward φ).leftAdjointObjIsDefined ((parallelPair M.toFreeYonedaCoproduct 0).obj WalkingParallelPair.one)

Tactic:
apply leftAdjointObjIsDefined_colimit _
      (fun _ ↦ pullbackObjIsDefined_free_yoneda _ _)

Premises used: CategoryTheory.Functor.leftAdjointObjIsDefined_colimit
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
Goal:
C D : Type u
inst : SmallCategory C
inst_1 : SmallCategory D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
⊢ (pushforward φ).IsRightAdjoint

Tactic:
isRightAdjoint_of_leftAdjointObjIsDefined_eq_top
    (pullbackObjIsDefined_eq_top φ)

Premises used: CategoryTheory.Functor.isRightAdjoint_of_leftAdjointObjIsDefined_eq_top, PresheafOfModules.pullbackObjIsDefined_eq_top
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ RingCat
S : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
φ : S ⟶ F.op ⋙ R
G : CategoryTheory.Functor.{v₂, v₃, u₂, u₃} D E
T : CategoryTheory.Functor.{v₃, u, u₃, u + 1} Eᵒᵖ RingCat
ψ : R ⟶ G.op ⋙ T
⊢ IsRightAdjoint (C := PresheafOfModules.{v, v₁, u₁, u} S) (D := PresheafOfModules.{v, v₁, u₁, u} S)
    (pushforward (F := 𝟭 C) (𝟙 S))

Tactic:
isRightAdjoint_of_iso (pushforwardId.{v} S).symm

Premises used: PresheafOfModules.pushforwardId, CategoryTheory.Iso.symm, CategoryTheory.Functor.isRightAdjoint_of_iso
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ RingCat
S : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
φ : S ⟶ F.op ⋙ R
G : CategoryTheory.Functor.{v₂, v₃, u₂, u₃} D E
T : CategoryTheory.Functor.{v₃, u, u₃, u + 1} Eᵒᵖ RingCat
ψ : R ⟶ G.op ⋙ T
inst_4 : (pushforward φ).IsRightAdjoint
inst_5 : (pushforward ψ).IsRightAdjoint
⊢ (pushforward (φ ≫ F.op.whiskerLeft ψ)).IsRightAdjoint

Tactic:
isRightAdjoint_of_iso (pushforwardComp.{v} φ ψ)

Premises used: CategoryTheory.Functor.isRightAdjoint_of_iso, PresheafOfModules.pushforwardComp
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ RingCat
S : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
φ : S ⟶ F.op ⋙ R
G : CategoryTheory.Functor.{v₂, v₃, u₂, u₃} D E
T : CategoryTheory.Functor.{v₃, u, u₃, u + 1} Eᵒᵖ RingCat
ψ : R ⟶ G.op ⋙ T
inst_4 : (pushforward φ).IsRightAdjoint
inst_5 : (pushforward ψ).IsRightAdjoint
T' : CategoryTheory.Functor.{v₄, u, u₄, u + 1} E'ᵒᵖ RingCat
G' : CategoryTheory.Functor.{v₃, v₄, u₃, u₄} E E'
ψ' : T ⟶ G'.op ⋙ T'
inst_6 : (pushforward ψ').IsRightAdjoint
⊢ Eq (α := pullback φ ⋙ pullback ψ ⋙ pullback ψ' ≅ pullback (φ ≫ F.op.whiskerLeft (ψ ≫ G.op.whiskerLeft ψ')))
    ((pullback φ).isoWhiskerLeft (pullbackComp ψ ψ') ≪≫ pullbackComp φ (ψ ≫ G.op.whiskerLeft ψ'))
    (((pullback φ).associator (pullback ψ) (pullback ψ')).symm ≪≫
      isoWhiskerRight (pullbackComp φ ψ) (pullback ψ') ≪≫ pullbackComp (φ ≫ F.op.whiskerLeft ψ) ψ')

Tactic:
Adjunction.leftAdjointCompIso_assoc _ _ _ _ _ _ _ _ _ _ (pushforward_assoc φ ψ ψ')

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Functor.op, CategoryTheory.Functor.comp, PresheafOfModules.pushforward_assoc, PresheafOfModules.pullbackComp, CategoryTheory.Adjunction.leftAdjointCompIso_assoc
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ RingCat
S : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
φ : S ⟶ F.op ⋙ R
inst_2 : (pushforward φ).IsRightAdjoint
⊢ pullbackComp (𝟙 S) φ = isoWhiskerRight (pullbackId S) (pullback φ) ≪≫ (pullback φ).leftUnitor

Tactic:
Adjunction.leftAdjointCompIso_id_comp _ _ _ _ (pushforward_comp_id φ)

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Functor.comp, CategoryTheory.Adjunction.leftAdjointCompIso_id_comp, PresheafOfModules.pullbackComp, PresheafOfModules.pullbackId, PresheafOfModules.pushforward_comp_id
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pullback
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ RingCat
S : CategoryTheory.Functor.{v₁, u, u₁, u + 1} Cᵒᵖ RingCat
φ : S ⟶ F.op ⋙ R
inst_2 : (pushforward φ).IsRightAdjoint
⊢ pullbackComp φ (𝟙 R) = (pullback φ).isoWhiskerLeft (pullbackId R) ≪≫ (pullback φ).rightUnitor

Tactic:
Adjunction.leftAdjointCompIso_comp_id _ _ _ _ (pushforward_id_comp φ)

Premises used: CategoryTheory.NatTrans.vcomp, CategoryTheory.Functor.comp, PresheafOfModules.pullbackComp, CategoryTheory.Adjunction.leftAdjointCompIso_comp_id, PresheafOfModules.pullbackId, PresheafOfModules.pushforward_id_comp
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ RingCat
M : PresheafOfModules.{u_1, v₂, u₂, u} R
X : Cᵒᵖ
⊢ M.map (F.op.map (𝟙 X)) =
    (ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((F.op ⋙ R).map (𝟙 X))) ⋯).inv.app
      (ModuleCat.of (↑((F.op ⋙ R).obj X) : Type u) (↑(M.obj (F.op.obj X)) : Type u_1))

Tactic:
ModuleCat.hom_ext
        -- Work around an instance diamond for `restrictScalarsId'`
        (@LinearMap.ext _ _ _ _ _ _ _ _ (_) (_) _ _ _ (fun x => ?_))

Premises used: LinearMap.ext, ModuleCat.hom_ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ RingCat
M : PresheafOfModules.{u_1, v₂, u₂, u} R
X : Cᵒᵖ
refine :
  ∀ (x : (↑(M.obj (F.op.obj X)) : Type u_1)),
    Eq (α :=
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) : Type u_1))
      ((ModuleCat.Hom.hom (M.map (F.op.map (𝟙 X))) :
            (a : (↑(M.obj (F.op.obj X)) : Type u_1)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) :
                Type u_1))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) : Type u_1))
      ((ModuleCat.Hom.hom
              ((ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((F.op ⋙ R).map (𝟙 X))) ⋯).inv.app
                (ModuleCat.of (↑((F.op ⋙ R).obj X) : Type u) (↑(M.obj (F.op.obj X)) : Type u_1))) :
            (a : (↑(M.obj (F.op.obj X)) : Type u_1)) →
              (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) :
                Type u_1))
          x :
        (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) : Type u_1))
⊢ M.map (F.op.map (𝟙 X)) =
    (ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((F.op ⋙ R).map (𝟙 X))) ⋯).inv.app
      (ModuleCat.of (↑((F.op ⋙ R).obj X) : Type u) (↑(M.obj (F.op.obj X)) : Type u_1))

Tactic:
refine ModuleCat.hom_ext
        -- Work around an instance diamond for `restrictScalarsId'`
        (@LinearMap.ext _ _ _ _ _ _ _ _ (_) (_) _ _ _ (fun x => ?_))

Premises used: LinearMap.ext, ModuleCat.hom_ext
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ RingCat
M : PresheafOfModules.{u_1, v₂, u₂, u} R
X : Cᵒᵖ
x : (↑(M.obj (F.op.obj X)) : Type u_1)
⊢ Eq (α :=
    (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) : Type u_1))
    ((@ConcreteCategory.hom _ (ModuleCat.moduleCategory (↑(R.obj (F.op.obj X)) : Type u))
            (fun (x1 x2 : ModuleCat.{u_1, u} (↑(R.obj (F.op.obj X)) : Type u)) ↦
              LinearMap.{u, u, u_1, u_1} (R := (↑(R.obj (F.op.obj X)) : Type u))
                (RingHom.id (↑(R.obj (F.op.obj X)) : Type u)) (↑x1 : Type u_1) (↑x2 : Type u_1))
            ModuleCat.carrier
            (fun (X_1 Y : ModuleCat.{u_1, u} (↑(R.obj (F.op.obj X)) : Type u)) ↦
              (LinearMap.instFunLike :
                FunLike
                  (LinearMap.{u, u, u_1, u_1} (R := (↑(R.obj (F.op.obj X)) : Type u))
                    (RingHom.id (↑(R.obj (F.op.obj X)) : Type u)) (↑X_1 : Type u_1) (↑Y : Type u_1))
                  (↑X_1 : Type u_1) (↑Y : Type u_1)))
            _ _ _
            (M.map (𝟙 (F.op.obj X)) :
              M.obj (F.op.obj X) ⟶
                (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 (F.op.obj X))))).obj (M.obj (F.op.obj X))) :
          (a : (↑(M.obj (F.op.obj X)) : Type u_1)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 (F.op.obj X))))).obj (M.obj (F.op.obj X))) :
              Type u_1))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (𝟙 (F.op.obj X))))).obj (M.obj (F.op.obj X))) : Type u_1))
    ((ModuleCat.Hom.hom
            ((ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((F.op ⋙ R).map (𝟙 X))) ⋯).inv.app
              (ModuleCat.of (↑((F.op ⋙ R).obj X) : Type u) (↑(M.obj (F.op.obj X)) : Type u_1))) :
          (a : (↑(M.obj (F.op.obj X)) : Type u_1)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) :
              Type u_1))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) : Type u_1))

Tactic:
simp
-- Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
D : Type u₂
inst_1 : Category.{v₂, u₂} D
E : Type u₃
inst_2 : Category.{v₃, u₃} E
E' : Type u₄
inst_3 : Category.{v₄, u₄} E'
F : CategoryTheory.Functor.{v₁, v₂, u₁, u₂} C D
R : CategoryTheory.Functor.{v₂, u, u₂, u + 1} Dᵒᵖ RingCat
M : PresheafOfModules.{u_1, v₂, u₂, u} R
X : Cᵒᵖ
x : (↑(M.obj (F.op.obj X)) : Type u_1)
⊢ Eq (α :=
    (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) : Type u_1))
    ((ModuleCat.Hom.hom (M.map (F.op.map (𝟙 X))) :
          (a : (↑(M.obj (F.op.obj X)) : Type u_1)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) :
              Type u_1))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) : Type u_1))
    ((ModuleCat.Hom.hom
            ((ModuleCat.restrictScalarsId' (RingCat.Hom.hom ((F.op ⋙ R).map (𝟙 X))) ⋯).inv.app
              (ModuleCat.of (↑((F.op ⋙ R).obj X) : Type u) (↑(M.obj (F.op.obj X)) : Type u_1))) :
          (a : (↑(M.obj (F.op.obj X)) : Type u_1)) →
            (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) :
              Type u_1))
        x :
      (↑((ModuleCat.restrictScalars (RingCat.Hom.hom (R.map (F.op.map (𝟙 X))))).obj (M.obj (F.op.obj X))) : Type u_1))

Tactic:
exact (M.congr_map_apply (F.op.map_id X) x).trans (by simp)

Premises used: CategoryTheory.Functor.op, PresheafOfModules.congr_map_apply, CategoryTheory.Functor.map_id, Eq.trans