mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsFilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)
⊢ F.Final

Tactic:
have := IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful F h
  refine Functor.final_of_exists_of_isFiltered F h (fun {d c} s s' => ?_)
  obtain ⟨c₀, ⟨f⟩⟩ := h (IsFiltered.coeq s s')
  refine ⟨c₀, F.preimage (IsFiltered.coeqHom s s' ≫ f), ?_⟩
  simp [reassoc_of% (IsFiltered.coeq_condition s s')]

Goal state after:
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: C : Type u₁
inst✝⁵ : Category.{v₁, u₁} C
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝³ : IsFiltered C
E : Type u₃
inst✝² : Category.{v₃, u₃} E
X : D
T : C ⥤ D
inst✝¹ : T.Final
S : D ⥤ E
inst✝ : S.Final
⊢ (post X T S).Final

Tactic:
by
  apply final_of_natIso (postIsoMap₂ X T S).symm

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)
j : J
k k' : K
f : k ⟶ k'
| (F.map (𝟙 j)).app k ≫ (F.obj j).map f

Tactic:
rw [← uncurry_obj_map F (𝟙 j ×ₘ f)]

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)
j : J
k k' : K
f : k ⟶ k'
| (uncurry.obj F).map (𝟙 j ×ₘ f)
Module: Mathlib.CategoryTheory.Limits.Preserves.Bifunctor

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝⁵ : Category.{v_1, u_1} J₁
inst✝⁴ : Category.{v_2, u_2} J₂
C₁ : Type u_3
C₂ : Type u_4
C : Type u_5
inst✝³ : Category.{v_3, u_3} C₁
inst✝² : Category.{v_4, u_4} C₂
inst✝¹ : Category.{v_5, u_5} C
K₁ : J₁ ⥤ C₁
K₂ : J₂ ⥤ C₂
G : C₁ ⥤ C₂ ⥤ C
inst✝ : PreservesColimit₂ K₁ K₂ G
c₁ : Cocone K₂
hc₁ : IsColimit c₁
c₂ : Cocone K₁
hc₂ : IsColimit c₂
⊢ Nonempty (IsColimit (G.flip.mapCocone₂ c₁ c₂))

Tactic:
constructor
    let E₀ : uncurry.obj (whiskeringLeft₂ C |>.obj K₂ |>.obj K₁ |>.obj G.flip) ≅
        uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G).flip :=
      Iso.refl _
    let E₁ : uncurry.obj (whiskeringLeft₂ C |>.obj K₂ |>.obj K₁ |>.obj G.flip) ≅
        Prod.swap _ _ ⋙ uncurry.obj (whiskeringLeft₂ C |>.obj K₁ |>.obj K₂ |>.obj G) :=
      E₀ ≪≫ uncurryObjFlip _
    refine IsColimit.precomposeInvEquiv E₁ _ ?_
    apply IsColimit.ofWhiskerEquivalence (e := Prod.braiding _ _)
    refine IsColimit.equivOfNatIsoOfIso (Iso.refl _) (G.mapCocone₂ c₂ c₁) _ ?_ |>.toFun <|
      isColimitOfPreserves₂ G hc₂ hc₁
    exact Cocone.ext (Iso.refl _) (fun ⟨j₁, j₂⟩ ↦ by simp [E₁, E₀])

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
⊢ (F.map f ≫ ↾fun x ↦ ModuleCat.freeMk x) = (↾fun x ↦ ModuleCat.freeMk x) ≫ ((freeObj F).presheaf ⋙ forget Ab).map f

Tactic:
ext; simp [presheaf]

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
inst✝¹ : HasLimitsOfShape J C
inst✝ : HasLimitsOfShape K C
x✝ : K × J
⊢ ((Prod.braiding K J).functor ⋙ uncurry.obj F).obj x✝ ≅ (Prod.swap K J ⋙ uncurry.obj F).obj x✝

Tactic:
rfl

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
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
x✝ : K × J
⊢ ((Prod.braiding K J).functor ⋙ uncurry.obj F).obj x✝ ≅ (Prod.swap K J ⋙ uncurry.obj F).obj x✝

Tactic:
rfl

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
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
⊢ limit G ≅ limit (curry.obj G ⋙ lim)

Tactic:
have i : G ≅ uncurry.obj ((@curry J _ K _ C _).obj G) := currying.symm.unitIso.app G

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
inst✝¹ : HasLimitsOfShape K C
inst✝ : HasLimit (curry.obj G ⋙ lim)
i : G ≅ uncurry.obj (curry.obj G)
⊢ limit G ≅ limit (curry.obj G ⋙ lim)
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
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
⊢ colimit G ≅ colimit (curry.obj G ⋙ colim)

Tactic:
have i : G ≅ uncurry.obj ((@curry J _ K _ C _).obj G) := currying.symm.unitIso.app G

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
inst✝¹ : HasColimitsOfShape K C
inst✝ : HasColimit (curry.obj G ⋙ colim)
i : G ≅ uncurry.obj (curry.obj G)
⊢ colimit G ≅ colimit (curry.obj G ⋙ colim)
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
X : C
⊢ F.leftAdjointObjIsDefined X ↔ (F ⋙ coyoneda.obj (op X)).IsCorepresentable

Tactic:
rfl

Goal state after:
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 : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
U : Cᵒᵖ
m : ↑(M.obj U)
⊢ 0 • ιM m = 0

Tactic:
simpa using smul_eq hcR hcM 0 m

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : D ⥤ C
J : Type u_1
inst✝ : Category.{v_1, u_1} J
R : J ⥤ F.PartialLeftAdjointSource
c : Cocone (R ⋙ F.leftAdjointObjIsDefined.ι)
hc : IsColimit c
c' : Cocone (R ⋙ F.partialLeftAdjoint)
hc' : IsColimit c'
Y : D
g : (F ⋙ coyoneda.obj (op c.pt)).obj Y
j j' : J
φ : j ⟶ j'
this : (R.map φ).hom ≫ c.ι.app j' = c.ι.app j
⊢ F.partialLeftAdjointHomEquiv
      (F.partialLeftAdjointMap (R.map φ) ≫ F.partialLeftAdjointHomEquiv.symm (c.ι.app j' ≫ g)) =
    F.partialLeftAdjointHomEquiv (F.partialLeftAdjointHomEquiv.symm (c.ι.app j ≫ g) ≫ 𝟙 Y)

Tactic:
rw [comp_id, Equiv.apply_symm_apply, partialLeftAdjointHomEquiv_map_comp,
              Equiv.apply_symm_apply, reassoc_of% this]

Goal state after:
Module: Mathlib.CategoryTheory.Adjunction.PartialAdjoint

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
⊢ F.rightAdjointObjIsDefined Y ↔ (F.op ⋙ yoneda.obj Y).IsRepresentable

Tactic:
rfl

Goal state after:
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 : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
N : ModuleCat ↑cR.pt
ψ : M ⟶ (constFunctor cR).obj N
φ : ModuleColimit hcR hcM →+ N.1
hφ : (homEquiv' hcR hcM) φ = (toPresheaf R).map ψ
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
⊢ r • (ConcreteCategory.hom (ψ.app U)) m =
    (ConcreteCategory.hom (cR.ι.app U)) r • (ConcreteCategory.hom (((toPresheaf R).map ψ).app U)) m

Tactic:
rfl

Goal state after:
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 : PresheafOfModules R
cM : Cocone M.presheaf
hcM : IsColimit cM
M'✝ : PresheafOfModules R
cM'✝ : Cocone M'✝.presheaf
hcM'✝ : IsColimit cM'✝
M'' : PresheafOfModules R
cM'' : Cocone M''.presheaf
hcM'' : IsColimit cM''
M' : PresheafOfModules R
cM' : Cocone M'.presheaf
hcM' : IsColimit cM'
f : M ⟶ M'
U : Cᵒᵖ
r : ↑(R.obj U)
m : ↑(M.obj U)
c : Cocone ((toPresheaf R).obj M) := (Cocone.precompose ((toPresheaf R).map f)).obj cM'
h₁ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      (r • m) =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) (r • m)
h₂ :
  ((AddCommGrpCat.Hom.hom (hcM.desc ((Cocone.precompose ((toPresheaf R).map f)).obj cM'))).comp
        (AddCommGrpCat.Hom.hom (cM.ι.app U)))
      m =
    (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) m
⊢ (ConcreteCategory.hom (((toPresheaf R).map f).app U ≫ cM'.ι.app U)) (r • m) =
    ιM ((ModuleCat.Hom.hom (f.app U)) (r • m))

Tactic:
rfl

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

Goal state before:
pp: C D : Type u
inst✝¹ : SmallCategory C
inst✝ : 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 (yoneda.obj (F.obj X)) ⟶ M
⊢ (ConcreteCategory.hom (g.app (op (F.obj X)))) (freeYonedaEquiv f) =
    (ConcreteCategory.hom (((pushforward φ).map g).app (op X))) (freeYonedaEquiv f)

Tactic:
rfl

Goal state after:
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:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : C ⥤ Type w
G G' : Subfunctor F
h : G ≤ G'
x✝¹ : C
x✝ : G.toFunctor.obj x✝¹
⊢ (hom ((homOfLe h ≫ G'.ι).app x✝¹)).toFun x✝ = (hom (G.ι.app x✝¹)).toFun x✝

Tactic:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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:
rfl

Goal state after:
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 : Cᵒᵖ
m₁ : ↑(M₁.obj X)
m₂ : ↑(M₂.obj X)
⊢ (ConcreteCategory.hom (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 X))) ⋯ (M₁.obj X)).inv)
        m₁ ⊗ₜ[↑(R.obj X)]
      (ConcreteCategory.hom (ModuleCat.restrictScalarsId'App (CommRingCat.Hom.hom (R.map (𝟙 X))) ⋯ (M₂.obj X)).inv) m₂ =
    m₁ ⊗ₜ[↑(R.obj X)] m₂

Tactic:
rfl

Goal state after:
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:
rfl

Goal state after:
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 : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
m : ↑(M.obj X)
⊢ 1 ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)] (ModuleCat.Hom.hom (M.map f)) m =
    1 ⊗ₜ[↑(R.obj Y)] (ConcreteCategory.hom (M.map f)) m

Tactic:
rfl

Goal state after:
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 : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X Y : Cᵒᵖ
f : X ⟶ Y
m : ↑(M.obj X)
⊢ (ModuleCat.Hom.hom (M.map f)) m ⊗ₜ[↑((R ⋙ forget₂ CommRingCat RingCat).obj Y)] 1 =
    (ConcreteCategory.hom (M.map f)) m ⊗ₜ[↑(R.obj Y)] 1

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Precoverage

Goal state before:
pp: case e'_5
C : Type u
inst✝¹ : Category.{v, u} C
J : Precoverage C
inst✝ : J.IsStableUnderBaseChange
ι : Type w
S : C
X : ι → C
f : (i : ι) → X i ⟶ S
hR : Presieve.ofArrows X f ∈ J.coverings S
Y : C
g : Y ⟶ S
P : ι → C
p₁ : (i : ι) → P i ⟶ Y
p₂ : (i : ι) → P i ⟶ X i
h : ∀ (i : ι), IsPullback (p₁ i) (p₂ i) g (f i)
a : ↑(Presieve.ofArrows X f).uncurry ⊕ ↑(Presieve.ofArrows P p₁).uncurry → ι :=
  fun i ↦ Sum.elim (fun i ↦ Presieve.ofArrows.idx ⋯) (fun i ↦ Presieve.ofArrows.idx ⋯) i
⊢ Presieve.ofArrows P p₁ = Presieve.ofArrows (P ∘ a) fun i ↦ p₁ (a i)

Tactic:
refine le_antisymm (fun Z g hg ↦ ?_) fun Z g ⟨i⟩ ↦ ⟨a i⟩
    exact .mk' (Sum.inr ⟨⟨_, _⟩, hg⟩) (by cat_disch) (by cat_disch)

Goal state after:
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₁ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X : Cᵒᵖ
⊢ (λ_ M₁).inv.app X = (λ_ (M₁.obj X)).inv

Tactic:
rfl

Goal state after:
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₂ : PresheafOfModules (R ⋙ forget₂ CommRingCat RingCat)
X : Cᵒᵖ
⊢ (β_ M₁ M₂).hom.app X = (β_ (M₁.obj X) (M₂.obj X)).hom

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
J : GrothendieckTopology C
ι : Type u_1
X : C
Z : ι → C
f : (i : ι) → Z i ⟶ X
R : (i : ι) → Presieve (Z i)
h : Sieve.ofArrows Z f ∈ J X
hR : ∀ (i : ι), Sieve.generate (R i) ∈ J (Z i)
⊢ Sieve.generate (Presieve.bindOfArrows Z f R) ∈ J X

Tactic:
by
  refine J.superset_covering (Presieve.bind_ofArrows_le_bindOfArrows _ _ _) ?_
  exact J.bind_covering h fun _ _ _ ↦ J.pullback_stable _ (hR _)

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: case refine_1
C : Type u
inst✝ : Category.{v, u} C
s : Set (GrothendieckTopology C)
⊢ ∀ {x y : GrothendieckTopology C}, x.sieves ≤ y.sieves ↔ x ≤ y

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Grothendieck

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
⊢ ⊥ < ⊤ ↔ Nonempty C

Tactic:
by
  contrapose!
  simp

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Y✝ : C
f : Y✝ ⟶ X
Y : C
⊢ f = f

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst✝ : ∀ (i : ι), HasPullback (g i) f
⊢ (ofArrows (fun i ↦ pullback (g i) f) fun x ↦ pullback.snd (g x) f) = pullbackArrows f (ofArrows Z g)

Tactic:
funext T

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
X Y : C
f : Y ⟶ X
ι : Type u_1
Z : ι → C
g : (i : ι) → Z i ⟶ X
inst✝ : ∀ (i : ι), HasPullback (g i) f
T : C
⊢ (ofArrows (fun i ↦ pullback (g i) f) fun x ↦ pullback.snd (g x) f) = pullbackArrows f (ofArrows Z g)
Module: Mathlib.CategoryTheory.Limits.Types.Equalizers

Goal state before:
pp: Y Z : Type u
g h : Y ⟶ Z
⊢ (equalizerIso g h).hom ≫ ↾Subtype.val = equalizer.ι g h

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mp
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
v : Z ⟶ X
Y : C
⊢ ⟨Z, v⟩ ∈ {⟨⟨Z, v⟩.fst, ⟨Z, v⟩.snd⟩}

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: case mpr
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
ι : Type u_1
Y : ι → C
f : (i : ι) → Y i ⟶ X
Z : C
v : Z ⟶ X
⊢ (∃ y, Y y = Z ∧ f y ≍ v) → ⟨Z, v⟩ ∈ (ofArrows Y f).uncurry

Tactic:
rintro ⟨i, rfl, h⟩; rw [← eq_of_heq h]; exact ⟨i⟩

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
arrows✝ : Presieve X
downward_closed✝¹ : ∀ {Y Z : C} {f : Y ⟶ X}, arrows✝ f → ∀ (g : Z ⟶ Y), arrows✝ (g ≫ f)
downward_closed✝ :
  ∀ {Y Z : C} {f : Y ⟶ X},
    { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows f →
      ∀ (g : Z ⟶ Y), { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows (g ≫ f)
⊢ { arrows := arrows✝, downward_closed := downward_closed✝¹ } =
    { arrows := { arrows := arrows✝, downward_closed := downward_closed✝¹ }.arrows,
      downward_closed := downward_closed✝ }

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: case mk
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X✝ Y✝ : C
S : Sieve X✝
R : Presieve X✝
X Y : C
f : X ⟶ Y
x : P.obj (op X)
⊢ X = X

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.EqualizerSheafCondition

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type (max v u)
X : C
R : Presieve X
z₁ z₂ : FirstObj P R
h :
  ∀ (Y : C) (f : Y ⟶ X) (hf : R f),
    (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩)) z₁ =
      (ConcreteCategory.hom (Pi.π (fun f ↦ P.obj (op f.fst)) ⟨Y, ⟨f, hf⟩⟩)) z₂
Y : C
f : Y ⟶ X
hf : R f
⊢ (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.fst)) { as := ⟨Y, ⟨f, hf⟩⟩ })) z₁ =
    (ConcreteCategory.hom (limit.π (Discrete.functor fun f ↦ P.obj (op f.fst)) { as := ⟨Y, ⟨f, hf⟩⟩ })) z₂

Tactic:
exact h Y f hf

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P Q U : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
f : P ⟶ Q
g : Q ⟶ U
⊢ (x.map f).map g = x.map (f ≫ g)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
I : Type u_1
Y : I → C
Z X : C
g : Z ⟶ X
⊢ (ofObjects Y X).arrows g ↔ ∃ i, Nonempty (Z ⟶ Y i)

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
R : Sieve X
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (functorPullback (𝟭 C) R).arrows f✝ ↔ R.arrows f✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.Sieves

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
X : C
E : Type u₃
inst✝ : Category.{v₃, u₃} E
G : D ⥤ E
R : Sieve ((F ⋙ G).obj X)
Y✝ : C
f✝ : Y✝ ⟶ X
⊢ (functorPullback (F ⋙ G) R).arrows f✝ ↔ (functorPullback F (functorPullback G R)).arrows f✝

Tactic:
rfl

Goal state after:
Module: Mathlib.CategoryTheory.Sites.IsSheafFor

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) ((ConcreteCategory.hom (P.map f₁.op)) t) =
    (ConcreteCategory.hom (P.map g₂.op)) (x f₂ h₂)

Tactic:
← ht _ h₂,

Goal state after:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
P : Cᵒᵖ ⥤ Type w
X : C
R : Presieve X
x : FamilyOfElements P R
t : P.obj (op X)
ht : x.IsAmalgamation t
Y₁ Y₂ Z : C
g₁ : Z ⟶ Y₁
g₂ : Z ⟶ Y₂
f₁ : Y₁ ⟶ X
f₂ : Y₂ ⟶ X
h₁ : R f₁
h₂ : R f₂
comm : g₁ ≫ f₁ = g₂ ≫ f₂
⊢ (ConcreteCategory.hom (P.map g₁.op)) ((ConcreteCategory.hom (P.map f₁.op)) t) =
    (ConcreteCategory.hom (P.map g₂.op)) ((ConcreteCategory.hom (P.map f₂.op)) t)