X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
⊢ ∃! x, f x = y
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
⊢ ∃! x, f x = y
let y' : PUnit ⟶ Y := fun _ => y
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
⊢ ∃! x, f x = y
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
⊢ ∃! x, f x = y
have hy' : y' ≫ g = y' ≫ h := funext fun _ => hy
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
⊢ ∀ (y_1 : X), (fun x => f x = y) y_1 → y_1 = ↑(Fork.IsLimit.lift' t y' hy') PUnit.unit
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
⊢ ∃! x, f x = y
refine' ⟨(Fork.IsLimit.lift' t _ hy').1 ⟨⟩, congr_fun (Fork.IsLimit.lift' t y' _).2 ⟨⟩, _⟩
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
⊢ x' = ↑(Fork.IsLimit.lift' t y' hy') PUnit.unit
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
⊢ ∀ (y_1 : X), (fun x => f x = y) y_1 → y_1 = ↑(Fork.IsLimit.lift' t y' hy') PUnit.unit
intro x' hx'
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
this : (fun x => x') = ↑(Fork.IsLimit.lift' t y' hy')
⊢ x' = ↑(Fork.IsLimit.lift' t y' hy') PUnit.unit

case this
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
⊢ (fun x => x') = ↑(Fork.IsLimit.lift' t y' hy')
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
⊢ x' = ↑(Fork.IsLimit.lift' t y' hy') PUnit.unit
suffices : (fun _ : PUnit => x') = (Fork.IsLimit.lift' t y' hy').1
case this
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
⊢ (fun x => x') = ↑(Fork.IsLimit.lift' t y' hy')
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
this : (fun x => x') = ↑(Fork.IsLimit.lift' t y' hy')
⊢ x' = ↑(Fork.IsLimit.lift' t y' hy') PUnit.unit

case this
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
⊢ (fun x => x') = ↑(Fork.IsLimit.lift' t y' hy')
rw [← this]
case this
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
⊢ (fun x => x') ≫ Fork.ι (Fork.ofι f w) = ↑(Fork.IsLimit.lift' t y' hy') ≫ Fork.ι (Fork.ofι f w)
case this
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
⊢ (fun x => x') = ↑(Fork.IsLimit.lift' t y' hy')
apply Fork.IsLimit.hom_ext t
case this.h
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
⊢ ((fun x => x') ≫ Fork.ι (Fork.ofι f w)) PUnit.unit =
    (↑(Fork.IsLimit.lift' t y' hy') ≫ Fork.ι (Fork.ofι f w)) PUnit.unit
case this
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
⊢ (fun x => x') ≫ Fork.ι (Fork.ofι f w) = ↑(Fork.IsLimit.lift' t y' hy') ≫ Fork.ι (Fork.ofι f w)
funext ⟨⟩
no goals
case this.h
X Y Z : Type u
f : X ⟶ Y
g h : Y ⟶ Z
w : f ≫ g = f ≫ h
t : IsLimit (Fork.ofι f w)
y : Y
hy : g y = h y
y' : PUnit ⟶ Y := fun x => y
hy' : y' ≫ g = y' ≫ h
x' : X
hx' : f x' = y
⊢ ((fun x => x') ≫ Fork.ι (Fork.ofι f w)) PUnit.unit =
    (↑(Fork.IsLimit.lift' t y' hy') ≫ Fork.ι (Fork.ofι f w)) PUnit.unit
apply hx'.trans (congr_fun (Fork.IsLimit.lift' t _ hy').2 ⟨⟩).symm