[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
⊢ Function.Injective fun x j => ↑(NatTrans.app D.π j) x
[PROOFSTEP]
let E := (forget C).mapCone D
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
⊢ Function.Injective fun x j => ↑(NatTrans.app D.π j) x
[PROOFSTEP]
let hE : IsLimit E := isLimitOfPreserves _ hD
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
⊢ Function.Injective fun x j => ↑(NatTrans.app D.π j) x
[PROOFSTEP]
let G := Types.limitCone.{w, v} (F ⋙ forget C)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
⊢ Function.Injective fun x j => ↑(NatTrans.app D.π j) x
[PROOFSTEP]
let hG := Types.limitConeIsLimit.{w, v} (F ⋙ forget C)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
⊢ Function.Injective fun x j => ↑(NatTrans.app D.π j) x
[PROOFSTEP]
let T : E.pt ≅ G.pt := hE.conePointUniqueUpToIso hG
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
⊢ Function.Injective fun x j => ↑(NatTrans.app D.π j) x
[PROOFSTEP]
change Function.Injective (T.hom ≫ fun x j => G.π.app j x)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
⊢ Function.Injective (T.hom ≫ fun x j => NatTrans.app G.π j x)
[PROOFSTEP]
have h : Function.Injective T.hom := by
  intro a b h
  suffices T.inv (T.hom a) = T.inv (T.hom b) by simpa
  rw [h]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
⊢ Function.Injective T.hom
[PROOFSTEP]
intro a b h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
a b : E.pt
h : T.hom a = T.hom b
⊢ a = b
[PROOFSTEP]
suffices T.inv (T.hom a) = T.inv (T.hom b) by simpa
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
a b : E.pt
h : T.hom a = T.hom b
this : T.inv (T.hom a) = T.inv (T.hom b)
⊢ a = b
[PROOFSTEP]
simpa
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
a b : E.pt
h : T.hom a = T.hom b
⊢ T.inv (T.hom a) = T.inv (T.hom b)
[PROOFSTEP]
rw [h]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
h : Function.Injective T.hom
⊢ Function.Injective (T.hom ≫ fun x j => NatTrans.app G.π j x)
[PROOFSTEP]
suffices Function.Injective fun (x : G.pt) j => G.π.app j x by exact this.comp h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
h : Function.Injective T.hom
this : Function.Injective fun x j => NatTrans.app G.π j x
⊢ Function.Injective (T.hom ≫ fun x j => NatTrans.app G.π j x)
[PROOFSTEP]
exact this.comp h
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
D : Cone F
hD : IsLimit D
E : Cone (F ⋙ forget C) := (forget C).mapCone D
hE : IsLimit E := isLimitOfPreserves (forget C) hD
G : Cone (F ⋙ forget C) := Types.limitCone (F ⋙ forget C)
hG : IsLimit (Types.limitCone (F ⋙ forget C)) := Types.limitConeIsLimit (F ⋙ forget C)
T : E.pt ≅ G.pt := IsLimit.conePointUniqueUpToIso hE hG
h : Function.Injective T.hom
⊢ Function.Injective fun x j => NatTrans.app G.π j x
[PROOFSTEP]
apply Subtype.ext
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h₀ : ↑(base f) x = ↑(base f) y
h : ∀ (j : ι), ↑(π f j) x = ↑(π f j) y
⊢ x = y
[PROOFSTEP]
apply Concrete.limit_ext
[GOAL]
case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h₀ : ↑(base f) x = ↑(base f) y
h : ∀ (j : ι), ↑(π f j) x = ↑(π f j) y
⊢ ∀ (j : WidePullbackShape ι), ↑(limit.π (wideCospan B X f) j) x = ↑(limit.π (wideCospan B X f) j) y
[PROOFSTEP]
rintro (_ | j)
[GOAL]
case a.none
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h₀ : ↑(base f) x = ↑(base f) y
h : ∀ (j : ι), ↑(π f j) x = ↑(π f j) y
⊢ ↑(limit.π (wideCospan B X f) none) x = ↑(limit.π (wideCospan B X f) none) y
[PROOFSTEP]
exact h₀
[GOAL]
case a.some
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
B : C
ι : Type w
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h₀ : ↑(base f) x = ↑(base f) y
h : ∀ (j : ι), ↑(π f j) x = ↑(π f j) y
j : ι
⊢ ↑(limit.π (wideCospan B X f) (some j)) x = ↑(limit.π (wideCospan B X f) (some j)) y
[PROOFSTEP]
apply h
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : ConcreteCategory C
J : Type w
inst✝⁴ : SmallCategory J
F : J ⥤ C
inst✝³ : PreservesLimit F (forget C)
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h : ∀ (j : ι), ↑(π f j) x = ↑(π f j) y
⊢ x = y
[PROOFSTEP]
apply Concrete.widePullback_ext _ _ _ _ h
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : ConcreteCategory C
J : Type w
inst✝⁴ : SmallCategory J
F : J ⥤ C
inst✝³ : PreservesLimit F (forget C)
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h : ∀ (j : ι), ↑(π f j) x = ↑(π f j) y
⊢ ↑(base f) x = ↑(base f) y
[PROOFSTEP]
inhabit ι
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : ConcreteCategory C
J : Type w
inst✝⁴ : SmallCategory J
F : J ⥤ C
inst✝³ : PreservesLimit F (forget C)
B : C
ι : Type w
inst✝² : Nonempty ι
X : ι → C
f : (j : ι) → X j ⟶ B
inst✝¹ : HasWidePullback B X f
inst✝ : PreservesLimit (wideCospan B X f) (forget C)
x y : (forget C).obj (widePullback B X f)
h : ∀ (j : ι), ↑(π f j) x = ↑(π f j) y
inhabited_h : Inhabited ι
⊢ ↑(base f) x = ↑(base f) y
[PROOFSTEP]
simp only [← π_arrow f default, comp_apply, h]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
I : MulticospanIndex C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit (MulticospanIndex.multicospan I) (forget C)
x y : (forget C).obj (multiequalizer I)
h : ∀ (t : I.L), ↑(Multiequalizer.ι I t) x = ↑(Multiequalizer.ι I t) y
⊢ x = y
[PROOFSTEP]
apply Concrete.limit_ext
[GOAL]
case a
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
I : MulticospanIndex C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit (MulticospanIndex.multicospan I) (forget C)
x y : (forget C).obj (multiequalizer I)
h : ∀ (t : I.L), ↑(Multiequalizer.ι I t) x = ↑(Multiequalizer.ι I t) y
⊢ ∀ (j : WalkingMulticospan I.fstTo I.sndTo),
    ↑(limit.π (MulticospanIndex.multicospan I) j) x = ↑(limit.π (MulticospanIndex.multicospan I) j) y
[PROOFSTEP]
rintro (a | b)
[GOAL]
case a.left
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
I : MulticospanIndex C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit (MulticospanIndex.multicospan I) (forget C)
x y : (forget C).obj (multiequalizer I)
h : ∀ (t : I.L), ↑(Multiequalizer.ι I t) x = ↑(Multiequalizer.ι I t) y
a : I.L
⊢ ↑(limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.left a)) x =
    ↑(limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.left a)) y
[PROOFSTEP]
apply h
[GOAL]
case a.right
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
I : MulticospanIndex C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit (MulticospanIndex.multicospan I) (forget C)
x y : (forget C).obj (multiequalizer I)
h : ∀ (t : I.L), ↑(Multiequalizer.ι I t) x = ↑(Multiequalizer.ι I t) y
b : I.R
⊢ ↑(limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.right b)) x =
    ↑(limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.right b)) y
[PROOFSTEP]
rw [← limit.w I.multicospan (WalkingMulticospan.Hom.fst b), comp_apply, comp_apply]
[GOAL]
case a.right
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
I : MulticospanIndex C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit (MulticospanIndex.multicospan I) (forget C)
x y : (forget C).obj (multiequalizer I)
h : ∀ (t : I.L), ↑(Multiequalizer.ι I t) x = ↑(Multiequalizer.ι I t) y
b : I.R
⊢ ↑((MulticospanIndex.multicospan I).map (WalkingMulticospan.Hom.fst b))
      (↑(limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.left (MulticospanIndex.fstTo I b))) x) =
    ↑((MulticospanIndex.multicospan I).map (WalkingMulticospan.Hom.fst b))
      (↑(limit.π (MulticospanIndex.multicospan I) (WalkingMulticospan.left (MulticospanIndex.fstTo I b))) y)
[PROOFSTEP]
simp [h]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
x : ↑(Functor.sections (MulticospanIndex.multicospan I ⋙ forget C))
i : I.R
⊢ ↑(MulticospanIndex.fst I i) ((fun i => ↑x (WalkingMulticospan.left i)) (MulticospanIndex.fstTo I i)) =
    ↑(MulticospanIndex.snd I i) ((fun i => ↑x (WalkingMulticospan.left i)) (MulticospanIndex.sndTo I i))
[PROOFSTEP]
have a := x.2 (WalkingMulticospan.Hom.fst i)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
x : ↑(Functor.sections (MulticospanIndex.multicospan I ⋙ forget C))
i : I.R
a :
  (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.fst i)
      (↑x (WalkingMulticospan.left (MulticospanIndex.fstTo I i))) =
    ↑x (WalkingMulticospan.right i)
⊢ ↑(MulticospanIndex.fst I i) ((fun i => ↑x (WalkingMulticospan.left i)) (MulticospanIndex.fstTo I i)) =
    ↑(MulticospanIndex.snd I i) ((fun i => ↑x (WalkingMulticospan.left i)) (MulticospanIndex.sndTo I i))
[PROOFSTEP]
have b := x.2 (WalkingMulticospan.Hom.snd i)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
x : ↑(Functor.sections (MulticospanIndex.multicospan I ⋙ forget C))
i : I.R
a :
  (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.fst i)
      (↑x (WalkingMulticospan.left (MulticospanIndex.fstTo I i))) =
    ↑x (WalkingMulticospan.right i)
b :
  (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.snd i)
      (↑x (WalkingMulticospan.left (MulticospanIndex.sndTo I i))) =
    ↑x (WalkingMulticospan.right i)
⊢ ↑(MulticospanIndex.fst I i) ((fun i => ↑x (WalkingMulticospan.left i)) (MulticospanIndex.fstTo I i)) =
    ↑(MulticospanIndex.snd I i) ((fun i => ↑x (WalkingMulticospan.left i)) (MulticospanIndex.sndTo I i))
[PROOFSTEP]
rw [← b] at a
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
x : ↑(Functor.sections (MulticospanIndex.multicospan I ⋙ forget C))
i : I.R
a :
  (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.fst i)
      (↑x (WalkingMulticospan.left (MulticospanIndex.fstTo I i))) =
    (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.snd i)
      (↑x (WalkingMulticospan.left (MulticospanIndex.sndTo I i)))
b :
  (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.snd i)
      (↑x (WalkingMulticospan.left (MulticospanIndex.sndTo I i))) =
    ↑x (WalkingMulticospan.right i)
⊢ ↑(MulticospanIndex.fst I i) ((fun i => ↑x (WalkingMulticospan.left i)) (MulticospanIndex.fstTo I i)) =
    ↑(MulticospanIndex.snd I i) ((fun i => ↑x (WalkingMulticospan.left i)) (MulticospanIndex.sndTo I i))
[PROOFSTEP]
exact a
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
x :
  { x //
    ∀ (i : I.R),
      ↑(MulticospanIndex.fst I i) (x (MulticospanIndex.fstTo I i)) =
        ↑(MulticospanIndex.snd I i) (x (MulticospanIndex.sndTo I i)) }
⊢ (fun j =>
      match j with
      | WalkingMulticospan.left a => ↑x a
      | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b))) ∈
    Functor.sections (MulticospanIndex.multicospan I ⋙ forget C)
[PROOFSTEP]
rintro (a | b) (a' | b') (f | f | f)
[GOAL]
case left.left.id
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
x :
  { x //
    ∀ (i : I.R),
      ↑(MulticospanIndex.fst I i) (x (MulticospanIndex.fstTo I i)) =
        ↑(MulticospanIndex.snd I i) (x (MulticospanIndex.sndTo I i)) }
a : I.L
⊢ (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.id (WalkingMulticospan.left a))
      ((fun j =>
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
        (WalkingMulticospan.left a)) =
    (fun j =>
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
      (WalkingMulticospan.left a)
[PROOFSTEP]
simp
[GOAL]
case left.right.fst
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
x :
  { x //
    ∀ (i : I.R),
      ↑(MulticospanIndex.fst I i) (x (MulticospanIndex.fstTo I i)) =
        ↑(MulticospanIndex.snd I i) (x (MulticospanIndex.sndTo I i)) }
b' : I.R
⊢ (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.fst b')
      ((fun j =>
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
        (WalkingMulticospan.left (MulticospanIndex.fstTo I b'))) =
    (fun j =>
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
      (WalkingMulticospan.right b')
[PROOFSTEP]
rfl
[GOAL]
case left.right.snd
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
x :
  { x //
    ∀ (i : I.R),
      ↑(MulticospanIndex.fst I i) (x (MulticospanIndex.fstTo I i)) =
        ↑(MulticospanIndex.snd I i) (x (MulticospanIndex.sndTo I i)) }
b' : I.R
⊢ (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.snd b')
      ((fun j =>
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
        (WalkingMulticospan.left (MulticospanIndex.sndTo I b'))) =
    (fun j =>
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
      (WalkingMulticospan.right b')
[PROOFSTEP]
dsimp
[GOAL]
case left.right.snd
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
x :
  { x //
    ∀ (i : I.R),
      ↑(MulticospanIndex.fst I i) (x (MulticospanIndex.fstTo I i)) =
        ↑(MulticospanIndex.snd I i) (x (MulticospanIndex.sndTo I i)) }
b' : I.R
⊢ (forget C).map (MulticospanIndex.snd I b') (↑x (MulticospanIndex.sndTo I b')) =
    ↑(MulticospanIndex.fst I b') (↑x (MulticospanIndex.fstTo I b'))
[PROOFSTEP]
exact (x.2 b').symm
[GOAL]
case right.right.id
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
x :
  { x //
    ∀ (i : I.R),
      ↑(MulticospanIndex.fst I i) (x (MulticospanIndex.fstTo I i)) =
        ↑(MulticospanIndex.snd I i) (x (MulticospanIndex.sndTo I i)) }
b : I.R
⊢ (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.id (WalkingMulticospan.right b))
      ((fun j =>
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
        (WalkingMulticospan.right b)) =
    (fun j =>
        match j with
        | WalkingMulticospan.left a => ↑x a
        | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
      (WalkingMulticospan.right b)
[PROOFSTEP]
simp
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
⊢ Function.LeftInverse
    (fun x =>
      {
        val := fun j =>
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)),
        property :=
          (_ :
            ∀ {j j' : WalkingMulticospan I.fstTo I.sndTo} (f : j ⟶ j'),
              (MulticospanIndex.multicospan I ⋙ forget C).map f
                  ((fun j =>
                      match j with
                      | WalkingMulticospan.left a => ↑x a
                      | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
                    j) =
                (fun j =>
                    match j with
                    | WalkingMulticospan.left a => ↑x a
                    | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
                  j') })
    fun x =>
    { val := fun i => ↑x (WalkingMulticospan.left i),
      property :=
        (_ :
          ∀ (i : I.R),
            (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.fst i)
                (↑x (WalkingMulticospan.left (MulticospanIndex.fstTo I i))) =
              (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.snd i)
                (↑x (WalkingMulticospan.left (MulticospanIndex.sndTo I i)))) }
[PROOFSTEP]
intro x
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
x : ↑(Functor.sections (MulticospanIndex.multicospan I ⋙ forget C))
⊢ (fun x =>
        {
          val := fun j =>
            match j with
            | WalkingMulticospan.left a => ↑x a
            | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)),
          property :=
            (_ :
              ∀ {j j' : WalkingMulticospan I.fstTo I.sndTo} (f : j ⟶ j'),
                (MulticospanIndex.multicospan I ⋙ forget C).map f
                    ((fun j =>
                        match j with
                        | WalkingMulticospan.left a => ↑x a
                        | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
                      j) =
                  (fun j =>
                      match j with
                      | WalkingMulticospan.left a => ↑x a
                      | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
                    j') })
      ((fun x =>
          { val := fun i => ↑x (WalkingMulticospan.left i),
            property :=
              (_ :
                ∀ (i : I.R),
                  (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.fst i)
                      (↑x (WalkingMulticospan.left (MulticospanIndex.fstTo I i))) =
                    (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.snd i)
                      (↑x (WalkingMulticospan.left (MulticospanIndex.sndTo I i)))) })
        x) =
    x
[PROOFSTEP]
ext (a | b)
[GOAL]
case a.h.left
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
x : ↑(Functor.sections (MulticospanIndex.multicospan I ⋙ forget C))
a : I.L
⊢ ↑((fun x =>
            {
              val := fun j =>
                match j with
                | WalkingMulticospan.left a => ↑x a
                | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)),
              property :=
                (_ :
                  ∀ {j j' : WalkingMulticospan I.fstTo I.sndTo} (f : j ⟶ j'),
                    (MulticospanIndex.multicospan I ⋙ forget C).map f
                        ((fun j =>
                            match j with
                            | WalkingMulticospan.left a => ↑x a
                            | WalkingMulticospan.right b =>
                              ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
                          j) =
                      (fun j =>
                          match j with
                          | WalkingMulticospan.left a => ↑x a
                          | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
                        j') })
          ((fun x =>
              { val := fun i => ↑x (WalkingMulticospan.left i),
                property :=
                  (_ :
                    ∀ (i : I.R),
                      (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.fst i)
                          (↑x (WalkingMulticospan.left (MulticospanIndex.fstTo I i))) =
                        (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.snd i)
                          (↑x (WalkingMulticospan.left (MulticospanIndex.sndTo I i)))) })
            x))
      (WalkingMulticospan.left a) =
    ↑x (WalkingMulticospan.left a)
[PROOFSTEP]
rfl
[GOAL]
case a.h.right
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
x : ↑(Functor.sections (MulticospanIndex.multicospan I ⋙ forget C))
b : I.R
⊢ ↑((fun x =>
            {
              val := fun j =>
                match j with
                | WalkingMulticospan.left a => ↑x a
                | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)),
              property :=
                (_ :
                  ∀ {j j' : WalkingMulticospan I.fstTo I.sndTo} (f : j ⟶ j'),
                    (MulticospanIndex.multicospan I ⋙ forget C).map f
                        ((fun j =>
                            match j with
                            | WalkingMulticospan.left a => ↑x a
                            | WalkingMulticospan.right b =>
                              ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
                          j) =
                      (fun j =>
                          match j with
                          | WalkingMulticospan.left a => ↑x a
                          | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
                        j') })
          ((fun x =>
              { val := fun i => ↑x (WalkingMulticospan.left i),
                property :=
                  (_ :
                    ∀ (i : I.R),
                      (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.fst i)
                          (↑x (WalkingMulticospan.left (MulticospanIndex.fstTo I i))) =
                        (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.snd i)
                          (↑x (WalkingMulticospan.left (MulticospanIndex.sndTo I i)))) })
            x))
      (WalkingMulticospan.right b) =
    ↑x (WalkingMulticospan.right b)
[PROOFSTEP]
rw [← x.2 (WalkingMulticospan.Hom.fst b)]
[GOAL]
case a.h.right
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
x : ↑(Functor.sections (MulticospanIndex.multicospan I ⋙ forget C))
b : I.R
⊢ ↑((fun x =>
            {
              val := fun j =>
                match j with
                | WalkingMulticospan.left a => ↑x a
                | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)),
              property :=
                (_ :
                  ∀ {j j' : WalkingMulticospan I.fstTo I.sndTo} (f : j ⟶ j'),
                    (MulticospanIndex.multicospan I ⋙ forget C).map f
                        ((fun j =>
                            match j with
                            | WalkingMulticospan.left a => ↑x a
                            | WalkingMulticospan.right b =>
                              ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
                          j) =
                      (fun j =>
                          match j with
                          | WalkingMulticospan.left a => ↑x a
                          | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
                        j') })
          ((fun x =>
              { val := fun i => ↑x (WalkingMulticospan.left i),
                property :=
                  (_ :
                    ∀ (i : I.R),
                      (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.fst i)
                          (↑x (WalkingMulticospan.left (MulticospanIndex.fstTo I i))) =
                        (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.snd i)
                          (↑x (WalkingMulticospan.left (MulticospanIndex.sndTo I i)))) })
            x))
      (WalkingMulticospan.right b) =
    (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.fst b)
      (↑x (WalkingMulticospan.left (MulticospanIndex.fstTo I b)))
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
⊢ Function.RightInverse
    (fun x =>
      {
        val := fun j =>
          match j with
          | WalkingMulticospan.left a => ↑x a
          | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)),
        property :=
          (_ :
            ∀ {j j' : WalkingMulticospan I.fstTo I.sndTo} (f : j ⟶ j'),
              (MulticospanIndex.multicospan I ⋙ forget C).map f
                  ((fun j =>
                      match j with
                      | WalkingMulticospan.left a => ↑x a
                      | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
                    j) =
                (fun j =>
                    match j with
                    | WalkingMulticospan.left a => ↑x a
                    | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
                  j') })
    fun x =>
    { val := fun i => ↑x (WalkingMulticospan.left i),
      property :=
        (_ :
          ∀ (i : I.R),
            (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.fst i)
                (↑x (WalkingMulticospan.left (MulticospanIndex.fstTo I i))) =
              (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.snd i)
                (↑x (WalkingMulticospan.left (MulticospanIndex.sndTo I i)))) }
[PROOFSTEP]
intro x
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
x :
  { x //
    ∀ (i : I.R),
      ↑(MulticospanIndex.fst I i) (x (MulticospanIndex.fstTo I i)) =
        ↑(MulticospanIndex.snd I i) (x (MulticospanIndex.sndTo I i)) }
⊢ (fun x =>
        { val := fun i => ↑x (WalkingMulticospan.left i),
          property :=
            (_ :
              ∀ (i : I.R),
                (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.fst i)
                    (↑x (WalkingMulticospan.left (MulticospanIndex.fstTo I i))) =
                  (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.snd i)
                    (↑x (WalkingMulticospan.left (MulticospanIndex.sndTo I i)))) })
      ((fun x =>
          {
            val := fun j =>
              match j with
              | WalkingMulticospan.left a => ↑x a
              | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)),
            property :=
              (_ :
                ∀ {j j' : WalkingMulticospan I.fstTo I.sndTo} (f : j ⟶ j'),
                  (MulticospanIndex.multicospan I ⋙ forget C).map f
                      ((fun j =>
                          match j with
                          | WalkingMulticospan.left a => ↑x a
                          | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
                        j) =
                    (fun j =>
                        match j with
                        | WalkingMulticospan.left a => ↑x a
                        | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
                      j') })
        x) =
    x
[PROOFSTEP]
ext i
[GOAL]
case a.h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type w
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesLimit F (forget C)
I : MulticospanIndex C
x :
  { x //
    ∀ (i : I.R),
      ↑(MulticospanIndex.fst I i) (x (MulticospanIndex.fstTo I i)) =
        ↑(MulticospanIndex.snd I i) (x (MulticospanIndex.sndTo I i)) }
i : I.L
⊢ ↑((fun x =>
            { val := fun i => ↑x (WalkingMulticospan.left i),
              property :=
                (_ :
                  ∀ (i : I.R),
                    (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.fst i)
                        (↑x (WalkingMulticospan.left (MulticospanIndex.fstTo I i))) =
                      (MulticospanIndex.multicospan I ⋙ forget C).map (WalkingMulticospan.Hom.snd i)
                        (↑x (WalkingMulticospan.left (MulticospanIndex.sndTo I i)))) })
          ((fun x =>
              {
                val := fun j =>
                  match j with
                  | WalkingMulticospan.left a => ↑x a
                  | WalkingMulticospan.right b => ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)),
                property :=
                  (_ :
                    ∀ {j j' : WalkingMulticospan I.fstTo I.sndTo} (f : j ⟶ j'),
                      (MulticospanIndex.multicospan I ⋙ forget C).map f
                          ((fun j =>
                              match j with
                              | WalkingMulticospan.left a => ↑x a
                              | WalkingMulticospan.right b =>
                                ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
                            j) =
                        (fun j =>
                            match j with
                            | WalkingMulticospan.left a => ↑x a
                            | WalkingMulticospan.right b =>
                              ↑(MulticospanIndex.fst I b) (↑x (MulticospanIndex.fstTo I b)))
                          j') })
            x))
      i =
    ↑x i
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
I : MulticospanIndex C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit (MulticospanIndex.multicospan I) (forget C)
⊢ (forget C).obj (multiequalizer I) ≃
    { x //
      ∀ (i : I.R),
        ↑(MulticospanIndex.fst I i) (x (MulticospanIndex.fstTo I i)) =
          ↑(MulticospanIndex.snd I i) (x (MulticospanIndex.sndTo I i)) }
[PROOFSTEP]
let h1 := limit.isLimit I.multicospan
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
I : MulticospanIndex C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit (MulticospanIndex.multicospan I) (forget C)
h1 : IsLimit (limit.cone (MulticospanIndex.multicospan I)) := limit.isLimit (MulticospanIndex.multicospan I)
⊢ (forget C).obj (multiequalizer I) ≃
    { x //
      ∀ (i : I.R),
        ↑(MulticospanIndex.fst I i) (x (MulticospanIndex.fstTo I i)) =
          ↑(MulticospanIndex.snd I i) (x (MulticospanIndex.sndTo I i)) }
[PROOFSTEP]
let h2 := isLimitOfPreserves (forget C) h1
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
I : MulticospanIndex C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit (MulticospanIndex.multicospan I) (forget C)
h1 : IsLimit (limit.cone (MulticospanIndex.multicospan I)) := limit.isLimit (MulticospanIndex.multicospan I)
h2 : IsLimit ((forget C).mapCone (limit.cone (MulticospanIndex.multicospan I))) := isLimitOfPreserves (forget C) h1
⊢ (forget C).obj (multiequalizer I) ≃
    { x //
      ∀ (i : I.R),
        ↑(MulticospanIndex.fst I i) (x (MulticospanIndex.fstTo I i)) =
          ↑(MulticospanIndex.snd I i) (x (MulticospanIndex.sndTo I i)) }
[PROOFSTEP]
let E := h2.conePointUniqueUpToIso (Types.limitConeIsLimit.{w, v} _)
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type w
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesLimit F (forget C)
I : MulticospanIndex C
inst✝¹ : HasMultiequalizer I
inst✝ : PreservesLimit (MulticospanIndex.multicospan I) (forget C)
h1 : IsLimit (limit.cone (MulticospanIndex.multicospan I)) := limit.isLimit (MulticospanIndex.multicospan I)
h2 : IsLimit ((forget C).mapCone (limit.cone (MulticospanIndex.multicospan I))) := isLimitOfPreserves (forget C) h1
E : ((forget C).mapCone (limit.cone (MulticospanIndex.multicospan I))).pt ≅
  (Types.limitCone (MulticospanIndex.multicospan I ⋙ forget C)).pt :=
  IsLimit.conePointUniqueUpToIso h2 (Types.limitConeIsLimit (MulticospanIndex.multicospan I ⋙ forget C))
⊢ (forget C).obj (multiequalizer I) ≃
    { x //
      ∀ (i : I.R),
        ↑(MulticospanIndex.fst I i) (x (MulticospanIndex.fstTo I i)) =
          ↑(MulticospanIndex.snd I i) (x (MulticospanIndex.sndTo I i)) }
[PROOFSTEP]
exact Equiv.trans E.toEquiv (Concrete.multiequalizerEquivAux.{w, v} I)
[GOAL]
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : ConcreteCategory C
M N K : C
f : M ⟶ N
inst✝ : HasCokernel f
g h : cokernel f ⟶ K
w : ∀ (n : (forget C).obj N), ↑g (↑(cokernel.π f) n) = ↑h (↑(cokernel.π f) n)
⊢ g = h
[PROOFSTEP]
ext x
[GOAL]
case h.w
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
inst✝¹ : ConcreteCategory C
M N K : C
f : M ⟶ N
inst✝ : HasCokernel f
g h : cokernel f ⟶ K
w : ∀ (n : (forget C).obj N), ↑g (↑(cokernel.π f) n) = ↑h (↑(cokernel.π f) n)
x : (forget C).obj N
⊢ ↑(coequalizer.π f 0 ≫ g) x = ↑(coequalizer.π f 0 ≫ h) x
[PROOFSTEP]
simpa using w x
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
⊢ let ff := fun a => ↑(NatTrans.app D.ι a.fst) a.snd;
  Function.Surjective ff
[PROOFSTEP]
intro ff
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
⊢ Function.Surjective ff
[PROOFSTEP]
let E := (forget C).mapCocone D
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
⊢ Function.Surjective ff
[PROOFSTEP]
let hE : IsColimit E := isColimitOfPreserves _ hD
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
⊢ Function.Surjective ff
[PROOFSTEP]
let G := Types.colimitCocone.{v, v} (F ⋙ forget C)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
⊢ Function.Surjective ff
[PROOFSTEP]
let hG := Types.colimitCoconeIsColimit.{v, v} (F ⋙ forget C)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
⊢ Function.Surjective ff
[PROOFSTEP]
let T : E ≅ G := hE.uniqueUpToIso hG
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
⊢ Function.Surjective ff
[PROOFSTEP]
let TX : E.pt ≅ G.pt := (Cocones.forget _).mapIso T
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ Function.Surjective ff
[PROOFSTEP]
suffices Function.Surjective (TX.hom ∘ ff) by
  intro a
  obtain ⟨b, hb⟩ := this (TX.hom a)
  refine'
    ⟨b, _⟩
      -- porting note: `apply_fun TX.inv at hb` does not work here
  replace hb := congr_arg TX.inv hb
  change (TX.hom ≫ TX.inv) (ff b) = (TX.hom ≫ TX.inv) _ at hb
  simpa only [TX.hom_inv_id] using hb
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
this : Function.Surjective (TX.hom ∘ ff)
⊢ Function.Surjective ff
[PROOFSTEP]
intro a
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
this : Function.Surjective (TX.hom ∘ ff)
a : (forget C).obj D.pt
⊢ ∃ a_1, ff a_1 = a
[PROOFSTEP]
obtain ⟨b, hb⟩ := this (TX.hom a)
[GOAL]
case intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
this : Function.Surjective (TX.hom ∘ ff)
a : (forget C).obj D.pt
b : (j : J) × (forget C).obj (F.obj j)
hb : (TX.hom ∘ ff) b = TX.hom a
⊢ ∃ a_1, ff a_1 = a
[PROOFSTEP]
refine'
  ⟨b, _⟩
    -- porting note: `apply_fun TX.inv at hb` does not work here
[GOAL]
case intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
this : Function.Surjective (TX.hom ∘ ff)
a : (forget C).obj D.pt
b : (j : J) × (forget C).obj (F.obj j)
hb : (TX.hom ∘ ff) b = TX.hom a
⊢ ff b = a
[PROOFSTEP]
replace hb := congr_arg TX.inv hb
[GOAL]
case intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
this : Function.Surjective (TX.hom ∘ ff)
a : (forget C).obj D.pt
b : (j : J) × (forget C).obj (F.obj j)
hb : TX.inv ((TX.hom ∘ ff) b) = TX.inv (TX.hom a)
⊢ ff b = a
[PROOFSTEP]
change (TX.hom ≫ TX.inv) (ff b) = (TX.hom ≫ TX.inv) _ at hb
[GOAL]
case intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
this : Function.Surjective (TX.hom ∘ ff)
a : (forget C).obj D.pt
b : (j : J) × (forget C).obj (F.obj j)
hb : (TX.hom ≫ TX.inv) (ff b) = (TX.hom ≫ TX.inv) a
⊢ ff b = a
[PROOFSTEP]
simpa only [TX.hom_inv_id] using hb
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ Function.Surjective (TX.hom ∘ ff)
[PROOFSTEP]
have : TX.hom ∘ ff = fun a => G.ι.app a.1 a.2 := by
  ext a
  change (E.ι.app a.1 ≫ hE.desc G) a.2 = _
  rw [hE.fac]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ TX.hom ∘ ff = fun a => NatTrans.app G.ι a.fst a.snd
[PROOFSTEP]
ext a
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
a : (j : J) × (forget C).obj (F.obj j)
⊢ (TX.hom ∘ ff) a = NatTrans.app G.ι a.fst a.snd
[PROOFSTEP]
change (E.ι.app a.1 ≫ hE.desc G) a.2 = _
[GOAL]
case h
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
a : (j : J) × (forget C).obj (F.obj j)
⊢ (NatTrans.app E.ι a.fst ≫ IsColimit.desc hE G) a.snd = NatTrans.app G.ι a.fst a.snd
[PROOFSTEP]
rw [hE.fac]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
this : TX.hom ∘ ff = fun a => NatTrans.app G.ι a.fst a.snd
⊢ Function.Surjective (TX.hom ∘ ff)
[PROOFSTEP]
rw [this]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
this : TX.hom ∘ ff = fun a => NatTrans.app G.ι a.fst a.snd
⊢ Function.Surjective fun a => NatTrans.app G.ι a.fst a.snd
[PROOFSTEP]
rintro ⟨⟨j, a⟩⟩
[GOAL]
case mk.mk
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
ff : (j : J) × (forget C).obj (F.obj j) → (forget C).obj D.pt := fun a => ↑(NatTrans.app D.ι a.fst) a.snd
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
this : TX.hom ∘ ff = fun a => NatTrans.app G.ι a.fst a.snd
b✝ : G.pt
j : J
a : (F ⋙ forget C).obj j
⊢ ∃ a_1, (fun a => NatTrans.app G.ι a.fst a.snd) a_1 = Quot.mk (Types.Quot.Rel (F ⋙ forget C)) { fst := j, snd := a }
[PROOFSTEP]
exact ⟨⟨j, a⟩, rfl⟩
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
x : (forget C).obj D.pt
⊢ ∃ j y, ↑(NatTrans.app D.ι j) y = x
[PROOFSTEP]
obtain ⟨a, rfl⟩ := Concrete.from_union_surjective_of_isColimit F hD x
[GOAL]
case intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
hD : IsColimit D
a : (j : J) × (forget C).obj (F.obj j)
⊢ ∃ j y, ↑(NatTrans.app D.ι j) y = (fun a => ↑(NatTrans.app D.ι a.fst) a.snd) a
[PROOFSTEP]
exact ⟨a.1, a.2, rfl⟩
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
⊢ ↑(NatTrans.app D.ι i) x = ↑(NatTrans.app D.ι j) y
[PROOFSTEP]
let E := (forget C).mapCocone D
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
⊢ ↑(NatTrans.app D.ι i) x = ↑(NatTrans.app D.ι j) y
[PROOFSTEP]
let hE : IsColimit E := isColimitOfPreserves _ hD
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
⊢ ↑(NatTrans.app D.ι i) x = ↑(NatTrans.app D.ι j) y
[PROOFSTEP]
let G := Types.colimitCocone.{v, v} (F ⋙ forget C)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
⊢ ↑(NatTrans.app D.ι i) x = ↑(NatTrans.app D.ι j) y
[PROOFSTEP]
let hG := Types.colimitCoconeIsColimit.{v, v} (F ⋙ forget C)
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
⊢ ↑(NatTrans.app D.ι i) x = ↑(NatTrans.app D.ι j) y
[PROOFSTEP]
let T : E ≅ G := hE.uniqueUpToIso hG
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
⊢ ↑(NatTrans.app D.ι i) x = ↑(NatTrans.app D.ι j) y
[PROOFSTEP]
let TX : E.pt ≅ G.pt := (Cocones.forget _).mapIso T
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ ↑(NatTrans.app D.ι i) x = ↑(NatTrans.app D.ι j) y
[PROOFSTEP]
apply
  (show Function.Bijective TX.hom by
      rw [← isIso_iff_bijective]
      apply IsIso.of_iso).1
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ Function.Bijective TX.hom
[PROOFSTEP]
rw [← isIso_iff_bijective]
[GOAL]
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ IsIso TX.hom
[PROOFSTEP]
apply IsIso.of_iso
[GOAL]
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ TX.hom (↑(NatTrans.app D.ι i) x) = TX.hom (↑(NatTrans.app D.ι j) y)
[PROOFSTEP]
change (E.ι.app i ≫ TX.hom) x = (E.ι.app j ≫ TX.hom) y
[GOAL]
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ (NatTrans.app E.ι i ≫ TX.hom) x = (NatTrans.app E.ι j ≫ TX.hom) y
[PROOFSTEP]
erw [T.hom.w, T.hom.w]
[GOAL]
case a
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ NatTrans.app G.ι i x = NatTrans.app G.ι j y
[PROOFSTEP]
obtain ⟨k, f, g, h⟩ := h
[GOAL]
case a.intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
k : J
f : i ⟶ k
g : j ⟶ k
h : ↑(F.map f) x = ↑(F.map g) y
⊢ NatTrans.app G.ι i x = NatTrans.app G.ι j y
[PROOFSTEP]
have : G.ι.app i x = (G.ι.app k (F.map f x) : G.pt) := Quot.sound ⟨f, rfl⟩
[GOAL]
case a.intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
k : J
f : i ⟶ k
g : j ⟶ k
h : ↑(F.map f) x = ↑(F.map g) y
this : NatTrans.app G.ι i x = NatTrans.app G.ι k (↑(F.map f) x)
⊢ NatTrans.app G.ι i x = NatTrans.app G.ι j y
[PROOFSTEP]
rw [this, h]
[GOAL]
case a.intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
k : J
f : i ⟶ k
g : j ⟶ k
h : ↑(F.map f) x = ↑(F.map g) y
this : NatTrans.app G.ι i x = NatTrans.app G.ι k (↑(F.map f) x)
⊢ NatTrans.app G.ι k (↑(F.map g) y) = NatTrans.app G.ι j y
[PROOFSTEP]
symm
[GOAL]
case a.intro.intro.intro
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ConcreteCategory C
J : Type v
inst✝¹ : SmallCategory J
F : J ⥤ C
inst✝ : PreservesColimit F (forget C)
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
k : J
f : i ⟶ k
g : j ⟶ k
h : ↑(F.map f) x = ↑(F.map g) y
this : NatTrans.app G.ι i x = NatTrans.app G.ι k (↑(F.map f) x)
⊢ NatTrans.app G.ι j y = NatTrans.app G.ι k (↑(F.map g) y)
[PROOFSTEP]
exact Quot.sound ⟨g, rfl⟩
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ↑(NatTrans.app D.ι i) x = ↑(NatTrans.app D.ι j) y
⊢ ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
[PROOFSTEP]
let E := (forget C).mapCocone D
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ↑(NatTrans.app D.ι i) x = ↑(NatTrans.app D.ι j) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
⊢ ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
[PROOFSTEP]
let hE : IsColimit E := isColimitOfPreserves _ hD
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ↑(NatTrans.app D.ι i) x = ↑(NatTrans.app D.ι j) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
⊢ ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
[PROOFSTEP]
let G := Types.colimitCocone.{v, v} (F ⋙ forget C)
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ↑(NatTrans.app D.ι i) x = ↑(NatTrans.app D.ι j) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
⊢ ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
[PROOFSTEP]
let hG := Types.colimitCoconeIsColimit.{v, v} (F ⋙ forget C)
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ↑(NatTrans.app D.ι i) x = ↑(NatTrans.app D.ι j) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
⊢ ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
[PROOFSTEP]
let T : E ≅ G := hE.uniqueUpToIso hG
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ↑(NatTrans.app D.ι i) x = ↑(NatTrans.app D.ι j) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
⊢ ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
[PROOFSTEP]
let TX : E.pt ≅ G.pt := (Cocones.forget _).mapIso T
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
h : ↑(NatTrans.app D.ι i) x = ↑(NatTrans.app D.ι j) y
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
⊢ ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
[PROOFSTEP]
replace h := congr_arg TX.hom h
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : TX.hom (↑(NatTrans.app D.ι i) x) = TX.hom (↑(NatTrans.app D.ι j) y)
⊢ ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
[PROOFSTEP]
change (E.ι.app i ≫ TX.hom) x = (E.ι.app j ≫ TX.hom) y at h
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : (NatTrans.app E.ι i ≫ TX.hom) x = (NatTrans.app E.ι j ≫ TX.hom) y
⊢ ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
[PROOFSTEP]
erw [T.hom.w, T.hom.w] at h
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : NatTrans.app G.ι i x = NatTrans.app G.ι j y
⊢ ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
[PROOFSTEP]
replace h := Quot.exact _ h
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
⊢ ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
[PROOFSTEP]
suffices
  ∀ (a b : Σ j, F.obj j) (_ : EqvGen (Limits.Types.Quot.Rel.{v, v} (F ⋙ forget C)) a b),
    ∃ (k : _) (f : a.1 ⟶ k) (g : b.1 ⟶ k), F.map f a.2 = F.map g b.2
  by exact this ⟨i, x⟩ ⟨j, y⟩ h
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
this :
  ∀ (a b : (j : J) × (forget C).obj (F.obj j)),
    EqvGen (Types.Quot.Rel (F ⋙ forget C)) a b → ∃ k f g, ↑(F.map f) a.snd = ↑(F.map g) b.snd
⊢ ∃ k f g, ↑(F.map f) x = ↑(F.map g) y
[PROOFSTEP]
exact this ⟨i, x⟩ ⟨j, y⟩ h
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
⊢ ∀ (a b : (j : J) × (forget C).obj (F.obj j)),
    EqvGen (Types.Quot.Rel (F ⋙ forget C)) a b → ∃ k f g, ↑(F.map f) a.snd = ↑(F.map g) b.snd
[PROOFSTEP]
intro a b h
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b : (j : J) × (forget C).obj (F.obj j)
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) a b
⊢ ∃ k f g, ↑(F.map f) a.snd = ↑(F.map g) b.snd
[PROOFSTEP]
induction h
[GOAL]
case rel
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ : (j : J) × (forget C).obj (F.obj j)
a✝ : Types.Quot.Rel (F ⋙ forget C) x✝ y✝
⊢ ∃ k f g, ↑(F.map f) x✝.snd = ↑(F.map g) y✝.snd
case refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ : (j : J) × (forget C).obj (F.obj j)
⊢ ∃ k f g, ↑(F.map f) x✝.snd = ↑(F.map g) x✝.snd
case symm
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ : (j : J) × (forget C).obj (F.obj j)
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a_ih✝ : ∃ k f g, ↑(F.map f) x✝.snd = ↑(F.map g) y✝.snd
⊢ ∃ k f g, ↑(F.map f) y✝.snd = ↑(F.map g) x✝.snd
case trans
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ z✝ : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y✝ z✝
a_ih✝¹ : ∃ k f g, ↑(F.map f) x✝.snd = ↑(F.map g) y✝.snd
a_ih✝ : ∃ k f g, ↑(F.map f) y✝.snd = ↑(F.map g) z✝.snd
⊢ ∃ k f g, ↑(F.map f) x✝.snd = ↑(F.map g) z✝.snd
[PROOFSTEP]
case rel x y hh =>
  obtain ⟨e, he⟩ := hh
  use y.1, e, 𝟙 _
  simpa using he.symm
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y : (j : J) × (forget C).obj (F.obj j)
hh : Types.Quot.Rel (F ⋙ forget C) x y
⊢ ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) y.snd
[PROOFSTEP]
case rel x y hh =>
  obtain ⟨e, he⟩ := hh
  use y.1, e, 𝟙 _
  simpa using he.symm
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y : (j : J) × (forget C).obj (F.obj j)
hh : Types.Quot.Rel (F ⋙ forget C) x y
⊢ ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) y.snd
[PROOFSTEP]
obtain ⟨e, he⟩ := hh
[GOAL]
case intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y : (j : J) × (forget C).obj (F.obj j)
e : x.fst ⟶ y.fst
he : y.snd = (F ⋙ forget C).map e x.snd
⊢ ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) y.snd
[PROOFSTEP]
use y.1, e, 𝟙 _
[GOAL]
case h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y : (j : J) × (forget C).obj (F.obj j)
e : x.fst ⟶ y.fst
he : y.snd = (F ⋙ forget C).map e x.snd
⊢ ↑(F.map e) x.snd = ↑(F.map (𝟙 y.fst)) y.snd
[PROOFSTEP]
simpa using he.symm
[GOAL]
case refl
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ : (j : J) × (forget C).obj (F.obj j)
⊢ ∃ k f g, ↑(F.map f) x✝.snd = ↑(F.map g) x✝.snd
case symm
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ : (j : J) × (forget C).obj (F.obj j)
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a_ih✝ : ∃ k f g, ↑(F.map f) x✝.snd = ↑(F.map g) y✝.snd
⊢ ∃ k f g, ↑(F.map f) y✝.snd = ↑(F.map g) x✝.snd
case trans
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ z✝ : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y✝ z✝
a_ih✝¹ : ∃ k f g, ↑(F.map f) x✝.snd = ↑(F.map g) y✝.snd
a_ih✝ : ∃ k f g, ↑(F.map f) y✝.snd = ↑(F.map g) z✝.snd
⊢ ∃ k f g, ↑(F.map f) x✝.snd = ↑(F.map g) z✝.snd
[PROOFSTEP]
case refl x => exact ⟨x.1, 𝟙 _, 𝟙 _, rfl⟩
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y }
a b x : (j : J) × (forget C).obj (F.obj j)
⊢ ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) x.snd
[PROOFSTEP]
case refl x => exact ⟨x.1, 𝟙 _, 𝟙 _, rfl⟩
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y }
a b x : (j : J) × (forget C).obj (F.obj j)
⊢ ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) x.snd
[PROOFSTEP]
exact ⟨x.1, 𝟙 _, 𝟙 _, rfl⟩
[GOAL]
case symm
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ : (j : J) × (forget C).obj (F.obj j)
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a_ih✝ : ∃ k f g, ↑(F.map f) x✝.snd = ↑(F.map g) y✝.snd
⊢ ∃ k f g, ↑(F.map f) y✝.snd = ↑(F.map g) x✝.snd
case trans
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ z✝ : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y✝ z✝
a_ih✝¹ : ∃ k f g, ↑(F.map f) x✝.snd = ↑(F.map g) y✝.snd
a_ih✝ : ∃ k f g, ↑(F.map f) y✝.snd = ↑(F.map g) z✝.snd
⊢ ∃ k f g, ↑(F.map f) x✝.snd = ↑(F.map g) z✝.snd
[PROOFSTEP]
case symm x y _ hh =>
  obtain ⟨k, f, g, hh⟩ := hh
  exact ⟨k, g, f, hh.symm⟩
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y : (j : J) × (forget C).obj (F.obj j)
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
hh : ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) y.snd
⊢ ∃ k f g, ↑(F.map f) y.snd = ↑(F.map g) x.snd
[PROOFSTEP]
case symm x y _ hh =>
  obtain ⟨k, f, g, hh⟩ := hh
  exact ⟨k, g, f, hh.symm⟩
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y : (j : J) × (forget C).obj (F.obj j)
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
hh : ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) y.snd
⊢ ∃ k f g, ↑(F.map f) y.snd = ↑(F.map g) x.snd
[PROOFSTEP]
obtain ⟨k, f, g, hh⟩ := hh
[GOAL]
case intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y : (j : J) × (forget C).obj (F.obj j)
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
k : J
f : x.fst ⟶ k
g : y.fst ⟶ k
hh : ↑(F.map f) x.snd = ↑(F.map g) y.snd
⊢ ∃ k f g, ↑(F.map f) y.snd = ↑(F.map g) x.snd
[PROOFSTEP]
exact ⟨k, g, f, hh.symm⟩
[GOAL]
case trans
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x : (forget C).obj (F.obj i)
y : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x } { fst := j, snd := y }
a b x✝ y✝ z✝ : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x✝ y✝
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y✝ z✝
a_ih✝¹ : ∃ k f g, ↑(F.map f) x✝.snd = ↑(F.map g) y✝.snd
a_ih✝ : ∃ k f g, ↑(F.map f) y✝.snd = ↑(F.map g) z✝.snd
⊢ ∃ k f g, ↑(F.map f) x✝.snd = ↑(F.map g) z✝.snd
[PROOFSTEP]
case trans x y z _ _ hh1 hh2 =>
  obtain ⟨k1, f1, g1, h1⟩ := hh1
  obtain ⟨k2, f2, g2, h2⟩ := hh2
  let k0 : J := IsFiltered.max k1 k2
  let e1 : k1 ⟶ k0 := IsFiltered.leftToMax _ _
  let e2 : k2 ⟶ k0 := IsFiltered.rightToMax _ _
  let k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
  let e : k0 ⟶ k := IsFiltered.coeqHom _ _
  use k, f1 ≫ e1 ≫ e, g2 ≫ e2 ≫ e
  simp only [F.map_comp, comp_apply, h1, ← h2]
  simp only [← comp_apply, ← F.map_comp]
  rw [IsFiltered.coeq_condition]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
hh1 : ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) y.snd
hh2 : ∃ k f g, ↑(F.map f) y.snd = ↑(F.map g) z.snd
⊢ ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) z.snd
[PROOFSTEP]
case trans x y z _ _ hh1 hh2 =>
  obtain ⟨k1, f1, g1, h1⟩ := hh1
  obtain ⟨k2, f2, g2, h2⟩ := hh2
  let k0 : J := IsFiltered.max k1 k2
  let e1 : k1 ⟶ k0 := IsFiltered.leftToMax _ _
  let e2 : k2 ⟶ k0 := IsFiltered.rightToMax _ _
  let k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
  let e : k0 ⟶ k := IsFiltered.coeqHom _ _
  use k, f1 ≫ e1 ≫ e, g2 ≫ e2 ≫ e
  simp only [F.map_comp, comp_apply, h1, ← h2]
  simp only [← comp_apply, ← F.map_comp]
  rw [IsFiltered.coeq_condition]
[GOAL]
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
hh1 : ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) y.snd
hh2 : ∃ k f g, ↑(F.map f) y.snd = ↑(F.map g) z.snd
⊢ ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) z.snd
[PROOFSTEP]
obtain ⟨k1, f1, g1, h1⟩ := hh1
[GOAL]
case intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
hh2 : ∃ k f g, ↑(F.map f) y.snd = ↑(F.map g) z.snd
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : ↑(F.map f1) x.snd = ↑(F.map g1) y.snd
⊢ ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) z.snd
[PROOFSTEP]
obtain ⟨k2, f2, g2, h2⟩ := hh2
[GOAL]
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : ↑(F.map f1) x.snd = ↑(F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : ↑(F.map f2) y.snd = ↑(F.map g2) z.snd
⊢ ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) z.snd
[PROOFSTEP]
let k0 : J := IsFiltered.max k1 k2
[GOAL]
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : ↑(F.map f1) x.snd = ↑(F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : ↑(F.map f2) y.snd = ↑(F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
⊢ ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) z.snd
[PROOFSTEP]
let e1 : k1 ⟶ k0 := IsFiltered.leftToMax _ _
[GOAL]
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : ↑(F.map f1) x.snd = ↑(F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : ↑(F.map f2) y.snd = ↑(F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
⊢ ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) z.snd
[PROOFSTEP]
let e2 : k2 ⟶ k0 := IsFiltered.rightToMax _ _
[GOAL]
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : ↑(F.map f1) x.snd = ↑(F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : ↑(F.map f2) y.snd = ↑(F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
⊢ ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) z.snd
[PROOFSTEP]
let k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
[GOAL]
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : ↑(F.map f1) x.snd = ↑(F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : ↑(F.map f2) y.snd = ↑(F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
⊢ ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) z.snd
[PROOFSTEP]
let e : k0 ⟶ k := IsFiltered.coeqHom _ _
[GOAL]
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : ↑(F.map f1) x.snd = ↑(F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : ↑(F.map f2) y.snd = ↑(F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
e : k0 ⟶ k := IsFiltered.coeqHom (g1 ≫ e1) (f2 ≫ e2)
⊢ ∃ k f g, ↑(F.map f) x.snd = ↑(F.map g) z.snd
[PROOFSTEP]
use k, f1 ≫ e1 ≫ e, g2 ≫ e2 ≫ e
[GOAL]
case h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : ↑(F.map f1) x.snd = ↑(F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : ↑(F.map f2) y.snd = ↑(F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
e : k0 ⟶ k := IsFiltered.coeqHom (g1 ≫ e1) (f2 ≫ e2)
⊢ ↑(F.map (f1 ≫ e1 ≫ e)) x.snd = ↑(F.map (g2 ≫ e2 ≫ e)) z.snd
[PROOFSTEP]
simp only [F.map_comp, comp_apply, h1, ← h2]
[GOAL]
case h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : ↑(F.map f1) x.snd = ↑(F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : ↑(F.map f2) y.snd = ↑(F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
e : k0 ⟶ k := IsFiltered.coeqHom (g1 ≫ e1) (f2 ≫ e2)
⊢ ↑(F.map (IsFiltered.coeqHom (g1 ≫ IsFiltered.leftToMax k1 k2) (f2 ≫ IsFiltered.rightToMax k1 k2)))
      (↑(F.map (IsFiltered.leftToMax k1 k2)) (↑(F.map g1) y.snd)) =
    ↑(F.map (IsFiltered.coeqHom (g1 ≫ IsFiltered.leftToMax k1 k2) (f2 ≫ IsFiltered.rightToMax k1 k2)))
      (↑(F.map (IsFiltered.rightToMax k1 k2)) (↑(F.map f2) y.snd))
[PROOFSTEP]
simp only [← comp_apply, ← F.map_comp]
[GOAL]
case h
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : ConcreteCategory C
J : Type v
inst✝² : SmallCategory J
F : J ⥤ C
inst✝¹ : PreservesColimit F (forget C)
inst✝ : IsFiltered J
D : Cocone F
i j : J
hD : IsColimit D
x✝ : (forget C).obj (F.obj i)
y✝ : (forget C).obj (F.obj j)
E : Cocone (F ⋙ forget C) := (forget C).mapCocone D
hE : IsColimit E := isColimitOfPreserves (forget C) hD
G : Cocone (F ⋙ forget C) := Types.colimitCocone (F ⋙ forget C)
hG : IsColimit (Types.colimitCocone (F ⋙ forget C)) := Types.colimitCoconeIsColimit (F ⋙ forget C)
T : E ≅ G := IsColimit.uniqueUpToIso hE hG
TX : E.pt ≅ G.pt := (Cocones.forget (F ⋙ forget C)).mapIso T
h : EqvGen (Types.Quot.Rel (F ⋙ forget C)) { fst := i, snd := x✝ } { fst := j, snd := y✝ }
a b x y z : (j : J) × (forget C).obj (F.obj j)
a✝¹ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) x y
a✝ : EqvGen (Types.Quot.Rel (F ⋙ forget C)) y z
k1 : J
f1 : x.fst ⟶ k1
g1 : y.fst ⟶ k1
h1 : ↑(F.map f1) x.snd = ↑(F.map g1) y.snd
k2 : J
f2 : y.fst ⟶ k2
g2 : z.fst ⟶ k2
h2 : ↑(F.map f2) y.snd = ↑(F.map g2) z.snd
k0 : J := IsFiltered.max k1 k2
e1 : k1 ⟶ k0 := IsFiltered.leftToMax k1 k2
e2 : k2 ⟶ k0 := IsFiltered.rightToMax k1 k2
k : J := IsFiltered.coeq (g1 ≫ e1) (f2 ≫ e2)
e : k0 ⟶ k := IsFiltered.coeqHom (g1 ≫ e1) (f2 ≫ e2)
⊢ ↑(F.map
          ((g1 ≫ IsFiltered.leftToMax k1 k2) ≫
            IsFiltered.coeqHom (g1 ≫ IsFiltered.leftToMax k1 k2) (f2 ≫ IsFiltered.rightToMax k1 k2)))
      y.snd =
    ↑(F.map
          ((f2 ≫ IsFiltered.rightToMax k1 k2) ≫
            IsFiltered.coeqHom (g1 ≫ IsFiltered.leftToMax k1 k2) (f2 ≫ IsFiltered.rightToMax k1 k2)))
      y.snd
[PROOFSTEP]
rw [IsFiltered.coeq_condition]
[GOAL]
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type v
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesColimit F (forget C)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
x : (forget C).obj (widePushout B X f)
⊢ (∃ y, ↑(head f) y = x) ∨ ∃ i y, ↑(ι f i) y = x
[PROOFSTEP]
obtain ⟨_ | j, y, rfl⟩ := Concrete.colimit_exists_rep _ x
[GOAL]
case intro.none.intro
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type v
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesColimit F (forget C)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : (forget C).obj ((wideSpan B X f).obj none)
⊢ (∃ y_1, ↑(head f) y_1 = ↑(colimit.ι (wideSpan B X f) none) y) ∨
    ∃ i y_1, ↑(ι f i) y_1 = ↑(colimit.ι (wideSpan B X f) none) y
[PROOFSTEP]
left
[GOAL]
case intro.none.intro.h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type v
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesColimit F (forget C)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : (forget C).obj ((wideSpan B X f).obj none)
⊢ ∃ y_1, ↑(head f) y_1 = ↑(colimit.ι (wideSpan B X f) none) y
[PROOFSTEP]
use y
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type v
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesColimit F (forget C)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : (forget C).obj ((wideSpan B X f).obj none)
⊢ ↑(head f) y = ↑(colimit.ι (wideSpan B X f) none) y
[PROOFSTEP]
rfl
[GOAL]
case intro.some.intro
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type v
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesColimit F (forget C)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : (forget C).obj ((wideSpan B X f).obj (some j))
⊢ (∃ y_1, ↑(head f) y_1 = ↑(colimit.ι (wideSpan B X f) (some j)) y) ∨
    ∃ i y_1, ↑(ι f i) y_1 = ↑(colimit.ι (wideSpan B X f) (some j)) y
[PROOFSTEP]
right
[GOAL]
case intro.some.intro.h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type v
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesColimit F (forget C)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : (forget C).obj ((wideSpan B X f).obj (some j))
⊢ ∃ i y_1, ↑(ι f i) y_1 = ↑(colimit.ι (wideSpan B X f) (some j)) y
[PROOFSTEP]
use j, y
[GOAL]
case h
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : ConcreteCategory C
J : Type v
inst✝³ : SmallCategory J
F : J ⥤ C
inst✝² : PreservesColimit F (forget C)
B : C
α : Type v
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
j : α
y : (forget C).obj ((wideSpan B X f).obj (some j))
⊢ ↑(ι f j) y = ↑(colimit.ι (wideSpan B X f) (some j)) y
[PROOFSTEP]
rfl
[GOAL]
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : ConcreteCategory C
J : Type v
inst✝⁴ : SmallCategory J
F : J ⥤ C
inst✝³ : PreservesColimit F (forget C)
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
x : (forget C).obj (widePushout B X f)
⊢ ∃ i y, ↑(ι f i) y = x
[PROOFSTEP]
rcases Concrete.widePushout_exists_rep f x with (⟨y, rfl⟩ | ⟨i, y, rfl⟩)
[GOAL]
case inl.intro
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : ConcreteCategory C
J : Type v
inst✝⁴ : SmallCategory J
F : J ⥤ C
inst✝³ : PreservesColimit F (forget C)
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : (forget C).obj B
⊢ ∃ i y_1, ↑(ι f i) y_1 = ↑(head f) y
[PROOFSTEP]
inhabit α
[GOAL]
case inl.intro
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : ConcreteCategory C
J : Type v
inst✝⁴ : SmallCategory J
F : J ⥤ C
inst✝³ : PreservesColimit F (forget C)
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : (forget C).obj B
inhabited_h : Inhabited α
⊢ ∃ i y_1, ↑(ι f i) y_1 = ↑(head f) y
[PROOFSTEP]
use default, f _ y
[GOAL]
case h
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : ConcreteCategory C
J : Type v
inst✝⁴ : SmallCategory J
F : J ⥤ C
inst✝³ : PreservesColimit F (forget C)
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
y : (forget C).obj B
inhabited_h : Inhabited α
⊢ ↑(ι f default) (↑(f default) y) = ↑(head f) y
[PROOFSTEP]
simp only [← arrow_ι _ default, comp_apply]
[GOAL]
case inr.intro.intro
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : ConcreteCategory C
J : Type v
inst✝⁴ : SmallCategory J
F : J ⥤ C
inst✝³ : PreservesColimit F (forget C)
B : C
α : Type v
inst✝² : Nonempty α
X : α → C
f : (j : α) → B ⟶ X j
inst✝¹ : HasWidePushout B X f
inst✝ : PreservesColimit (wideSpan B X f) (forget C)
i : α
y : (forget C).obj (X i)
⊢ ∃ i_1 y_1, ↑(ι f i_1) y_1 = ↑(ι f i) y
[PROOFSTEP]
use i, y