[GOAL]
J : Type v₁
⊢ IsConnected (WidePullbackShape J)
[PROOFSTEP]
apply IsConnected.of_induct
[GOAL]
case h
J : Type v₁
⊢ ∀ (p : Set (WidePullbackShape J)),
    ?j₀ ∈ p → (∀ {j₁ j₂ : WidePullbackShape J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : WidePullbackShape J), j ∈ p
case j₀ J : Type v₁ ⊢ WidePullbackShape J
[PROOFSTEP]
introv hp t
[GOAL]
case h
J : Type v₁
p : Set (WidePullbackShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePullbackShape J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : WidePullbackShape J
⊢ j ∈ p
case j₀ J : Type v₁ ⊢ WidePullbackShape J
[PROOFSTEP]
cases j
[GOAL]
case h.none
J : Type v₁
p : Set (WidePullbackShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePullbackShape J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
⊢ none ∈ p
[PROOFSTEP]
exact hp
[GOAL]
case h.some
J : Type v₁
p : Set (WidePullbackShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePullbackShape J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
val✝ : J
⊢ some val✝ ∈ p
[PROOFSTEP]
rwa [t (WidePullbackShape.Hom.term _)]
[GOAL]
J : Type v₁
⊢ IsConnected (WidePushoutShape J)
[PROOFSTEP]
apply IsConnected.of_induct
[GOAL]
case h
J : Type v₁
⊢ ∀ (p : Set (WidePushoutShape J)),
    ?j₀ ∈ p → (∀ {j₁ j₂ : WidePushoutShape J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : WidePushoutShape J), j ∈ p
case j₀ J : Type v₁ ⊢ WidePushoutShape J
[PROOFSTEP]
introv hp t
[GOAL]
case h
J : Type v₁
p : Set (WidePushoutShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : WidePushoutShape J
⊢ j ∈ p
case j₀ J : Type v₁ ⊢ WidePushoutShape J
[PROOFSTEP]
cases j
[GOAL]
case h.none
J : Type v₁
p : Set (WidePushoutShape J)
hp : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
⊢ none ∈ p
[PROOFSTEP]
exact hp
[GOAL]
case h.some
J : Type v₁
p : Set (WidePushoutShape J)
hp : none ∈ p
t : ∀ {j₁ j₂ : WidePushoutShape J}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
val✝ : J
⊢ some val✝ ∈ p
[PROOFSTEP]
rwa [← t (WidePushoutShape.Hom.init _)]
[GOAL]
⊢ IsConnected WalkingParallelPair
[PROOFSTEP]
apply IsConnected.of_induct
[GOAL]
case h
⊢ ∀ (p : Set WalkingParallelPair),
    ?j₀ ∈ p → (∀ {j₁ j₂ : WalkingParallelPair}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)) → ∀ (j : WalkingParallelPair), j ∈ p
case j₀ ⊢ WalkingParallelPair
[PROOFSTEP]
introv _ t
[GOAL]
case h
p : Set WalkingParallelPair
a✝ : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
j : WalkingParallelPair
⊢ j ∈ p
case j₀ ⊢ WalkingParallelPair
[PROOFSTEP]
cases j
[GOAL]
case h.zero
p : Set WalkingParallelPair
a✝ : ?j₀ ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
⊢ WalkingParallelPair.zero ∈ p
[PROOFSTEP]
rwa [t WalkingParallelPairHom.left]
[GOAL]
case h.one
p : Set WalkingParallelPair
a✝ : WalkingParallelPair.one ∈ p
t : ∀ {j₁ j₂ : WalkingParallelPair}, (j₁ ⟶ j₂) → (j₁ ∈ p ↔ j₂ ∈ p)
⊢ WalkingParallelPair.one ∈ p
[PROOFSTEP]
assumption
[GOAL]
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ (fun s => prod.lift (NatTrans.app s.π (Classical.arbitrary J) ≫ prod.fst) (IsLimit.lift l (forgetCone s))) s ≫
      NatTrans.app ((prod.functor.obj X).mapCone c).π j =
    NatTrans.app s.π j
[PROOFSTEP]
apply prod.hom_ext
[GOAL]
case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ ((fun s => prod.lift (NatTrans.app s.π (Classical.arbitrary J) ≫ prod.fst) (IsLimit.lift l (forgetCone s))) s ≫
        NatTrans.app ((prod.functor.obj X).mapCone c).π j) ≫
      prod.fst =
    NatTrans.app s.π j ≫ prod.fst
[PROOFSTEP]
erw [assoc, limMap_π, comp_id, limit.lift_π]
[GOAL]
case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ NatTrans.app (BinaryFan.mk (NatTrans.app s.π (Classical.arbitrary J) ≫ prod.fst) (IsLimit.lift l (forgetCone s))).π
      { as := WalkingPair.left } =
    NatTrans.app s.π j ≫ prod.fst
[PROOFSTEP]
exact (nat_trans_from_is_connected (s.π ≫ γ₁ X) j (Classical.arbitrary _)).symm
[GOAL]
case h₂
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
j : J
⊢ ((fun s => prod.lift (NatTrans.app s.π (Classical.arbitrary J) ≫ prod.fst) (IsLimit.lift l (forgetCone s))) s ≫
        NatTrans.app ((prod.functor.obj X).mapCone c).π j) ≫
      prod.snd =
    NatTrans.app s.π j ≫ prod.snd
[PROOFSTEP]
simp [← l.fac (forgetCone s) j]
[GOAL]
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ NatTrans.app ((prod.functor.obj X).mapCone c).π j = NatTrans.app s.π j
⊢ m = (fun s => prod.lift (NatTrans.app s.π (Classical.arbitrary J) ≫ prod.fst) (IsLimit.lift l (forgetCone s))) s
[PROOFSTEP]
apply prod.hom_ext
[GOAL]
case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ NatTrans.app ((prod.functor.obj X).mapCone c).π j = NatTrans.app s.π j
⊢ m ≫ prod.fst =
    (fun s => prod.lift (NatTrans.app s.π (Classical.arbitrary J) ≫ prod.fst) (IsLimit.lift l (forgetCone s))) s ≫
      prod.fst
[PROOFSTEP]
erw [limit.lift_π, ← L (Classical.arbitrary J), assoc, limMap_π, comp_id]
[GOAL]
case h₁
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ NatTrans.app ((prod.functor.obj X).mapCone c).π j = NatTrans.app s.π j
⊢ m ≫ prod.fst =
    NatTrans.app (BinaryFan.mk (m ≫ limit.π (pair X c.pt) { as := WalkingPair.left }) (IsLimit.lift l (forgetCone s))).π
      { as := WalkingPair.left }
[PROOFSTEP]
rfl
[GOAL]
case h₂
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ NatTrans.app ((prod.functor.obj X).mapCone c).π j = NatTrans.app s.π j
⊢ m ≫ prod.snd =
    (fun s => prod.lift (NatTrans.app s.π (Classical.arbitrary J) ≫ prod.fst) (IsLimit.lift l (forgetCone s))) s ≫
      prod.snd
[PROOFSTEP]
rw [limit.lift_π]
[GOAL]
case h₂
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ NatTrans.app ((prod.functor.obj X).mapCone c).π j = NatTrans.app s.π j
⊢ m ≫ prod.snd =
    NatTrans.app (BinaryFan.mk (NatTrans.app s.π (Classical.arbitrary J) ≫ prod.fst) (IsLimit.lift l (forgetCone s))).π
      { as := WalkingPair.right }
[PROOFSTEP]
apply l.uniq (forgetCone s)
[GOAL]
case h₂.x
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ NatTrans.app ((prod.functor.obj X).mapCone c).π j = NatTrans.app s.π j
⊢ ∀ (j : J), (m ≫ prod.snd) ≫ NatTrans.app c.π j = NatTrans.app (forgetCone s).π j
[PROOFSTEP]
intro j
[GOAL]
case h₂.x
C : Type u₂
inst✝³ : Category.{v₂, u₂} C
inst✝² : HasBinaryProducts C
J : Type v₂
inst✝¹ : SmallCategory J
inst✝ : IsConnected J
X : C
K : J ⥤ C
c : Cone K
l : IsLimit c
s : Cone (K ⋙ prod.functor.obj X)
m : s.pt ⟶ ((prod.functor.obj X).mapCone c).pt
L : ∀ (j : J), m ≫ NatTrans.app ((prod.functor.obj X).mapCone c).π j = NatTrans.app s.π j
j : J
⊢ (m ≫ prod.snd) ≫ NatTrans.app c.π j = NatTrans.app (forgetCone s).π j
[PROOFSTEP]
simp [← L j]
