mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan

Goal state before:
pp: case none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right
hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst
hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd
⊢ F.obj none ≅ G.obj none

pp: case some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right
hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst
hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd
⊢ F.obj (some WalkingPair.left) ≅ G.obj (some WalkingPair.left)

pp: case some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right
hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst
hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd
⊢ F.obj (some WalkingPair.right) ≅ G.obj (some WalkingPair.right)

Tactic:
;

Goal state after:
case none
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right
hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst
hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd
⊢ F.obj none ≅ G.obj none

case some.left
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right
hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst
hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd
⊢ F.obj (some WalkingPair.left) ≅ G.obj (some WalkingPair.left)

case some.right
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X Y Z X' Y' Z' : C
iX : X ≅ X'
iY : Y ≅ Y'
iZ : Z ≅ Z'
F G : WalkingSpan ⥤ C
z : F.obj WalkingSpan.zero ≅ G.obj WalkingSpan.zero
l : F.obj WalkingSpan.left ≅ G.obj WalkingSpan.left
r : F.obj WalkingSpan.right ≅ G.obj WalkingSpan.right
hl : F.map fst ≫ l.hom = z.hom ≫ G.map fst
hr : F.map snd ≫ r.hom = z.hom ≫ G.map snd
⊢ F.obj (some WalkingPair.right) ≅ G.obj (some WalkingPair.right)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
w : f ≫ t.ι.app WalkingSpan.left = t.ι.app WalkingSpan.zero ≫ 𝟙 t.pt
⊢ t.ι.app WalkingSpan.zero = f ≫ t.inl

Tactic:
;

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
t : PushoutCocone f g
w : f ≫ t.ι.app WalkingSpan.left = t.ι.app WalkingSpan.zero ≫ 𝟙 t.pt
⊢ t.ι.app WalkingSpan.zero = f ≫ t.inl
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x✝ : Over Y
⊢ { left := x✝.left, right := x✝.right, hom := x✝.hom } = x✝

Tactic:
;

Goal state after:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x✝ : Over Y
⊢ { left := x✝.left, right := x✝.right, hom := x✝.hom } = x✝
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x✝ : Over Y
⊢ Hom.left ((mapId Y).hom.app x✝) = Hom.left (eqToHom ⋯)

Tactic:
;

Goal state after:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x✝ : Over Y
⊢ Hom.left ((mapId Y).hom.app x✝) = Hom.left (eqToHom ⋯)
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
x✝ : Over X
⊢ Hom.left ((mapComp f g).hom.app x✝) = Hom.left (eqToHom ⋯)

Tactic:
;

Goal state after:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X Y Z : T
f : X ⟶ Y
g : Y ⟶ Z
x✝ : Over X
⊢ Hom.left ((mapComp f g).hom.app x✝) = Hom.left (eqToHom ⋯)
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Over X
φ : f✝ ⟶ g✝
f g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
⊢ l ≫ f.hom = m ≫ f.hom

Tactic:
;

Goal state after:
T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Over X
φ : f✝ ⟶ g✝
f g : Over X
k : f ⟶ g
inst✝ : Mono k
Y : T
l m : Y ⟶ f.left
a : l ≫ Hom.left k = m ≫ Hom.left k
⊢ l ≫ f.hom = m ≫ f.hom
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
f✝ g : Over X
φ : f✝ ⟶ g
f : Over X
X✝ Y✝ : Over f
κ : X✝ ⟶ Y✝
⊢ Hom.left (Hom.left κ) ≫ Hom.left Y✝.hom = Hom.left X✝.hom

Tactic:
;

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
f✝ g : Over X
φ : f✝ ⟶ g
f : Over X
X✝ Y✝ : Over f
κ : X✝ ⟶ Y✝
⊢ Hom.left (Hom.left κ) ≫ Hom.left Y✝.hom = Hom.left X✝.hom
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
f✝ g : Over X
φ : f✝ ⟶ g
f : Over X
X✝ Y✝ : Over f
κ : X✝ ⟶ Y✝
⊢ Hom.left (Hom.left κ) ≫ Hom.left Y✝.hom = Hom.left (Hom.left κ ≫ Y✝.hom)

Tactic:
;

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
f✝ g : Over X
φ : f✝ ⟶ g
f : Over X
X✝ Y✝ : Over f
κ : X✝ ⟶ Y✝
⊢ Hom.left (Hom.left κ) ≫ Hom.left Y✝.hom = Hom.left (Hom.left κ ≫ Y✝.hom)
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
f✝ g : Over X
φ : f✝ ⟶ g
f : Over X
X✝ Y✝ : Over f
κ : X✝ ⟶ Y✝
⊢ Hom.left (Hom.left κ) ≫ (mk (Hom.left Y✝.hom)).hom = (mk (Hom.left X✝.hom)).hom

Tactic:
dsimp; rw [← Over.w κ]; rfl

Goal state after:
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
X✝ : T
f g : Over X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : D ⟶ (Functor.const J).obj X
c : Cone D
p : c.pt ⟶ X
hp : ∀ (j : J), c.π.app j ≫ s.app j = p
hc : IsLimit c
t : Cone (Over.lift D s)
x✝ : t.pt ⟶ (liftCone D s c p hp).pt
hm : ∀ (j : J), x✝ ≫ (liftCone D s c p hp).π.app j = t.π.app j
⊢ Hom.left x✝ = Hom.left (homMk (hc.lift ((forget X).mapCone t)) ⋯)

Tactic:
refine hc.hom_ext (fun j ↦ ?_)

Goal state after:
T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
X✝ : T
f g : Over X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : D ⟶ (Functor.const J).obj X
c : Cone D
p : c.pt ⟶ X
hp : ∀ (j : J), c.π.app j ≫ s.app j = p
hc : IsLimit c
t : Cone (Over.lift D s)
x✝ : t.pt ⟶ (liftCone D s c p hp).pt
hm : ∀ (j : J), x✝ ≫ (liftCone D s c p hp).π.app j = t.π.app j
j : J
⊢ Hom.left x✝ ≫ c.π.app j = Hom.left (homMk (hc.lift ((forget X).mapCone t)) ⋯) ≫ c.π.app j
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
X : T
Y : Over X
X✝ Y✝ : CostructuredArrow (toOver F X) Y
f : X✝ ⟶ Y✝
⊢ F.map f.left.left ≫ (mk (Over.Hom.left Y✝.hom)).hom = (mk (Over.Hom.left ((toOver F X).map f.left ≫ Y✝.hom))).hom

Tactic:
;

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
X : T
Y : Over X
X✝ Y✝ : CostructuredArrow (toOver F X) Y
f : X✝ ⟶ Y✝
⊢ F.map f.left.left ≫ (mk (Over.Hom.left Y✝.hom)).hom = (mk (Over.Hom.left ((toOver F X).map f.left ≫ Y✝.hom))).hom
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
X : T
Y : Over X
X✝ Y✝ : CostructuredArrow F Y.left
f : X✝ ⟶ Y✝
⊢ Over.Hom.left ((toOver F X).map (homMk f.left ⋯) ≫ (mk (Over.homMk Y✝.hom ⋯)).hom) =
    Over.Hom.left (mk (Over.homMk X✝.hom ⋯)).hom

Tactic:
;

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
X : T
Y : Over X
X✝ Y✝ : CostructuredArrow F Y.left
f : X✝ ⟶ Y✝
⊢ Over.Hom.left ((toOver F X).map (homMk f.left ⋯) ≫ (mk (Over.homMk Y✝.hom ⋯)).hom) =
    Over.Hom.left (mk (Over.homMk X✝.hom ⋯)).hom
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Under X
f g : U ⟶ V
left✝ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝ : (Functor.fromPUnit X).map left✝ ≫ V.hom = U.hom ≫ (𝟭 T).map b
h : Hom.right { left := left✝, right := b, w := w✝ } = Hom.right g
⊢ { left := left✝, right := b, w := w✝ } = g

Tactic:
;

Goal state after:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Under X
f g : U ⟶ V
left✝ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝ : (Functor.fromPUnit X).map left✝ ≫ V.hom = U.hom ≫ (𝟭 T).map b
h : Hom.right { left := left✝, right := b, w := w✝ } = Hom.right g
⊢ { left := left✝, right := b, w := w✝ } = g
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: case e_left
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Under X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (Functor.fromPUnit X).map left✝¹ ≫ V.hom = U.hom ≫ (𝟭 T).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (Functor.fromPUnit X).map left✝ ≫ V.hom = U.hom ≫ (𝟭 T).map e
h : Hom.right { left := left✝¹, right := b, w := w✝¹ } = Hom.right { left := left✝, right := e, w := w✝ }
⊢ left✝¹ = left✝

Tactic:
;

Goal state after:
case e_left
T : Type u₁
inst✝ : Category.{v₁, u₁} T
X : T
U V : Under X
f g : U ⟶ V
left✝¹ : U.left ⟶ V.left
b : U.right ⟶ V.right
w✝¹ : (Functor.fromPUnit X).map left✝¹ ≫ V.hom = U.hom ≫ (𝟭 T).map b
left✝ : U.left ⟶ V.left
e : U.right ⟶ V.right
w✝ : (Functor.fromPUnit X).map left✝ ≫ V.hom = U.hom ≫ (𝟭 T).map e
h : Hom.right { left := left✝¹, right := b, w := w✝¹ } = Hom.right { left := left✝, right := e, w := w✝ }
⊢ left✝¹ = left✝
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x✝ : Under Y
⊢ { left := x✝.left, right := x✝.right, hom := x✝.hom } = x✝

Tactic:
;

Goal state after:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x✝ : Under Y
⊢ { left := x✝.left, right := x✝.right, hom := x✝.hom } = x✝
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x✝ : Under Y
⊢ Hom.right ((mapId Y).hom.app x✝) = Hom.right (eqToHom ⋯)

Tactic:
;

Goal state after:
T : Type u₁
inst✝ : Category.{v₁, u₁} T
Y : T
x✝ : Under Y
⊢ Hom.right ((mapId Y).hom.app x✝) = Hom.right (eqToHom ⋯)
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
⊢ g.hom ≫ l = g.hom ≫ m

Tactic:
;

Goal state after:
T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
⊢ g.hom ≫ l = g.hom ≫ m
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l ⋯
⊢ k ≫ l' = k ≫ homMk m ⋯

Tactic:
;

Goal state after:
T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := homMk l ⋯
⊢ k ≫ l' = k ≫ homMk m ⋯
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := ⋯
⊢ Hom.right (k ≫ l') = Hom.right (k ≫ homMk m ⋯)

Tactic:
;

Goal state after:
T : Type u₁
inst✝² : Category.{v₁, u₁} T
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
X : T
f✝ g✝ : Under X
φ : f✝ ⟶ g✝
f g : Under X
k : f ⟶ g
inst✝ : Epi k
Y : T
l m : g.right ⟶ Y
a : Hom.right k ≫ l = Hom.right k ≫ m
l' : g ⟶ mk (g.hom ≫ m) := ⋯
⊢ Hom.right (k ≫ l') = Hom.right (k ≫ homMk m ⋯)
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Under X
f : (post F).obj A ⟶ (post F).obj B
a : A.right ⟶ B.right
ha : F.map a = Hom.right f
⊢ Hom.right ((post F).map (homMk a ⋯)) = Hom.right f

Tactic:
;

Goal state after:
T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D : Type u₂
inst✝² : Category.{v₂, u₂} D
X : T
f✝ g : Under X
φ : f✝ ⟶ g
F : T ⥤ D
inst✝¹ : F.Faithful
inst✝ : F.Full
A B : Under X
f : (post F).obj A ⟶ (post F).obj B
a : A.right ⟶ B.right
ha : F.map a = Hom.right f
⊢ Hom.right ((post F).map (homMk a ⋯)) = Hom.right f
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
X✝ : T
f g : Under X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : (Functor.const J).obj X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
x✝ : (liftCocone D s c p hp).pt ⟶ t.pt
hm : ∀ (j : J), (liftCocone D s c p hp).ι.app j ≫ x✝ = t.ι.app j
⊢ Hom.right x✝ = Hom.right (homMk (hc.desc ((forget X).mapCocone t)) ⋯)

Tactic:
refine hc.hom_ext (fun j ↦ ?_)

Goal state after:
T : Type u₁
inst✝³ : Category.{v₁, u₁} T
D✝ : Type u₂
inst✝² : Category.{v₂, u₂} D✝
X✝ : T
f g : Under X✝
φ : f ⟶ g
F : T ⥤ D✝
J : Type u_1
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Nonempty J
D : J ⥤ T
X : T
s : (Functor.const J).obj X ⟶ D
c : Cocone D
p : X ⟶ c.pt
hp : ∀ (j : J), s.app j ≫ c.ι.app j = p
hc : IsColimit c
t : Cocone (Under.lift D s)
x✝ : (liftCocone D s c p hp).pt ⟶ t.pt
hm : ∀ (j : J), (liftCocone D s c p hp).ι.app j ≫ x✝ = t.ι.app j
j : J
⊢ c.ι.app j ≫ Hom.right x✝ = c.ι.app j ≫ Hom.right (homMk (hc.desc ((forget X).mapCocone t)) ⋯)
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
Y✝ Z✝ : StructuredArrow X (proj Y F)
m : Y✝ ⟶ Z✝
this : Y✝.hom ≫ (proj Y F).map (Hom.right m) = Z✝.hom
⊢ Y✝.hom ≫ (proj X (proj Y F) ⋙ proj Y F).map m = Z✝.hom

Tactic:
;

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
Y✝ Z✝ : StructuredArrow X (proj Y F)
m : Y✝ ⟶ Z✝
this : Y✝.hom ≫ (proj Y F).map (Hom.right m) = Z✝.hom
⊢ Y✝.hom ≫ (proj X (proj Y F) ⋙ proj Y F).map m = Z✝.hom
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
Y✝ Z✝ : StructuredArrow Y (Under.forget X ⋙ F)
m : Y✝ ⟶ Z✝
this : Y✝.hom ≫ (Under.forget X ⋙ F).map (Hom.right m) = Z✝.hom
⊢ Y✝.hom ≫ F.map ((proj Y (Under.forget X ⋙ F) ⋙ Under.forget X).map m) = Z✝.hom

Tactic:
;

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : D ⥤ T
Y : T
X : D
Y✝ Z✝ : StructuredArrow Y (Under.forget X ⋙ F)
m : Y✝ ⟶ Z✝
this : Y✝.hom ≫ (Under.forget X ⋙ F).map (Hom.right m) = Z✝.hom
⊢ Y✝.hom ≫ F.map ((proj Y (Under.forget X ⋙ F) ⋙ Under.forget X).map m) = Z✝.hom
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : StructuredArrow X.2 (Under.forget X.1)
m : Y✝ ⟶ Z✝
this : Y✝.hom ≫ (Under.forget X.1).map (Hom.right m) = Z✝.hom
⊢ (Y✝.right.hom, Y✝.hom) ≫ (Functor.diag T).map ((proj X.2 (Under.forget X.1) ⋙ Under.forget X.1).map m) =
    (Z✝.right.hom, Z✝.hom)

Tactic:
;

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : StructuredArrow X.2 (Under.forget X.1)
m : Y✝ ⟶ Z✝
this : Y✝.hom ≫ (Under.forget X.1).map (Hom.right m) = Z✝.hom
⊢ (Y✝.right.hom, Y✝.hom) ≫ (Functor.diag T).map ((proj X.2 (Under.forget X.1) ⋙ Under.forget X.1).map m) =
    (Z✝.right.hom, Z✝.hom)
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
Y✝ Z✝ : CostructuredArrow (proj F Y) X
m : Y✝ ⟶ Z✝
this : (proj F Y).map m.left ≫ Z✝.hom = Y✝.hom ≫ (Functor.fromPUnit X).map m.right
⊢ (proj (proj F Y) X ⋙ proj F Y).map m ≫ Z✝.hom = Y✝.hom

Tactic:
;

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
Y✝ Z✝ : CostructuredArrow (proj F Y) X
m : Y✝ ⟶ Z✝
this : (proj F Y).map m.left ≫ Z✝.hom = Y✝.hom ≫ (Functor.fromPUnit X).map m.right
⊢ (proj (proj F Y) X ⋙ proj F Y).map m ≫ Z✝.hom = Y✝.hom
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
Y✝ Z✝ : CostructuredArrow (Over.forget X ⋙ F) Y
m : Y✝ ⟶ Z✝
this : (Over.forget X ⋙ F).map m.left ≫ Z✝.hom = Y✝.hom ≫ (Functor.fromPUnit Y).map m.right
⊢ F.map ((proj (Over.forget X ⋙ F) Y ⋙ Over.forget X).map m) ≫ Z✝.hom = Y✝.hom

Tactic:
;

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F : T ⥤ D
Y : D
X : T
Y✝ Z✝ : CostructuredArrow (Over.forget X ⋙ F) Y
m : Y✝ ⟶ Z✝
this : (Over.forget X ⋙ F).map m.left ≫ Z✝.hom = Y✝.hom ≫ (Functor.fromPUnit Y).map m.right
⊢ F.map ((proj (Over.forget X ⋙ F) Y ⋙ Over.forget X).map m) ≫ Z✝.hom = Y✝.hom
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : CostructuredArrow (Functor.diag T) X
m : Y✝ ⟶ Z✝
this : ((Functor.diag T).map m.left ≫ Z✝.hom).1 = (Y✝.hom ≫ (Functor.fromPUnit X).map m.right).1
⊢ (proj (Functor.diag T) X).map m ≫ Z✝.hom.1 = Y✝.hom.1

Tactic:
;

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : CostructuredArrow (Functor.diag T) X
m : Y✝ ⟶ Z✝
this : ((Functor.diag T).map m.left ≫ Z✝.hom).1 = (Y✝.hom ≫ (Functor.fromPUnit X).map m.right).1
⊢ (proj (Functor.diag T) X).map m ≫ Z✝.hom.1 = Y✝.hom.1
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : CostructuredArrow (Functor.diag T) X
m : Y✝ ⟶ Z✝
this : ((Functor.diag T).map m.left ≫ Z✝.hom).2 = (Y✝.hom ≫ (Functor.fromPUnit X).map m.right).2
⊢ (Over.forget X.1).map (((proj (Functor.diag T) X).toOver X.1 (fun g ↦ g.hom.1) ⋯).map m) ≫ Z✝.hom.2 = Y✝.hom.2

Tactic:
;

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : CostructuredArrow (Functor.diag T) X
m : Y✝ ⟶ Z✝
this : ((Functor.diag T).map m.left ≫ Z✝.hom).2 = (Y✝.hom ≫ (Functor.fromPUnit X).map m.right).2
⊢ (Over.forget X.1).map (((proj (Functor.diag T) X).toOver X.1 (fun g ↦ g.hom.1) ⋯).map m) ≫ Z✝.hom.2 = Y✝.hom.2
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : CostructuredArrow (Over.forget X.1) X.2
m : Y✝ ⟶ Z✝
this : (Over.forget X.1).map m.left ≫ Z✝.hom = Y✝.hom ≫ (Functor.fromPUnit X.2).map m.right
⊢ (Functor.diag T).map ((proj (Over.forget X.1) X.2 ⋙ Over.forget X.1).map m) ≫ (Z✝.left.hom, Z✝.hom) =
    (Y✝.left.hom, Y✝.hom)

Tactic:
;

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T × T
Y✝ Z✝ : CostructuredArrow (Over.forget X.1) X.2
m : Y✝ ⟶ Z✝
this : (Over.forget X.1).map m.left ≫ Z✝.hom = Y✝.hom ≫ (Functor.fromPUnit X.2).map m.right
⊢ (Functor.diag T).map ((proj (Over.forget X.1) X.2 ⋙ Over.forget X.1).map m) ≫ (Z✝.left.hom, Z✝.hom) =
    (Y✝.left.hom, Y✝.hom)
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : Over (op X)
f : Z ⟶ Y
⊢ Y.hom.unop ≫ (Hom.left f).unop = Z.hom.unop

Tactic:
;

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : Over (op X)
f : Z ⟶ Y
⊢ Y.hom.unop ≫ (Hom.left f).unop = Z.hom.unop
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : (Under X)ᵒᵖ
f : Z ⟶ Y
⊢ (Under.Hom.right f.unop).op ≫ (unop Y).hom.op = (unop Z).hom.op

Tactic:
;

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : (Under X)ᵒᵖ
f : Z ⟶ Y
⊢ (Under.Hom.right f.unop).op ≫ (unop Y).hom.op = (unop Z).hom.op
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : Under (op X)
f : Z ⟶ Y
⊢ (Hom.right f).unop ≫ Z.hom.unop = Y.hom.unop

Tactic:
;

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : Under (op X)
f : Z ⟶ Y
⊢ (Hom.right f).unop ≫ Z.hom.unop = Y.hom.unop
Module: Mathlib.CategoryTheory.Comma.Over.Basic

Goal state before:
pp: T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : (Over X)ᵒᵖ
f : Z ⟶ Y
⊢ (unop Z).hom.op ≫ (Over.Hom.left f.unop).op = (unop Y).hom.op

Tactic:
;

Goal state after:
T : Type u₁
inst✝¹ : Category.{v₁, u₁} T
D : Type u₂
inst✝ : Category.{v₂, u₂} D
X : T
Z Y : (Over X)ᵒᵖ
f : Z ⟶ Y
⊢ (unop Z).hom.op ≫ (Over.Hom.left f.unop).op = (unop Y).hom.op
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst✝¹ : Mono i
inst✝ : HasPullback f g
⊢ (pullback.fst f g ≫ f) ≫ i = (pullback.snd f g ≫ g) ≫ i

Tactic:
;

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst✝¹ : Mono i
inst✝ : HasPullback f g
⊢ (pullback.fst f g ≫ f) ≫ i = (pullback.snd f g ≫ g) ≫ i
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst✝¹ : Mono i
inst✝ : HasPullback f g
⊢ pullback.fst f g ≫ f = pullback.snd f g ≫ g

Tactic:
;

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
W X Y Z : C
f : X ⟶ W
g : Y ⟶ W
i : W ⟶ Z
inst✝¹ : Mono i
inst✝ : HasPullback f g
⊢ pullback.fst f g ≫ f = pullback.snd f g ≫ g