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✝¹ : IsCofilteredOrEmpty C
T : C ⥤ D
inst✝ : T.Initial
Y : D
⊢ (proj T Y).Initial

Tactic:
by

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
T : C ⥤ D
inst✝² : T.Final
S : D ⥤ E
inst✝¹ : S.Final
T' : C ⥤ E
d : D
e : E
u : e ⟶ S.obj d
α : T ⋙ S ⟶ T'
inst✝ : IsIso α
⊢ (map₂ u α).Final

Tactic:
by

Goal state after:
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
inst✝¹ : ∀ (x : C₂), PreservesColimit K₁ (G.flip.obj x)
inst✝ : ∀ (x : C₁), PreservesColimit K₂ (G.obj x)
c₁ : Cocone K₁
hc₁ : IsColimit c₁
c₂ : Cocone K₂
hc₂ : IsColimit c₂
Q₀ : DiagramOfCocones ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) :=
  { obj := fun j₁ ↦ (G.obj (K₁.obj j₁)).mapCocone c₂,
    map := fun {j j'} f ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsColimit (Q₀.obj j₁) := fun j ↦ isColimitOfPreserves (G.obj (K₁.obj j)) hc₂
E₀ : Q₀.coconePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun x ↦ Iso.refl (Q₀.coconePoints.obj x)) ⋯
j₁ : J₁
⊢ ((Cocone.precompose E₀.hom).obj (coconeOfCoconeUncurry P (G.mapCocone₂ c₁ c₂))).ι.app j₁ ≫
      (Iso.refl ((Cocone.precompose E₀.hom).obj (coconeOfCoconeUncurry P (G.mapCocone₂ c₁ c₂))).pt).hom =
    ((G.flip.obj c₂.pt).mapCocone c₁).ι.app j₁

Tactic:
by

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
S S' : D
f : S ⟶ S'
T : C ⥤ D
inst✝ : T.Final
this : IsIso (𝟙 T)
⊢ (map₂ f (𝟙 T)).Final

Tactic:
by

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
S S' : D
f : S ⟶ S'
T : C ⥤ D
inst✝ : T.Final
⊢ (map f).Final

Tactic:
by

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

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✝³ : IsCofiltered C
E : Type u₃
inst✝² : Category.{v₃, u₃} E
T : C ⥤ D
inst✝¹ : T.Initial
S : D ⥤ E
inst✝ : S.Initial
d : D
e : E
u : S.obj d ⟶ e
⊢ (map₂ (𝟙 (T ⋙ S)) u).Initial

Tactic:
by

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✝³ : IsCofiltered C
E : Type u₃
inst✝² : Category.{v₃, u₃} E
X : D
T : C ⥤ D
inst✝¹ : T.Initial
S : D ⥤ E
inst✝ : S.Initial
⊢ (post T S X).Initial

Tactic:
by

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
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
i : I s
⊢ i ⟶ (Pi.eval I s).obj (Function.update (fun t ↦ ⋯.some) s i)

Tactic:
by

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.obj j).map f ≫ c.ι.app (j, k') = c.ι.app (j, k) ≫ ((const K).obj c.pt).map f

Tactic:
by

Goal state after:
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₂
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 (uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip))
E₁ : uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip) ≅
  Prod.swap J₂ J₁ ⋙ uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) :=
  E₀ ≪≫ ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).uncurryObjFlip
x✝ : J₁ × J₂
j₁ : J₁
j₂ : J₂
⊢ ((Cocone.precompose (Iso.refl (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))).inv).obj
              (G.mapCocone₂ c₂ c₁)).ι.app
        (j₁, j₂) ≫
      (Iso.refl
          ((Cocone.precompose (Iso.refl (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))).inv).obj
              (G.mapCocone₂ c₂ c₁)).pt).hom =
    (Cocone.whisker (Prod.braiding J₁ J₂).functor ((Cocone.precompose E₁.inv).obj (G.flip.mapCocone₂ c₁ c₂))).ι.app
      (j₁, j₂)

Tactic:
by

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

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
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
⊢ (Pi.eval I s).Final

Tactic:
classical
  apply Functor.final_of_exists_of_isFiltered
  · exact fun i => ⟨Function.update (fun t => nonempty.some) s i, ⟨by simpa using 𝟙 _⟩⟩
  · intro d c f g
    let c't : (∀ s, (c' : I s) × (c s ⟶ c')) := Function.update (fun t => ⟨c t, 𝟙 (c t)⟩)
      s ⟨coeq f g, coeqHom f g⟩
    refine ⟨fun t => (c't t).1, fun t => (c't t).2, ?_⟩
    dsimp only [Pi.eval_obj, Pi.eval_map, c't]
    rw [Function.update_self]
    simpa using coeq_condition _ _

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
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsFiltered (I s)
s : α
⊢ (Pi.eval I s).Final

Tactic:
by

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' : J
f : j ⟶ j'
⊢ ∀ (j_1 : K),
    (D.obj j).ι.app j_1 ≫
        D.coconePoints.map f ≫ (Q j').desc { pt := c.pt, ι := { app := fun k ↦ c.ι.app (j', k), naturality := ⋯ } } =
      (D.obj j).ι.app j_1 ≫
        (Q j).desc { pt := c.pt, ι := { app := fun k ↦ c.ι.app (j, k), naturality := ⋯ } } ≫ ((const J).obj c.pt).map f

Tactic:
by

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
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsCofiltered (I s)
s : α
i : I s
⊢ (Pi.eval I s).obj (Function.update (fun t ↦ ⋯.some) s i) ⟶ i

Tactic:
by

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 (curry.obj G)
Q : (j : J) → IsColimit (D.obj j)
c : Cocone G
j x✝¹ : J
x✝ : j ⟶ x✝¹
⊢ ∀ (j_1 : K),
    (D.obj j).ι.app j_1 ≫
        D.coconePoints.map x✝ ≫ (Q x✝¹).desc { pt := c.pt, ι := { app := fun k ↦ c.ι.app (x✝¹, k), naturality := ⋯ } } =
      (D.obj j).ι.app j_1 ≫
        (Q j).desc { pt := c.pt, ι := { app := fun k ↦ c.ι.app (j, k), naturality := ⋯ } } ≫ ((const J).obj c.pt).map x✝

Tactic:
by

Goal state after:
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✝ : PreservesLimit₂ K₁ K₂ G
c₁ : Cone K₁
hc₁ : IsLimit c₁
c₂ : Cone K₂
hc₂ : IsLimit c₂
c₃ : Cone (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
hc₃ : IsLimit c₃
j : J₁ × J₂
⊢ (isoObjConePointsOfIsLimit G hc₁ hc₂ hc₃).hom ≫ c₃.π.app j =
    (G.map (c₁.π.app j.1)).app c₂.pt ≫ (G.obj (K₁.obj j.1)).map (c₂.π.app j.2)

Tactic:
by

Goal state after:
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✝ : PreservesLimit₂ K₁ K₂ G
c₁ : Cone K₁
hc₁ : IsLimit c₁
c₂ : Cone K₂
hc₂ : IsLimit c₂
c₃ : Cone (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))
hc₃ : IsLimit c₃
j : J₁ × J₂
⊢ (isoObjConePointsOfIsLimit G hc₁ hc₂ hc₃).inv ≫
      (G.map (c₁.π.app j.1)).app c₂.pt ≫ (G.obj (K₁.obj j.1)).map (c₂.π.app j.2) =
    c₃.π.app j

Tactic:
by

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
α : Type u₁
I : α → Type u₂
inst✝¹ : (s : α) → Category.{v₂, u₂} (I s)
inst✝ : ∀ (s : α), IsCofiltered (I s)
s : α
⊢ (Pi.eval I s).Initial

Tactic:
by

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

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsDirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ hf.functor.Final ↔ ∀ (j₂ : J₂), ∃ j₁, j₂ ≤ f j₁

Tactic:
by

Goal state after:
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✝² : PreservesLimit₂ K₁ K₂ G
inst✝¹ : ∀ (x : C₂), PreservesLimit K₁ (G.flip.obj x)
inst✝ : ∀ (x : C₁), PreservesLimit K₂ (G.obj x)
c₁ : Cone K₁
hc₁ : IsLimit c₁
c₂ : Cone K₂
hc₂ : IsLimit c₂
Q₀ : DiagramOfCones ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) :=
  { obj := fun j₁ ↦ (G.obj (K₁.obj j₁)).mapCone c₂,
    map := fun {j j'} f ↦ { hom := (G.map (K₁.map f)).app c₂.pt, w := ⋯ }, id := ⋯, comp := ⋯ }
P : (j₁ : J₁) → IsLimit (Q₀.obj j₁) := fun x ↦ isLimitOfPreserves (G.obj (K₁.obj x)) hc₂
E₀ : Q₀.conePoints ≅ K₁ ⋙ G.flip.obj c₂.pt := NatIso.ofComponents (fun x ↦ Iso.refl (Q₀.conePoints.obj x)) ⋯
j₁ : J₁
⊢ ((Cone.postcompose E₀.hom).obj (coneOfConeUncurry P (G.mapCone₂ c₁ c₂))).π.app j₁ =
    (Iso.refl ((Cone.postcompose E₀.hom).obj (coneOfConeUncurry P (G.mapCone₂ c₁ c₂))).pt).hom ≫
      ((G.flip.obj c₂.pt).mapCone c₁).π.app j₁

Tactic:
by

Goal state after:
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✝ : PreservesLimit₂ K₁ K₂ G
c₁ : Cone K₂
hc₁ : IsLimit c₁
c₂ : Cone K₁
hc₂ : IsLimit c₂
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 (uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip))
E₁ : uncurry.obj ((((whiskeringLeft₂ C).obj K₂).obj K₁).obj G.flip) ≅
  Prod.swap J₂ J₁ ⋙ uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G) :=
  E₀ ≪≫ ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G).uncurryObjFlip
x✝ : J₁ × J₂
j₁ : J₁
j₂ : J₂
⊢ ((Cone.postcompose (Iso.refl (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))).hom).obj
            (G.mapCone₂ c₂ c₁)).π.app
      (j₁, j₂) =
    (Iso.refl
          ((Cone.postcompose (Iso.refl (uncurry.obj ((((whiskeringLeft₂ C).obj K₁).obj K₂).obj G))).hom).obj
              (G.mapCone₂ c₂ c₁)).pt).hom ≫
      (Cone.whisker (Prod.braiding J₁ J₂).functor ((Cone.postcompose E₁.hom).obj (G.flip.mapCone₂ c₁ c₂))).π.app
        (j₁, j₂)

Tactic:
by

Goal state after:
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✝ : PreservesLimit₂ K₁ K₂ G
c₁ : Cone K₂
hc₁ : IsLimit c₁
c₂ : Cone K₁
hc₂ : IsLimit c₂
⊢ Nonempty (IsLimit (G.flip.mapCone₂ c₁ c₂))

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Surjective ⇑(ConcreteCategory.hom (f.app X))
Z✝ : PresheafOfModules R
g₁ g₂ : M₂ ⟶ Z✝
hg : f ≫ g₁ = f ≫ g₂
⊢ g₁ = g₂

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
hf : ∀ ⦃X : Cᵒᵖ⦄, Function.Injective ⇑(ConcreteCategory.hom (f.app X))
M : PresheafOfModules R
g₁ g₂ : M ⟶ M₁
hg : g₁ ≫ f = g₂ ≫ f
⊢ g₁ = g₂

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
inst✝ : Epi f
X : Cᵒᵖ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.app X))

Tactic:
by

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
R : Cᵒᵖ ⥤ RingCat
M₁ M₂ : PresheafOfModules R
f : M₁ ⟶ M₂
inst✝ : Mono f
X : Cᵒᵖ
⊢ Function.Injective ⇑(ConcreteCategory.hom (f.app X))

Tactic:
by

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

Goal state before:
pp: J₁ : Type u_1
J₂ : Type u_2
inst✝² : Preorder J₁
inst✝¹ : Preorder J₂
inst✝ : IsCodirectedOrder J₁
f : J₁ → J₂
hf : Monotone f
⊢ hf.functor.Initial ↔ ∀ (j₁ : J₂), ∃ j₂, f j₂ ≤ j₁

Tactic:
by

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 : 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'
⊢ ((const (J × K)).obj s.pt).map f ≫ s.π.app p'.1 ≫ (D.obj p'.1).π.app p'.2 =
    (s.π.app p.1 ≫ (D.obj p.1).π.app p.2) ≫ (uncurry.obj F).map f

Tactic:
by

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 : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
j : J
⊢ P.lift { pt := s.pt, π := { app := fun p ↦ s.π.app p.1 ≫ (D.obj p.1).π.app p.2, naturality := ⋯ } } ≫
      (coneOfConeUncurry Q c).π.app j =
    s.π.app j

Tactic:
by

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 : DiagramOfCones F
Q : (j : J) → IsLimit (D.obj j)
c : Cone (uncurry.obj F)
P : IsLimit c
s : Cone D.conePoints
m : s.pt ⟶ (coneOfConeUncurry Q c).pt
w : ∀ (j : J), m ≫ (coneOfConeUncurry Q c).π.app j = s.π.app j
⊢ m = P.lift { pt := s.pt, π := { app := fun p ↦ s.π.app p.1 ≫ (D.obj p.1).π.app p.2, naturality := ⋯ } }

Tactic:
by

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 : 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:
by

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 : 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) → Cone D.conePoints :=
  fun s ↦
    { pt := s.pt,
      π :=
        { app := fun j ↦ (Q j).lift ((Cone.postcompose (E j).hom).obj (Cone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cone (uncurry.obj F)
p : J × K
⊢ P.lift (S s) ≫ c.π.app p = s.π.app p

Tactic:
by

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 : 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) → Cone D.conePoints :=
  fun s ↦
    { pt := s.pt,
      π :=
        { app := fun j ↦ (Q j).lift ((Cone.postcompose (E j).hom).obj (Cone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cone (uncurry.obj F)
f : s.pt ⟶ c.pt
hf : ∀ (j : J × K), f ≫ c.π.app j = s.π.app j
j : J
k : K
⊢ (f ≫ (coneOfConeUncurry Q c).π.app j) ≫ (D.obj j).π.app k = (S s).π.app j ≫ (D.obj j).π.app k

Tactic:
by

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'
⊢ (uncurry.obj F).map f ≫ (D.obj p'.1).ι.app p'.2 ≫ s.ι.app p'.1 =
    ((D.obj p.1).ι.app p.2 ≫ s.ι.app p.1) ≫ ((const (J × K)).obj s.pt).map f

Tactic:
by

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
j : J
⊢ (coconeOfCoconeUncurry Q c).ι.app j ≫
      P.desc { pt := s.pt, ι := { app := fun p ↦ (D.obj p.1).ι.app p.2 ≫ s.ι.app p.1, naturality := ⋯ } } =
    s.ι.app j

Tactic:
by

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
m : (coconeOfCoconeUncurry Q c).pt ⟶ s.pt
w : ∀ (j : J), (coconeOfCoconeUncurry Q c).ι.app j ≫ m = s.ι.app j
⊢ m = P.desc { pt := s.pt, ι := { app := fun p ↦ (D.obj p.1).ι.app p.2 ≫ s.ι.app p.1, naturality := ⋯ } }

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
X : C
x : ↑(M.obj (Opposite.op X))
⊢ (ConcreteCategory.hom ((freeYonedaEquiv.symm x).app (Opposite.op X)))
      (ModuleCat.freeMk (𝟙 (Opposite.unop (Opposite.op X)))) =
    x

Tactic:
by

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 (coconeOfCoconeUncurry 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 : Cocone (uncurry.obj F)
j j' : J
f : j ⟶ j'
k : K
⊢ (D.obj j).ι.app k ≫
      D.coconePoints.map f ≫ (Q j').desc ((Cocone.precompose (E j').inv).obj (Cocone.whisker (Prod.sectR j' K) s)) =
    (D.obj j).ι.app k ≫
      (Q j).desc ((Cocone.precompose (E j).inv).obj (Cocone.whisker (Prod.sectR j K) s)) ≫ ((const J).obj s.pt).map f

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
⊢ ObjectProperty.Small.{u, max u v, max u (v + 1)} (freeYoneda R)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
⊢ (freeYoneda R).IsSeparating

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
R : Cᵒᵖ ⥤ RingCat
M : PresheafOfModules R
m : M.Elements
⊢ (ConcreteCategory.hom (m.fromFreeYoneda.app m.fst)) (ModuleCat.freeMk (𝟙 (Opposite.unop m.fst))) = m.snd

Tactic:
by

Goal state after:
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
⊢ M.ιFreeYonedaCoproduct m ≫ M.fromFreeYonedaCoproduct = m.fromFreeYoneda

Tactic:
by

Goal state after: