mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
p p' : J × K
f : p ⟶ p'
⊢ 𝟙 s.pt ≫ s.π.app p'.1 ≫ (D.obj p'.1).π.app p'.2 =
    (s.π.app p.1 ≫ (D.obj p.1).π.app p.2) ≫ (F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2

Tactic:
;

Goal state after:
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
p p' : J × K
f : p ⟶ p'
⊢ 𝟙 s.pt ≫ s.π.app p'.1 ≫ (D.obj p'.1).π.app p'.2 =
    (s.π.app p.1 ≫ (D.obj p.1).π.app p.2) ≫ (F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit (coneOfConeUncurry Q c)
E : (j : J) → Prod.sectR j K ⋙ uncurry.obj F ≅ F.obj j :=
  fun j ↦ NatIso.ofComponents (fun x ↦ Iso.refl ((Prod.sectR j K ⋙ uncurry.obj F).obj x)) ⋯
s : Cone (uncurry.obj F)
j' j : J
f : j' ⟶ j
k : K
⊢ (((const J).obj s.pt).map f ≫ (Q j).lift ((Cone.postcompose (E j).hom).obj (Cone.whisker (Prod.sectR j K) s))) ≫
      (D.obj j).π.app k =
    ((Q j').lift ((Cone.postcompose (E j').hom).obj (Cone.whisker (Prod.sectR j' K) s)) ≫ D.conePoints.map f) ≫
      (D.obj j).π.app k

Tactic:
simpa [E] using s.π.naturality ((Prod.sectL J k).map f)

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Fubini

Goal state before:
pp: J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
p p' : J × K
f : p ⟶ p'
⊢ ((F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2) ≫ (D.obj p'.1).ι.app p'.2 ≫ s.ι.app p'.1 =
    ((D.obj p.1).ι.app p.2 ≫ s.ι.app p.1) ≫ 𝟙 s.pt

Tactic:
;

Goal state after:
J : Type u_1
K : Type u_2
inst✝² : Category.{v_1, u_1} J
inst✝¹ : Category.{v_2, u_2} K
C : Type u_3
inst✝ : Category.{v_3, u_3} C
F : J ⥤ K ⥤ C
G : J × K ⥤ C
D : DiagramOfCocones F
Q : (j : J) → IsColimit (D.obj j)
c : Cocone (uncurry.obj F)
P : IsColimit c
s : Cocone D.coconePoints
p p' : J × K
f : p ⟶ p'
⊢ ((F.map f.1).app p.2 ≫ (F.obj p'.1).map f.2) ≫ (D.obj p'.1).ι.app p'.2 ≫ s.ι.app p'.1 =
    ((D.obj p.1).ι.app p.2 ≫ s.ι.app p.1) ≫ 𝟙 s.pt
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Generator

Goal state before:
pp: C : Type u
inst✝ : SmallCategory C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
m : M.Elements
⊢ (ConcreteCategory.hom (M.fromFreeYonedaCoproduct.app m.fst)) (M.freeYonedaCoproductMk m) = m.snd

Tactic:
by
  rw [freeYonedaCoproductMk, M.ι_fromFreeYonedaCoproduct_apply m, m.fromFreeYoneda_app_apply]

Goal state after:
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Free

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : F.obj X
⊢ (ConcreteCategory.hom (F.map f ≫ ↾fun x ↦ ModuleCat.freeMk x)).toFun x✝ =
    (ConcreteCategory.hom ((↾fun x ↦ ModuleCat.freeMk x) ≫ ((freeObj F).presheaf ⋙ forget Ab).map f)).toFun x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : F.obj X
⊢ (ConcreteCategory.hom (F.map f ≫ ↾fun x ↦ ModuleCat.freeMk x)).toFun x✝ =
    (ConcreteCategory.hom ((↾fun x ↦ ModuleCat.freeMk x) ≫ ((freeObj F).presheaf ⋙ forget Ab).map f)).toFun x✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Free

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
ψ : freeObj F ⟶ G
X : Cᵒᵖ
⊢ ((fun φ ↦ freeObjDesc φ)
          ((fun ψ ↦ freeAdjunctionUnit R F ≫ Functor.whiskerRight ((toPresheaf R).map ψ) (forget Ab)) ψ)).app
      X =
    ψ.app X

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
ψ : freeObj F ⟶ G
X : Cᵒᵖ
⊢ ((fun φ ↦ freeObjDesc φ)
          ((fun ψ ↦ freeAdjunctionUnit R F ≫ Functor.whiskerRight ((toPresheaf R).map ψ) (forget Ab)) ψ)).app
      X =
    ψ.app X
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Free

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
ψ : freeObj F ⟶ G
X : Cᵒᵖ
⊢ ModuleCat.freeDesc ((↾fun x ↦ ModuleCat.freeMk x) ≫ ↾⇑(ConcreteCategory.hom (((toPresheaf R).map ψ).app X))) = ψ.app X

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
ψ : freeObj F ⟶ G
X : Cᵒᵖ
⊢ ModuleCat.freeDesc ((↾fun x ↦ ModuleCat.freeMk x) ≫ ↾⇑(ConcreteCategory.hom (((toPresheaf R).map ψ).app X))) = ψ.app X
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Free

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
ψ : freeObj F ⟶ G
X : Cᵒᵖ
x : F.obj X
⊢ (ConcreteCategory.hom
        (ModuleCat.freeDesc ((↾fun x ↦ ModuleCat.freeMk x) ≫ ↾⇑(ConcreteCategory.hom (((toPresheaf R).map ψ).app X)))))
      (ModuleCat.freeMk x) =
    (ConcreteCategory.hom (ψ.app X)) (ModuleCat.freeMk x)

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
ψ : freeObj F ⟶ G
X : Cᵒᵖ
x : F.obj X
⊢ (ConcreteCategory.hom
        (ModuleCat.freeDesc ((↾fun x ↦ ModuleCat.freeMk x) ≫ ↾⇑(ConcreteCategory.hom (((toPresheaf R).map ψ).app X)))))
      (ModuleCat.freeMk x) =
    (ConcreteCategory.hom (ψ.app X)) (ModuleCat.freeMk x)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Free

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
φ : F ⟶ G.presheaf ⋙ forget Ab
x✝¹ : Cᵒᵖ
x✝ : F.obj x✝¹
⊢ (ConcreteCategory.hom
          (((fun ψ ↦ freeAdjunctionUnit R F ≫ Functor.whiskerRight ((toPresheaf R).map ψ) (forget Ab))
                ((fun φ ↦ freeObjDesc φ) φ)).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom (φ.app x✝¹)).toFun x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
φ : F ⟶ G.presheaf ⋙ forget Ab
x✝¹ : Cᵒᵖ
x✝ : F.obj x✝¹
⊢ (ConcreteCategory.hom
          (((fun ψ ↦ freeAdjunctionUnit R F ≫ Functor.whiskerRight ((toPresheaf R).map ψ) (forget Ab))
                ((fun φ ↦ freeObjDesc φ) φ)).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom (φ.app x✝¹)).toFun x✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Free

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G✝ : PresheafOfModules R
F₁ F₂ : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
f : F₁ ⟶ F₂
g : F₂ ⟶ (toPresheaf R ⋙ (Functor.whiskeringRight Cᵒᵖ Ab (Type u)).obj (forget Ab)).obj G
x✝¹ : Cᵒᵖ
x✝ : F₁.obj x✝¹
⊢ (ConcreteCategory.hom
          ((freeAdjunctionUnit R F₁ ≫
                Functor.whiskerRight ((toPresheaf R).map (freeHomEquiv.symm (f ≫ g))) (forget Ab)).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((freeAdjunctionUnit R F₁ ≫
                Functor.whiskerRight ((toPresheaf R).map ((free R).map f ≫ freeHomEquiv.symm g)) (forget Ab)).app
            x✝¹)).toFun
      x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
F : Cᵒᵖ ⥤ Type u
G✝ : PresheafOfModules R
F₁ F₂ : Cᵒᵖ ⥤ Type u
G : PresheafOfModules R
f : F₁ ⟶ F₂
g : F₂ ⟶ (toPresheaf R ⋙ (Functor.whiskeringRight Cᵒᵖ Ab (Type u)).obj (forget Ab)).obj G
x✝¹ : Cᵒᵖ
x✝ : F₁.obj x✝¹
⊢ (ConcreteCategory.hom
          ((freeAdjunctionUnit R F₁ ≫
                Functor.whiskerRight ((toPresheaf R).map (freeHomEquiv.symm (f ≫ g))) (forget Ab)).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          ((freeAdjunctionUnit R F₁ ≫
                Functor.whiskerRight ((toPresheaf R).map ((free R).map f ≫ freeHomEquiv.symm g)) (forget Ab)).app
            x✝¹)).toFun
      x✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : ModuleCat ↑cR.pt
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : ↑(R.obj X)
⊢ (RingCat.Hom.hom (cR.ι.app X)) x✝ = ((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f))) x✝

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : ModuleCat ↑cR.pt
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : ↑(R.obj X)
⊢ (RingCat.Hom.hom (cR.ι.app X)) x✝ = ((RingCat.Hom.hom (cR.ι.app Y)).comp (RingCat.Hom.hom (R.map f))) x✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : ModuleCat ↑cR.pt
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : ↑(R.obj X)
⊢ (RingCat.Hom.hom (cR.ι.app X)) x✝ = (RingCat.Hom.hom (cR.ι.app Y)) ((RingCat.Hom.hom (R.map f)) x✝)

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : ModuleCat ↑cR.pt
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : ↑(R.obj X)
⊢ (RingCat.Hom.hom (cR.ι.app X)) x✝ = (RingCat.Hom.hom (cR.ι.app Y)) ((RingCat.Hom.hom (R.map f)) x✝)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : ModuleCat ↑cR.pt
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : ↑(R.obj X)
⊢ (RingCat.Hom.hom (R.map f ≫ cR.ι.app Y)) x✝ = (RingCat.Hom.hom (cR.ι.app Y)) ((RingCat.Hom.hom (R.map f)) x✝)

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
M : ModuleCat ↑cR.pt
X Y : Cᵒᵖ
f : X ⟶ Y
x✝ : ↑(R.obj X)
⊢ (RingCat.Hom.hom (R.map f ≫ cR.ι.app Y)) x✝ = (RingCat.Hom.hom (cR.ι.app Y)) ((RingCat.Hom.hom (R.map f)) x✝)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
X✝ Y✝ Z✝ : PresheafOfModules R
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ModuleCat.Hom.hom
      (ModuleCat.ofHom
        (ModuleColimit.map hcR (colimit.isColimit X✝.presheaf) (colimit.isColimit Z✝.presheaf) (f ≫ g))) =
    ModuleCat.Hom.hom
      (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X✝.presheaf) (colimit.isColimit Y✝.presheaf) f) ≫
        ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit Y✝.presheaf) (colimit.isColimit Z✝.presheaf) g))

Tactic:
;

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : LocallySmall.{w, v, u} C
inst✝¹ : IsCofiltered C
inst✝ : InitiallySmall C
R : Cᵒᵖ ⥤ RingCat
cR : Cocone R
hcR : IsColimit cR
X✝ Y✝ Z✝ : PresheafOfModules R
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ModuleCat.Hom.hom
      (ModuleCat.ofHom
        (ModuleColimit.map hcR (colimit.isColimit X✝.presheaf) (colimit.isColimit Z✝.presheaf) (f ≫ g))) =
    ModuleCat.Hom.hom
      (ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit X✝.presheaf) (colimit.isColimit Y✝.presheaf) f) ≫
        ModuleCat.ofHom (ModuleColimit.map hcR (colimit.isColimit Y✝.presheaf) (colimit.isColimit Z✝.presheaf) g))
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

Goal state before:
pp: C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
T : Eᵒᵖ ⥤ RingCat
G : D ⥤ E
ψ : R ⟶ G.op ⋙ T
T' : E'ᵒᵖ ⥤ RingCat
G' : E ⥤ E'
ψ' : T ⟶ G'.op ⋙ T'
x✝¹ : PresheafOfModules T'
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward ψ' ⋙ pushforward ψ ⋙ pushforward φ).obj x✝¹).obj X✝)
⊢ (ModuleCat.Hom.hom
        ((((pushforward ψ').isoWhiskerLeft (pushforwardComp φ ψ) ≪≫ pushforwardComp (φ ≫ F.op.whiskerLeft ψ) ψ').hom.app
              x✝¹).app
          X✝))
      x✝ =
    (ModuleCat.Hom.hom
        (((((pushforward ψ').associator (pushforward ψ) (pushforward φ)).symm ≪≫
                    isoWhiskerRight (pushforwardComp ψ ψ') (pushforward φ) ≪≫
                      pushforwardComp φ (ψ ≫ G.op.whiskerLeft ψ')).hom.app
              x✝¹).app
          X✝))
      x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
D : Type u₂
inst✝² : Category.{v₂, u₂} D
E : Type u₃
inst✝¹ : Category.{v₃, u₃} E
E' : Type u₄
inst✝ : Category.{v₄, u₄} E'
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
T : Eᵒᵖ ⥤ RingCat
G : D ⥤ E
ψ : R ⟶ G.op ⋙ T
T' : E'ᵒᵖ ⥤ RingCat
G' : E ⥤ E'
ψ' : T ⟶ G'.op ⋙ T'
x✝¹ : PresheafOfModules T'
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward ψ' ⋙ pushforward ψ ⋙ pushforward φ).obj x✝¹).obj X✝)
⊢ (ModuleCat.Hom.hom
        ((((pushforward ψ').isoWhiskerLeft (pushforwardComp φ ψ) ≪≫ pushforwardComp (φ ≫ F.op.whiskerLeft ψ) ψ').hom.app
              x✝¹).app
          X✝))
      x✝ =
    (ModuleCat.Hom.hom
        (((((pushforward ψ').associator (pushforward ψ) (pushforward φ)).symm ≪≫
                    isoWhiskerRight (pushforwardComp ψ ψ') (pushforward φ) ≪≫
                      pushforwardComp φ (ψ ≫ G.op.whiskerLeft ψ')).hom.app
              x✝¹).app
          X✝))
      x✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
x✝¹ : PresheafOfModules R
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward φ ⋙ pushforward (𝟙 S)).obj x✝¹).obj X✝)
⊢ (ModuleCat.Hom.hom (((pushforwardComp (𝟙 S) φ).hom.app x✝¹).app X✝)) x✝ =
    (ModuleCat.Hom.hom
        ((((pushforward φ).isoWhiskerLeft (pushforwardId S) ≪≫ (pushforward φ).rightUnitor).hom.app x✝¹).app X✝))
      x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
x✝¹ : PresheafOfModules R
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward φ ⋙ pushforward (𝟙 S)).obj x✝¹).obj X✝)
⊢ (ModuleCat.Hom.hom (((pushforwardComp (𝟙 S) φ).hom.app x✝¹).app X✝)) x✝ =
    (ModuleCat.Hom.hom
        ((((pushforward φ).isoWhiskerLeft (pushforwardId S) ≪≫ (pushforward φ).rightUnitor).hom.app x✝¹).app X✝))
      x✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Pushforward

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
x✝¹ : PresheafOfModules R
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward (𝟙 R) ⋙ pushforward φ).obj x✝¹).obj X✝)
⊢ (ModuleCat.Hom.hom (((pushforwardComp φ (𝟙 R)).hom.app x✝¹).app X✝)) x✝ =
    (ModuleCat.Hom.hom
        (((isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor).hom.app x✝¹).app X✝))
      x✝

Tactic:
;

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
R : Dᵒᵖ ⥤ RingCat
S : Cᵒᵖ ⥤ RingCat
φ : S ⟶ F.op ⋙ R
x✝¹ : PresheafOfModules R
X✝ : Cᵒᵖ
x✝ : ↑(((pushforward (𝟙 R) ⋙ pushforward φ).obj x✝¹).obj X✝)
⊢ (ModuleCat.Hom.hom (((pushforwardComp φ (𝟙 R)).hom.app x✝¹).app X✝)) x✝ =
    (ModuleCat.Hom.hom
        (((isoWhiskerRight (pushforwardId R) (pushforward φ) ≪≫ (pushforward φ).leftUnitor).hom.app x✝¹).app X✝))
      x✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ConcreteCategory.hom (M₁.map f)) (a • m₁) ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂ =
    a • (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ConcreteCategory.hom (M₁.map f)) (a • m₁) ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂ =
    a • (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ ((ConcreteCategory.hom ((R ⋙ forget₂ CommRingCat RingCat).map f)) a •
        (ConcreteCategory.hom (M₁.map f)) m₁) ⊗ₜ[↑(R.obj Y)]
      (ConcreteCategory.hom (M₂.map f)) m₂ =
    a • (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ ((ConcreteCategory.hom ((R ⋙ forget₂ CommRingCat RingCat).map f)) a •
        (ConcreteCategory.hom (M₁.map f)) m₁) ⊗ₜ[↑(R.obj Y)]
      (ConcreteCategory.hom (M₂.map f)) m₂ =
    a • (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) (a • m₂) =
    a • (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) (a • m₂) =
    a • (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ConcreteCategory.hom (R.map f)) a •
      (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂ =
    a • (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ M₄ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
a : ↑((R ⋙ forget₂ CommRingCat RingCat).obj X)
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ConcreteCategory.hom (R.map f)) a •
      (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂ =
    a • (ConcreteCategory.hom (M₁.map f)) m₁ ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M₂.map f)) m₂
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝² x✝¹ : Cᵒᵖ
x✝ : x✝² ⟶ x✝¹
m₁✝ : ↑(M₁.obj x✝²)
m₂✝ : ↑(M₂.obj x✝²)
m₃✝ : ↑(M₃.obj x✝²)
⊢ (ConcreteCategory.hom
        ((Monoidal.tensorObj (Monoidal.tensorObj M₁ M₂) M₃).map x✝ ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map x✝))).map
            (α_ (M₁.obj x✝¹) (M₂.obj x✝¹) (M₃.obj x✝¹)).hom))
      (m₁✝ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj x✝²)] m₂✝ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj x✝²)] m₃✝) =
    (ConcreteCategory.hom
        ((α_ (M₁.obj x✝²) (M₂.obj x✝²) (M₃.obj x✝²)).hom ≫ (Monoidal.tensorObj M₁ (Monoidal.tensorObj M₂ M₃)).map x✝))
      (m₁✝ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj x✝²)] m₂✝ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj x✝²)] m₃✝)

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
M₁ M₂ M₃ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝² x✝¹ : Cᵒᵖ
x✝ : x✝² ⟶ x✝¹
m₁✝ : ↑(M₁.obj x✝²)
m₂✝ : ↑(M₂.obj x✝²)
m₃✝ : ↑(M₃.obj x✝²)
⊢ (ConcreteCategory.hom
        ((Monoidal.tensorObj (Monoidal.tensorObj M₁ M₂) M₃).map x✝ ≫
          (ModuleCat.restrictScalars (RingCat.Hom.hom ((R ⋙ forget₂ CommRingCat RingCat).map x✝))).map
            (α_ (M₁.obj x✝¹) (M₂.obj x✝¹) (M₃.obj x✝¹)).hom))
      (m₁✝ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj x✝²)] m₂✝ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj x✝²)] m₃✝) =
    (ConcreteCategory.hom
        ((α_ (M₁.obj x✝²) (M₂.obj x✝²) (M₃.obj x✝²)).hom ≫ (Monoidal.tensorObj M₁ (Monoidal.tensorObj M₂ M₃)).map x✝))
      (m₁✝ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj x✝²)] m₂✝ ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj x✝²)] m₃✝)
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X₁✝ Y₁✝ X₂✝ Y₂✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : X₂✝ ⟶ Y₂✝
X✝ : Cᵒᵖ
⊢ (x✝¹ ⊗ₘ x✝).app X✝ = (x✝¹ ▷ X₂✝ ≫ Y₁✝ ◁ x✝).app X✝

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X₁✝ Y₁✝ X₂✝ Y₂✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝¹ : X₁✝ ⟶ Y₁✝
x✝ : X₂✝ ⟶ Y₂✝
X✝ : Cᵒᵖ
⊢ (x✝¹ ⊗ₘ x✝).app X✝ = (x✝¹ ▷ X₂✝ ≫ Y₁✝ ◁ x✝).app X✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ : Cᵒᵖ
⊢ (𝟙 x✝¹ ⊗ₘ 𝟙 x✝).app X✝ = (𝟙 (x✝¹ ⊗ x✝)).app X✝

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
x✝¹ x✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X✝ : Cᵒᵖ
⊢ (𝟙 x✝¹ ⊗ₘ 𝟙 x✝).app X✝ = (𝟙 (x✝¹ ⊗ x✝)).app X✝
Module: Mathlib.Algebra.Category.ModuleCat.Presheaf.Monoidal

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝³ : X₁✝ ⟶ Y₁✝
x✝² : X₂✝ ⟶ Y₂✝
x✝¹ : Y₁✝ ⟶ Z₁✝
x✝ : Y₂✝ ⟶ Z₂✝
X✝ : Cᵒᵖ
⊢ ((x✝³ ⊗ₘ x✝²) ≫ (x✝¹ ⊗ₘ x✝)).app X✝ = (x✝³ ≫ x✝¹ ⊗ₘ x✝² ≫ x✝).app X✝

Tactic:
;

Goal state after:
C : Type u_1
inst✝ : Category.{v_1, u_1} C
R : Cᵒᵖ ⥤ CommRingCat
X₁✝ Y₁✝ Z₁✝ X₂✝ Y₂✝ Z₂✝ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
x✝³ : X₁✝ ⟶ Y₁✝
x✝² : X₂✝ ⟶ Y₂✝
x✝¹ : Y₁✝ ⟶ Z₁✝
x✝ : Y₂✝ ⟶ Z₂✝
X✝ : Cᵒᵖ
⊢ ((x✝³ ⊗ₘ x✝²) ≫ (x✝¹ ⊗ₘ x✝)).app X✝ = (x✝³ ≫ x✝¹ ⊗ₘ x✝² ≫ x✝).app X✝