no goals
J : Type w
C : Type u
inst✝² : Category C
D : Type ?u.242573
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
⊢ ∀ (j : J), (fun j => g ≫ π arrows j) j ≫ arrows j = g ≫ base arrows
aesop_cat
case a
J : Type w
C : Type u
inst✝² : Category C
D : Type u_1
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
⊢ ∀ (j : J), g ≫ π arrows j = g ≫ π arrows j

case a
J : Type w
C : Type u
inst✝² : Category C
D : Type u_1
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
⊢ g ≫ base arrows = g ≫ base arrows
J : Type w
C : Type u
inst✝² : Category C
D : Type u_1
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
⊢ g = lift (g ≫ base arrows) (fun j => g ≫ π arrows j) (_ : ∀ (j : J), (g ≫ π arrows j) ≫ arrows j = g ≫ base arrows)
apply eq_lift_of_comp_eq
case a
J : Type w
C : Type u
inst✝² : Category C
D : Type u_1
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
⊢ g ≫ base arrows = g ≫ base arrows
case a
J : Type w
C : Type u
inst✝² : Category C
D : Type u_1
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
⊢ ∀ (j : J), g ≫ π arrows j = g ≫ π arrows j

case a
J : Type w
C : Type u
inst✝² : Category C
D : Type u_1
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
⊢ g ≫ base arrows = g ≫ base arrows
aesop_cat
no goals
case a
J : Type w
C : Type u
inst✝² : Category C
D : Type u_1
inst✝¹ : Category D
B : D
objs : J → D
arrows : (j : J) → objs j ⟶ B
inst✝ : HasWidePullback B objs arrows
X : D
f : X ⟶ B
fs : (j : J) → X ⟶ objs j
w : ∀ (j : J), fs j ≫ arrows j = f
g : X ⟶ widePullback B (fun j => objs j) arrows
⊢ g ≫ base arrows = g ≫ base arrows
rfl