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

Goal state before:
pp: case none
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
⊢ g ≫ (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π.app none =
    (WidePullbackShape.mkCone f fs w).π.app none

pp: case some
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
val✝ : J
⊢ g ≫ (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π.app (some val✝) =
    (WidePullbackShape.mkCone f fs w).π.app (some val✝)

Tactic:
·

Goal state after:
case none
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
⊢ g ≫ (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π.app none =
    (WidePullbackShape.mkCone f fs w).π.app none
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) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
val✝ : J
⊢ g ≫ (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π.app (some val✝) =
    (WidePullbackShape.mkCone f fs w).π.app (some val✝)

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) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g ≫ π arrows j = fs j
h2 : g ≫ base arrows = f
val✝ : J
⊢ g ≫ (limit.cone (WidePullbackShape.wideCospan B objs arrows)).π.app (some val✝) =
    (WidePullbackShape.mkCone f fs w).π.app (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g1 g2 : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
⊢ g1 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) none =
    g2 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) none

pp: case some
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g1 g2 : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
val✝ : J
⊢ g1 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) (some val✝) =
    g2 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) (some val✝)

Tactic:
·

Goal state after:
case none
J : Type w
C : Type u
inst✝¹ : Category.{v, u} C
B : C
objs : J → C
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g1 g2 : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
⊢ g1 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) none =
    g2 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) none
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) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g1 g2 : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
val✝ : J
⊢ g1 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) (some val✝) =
    g2 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) (some val✝)

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) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : C
g1 g2 : X ⟶ widePullback B objs arrows
h1 : ∀ (j : J), g1 ≫ π arrows j = g2 ≫ π arrows j
h2 : g1 ≫ base arrows = g2 ≫ base arrows
val✝ : J
⊢ g1 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) (some val✝) =
    g2 ≫ limit.π (WidePullbackShape.wideCospan B objs arrows) (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
⊢ lift t ≫ s.π.app none = t.π.app none

pp: case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
val✝ : ι
⊢ lift t ≫ s.π.app (some val✝) = t.π.app (some val✝)

Tactic:
·

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
⊢ lift t ≫ s.π.app none = t.π.app none
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
val✝ : ι
⊢ lift t ≫ s.π.app (some val✝) = t.π.app (some val✝)

Tactic:
·

Goal state after:
case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
lift : (t : WidePullbackCone f) → t.pt ⟶ s.pt
facbase : ∀ (t : WidePullbackCone f), lift t ≫ s.base = t.base
facπ : ∀ (t : WidePullbackCone f) (i : ι), lift t ≫ s.π i = t.π i
uniq : ∀ (t : WidePullbackCone f) (m : t.pt ⟶ s.pt), m ≫ s.base = t.base → (∀ (i : ι), m ≫ s.π i = t.π i) → m = lift t
t : Cone (WidePullbackShape.wideCospan X Y f)
val✝ : ι
⊢ lift t ≫ s.π.app (some val✝) = t.π.app (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
⊢ k ≫ s.π.app none = l ≫ s.π.app none

pp: case some
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
j : ι
⊢ k ≫ s.π.app (some j) = l ≫ s.π.app (some j)

Tactic:
·

Goal state after:
case none
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
⊢ k ≫ s.π.app none = l ≫ s.π.app none
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case some
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
j : ι
⊢ k ≫ s.π.app (some j) = l ≫ s.π.app (some j)

Tactic:
·

Goal state after:
case some
C : Type u
inst✝ : Category.{v, u} C
ι : Type u_1
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s : WidePullbackCone f
hs : IsLimit s
W : C
k l : W ⟶ s.pt
hbase : k ≫ s.base = l ≫ s.base
hπ : ∀ (i : ι), k ≫ s.π i = l ≫ s.π i
j : ι
⊢ k ≫ s.π.app (some j) = l ≫ s.π.app (some j)
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s t : WidePullbackCone f
e : s.pt ≅ t.pt
base : e.hom ≫ t.base = s.base
π : ∀ (i : ι), e.hom ≫ t.π i = s.π i
⊢ s.π.app none = e.hom ≫ t.π.app none

pp: case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s t : WidePullbackCone f
e : s.pt ≅ t.pt
base : e.hom ≫ t.base = s.base
π : ∀ (i : ι), e.hom ≫ t.π i = s.π i
val✝ : ι
⊢ s.π.app (some val✝) = e.hom ≫ t.π.app (some val✝)

Tactic:
·

Goal state after:
case none
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s t : WidePullbackCone f
e : s.pt ≅ t.pt
base : e.hom ≫ t.base = s.base
π : ∀ (i : ι), e.hom ≫ t.π i = s.π i
⊢ s.π.app none = e.hom ≫ t.π.app none
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s t : WidePullbackCone f
e : s.pt ≅ t.pt
base : e.hom ≫ t.base = s.base
π : ∀ (i : ι), e.hom ≫ t.π i = s.π i
val✝ : ι
⊢ s.π.app (some val✝) = e.hom ≫ t.π.app (some val✝)

Tactic:
·

Goal state after:
case some
J : Type w
C : Type u
inst✝ : Category.{v, u} C
ι✝ : Type u_1
X✝ : C
Y✝ : ι✝ → C
f✝ : (i : ι✝) → Y✝ i ⟶ X✝
ι : Type u_2
X : C
Y : ι → C
f : (i : ι) → Y i ⟶ X
s t : WidePullbackCone f
e : s.pt ≅ t.pt
base : e.hom ≫ t.base = s.base
π : ∀ (i : ι), e.hom ≫ t.π i = s.π i
val✝ : ι
⊢ s.π.app (some val✝) = e.hom ≫ t.π.app (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: β : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝¹ : Category.{v, u} C
f : β → C
inst✝ : HasCoproduct f
⊢ IsIso (Sigma.desc fun a ↦ Sigma.ι f a)

Tactic:
by
  convert! IsIso.id _
  ext
  simp

Goal state after:
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 : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ (t :
      Cofan fun x ↦
        match x with
        | ⟨a, b⟩ => Y a b) →
    (mk c.pt fun x ↦
          match x with
          | ⟨a, b⟩ => π a b ≫ c.inj a).pt ⟶
      t.pt

pp: case refine_2
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ ∀
    (t :
      Cofan fun x ↦
        match x with
        | ⟨a, b⟩ => Y a b)
    (j : (a : α) × β a),
    (mk c.pt fun x ↦
              match x with
              | ⟨a, b⟩ => π a b ≫ c.inj a).inj
          j ≫
        ?refine_1 t =
      t.inj j

pp: case refine_3
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ ∀
    (t :
      Cofan fun x ↦
        match x with
        | ⟨a, b⟩ => Y a b)
    (m :
      (mk c.pt fun x ↦
            match x with
            | ⟨a, b⟩ => π a b ≫ c.inj a).pt ⟶
        t.pt),
    (∀ (j : (a : α) × β a),
        (mk c.pt fun x ↦
                  match x with
                  | ⟨a, b⟩ => π a b ≫ c.inj a).inj
              j ≫
            m =
          t.inj j) →
      m = ?refine_1 t

Tactic:
·

Goal state after:
case refine_1
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ (t :
      Cofan fun x ↦
        match x with
        | ⟨a, b⟩ => Y a b) →
    (mk c.pt fun x ↦
          match x with
          | ⟨a, b⟩ => π a b ≫ c.inj a).pt ⟶
      t.pt
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 : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ ∀
    (t :
      Cofan fun x ↦
        match x with
        | ⟨a, b⟩ => Y a b)
    (j : (a : α) × β a),
    (mk c.pt fun x ↦
              match x with
              | ⟨a, b⟩ => π a b ≫ c.inj a).inj
          j ≫
        hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩)) =
      t.inj j

pp: case refine_3
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ ∀
    (t :
      Cofan fun x ↦
        match x with
        | ⟨a, b⟩ => Y a b)
    (m :
      (mk c.pt fun x ↦
            match x with
            | ⟨a, b⟩ => π a b ≫ c.inj a).pt ⟶
        t.pt),
    (∀ (j : (a : α) × β a),
        (mk c.pt fun x ↦
                  match x with
                  | ⟨a, b⟩ => π a b ≫ c.inj a).inj
              j ≫
            m =
          t.inj j) →
      m = hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩))

Tactic:
·

Goal state after:
case refine_2
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ ∀
    (t :
      Cofan fun x ↦
        match x with
        | ⟨a, b⟩ => Y a b)
    (j : (a : α) × β a),
    (mk c.pt fun x ↦
              match x with
              | ⟨a, b⟩ => π a b ≫ c.inj a).inj
          j ≫
        hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩)) =
      t.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 : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan fun x ↦
    match x with
    | ⟨a, b⟩ => Y a b
a : α
b : β a
⊢ π a b ≫ (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩)).ι.app { as := a } = t.inj ⟨a, b⟩

Tactic:
(hs a).fac

Goal state after:
case refine_2
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan fun x ↦
    match x with
    | ⟨a, b⟩ => Y a b
a : α
b : β a
⊢ (mk t.pt fun b ↦ t.inj ⟨{ as := a }.as, b⟩).ι.app { as := b } = t.inj ⟨a, b⟩
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case refine_3
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ ∀
    (t :
      Cofan fun x ↦
        match x with
        | ⟨a, b⟩ => Y a b)
    (m :
      (mk c.pt fun x ↦
            match x with
            | ⟨a, b⟩ => π a b ≫ c.inj a).pt ⟶
        t.pt),
    (∀ (j : (a : α) × β a),
        (mk c.pt fun x ↦
                  match x with
                  | ⟨a, b⟩ => π a b ≫ c.inj a).inj
              j ≫
            m =
          t.inj j) →
      m = hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩))

Tactic:
·

Goal state after:
case refine_3
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
⊢ ∀
    (t :
      Cofan fun x ↦
        match x with
        | ⟨a, b⟩ => Y a b)
    (m :
      (mk c.pt fun x ↦
            match x with
            | ⟨a, b⟩ => π a b ≫ c.inj a).pt ⟶
        t.pt),
    (∀ (j : (a : α) × β a),
        (mk c.pt fun x ↦
                  match x with
                  | ⟨a, b⟩ => π a b ≫ c.inj a).inj
              j ≫
            m =
          t.inj j) →
      m = hc.desc (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩))
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none
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
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
⊢ (colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι.app none ≫ g =
    (WidePushoutShape.mkCocone f fs w).ι.app none

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
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
val✝ : J
⊢ (colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι.app (some val✝) ≫ g =
    (WidePushoutShape.mkCocone f fs w).ι.app (some val✝)

Tactic:
·

Goal state after:
case none
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
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
⊢ (colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι.app none ≫ g =
    (WidePushoutShape.mkCocone f fs w).ι.app none
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
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
val✝ : J
⊢ (colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι.app (some val✝) ≫ g =
    (WidePushoutShape.mkCocone f fs w).ι.app (some val✝)

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
f : B ⟶ X
fs : (j : J) → objs j ⟶ X
w : ∀ (j : J), arrows j ≫ fs j = f
g : widePushout B objs arrows ⟶ X
h1 : ∀ (j : J), ι arrows j ≫ g = fs j
h2 : head arrows ≫ g = f
val✝ : J
⊢ (colimit.cocone (WidePushoutShape.wideSpan B objs arrows)).ι.app (some val✝) ≫ g =
    (WidePushoutShape.mkCocone f fs w).ι.app (some val✝)
Module: Mathlib.CategoryTheory.Limits.Shapes.Products

Goal state before:
pp: case refine_3
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan fun x ↦
    match x with
    | ⟨a, b⟩ => Y a b
m :
  (mk c.pt fun x ↦
        match x with
        | ⟨a, b⟩ => π a b ≫ c.inj a).pt ⟶
    t.pt
h :
  ∀ (j : (a : α) × β a),
    (mk c.pt fun x ↦
              match x with
              | ⟨a, b⟩ => π a b ≫ c.inj a).inj
          j ≫
        m =
      t.inj j
x✝¹ : Discrete α
a : α
x✝ : Discrete (β a)
b : β a
⊢ (mk (X a) (π a)).ι.app { as := b } ≫ c.ι.app { as := a } ≫ m =
    (mk (X a) (π a)).ι.app { as := b } ≫ (mk t.1 fun a ↦ (hs a).desc (mk t.pt fun b ↦ t.inj ⟨a, b⟩)).ι.app { as := a }

Tactic:
(hs a).fac

Goal state after:
case refine_3
β✝ : Type w
α : Type w₂
γ : Type w₃
C : Type u
inst✝ : Category.{v, u} C
X : α → C
c : Cofan X
hc : IsColimit c
β : α → Type u_1
Y : (a : α) → β a → C
π : (a : α) → (b : β a) → Y a b ⟶ X a
hs : (a : α) → IsColimit (mk (X a) (π a))
t :
  Cofan fun x ↦
    match x with
    | ⟨a, b⟩ => Y a b
m :
  (mk c.pt fun x ↦
        match x with
        | ⟨a, b⟩ => π a b ≫ c.inj a).pt ⟶
    t.pt
h :
  ∀ (j : (a : α) × β a),
    (mk c.pt fun x ↦
              match x with
              | ⟨a, b⟩ => π a b ≫ c.inj a).inj
          j ≫
        m =
      t.inj j
x✝¹ : Discrete α
a : α
x✝ : Discrete (β a)
b : β a
⊢ (mk (X a) (π a)).ι.app { as := b } ≫ c.ι.app { as := a } ≫ m =
    (mk t.pt fun b ↦ t.inj ⟨{ as := a }.as, b⟩).ι.app { as := b }
Module: Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks

Goal state before:
pp: case none
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
⊢ colimit.ι (WidePushoutShape.wideSpan B objs arrows) none ≫ g1 =
    colimit.ι (WidePushoutShape.wideSpan B objs arrows) none ≫ g2

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 none
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
⊢ colimit.ι (WidePushoutShape.wideSpan B objs arrows) none ≫ g1 =
    colimit.ι (WidePushoutShape.wideSpan B objs arrows) none ≫ g2