awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
s :
  PullbackCone (Y := TopCat.of PUnit.{u + 1}) f
    (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
l : (x : (↑s.pt : Type u)) → (↑X' : Type u)
hl :
  ∀ (x : (↑s.pt : Type u)),
    (fun (y : (↑X' : Type u)) ↦
        Eq (α :=
          (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                { as := WalkingPair.left : Discrete WalkingPair }) :
            Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  s.fst :
                (a : (↑s.pt : Type u)) →
                  (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                        { as := WalkingPair.left }) :
                    Type u))
              x :
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.left : Discrete WalkingPair }) :
              Type u))
          (Sum.inl y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
      (l x)
hl' :
  ∀ (x : (↑s.pt : Type u)) (y : (↑X' : Type u)),
    (fun (y : (↑X' : Type u)) ↦
          Eq (α :=
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.left : Discrete WalkingPair }) :
              Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) s.fst :
                  (a : (↑s.pt : Type u)) →
                    (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                          { as := WalkingPair.left }) :
                      Type u))
                x :
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                    { as := WalkingPair.left : Discrete WalkingPair }) :
                Type u))
            (Sum.inl y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
        y →
      y = l x
⊢ Continuous l
have h₁ : Continuous (Y := (↑X' : Type u) ⊕ (↑Y' : Type u)) (Sum.inl ∘ l)
Tactic: apply (IsEmbedding.inl (X := X') (Y := Y')).isInducing.continuous_iff.mpr
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
s :
  PullbackCone (Y := TopCat.of PUnit.{u + 1}) f
    (BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
l : (x : (↑s.pt : Type u)) → (↑X' : Type u)
hl :
  ∀ (x : (↑s.pt : Type u)),
    (fun (y : (↑X' : Type u)) ↦
        Eq (α :=
          (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                { as := WalkingPair.left : Discrete WalkingPair }) :
            Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  s.fst :
                (a : (↑s.pt : Type u)) →
                  (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                        { as := WalkingPair.left }) :
                    Type u))
              x :
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.left : Discrete WalkingPair }) :
              Type u))
          (Sum.inl y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
      (l x)
hl' :
  ∀ (x : (↑s.pt : Type u)) (y : (↑X' : Type u)),
    (fun (y : (↑X' : Type u)) ↦
          Eq (α :=
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.left : Discrete WalkingPair }) :
              Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) s.fst :
                  (a : (↑s.pt : Type u)) →
                    (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                          { as := WalkingPair.left }) :
                      Type u))
                x :
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                    { as := WalkingPair.left : Discrete WalkingPair }) :
                Type u))
            (Sum.inl y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
        y →
      y = l x
⊢ Continuous (Y := (↑X' : Type u) ⊕ (↑Y' : Type u)) (Sum.inl ∘ l)
have h : ((↑X' : Type u) ⊕ (↑Y' : Type u)) =
    (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
          { as := WalkingPair.left : Discrete WalkingPair }) :
      Type u) →
  Sum.inl ∘ l = (TopCat.Hom.hom s.fst).toFun
Tactic: convert! s.fst.hom.2 using 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
⊢ IsPullback (X'.binaryCofan Y').inr αY f
    (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
have h₁ : (s :
    PullbackCone (Y := TopCat.of PUnit.{u + 1}) f
      (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))) →
  { l : s.pt ⟶ (PullbackCone.mk (X'.binaryCofan Y').inr αY sorry).pt //
    l ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY sorry).fst = s.fst ∧
      l ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY sorry).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (X'.binaryCofan Y').inr αY sorry).pt},
          m ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY sorry).fst = s.fst →
            m ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY sorry).snd = s.snd → m = l }
Tactic: refine ⟨⟨hαY.symm⟩, ⟨PullbackCone.isLimitAux' _ ?_⟩⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
s :
  PullbackCone (Y := TopCat.of PUnit.{u + 1}) f
    (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
x : (↑s.pt : Type u)
⊢ ∃! y : (↑Y' : Type u),
    Eq (α :=
      (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
            { as := WalkingPair.right : Discrete WalkingPair }) :
        Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              s.fst :
            (a : (↑s.pt : Type u)) →
              (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj { as := WalkingPair.right }) :
                Type u))
          x :
        (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
              { as := WalkingPair.right : Discrete WalkingPair }) :
          Type u))
      (Sum.inr y : (↑X' : Type u) ⊕ (↑Y' : Type u))
have inl : ∀ (val : (↑X' : Type u))
  (h :
    Eq (α :=
      (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
            { as := WalkingPair.right : Discrete WalkingPair }) :
        Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              s.fst :
            (a : (↑s.pt : Type u)) →
              (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj { as := WalkingPair.right }) :
                Type u))
          x :
        (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
              { as := WalkingPair.right : Discrete WalkingPair }) :
          Type u))
      (Sum.inl val : (↑X' : Type u) ⊕ (↑Y' : Type u))),
  ∃! y : (↑Y' : Type u), Sum.inl val = Sum.inr y
Tactic: rcases h : s.fst x with val | val
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
s :
  PullbackCone (Y := TopCat.of PUnit.{u + 1}) f
    (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
⊢ { l : s.pt ⟶ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).pt //
    l ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).fst = s.fst ∧
      l ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).snd = s.snd ∧
        ∀ {m : s.pt ⟶ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).pt},
          m ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).fst = s.fst →
            m ≫ (PullbackCone.mk (X'.binaryCofan Y').inr αY ⋯).snd = s.snd → m = l }
have this : ∀ (x : (↑s.pt : Type u)),
  ∃! y : (↑Y' : Type u),
    Eq (α :=
      (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
            { as := WalkingPair.right : Discrete WalkingPair }) :
        Type u))
      ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
              s.fst :
            (a : (↑s.pt : Type u)) →
              (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj { as := WalkingPair.right }) :
                Type u))
          x :
        (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
              { as := WalkingPair.right : Discrete WalkingPair }) :
          Type u))
      (Sum.inr y : (↑X' : Type u) ⊕ (↑Y' : Type u))
Tactic: have : ∀ x, ∃! y, s.fst x = Sum.inr y := by
        intro x
        rcases h : s.fst x with val | val
        · apply_fun f at h
          cases ((ConcreteCategory.congr_hom s.condition x).symm.trans h).trans
            (ConcreteCategory.congr_hom hαX val :).symm
        · exact ⟨val, rfl, fun y h => Sum.inr_injective h.symm⟩
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
s :
  PullbackCone (Y := TopCat.of PUnit.{u + 1}) f
    (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
l : (x : (↑s.pt : Type u)) → (↑Y' : Type u)
hl :
  ∀ (x : (↑s.pt : Type u)),
    (fun (y : (↑Y' : Type u)) ↦
        Eq (α :=
          (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                { as := WalkingPair.right : Discrete WalkingPair }) :
            Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  s.fst :
                (a : (↑s.pt : Type u)) →
                  (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                        { as := WalkingPair.right }) :
                    Type u))
              x :
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.right : Discrete WalkingPair }) :
              Type u))
          (Sum.inr y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
      (l x)
hl' :
  ∀ (x : (↑s.pt : Type u)) (y : (↑Y' : Type u)),
    (fun (y : (↑Y' : Type u)) ↦
          Eq (α :=
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.right : Discrete WalkingPair }) :
              Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) s.fst :
                  (a : (↑s.pt : Type u)) →
                    (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                          { as := WalkingPair.right }) :
                      Type u))
                x :
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                    { as := WalkingPair.right : Discrete WalkingPair }) :
                Type u))
            (Sum.inr y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
        y →
      y = l x
⊢ Continuous l
have h₁ : Continuous (Y := (↑X' : Type u) ⊕ (↑Y' : Type u)) (Sum.inr ∘ l)
Tactic: apply (IsEmbedding.inr (X := X') (Y := Y')).isInducing.continuous_iff.mpr
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
J : Type v'
inst : Category.{u', v'} J
C : Type u
inst_1 : Category.{v, u} C
D : Type u''
inst_2 : Category.{v'', u''} D
X Y : C
X' Y' : TopCat
αX : X' ⟶ TopCat.of PUnit.{u + 1}
αY : Y' ⟶ TopCat.of PUnit.{u + 1}
f :
  (X'.binaryCofan Y').pt ⟶
    Cocone.pt (F := pair (TopCat.of PUnit.{u + 1}) (TopCat.of PUnit.{u + 1}))
      ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1}))
hαX :
  αX ≫ BinaryCofan.inl ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inl ≫ f
hαY :
  αY ≫ BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})) = (X'.binaryCofan Y').inr ≫ f
s :
  PullbackCone (Y := TopCat.of PUnit.{u + 1}) f
    (BinaryCofan.inr ((TopCat.of PUnit.{u + 1}).binaryCofan (TopCat.of PUnit.{u + 1})))
l : (x : (↑s.pt : Type u)) → (↑Y' : Type u)
hl :
  ∀ (x : (↑s.pt : Type u)),
    (fun (y : (↑Y' : Type u)) ↦
        Eq (α :=
          (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                { as := WalkingPair.right : Discrete WalkingPair }) :
            Type u))
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  s.fst :
                (a : (↑s.pt : Type u)) →
                  (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                        { as := WalkingPair.right }) :
                    Type u))
              x :
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.right : Discrete WalkingPair }) :
              Type u))
          (Sum.inr y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
      (l x)
hl' :
  ∀ (x : (↑s.pt : Type u)) (y : (↑Y' : Type u)),
    (fun (y : (↑Y' : Type u)) ↦
          Eq (α :=
            (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                  { as := WalkingPair.right : Discrete WalkingPair }) :
              Type u))
            ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                    TopCat.carrier) s.fst :
                  (a : (↑s.pt : Type u)) →
                    (↑(((Functor.const (Discrete WalkingPair)).obj (X'.binaryCofan Y').pt).obj
                          { as := WalkingPair.right }) :
                      Type u))
                x :
              (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
                    { as := WalkingPair.right : Discrete WalkingPair }) :
                Type u))
            (Sum.inr y : (↑X' : Type u) ⊕ (↑Y' : Type u)))
        y →
      y = l x
⊢ Continuous (Y := (↑X' : Type u) ⊕ (↑Y' : Type u)) (Sum.inr ∘ l)
have h : ((↑X' : Type u) ⊕ (↑Y' : Type u)) =
    (↑(Functor.obj (Functor.obj (Functor.const (Discrete WalkingPair)) (X'.binaryCofan Y').pt)
          { as := WalkingPair.right : Discrete WalkingPair }) :
      Type u) →
  Sum.inr ∘ l = (TopCat.Hom.hom s.fst).toFun
Tactic: convert! s.fst.hom.2 using 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (hypothesis)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
⊢ FinitaryExtensive.{v'', u''} D
have this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
Tactic: have : PreservesColimitsOfSize Gl := adj.leftAdjoint_preservesColimits
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
⊢ FinitaryExtensive.{v'', u''} D
have van_kampen' : ∀ {X Y : D} (c : BinaryCofan.{v'', u''} X Y) (a : IsColimit c), IsVanKampenColimit c
Tactic: constructor
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
⊢ IsVanKampenColimit c
have van_kampen' : IsVanKampenColimit
  (Functor.obj
    (Cocone.precompose
      (Iso.hom (Functor.isoWhiskerLeft (pair X Y) (asIso adj.counit) ≪≫ Functor.rightUnitor (pair X Y))))
    c)
Tactic: apply (IsVanKampenColimit.precompose_isIso_iff
    (Functor.isoWhiskerLeft _ (asIso adj.counit) ≪≫ Functor.rightUnitor _).hom).mp
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
⊢ pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)
have h_obj : ∀ (X_1 : Discrete WalkingPair), (pair X Y ⋙ Gr).obj X_1 = Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) X_1
Tactic: apply Functor.hext
-- Lean 4 proof step from Mathlib.CategoryTheory.Extensive (goal)
Goal:
C : Type u
inst : Category.{v, u} C
D : Type u''
inst_1 : Category.{v'', u''} D
inst_2 : HasFiniteCoproducts.{v'', u''} D
inst_3 : HasPullbacksOfInclusions.{v'', u''} D
inst_4 : FinitaryExtensive.{v, u} C
Gl : Functor.{v, v'', u, u''} C D
Gr : Functor.{v'', v, u'', u} D C
adj : Gl ⊣ Gr
inst_5 : Gr.Full
inst_6 : Gr.Faithful
inst_7 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), HasPullback (Gr.map f) (adj.unit.app Y)
inst_8 : ∀ (X : D) (Y : C) (f : X ⟶ Gl.obj Y), PreservesLimit (cospan (Gr.map f) (adj.unit.app Y)) Gl
inst_9 : PreservesPullbacksOfInclusions Gl
this : PreservesColimitsOfSize.{v'', v'', v, v'', u, u''} Gl
X Y : D
c : BinaryCofan.{v'', u''} X Y
hc : IsColimit c
h_obj :
  ∀ (X_1 : Discrete WalkingPair), (pair X Y ⋙ Gr).obj X_1 = Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) X_1
⊢ pair X Y ⋙ Gr = pair (Gr.obj X) (Gr.obj Y)
have h_map : ∀ (X_1 Y_1 : Discrete WalkingPair) (f : X_1 ⟶ Y_1),
  HEq ((pair X Y ⋙ Gr).map f) (β :=
    Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) X_1 ⟶
      Functor.obj.{0, v, 0, u} (pair (Gr.obj X) (Gr.obj Y)) Y_1)
    (Functor.map (pair (Gr.obj X) (Gr.obj Y)) f)
Tactic: apply Functor.hext