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 C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
⊢ g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right ≫ t) =
    (StructuredArrow.mk (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right ≫ t))).hom

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
c : C
t : IsFiltered.max f.right g.right ⟶ c
ht :
  (f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right)) ≫ F.map t =
    (g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right)) ≫ F.map t
⊢ g.hom ≫ F.map (IsFiltered.rightToMax f.right g.right) ≫ F.map t =
    f.hom ≫ F.map (IsFiltered.leftToMax f.right g.right) ≫ F.map t
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
η μ : f ⟶ g
⊢ η ≫ StructuredArrow.homMk (IsFiltered.coeqHom (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ)) ⋯ =
    μ ≫ StructuredArrow.homMk (IsFiltered.coeqHom (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ)) ⋯

Tactic:
simpa using

Goal state after:
case refine_2
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : IsFilteredOrEmpty C
d : D
h₁ : ∃ c, Nonempty (d ⟶ F.obj c)
h₂ : ∀ {c : C} (s s' : d ⟶ F.obj c), ∃ c' t, s ≫ F.map t = s' ≫ F.map t
this : Nonempty (StructuredArrow d F)
f g : StructuredArrow d F
η μ : f ⟶ g
⊢ StructuredArrow.Hom.right η ≫ IsFiltered.coeqHom (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ) =
    StructuredArrow.Hom.right μ ≫ IsFiltered.coeqHom (StructuredArrow.Hom.right η) (StructuredArrow.Hom.right μ)
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 D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
d : Dᵒᵖ
⊢ ∃ c, Nonempty (d ⟶ F.op.obj c)

Tactic:
obtain ⟨c, ⟨f⟩⟩ := h d.unop

Goal state after:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝² : IsCofilteredOrEmpty D
inst✝¹ : F.Full
inst✝ : F.Faithful
h : ∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)
d : Dᵒᵖ
c : C
f : F.obj c ⟶ unop d
⊢ ∃ c, Nonempty (d ⟶ F.op.obj c)
Module: Mathlib.CategoryTheory.Limits.FinallySmall

Goal state before:
pp: J : Type u
inst✝³ : Category.{v, u} J
K : Type u₁
inst✝² : Category.{v₁, u₁} K
inst✝¹ : LocallySmall.{w, v, u} J
inst✝ : InitiallySmall J
X : J
⊢ InitiallySmall (Over X)

Tactic:
by
  have : InitiallySmall.{w} (CostructuredArrow (fromInitialModel.{w} J) X) :=
    initiallySmall_of_essentiallySmall _
  exact initiallySmall_of_initial_of_initiallySmall
    (CostructuredArrow.toOver (fromInitialModel.{w} J) X)

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

Goal state before:
pp: J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsCofilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
⊢ InitiallySmall J

Tactic:
suffices Functor.Initial (ObjectProperty.ι (· ∈ s)) from
    initiallySmall_of_initial_of_essentiallySmall (ObjectProperty.ι (· ∈ s))

Goal state after:
J : Type u
inst✝² : Category.{v, u} J
inst✝¹ : IsCofilteredOrEmpty J
s : Set J
inst✝ : Small.{v, u} ↑s
hs : ∀ (i : J), ∃ j ∈ s, Nonempty (j ⟶ i)
⊢ (ObjectProperty.ι fun x ↦ x ∈ s).Initial
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)
j : J
k k' : K
f : k ⟶ k'
⊢ ((const K).obj c.pt).map f ≫ c.π.app (j, k') = c.π.app (j, k) ≫ (F.obj j).map f

Tactic:
simpa using

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

Tactic:
simpa using

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)
j j' : J
f : j ⟶ j'
k : K
⊢ c.π.app (j', k) = c.π.app (j, k) ≫ (F.map f).app k
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:
simpa using

Goal state after:
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 ⟶ i
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₂
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 : α
d : I s
c : (i : α) → I i
f g : d ⟶ (Pi.eval I s).obj c
c't : (s : α) → (c' : I s) × (c s ⟶ c') := Function.update (fun t ↦ ⟨c t, 𝟙 (c t)⟩) s ⟨coeq f g, coeqHom f g⟩
⊢ f ≫ ⟨coeq f g, coeqHom f g⟩.snd = g ≫ ⟨coeq f g, coeqHom f g⟩.snd

Tactic:
simpa using

Goal state after:
case h₂
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 : α
d : I s
c : (i : α) → I i
f g : d ⟶ (Pi.eval I s).obj c
c't : (s : α) → (c' : I s) × (c s ⟶ c') := Function.update (fun t ↦ ⟨c t, 𝟙 (c t)⟩) s ⟨coeq f g, coeqHom f g⟩
⊢ f ≫ coeqHom f g = g ≫ coeqHom f g
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:
simpa using

Goal state after:
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
⊢ i ⟶ i
Module: Mathlib.CategoryTheory.Filtered.Final

Goal state before:
pp: case h₂
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 : α
d : I s
c : (i : α) → I i
f g : (Pi.eval I s).obj c ⟶ d
c't : (s : α) → (c' : I s) × (c' ⟶ c s) := Function.update (fun t ↦ ⟨c t, 𝟙 (c t)⟩) s ⟨eq f g, eqHom f g⟩
⊢ ⟨eq f g, eqHom f g⟩.snd ≫ f = ⟨eq f g, eqHom f g⟩.snd ≫ g

Tactic:
simpa using

Goal state after:
case h₂
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 : α
d : I s
c : (i : α) → I i
f g : (Pi.eval I s).obj c ⟶ d
c't : (s : α) → (c' : I s) × (c' ⟶ c s) := Function.update (fun t ↦ ⟨c t, 𝟙 (c t)⟩) s ⟨eq f g, eqHom f g⟩
⊢ eqHom f g ≫ f = eqHom f g ≫ g
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 using

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 (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
⊢ s.π.app (j, k) = s.π.app (j', k) ≫ (F.map f).app k
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:
simpa using

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 (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 ≫ c.π.app (j, k) = s.π.app (j, k)
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:
simpa using

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 (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
⊢ (F.map f).app k ≫ s.ι.app (j', k) = s.ι.app (j, k)
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) → Cocone D.coconePoints :=
  fun s ↦
    { pt := s.pt,
      ι :=
        { app := fun j ↦ (Q j).desc ((Cocone.precompose (E j).inv).obj (Cocone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cocone (uncurry.obj F)
f : c.pt ⟶ s.pt
hf : ∀ (j : J × K), c.ι.app j ≫ f = s.ι.app j
j : J
k : K
⊢ (D.obj j).ι.app k ≫ (coconeOfCoconeUncurry Q c).ι.app j ≫ f = (D.obj j).ι.app k ≫ (S s).ι.app j

Tactic:
simpa using

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 (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) → Cocone D.coconePoints :=
  fun s ↦
    { pt := s.pt,
      ι :=
        { app := fun j ↦ (Q j).desc ((Cocone.precompose (E j).inv).obj (Cocone.whisker (Prod.sectR j K) s)),
          naturality := ⋯ } }
s : Cocone (uncurry.obj F)
f : c.pt ⟶ s.pt
hf : ∀ (j : J × K), c.ι.app j ≫ f = s.ι.app j
j : J
k : K
⊢ c.ι.app (j, k) ≫ f = s.ι.app (j, k)
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
inst✝¹ : HasColimitsOfShape J C
inst✝ : HasColimitsOfShape K C
k : K
j : J
⊢ colimit.ι (F.obj j) k ≫ colimit.ι (F ⋙ colim) j ≫ (colimitFlipCompColimIsoColimitCompColim F).inv =
    colimit.ι (F.flip.obj k) j ≫ colimit.ι (F.flip ⋙ colim) k

Tactic:
dsimp [colimitFlipCompColimIsoColimitCompColim]
  conv_lhs => slice 1 3
  simp [Equivalence.counitInv]

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'
U : Cᵒᵖ
a : (R ⋙ forget RingCat).obj U
x₁ : (M.presheaf ⋙ forget AddCommGrpCat).obj U
x₂ : (M'.presheaf ⋙ forget AddCommGrpCat).obj U
⊢ ∃ U_1 a_1 x₁_1 x₂_1,
    (ιR cR) a_1 =
        ((ConcreteCategory.hom
              ((((forget RingCat).mapCocone cR).tensor
                      (((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM'))).ι.app
                U))
            (a, x₁, x₂)).1 ∧
      ιM x₁_1 =
          ((ConcreteCategory.hom
                  ((((forget RingCat).mapCocone cR).tensor
                          (((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM'))).ι.app
                    U))
                (a, x₁, x₂)).2.1 ∧
        ιM x₂_1 =
          ((ConcreteCategory.hom
                  ((((forget RingCat).mapCocone cR).tensor
                          (((forget AddCommGrpCat).mapCocone cM).tensor ((forget AddCommGrpCat).mapCocone cM'))).ι.app
                    U))
                (a, x₁, x₂)).2.2

Tactic:
exact ⟨U, a, x₁, x₂, rfl, rfl, 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)
⊢ 1 • ιM m = ιM m

Tactic:
simpa using

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 : 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)
⊢ 1 • ιM m = ιM m
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ᵒᵖ
r : ↑(R.obj U)
⊢ (ιR cR) r • 0 = 0

Tactic:
simpa using

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 : 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ᵒᵖ
r : ↑(R.obj U)
⊢ (ιR cR) r • 0 = 0
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''
r₁ r₂ : ↑cR.pt
m : ModuleColimit hcR hcM
⊢ (r₁ + r₂) • m = r₁ • m + r₂ • m

Tactic:
obtain ⟨U, r₁, r₂, m, rfl, rfl, rfl⟩ := jointly_surjective₃ r₁ r₂ m
    simp only [smul_eq, ← map_add, add_smul]

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
h : ∀ (X : C), (F ⋙ coyoneda.obj (op X)).IsCorepresentable
⊢ F.IsRightAdjoint

Tactic:
exact (Adjunction.adjunctionOfEquivLeft
    (fun X Y ↦ (F ⋙ coyoneda.obj (op X)).corepresentableBy.homEquiv)
    (fun X Y Y' g f ↦ by apply CorepresentableBy.homEquiv_comp)).isRightAdjoint

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
h : F.IsRightAdjoint
X : C
⊢ F.leftAdjointObjIsDefined X ↔ ⊤ X

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ C
h : F.IsRightAdjoint
X : C
⊢ F.leftAdjointObjIsDefined 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 : 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

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 : 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
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
h : F.IsLeftAdjoint
X : D
⊢ F.rightAdjointObjIsDefined X ↔ ⊤ X

Tactic:
simpa using

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
h : F.IsLeftAdjoint
X : D
⊢ F.rightAdjointObjIsDefined X
Module: Mathlib.CategoryTheory.Adjunction.CompositionIso

Goal state before:
pp: C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₁₃ : C₁ ⥤ C₃
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₁ : C₃ ⥤ C₁
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
e₁₂₃ : G₃₂ ⋙ G₂₁ ≅ G₃₁
e₀₁₃ : G₃₁ ⋙ G₁₀ ≅ G₃₀
e₀₂₃ : G₃₂ ⋙ G₂₀ ≅ G₃₀
h : G₃₂.isoWhiskerLeft e₀₁₂ ≪≫ e₀₂₃ = (G₃₂.associator G₂₁ G₁₀).symm ≪≫ isoWhiskerRight e₁₂₃ G₁₀ ≪≫ e₀₁₃
⊢ e₀₂₃.symm.hom ≫ G₃₂.whiskerLeft e₀₁₂.symm.hom =
    e₀₁₃.symm.hom ≫ whiskerRight e₁₂₃.symm.hom G₁₀ ≫ (G₃₂.associator G₂₁ G₁₀).hom

Tactic:
simpa using

Goal state after:
C₀ : Type u_1
C₁ : Type u_2
C₂ : Type u_3
C₃ : Type u_4
inst✝³ : Category.{v_1, u_1} C₀
inst✝² : Category.{v_2, u_2} C₁
inst✝¹ : Category.{v_3, u_3} C₂
inst✝ : Category.{v_4, u_4} C₃
F₀₁ : C₀ ⥤ C₁
F₁₂ : C₁ ⥤ C₂
F₂₃ : C₂ ⥤ C₃
F₀₂ : C₀ ⥤ C₂
F₁₃ : C₁ ⥤ C₃
F₀₃ : C₀ ⥤ C₃
G₁₀ : C₁ ⥤ C₀
G₂₁ : C₂ ⥤ C₁
G₃₂ : C₃ ⥤ C₂
G₂₀ : C₂ ⥤ C₀
G₃₁ : C₃ ⥤ C₁
G₃₀ : C₃ ⥤ C₀
adj₀₁ : F₀₁ ⊣ G₁₀
adj₁₂ : F₁₂ ⊣ G₂₁
adj₂₃ : F₂₃ ⊣ G₃₂
adj₀₂ : F₀₂ ⊣ G₂₀
adj₁₃ : F₁₃ ⊣ G₃₁
adj₀₃ : F₀₃ ⊣ G₃₀
e₀₁₂ : G₂₁ ⋙ G₁₀ ≅ G₂₀
e₁₂₃ : G₃₂ ⋙ G₂₁ ≅ G₃₁
e₀₁₃ : G₃₁ ⋙ G₁₀ ≅ G₃₀
e₀₂₃ : G₃₂ ⋙ G₂₀ ≅ G₃₀
h : G₃₂.isoWhiskerLeft e₀₁₂ ≪≫ e₀₂₃ = (G₃₂.associator G₂₁ G₁₀).symm ≪≫ isoWhiskerRight e₁₂₃ G₁₀ ≪≫ e₀₁₃
⊢ e₀₂₃.inv ≫ G₃₂.whiskerLeft e₀₁₂.inv = e₀₁₃.inv ≫ whiskerRight e₁₂₃.inv G₁₀ ≫ (G₃₂.associator G₂₁ G₁₀).hom