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

Goal state before:
pp: case some
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
g1 g2 : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
val✝ : J
⊢ colimit.ι (WidePushoutShape.wideSpan B objs arrows) (some val✝) ≫ g1 =
    colimit.ι (WidePushoutShape.wideSpan B objs arrows) (some val✝) ≫ g2

Tactic:
·

Goal state after:
case some
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → B ⟶ objs j
inst✝ : HasWidePushout B objs arrows
X : C
g1 g2 : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g1 = ι arrows j ≫ g2
h2 : head arrows ≫ g1 = head arrows ≫ g2
val✝ : J
⊢ colimit.ι (WidePushoutShape.wideSpan B objs arrows) (some val✝) ≫ g1 =
    colimit.ι (WidePushoutShape.wideSpan B objs arrows) (some val✝) ≫ g2
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryFan X Y
lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)
hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.fst = f
hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.snd = g
uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), m ≫ s.fst = f → m ≫ s.snd = g → m = lift f g
⊢ ∀ (s_1 : Cone (pair X Y)) (j : Discrete WalkingPair), lift (fst s_1) (snd s_1) ≫ s.π.app j = s_1.π.app j

Tactic:
rintro t (rfl | rfl)

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryFan X Y
lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)
hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.fst = f
hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.snd = g
uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), m ≫ s.fst = f → m ≫ s.snd = g → m = lift f g
t : Cone (pair X Y)
⊢ lift (fst t) (snd t) ≫ s.π.app { as := left } = t.π.app { as := left }

case right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryFan X Y
lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)
hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.fst = f
hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.snd = g
uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), m ≫ s.fst = f → m ≫ s.snd = g → m = lift f g
t : Cone (pair X Y)
⊢ lift (fst t) (snd t) ≫ s.π.app { as := right } = t.π.app { as := right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryFan X Y
lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)
hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.fst = f
hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.snd = g
uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), m ≫ s.fst = f → m ≫ s.snd = g → m = lift f g
t : Cone (pair X Y)
⊢ lift (fst t) (snd t) ≫ s.π.app { as := left } = t.π.app { as := left }

pp: case right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryFan X Y
lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)
hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.fst = f
hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.snd = g
uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), m ≫ s.fst = f → m ≫ s.snd = g → m = lift f g
t : Cone (pair X Y)
⊢ lift (fst t) (snd t) ≫ s.π.app { as := right } = t.π.app { as := right }

Tactic:
·

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryFan X Y
lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)
hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.fst = f
hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.snd = g
uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), m ≫ s.fst = f → m ≫ s.snd = g → m = lift f g
t : Cone (pair X Y)
⊢ lift (fst t) (snd t) ≫ s.π.app { as := left } = t.π.app { as := left }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryFan X Y
lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)
hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.fst = f
hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.snd = g
uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), m ≫ s.fst = f → m ≫ s.snd = g → m = lift f g
t : Cone (pair X Y)
⊢ lift (fst t) (snd t) ≫ s.π.app { as := right } = t.π.app { as := right }

Tactic:
·

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryFan X Y
lift : {T : C} → (T ⟶ X) → (T ⟶ Y) → (T ⟶ s.pt)
hl₁ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.fst = f
hl₂ : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y), lift f g ≫ s.snd = g
uniq : ∀ {T : C} (f : T ⟶ X) (g : T ⟶ Y) (m : T ⟶ s.pt), m ≫ s.fst = f → m ≫ s.snd = g → m = lift f g
t : Cone (pair X Y)
⊢ lift (fst t) (snd t) ≫ s.π.app { as := right } = t.π.app { as := right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
⊢ ∀ (s_1 : Cocone (pair X Y)) (j : Discrete WalkingPair), s.ι.app j ≫ desc (inl s_1) (inr s_1) = s_1.ι.app j

Tactic:
rintro t (rfl | rfl)

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
t : Cocone (pair X Y)
⊢ s.ι.app { as := left } ≫ desc (inl t) (inr t) = t.ι.app { as := left }

case right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
t : Cocone (pair X Y)
⊢ s.ι.app { as := right } ≫ desc (inl t) (inr t) = t.ι.app { as := right }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
t : Cocone (pair X Y)
⊢ s.ι.app { as := left } ≫ desc (inl t) (inr t) = t.ι.app { as := left }

pp: case right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
t : Cocone (pair X Y)
⊢ s.ι.app { as := right } ≫ desc (inl t) (inr t) = t.ι.app { as := right }

Tactic:
·

Goal state after:
case left
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
t : Cocone (pair X Y)
⊢ s.ι.app { as := left } ≫ desc (inl t) (inr t) = t.ι.app { as := left }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
t : Cocone (pair X Y)
⊢ s.ι.app { as := right } ≫ desc (inl t) (inr t) = t.ι.app { as := right }

Tactic:
·

Goal state after:
case right
C : Type u
inst✝ : Category.{v, u} C
X Y : C
s : BinaryCofan X Y
desc : {T : C} → (X ⟶ T) → (Y ⟶ T) → (s.pt ⟶ T)
hd₁ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inl ≫ desc f g = f
hd₂ : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T), s.inr ≫ desc f g = g
uniq : ∀ {T : C} (f : X ⟶ T) (g : Y ⟶ T) (m : s.pt ⟶ T), s.inl ≫ m = f → s.inr ≫ m = g → m = desc f g
t : Cocone (pair X Y)
⊢ s.ι.app { as := right } ≫ desc (inl t) (inr t) = t.ι.app { as := right }
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case refine_1
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Fan fun x ↦ Y
j : J
⊢ (s.proj default ≫ e.inv) ≫ (mk X fun x ↦ e.hom).proj j = s.proj j

pp: case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Fan fun x ↦ Y
m : s.pt ⟶ (mk X fun x ↦ e.hom).pt
hm : ∀ (j : J), m ≫ (mk X fun x ↦ e.hom).proj j = s.proj j
⊢ m = s.proj default ≫ e.inv

Tactic:
·

Goal state after:
case refine_1
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Fan fun x ↦ Y
j : J
⊢ (s.proj default ≫ e.inv) ≫ (mk X fun x ↦ e.hom).proj j = s.proj j
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Fan fun x ↦ Y
m : s.pt ⟶ (mk X fun x ↦ e.hom).pt
hm : ∀ (j : J), m ≫ (mk X fun x ↦ e.hom).proj j = s.proj j
⊢ m = s.proj default ≫ e.inv

Tactic:
·

Goal state after:
case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Fan fun x ↦ Y
m : s.pt ⟶ (mk X fun x ↦ e.hom).pt
hm : ∀ (j : J), m ≫ (mk X fun x ↦ e.hom).proj j = s.proj j
⊢ m = s.proj default ≫ e.inv
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case refine_1
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Cofan fun x ↦ X
j : J
⊢ (mk Y fun x ↦ e.hom).inj j ≫ e.inv ≫ s.inj default = s.inj j

pp: case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Cofan fun x ↦ X
m : (mk Y fun x ↦ e.hom).pt ⟶ s.pt
hm : ∀ (j : J), (mk Y fun x ↦ e.hom).inj j ≫ m = s.inj j
⊢ m = e.inv ≫ s.inj default

Tactic:
·

Goal state after:
case refine_1
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Cofan fun x ↦ X
j : J
⊢ (mk Y fun x ↦ e.hom).inj j ≫ e.inv ≫ s.inj default = s.inj j
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Cofan fun x ↦ X
m : (mk Y fun x ↦ e.hom).pt ⟶ s.pt
hm : ∀ (j : J), (mk Y fun x ↦ e.hom).inj j ≫ m = s.inj j
⊢ m = e.inv ≫ s.inj default

Tactic:
·

Goal state after:
case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
e : X ≅ Y
J : Type u_1
inst✝ : Unique J
s : Cofan fun x ↦ X
m : (mk Y fun x ↦ e.hom).pt ⟶ s.pt
hm : ∀ (j : J), (mk Y fun x ↦ e.hom).inj j ≫ m = s.inj j
⊢ m = e.inv ≫ s.inj default
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) → IsIso c.fst

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ IsIso c.fst → Nonempty (IsLimit c)

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ Nonempty (IsLimit c) → IsIso c.fst
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ IsIso c.fst → Nonempty (IsLimit c)

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsTerminal Y
c : BinaryFan X Y
⊢ IsIso c.fst → Nonempty (IsLimit c)
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case lift
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ (s : BinaryFan X' ((pair X Y).obj { as := right })) →
    s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }

pp: case fac_left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right })), ?lift s ≫ c.fst ≫ f = s.fst

pp: case fac_right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right })), ?lift s ≫ c.snd = s.snd

pp: case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right }))
    (m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    m ≫ c.fst ≫ f = s.fst → m ≫ c.snd = s.snd → m = ?lift s

Tactic:
·

Goal state after:
case lift
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ (s : BinaryFan X' ((pair X Y).obj { as := right })) →
    s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case fac_left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right })), IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.fst ≫ f = s.fst

pp: case fac_right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right })), IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.snd = s.snd

pp: case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right }))
    (m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    m ≫ c.fst ≫ f = s.fst → m ≫ c.snd = s.snd → m = IsLimit.lift h (s.fst ≫ inv f) s.snd

Tactic:
·

Goal state after:
case fac_left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right })), IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.fst ≫ f = s.fst
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case fac_right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right })), IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.snd = s.snd

pp: case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right }))
    (m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    m ≫ c.fst ≫ f = s.fst → m ≫ c.snd = s.snd → m = IsLimit.lift h (s.fst ≫ inv f) s.snd

Tactic:
·

Goal state after:
case fac_right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right })), IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.snd = s.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right }))
    (m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    m ≫ c.fst ≫ f = s.fst → m ≫ c.snd = s.snd → m = IsLimit.lift h (s.fst ≫ inv f) s.snd

Tactic:
·

Goal state after:
case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
⊢ ∀ (s : BinaryFan X' ((pair X Y).obj { as := right }))
    (m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }),
    m ≫ c.fst ≫ f = s.fst → m ≫ c.snd = s.snd → m = IsLimit.lift h (s.fst ≫ inv f) s.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case uniq.h₁
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
s : BinaryFan X' ((pair X Y).obj { as := right })
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }
e₁ : m ≫ c.fst ≫ f = s.fst
e₂ : m ≫ c.snd = s.snd
⊢ m ≫ c.fst = IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.fst

pp: case uniq.h₂
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
s : BinaryFan X' ((pair X Y).obj { as := right })
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }
e₁ : m ≫ c.fst ≫ f = s.fst
e₂ : m ≫ c.snd = s.snd
⊢ m ≫ c.snd = IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.snd

Tactic:
·

Goal state after:
case uniq.h₁
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
s : BinaryFan X' ((pair X Y).obj { as := right })
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }
e₁ : m ≫ c.fst ≫ f = s.fst
e₂ : m ≫ c.snd = s.snd
⊢ m ≫ c.fst = IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.fst
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case uniq.h₂
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
s : BinaryFan X' ((pair X Y).obj { as := right })
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }
e₁ : m ≫ c.fst ≫ f = s.fst
e₂ : m ≫ c.snd = s.snd
⊢ m ≫ c.snd = IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.snd

Tactic:
·

Goal state after:
case uniq.h₂
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryFan X Y
f : X ⟶ X'
inst✝ : IsIso f
h : IsLimit c
s : BinaryFan X' ((pair X Y).obj { as := right })
m : s.pt ⟶ ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left }
e₁ : m ≫ c.fst ≫ f = s.fst
e₂ : m ≫ c.snd = s.snd
⊢ m ≫ c.snd = IsLimit.lift h (s.fst ≫ inv f) s.snd ≫ c.snd
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) → IsIso c.inl

pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ IsIso c.inl → Nonempty (IsColimit c)

Tactic:
·

Goal state after:
case mp
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ Nonempty (IsColimit c) → IsIso c.inl
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case refine_1
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Fan fun j ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan fun i ↦ (c i).pt
hc' : IsLimit c'
t : Fan fun p ↦ X p.1 p.2
⊢ t.pt ⟶ (Fan.mk c'.pt fun p ↦ c'.proj p.1 ≫ (c p.1).proj p.2).pt

pp: case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Fan fun j ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan fun i ↦ (c i).pt
hc' : IsLimit c'
⊢ ∀ (s : Fan fun p ↦ X p.1 p.2) (j : ι × ι'),
    ?refine_1 ≫ (Fan.mk c'.pt fun p ↦ c'.proj p.1 ≫ (c p.1).proj p.2).proj j = s.proj j

pp: case refine_3
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Fan fun j ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan fun i ↦ (c i).pt
hc' : IsLimit c'
t : Fan fun p ↦ X p.1 p.2
m : t.pt ⟶ (Fan.mk c'.pt fun p ↦ c'.proj p.1 ≫ (c p.1).proj p.2).pt
hm : ∀ (j : ι × ι'), m ≫ (Fan.mk c'.pt fun p ↦ c'.proj p.1 ≫ (c p.1).proj p.2).proj j = t.proj j
⊢ m = ?refine_1

Tactic:
·

Goal state after:
case refine_1
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Fan fun j ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan fun i ↦ (c i).pt
hc' : IsLimit c'
t : Fan fun p ↦ X p.1 p.2
⊢ t.pt ⟶ (Fan.mk c'.pt fun p ↦ c'.proj p.1 ≫ (c p.1).proj p.2).pt
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ IsIso c.inl → Nonempty (IsColimit c)

Tactic:
·

Goal state after:
case mpr
C : Type u
inst✝ : Category.{v, u} C
X Y : C
h : IsInitial Y
c : BinaryCofan X Y
⊢ IsIso c.inl → Nonempty (IsColimit c)
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Fan fun j ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan fun i ↦ (c i).pt
hc' : IsLimit c'
⊢ ∀ (s : Fan fun p ↦ X p.1 p.2) (j : ι × ι'),
    (lift hc' fun i ↦ lift (hc i) fun j ↦ s.proj (i, j)) ≫
        (Fan.mk c'.pt fun p ↦ c'.proj p.1 ≫ (c p.1).proj p.2).proj j =
      s.proj j

pp: case refine_3
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Fan fun j ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan fun i ↦ (c i).pt
hc' : IsLimit c'
t : Fan fun p ↦ X p.1 p.2
m : t.pt ⟶ (Fan.mk c'.pt fun p ↦ c'.proj p.1 ≫ (c p.1).proj p.2).pt
hm : ∀ (j : ι × ι'), m ≫ (Fan.mk c'.pt fun p ↦ c'.proj p.1 ≫ (c p.1).proj p.2).proj j = t.proj j
⊢ m = lift hc' fun i ↦ lift (hc i) fun j ↦ t.proj (i, j)

Tactic:
·

Goal state after:
case refine_2
β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
ι' : Type u_2
X : ι → ι' → C
c : (i : ι) → Fan fun j ↦ X i j
hc : (i : ι) → IsLimit (c i)
c' : Fan fun i ↦ (c i).pt
hc' : IsLimit c'
⊢ ∀ (s : Fan fun p ↦ X p.1 p.2) (j : ι × ι'),
    (lift hc' fun i ↦ lift (hc i) fun j ↦ s.proj (i, j)) ≫
        (Fan.mk c'.pt fun p ↦ c'.proj p.1 ≫ (c p.1).proj p.2).proj j =
      s.proj j
Module: Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts

Goal state before:
pp: case desc
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ (s : BinaryCofan X' ((pair X Y).obj { as := right })) →
    ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt

pp: case fac_left
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan X' ((pair X Y).obj { as := right })), (f ≫ c.inl) ≫ ?desc s = s.inl

pp: case fac_right
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan X' ((pair X Y).obj { as := right })), c.inr ≫ ?desc s = s.inr

pp: case uniq
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ ∀ (s : BinaryCofan X' ((pair X Y).obj { as := right }))
    (m : ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt),
    (f ≫ c.inl) ≫ m = s.inl → c.inr ≫ m = s.inr → m = ?desc s

Tactic:
·

Goal state after:
case desc
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ X Y X' : C
c : BinaryCofan X Y
f : X' ⟶ X
inst✝ : IsIso f
h : IsColimit c
⊢ (s : BinaryCofan X' ((pair X Y).obj { as := right })) →
    ((Functor.const (Discrete WalkingPair)).obj c.pt).obj { as := left } ⟶ s.pt