awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf :
  IsInducing (X := (↑W : Type u)) (Y := (↑X : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑W : Type u)) → (↑X : Type u))
hg :
  IsInducing (X := (↑Y : Type u)) (Y := (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
      (a : (↑Y : Type u)) → (↑Z : Type u))
⊢ Eq (α := TopologicalSpace (↑(W ⨯ Y) : Type u)) (W ⨯ Y).str
    (induced (Y := (↑(X ⨯ Z) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
            W ⨯ Y) (Y := X ⨯ Z) (prod.map f g)) :
        (a : (↑(W ⨯ Y) : Type u)) → (↑(X ⨯ Z) : Type u))
      (X ⨯ Z).str)
have eq_induced : Eq (α := TopologicalSpace (↑(W ⨯ Y) : Type u))
  (induced
      (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (W ⨯ Y) _ prod.fst) :
        (a : (↑(W ⨯ Y) : Type u)) → (↑W : Type u))
      W.str ⊓
    induced
      (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (W ⨯ Y) _ prod.snd) :
        (a : (↑(W ⨯ Y) : Type u)) → (↑Y : Type u))
      Y.str)
  (induced (Y := (↑W : Type u))
      (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (W ⨯ Y) _ prod.fst) :
        (a : (↑(W ⨯ Y) : Type u)) → (↑W : Type u))
      (induced
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
          (a : (↑W : Type u)) → (↑X : Type u))
        X.str) ⊓
    induced (Y := (↑Y : Type u))
      (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (W ⨯ Y) _ prod.snd) :
        (a : (↑(W ⨯ Y) : Type u)) → (↑Y : Type u))
      (induced
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        Z.str))
Tactic: simp_rw [prod_topology, induced_inf, induced_compose, ← coe_comp,
    prod.map_fst, prod.map_snd, coe_comp, ← induced_compose (g := f), ← induced_compose (g := g)]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf :
  IsInducing (X := (↑W : Type u)) (Y := (↑X : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑W : Type u)) → (↑X : Type u))
hg :
  IsInducing (X := (↑Y : Type u)) (Y := (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
      (a : (↑Y : Type u)) → (↑Z : Type u))
⊢ Eq (α := TopologicalSpace (↑(W ⨯ Y) : Type u))
    (induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (W ⨯ Y) _ prod.fst) :
          (a : (↑(W ⨯ Y) : Type u)) → (↑W : Type u))
        W.str ⊓
      induced
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (W ⨯ Y) _ prod.snd) :
          (a : (↑(W ⨯ Y) : Type u)) → (↑Y : Type u))
        Y.str)
    (induced (Y := (↑W : Type u))
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (W ⨯ Y) _ prod.fst) :
          (a : (↑(W ⨯ Y) : Type u)) → (↑W : Type u))
        (induced
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
            (a : (↑W : Type u)) → (↑X : Type u))
          X.str) ⊓
      induced (Y := (↑Y : Type u))
        (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
              (W ⨯ Y) _ prod.snd) :
          (a : (↑(W ⨯ Y) : Type u)) → (↑Y : Type u))
        (induced
          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
            (a : (↑Y : Type u)) → (↑Z : Type u))
          Z.str))
have eq_induced : Eq (α := TopologicalSpace (↑(W ⨯ Y) : Type u))
  (induced
      (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (W ⨯ Y) _ prod.fst) :
        (a : (↑(W ⨯ Y) : Type u)) → (↑W : Type u))
      W.str ⊓
    induced
      (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (W ⨯ Y) _ prod.snd) :
        (a : (↑(W ⨯ Y) : Type u)) → (↑Y : Type u))
      Y.str)
  (induced
      (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (W ⨯ Y) _ prod.fst) :
        (a : (↑(W ⨯ Y) : Type u)) → (↑W : Type u))
      W.str ⊓
    induced (Y := (↑Y : Type u))
      (⇑(@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (W ⨯ Y) _ prod.snd) :
        (a : (↑(W ⨯ Y) : Type u)) → (↑Y : Type u))
      (induced
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
          (a : (↑Y : Type u)) → (↑Z : Type u))
        Z.str))
Tactic: rw [← hf.eq_induced, ← hg.eq_induced]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (hypothesis)
Goal:
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf :
  IsEmbedding (X := (↑W : Type u)) (Y := (↑X : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑W : Type u)) → (↑X : Type u))
hg :
  IsEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
      (a : (↑Y : Type u)) → (↑Z : Type u))
⊢ Function.Injective (α := (↑(W ⨯ Y) : Type u)) (β := (↑(X ⨯ Z) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          W ⨯ Y) (Y := X ⨯ Z) (prod.map f g)) :
      (a : (↑(W ⨯ Y) : Type u)) → (↑(X ⨯ Z) : Type u))
have this : Mono f
Tactic: haveI := (TopCat.mono_iff_injective _).mpr hf.injective
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (hypothesis)
Goal:
W X Y Z : TopCat
f : W ⟶ X
g : Y ⟶ Z
hf :
  IsEmbedding (X := (↑W : Type u)) (Y := (↑X : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) f) :
      (a : (↑W : Type u)) → (↑X : Type u))
hg :
  IsEmbedding (X := (↑Y : Type u)) (Y := (↑Z : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) g) :
      (a : (↑Y : Type u)) → (↑Z : Type u))
this : Mono f
⊢ Function.Injective (α := (↑(W ⨯ Y) : Type u)) (β := (↑(X ⨯ Z) : Type u))
    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (X :=
          W ⨯ Y) (Y := X ⨯ Z) (prod.map f g)) :
      (a : (↑(W ⨯ Y) : Type u)) → (↑(X ⨯ Z) : Type u))
have this₁ : Mono g
Tactic: haveI := (TopCat.mono_iff_injective _).mpr hg.injective
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
J : Type v
inst : Category.{w, v} J
X Y : TopCat
⊢ IsColimit (X.binaryCofan Y)
have refine_1 : ∀ (s : BinaryCofan X Y),
  Continuous (X := (↑X : Type u) ⊕ (↑Y : Type u)) (Y := (↑s.1 : Type u))
    (Sum.elim
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) s.inl) :
        (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
          (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) s.inr) :
        (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
          (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) : Type u)))
Tactic: refine Limits.BinaryCofan.isColimitMk (fun s => ofHom
    { toFun := Sum.elim s.inl s.inr, continuous_toFun := ?_ }) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
J : Type v
inst : Category.{w, v} J
X Y : TopCat
refine_1 :
  ∀ (s : BinaryCofan X Y),
    Continuous (X := (↑X : Type u) ⊕ (↑Y : Type u)) (Y := (↑s.1 : Type u))
      (Sum.elim
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              s.inl) :
          (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
            (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u))
        (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier)
              s.inr) :
          (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
            (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) : Type u)))
⊢ IsColimit (X.binaryCofan Y)
have refine_2 : ∀ (s : BinaryCofan X Y),
  ofHom { toFun := Sum.inl, continuous_toFun := sorry : C((↑X : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫
      (fun (s : BinaryCofan X Y) ↦
          (ofHom
              {
                toFun :=
                  Sum.elim
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          carrier) s.inl) :
                      (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
                        (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u))
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          carrier) s.inr) :
                      (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
                        (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) :
                          Type u)),
                continuous_toFun := sorry } :
            of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ of (↑s.1 : Type u)))
        s =
    s.inl
Tactic: refine Limits.BinaryCofan.isColimitMk (fun s => ofHom
    { toFun := Sum.elim s.inl s.inr, continuous_toFun := ?_ }) ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
J : Type v
inst : Category.{w, v} J
X Y : TopCat
s : BinaryCofan X Y
⊢ ofHom { toFun := Sum.inl, continuous_toFun := ⋯ : C((↑X : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫
      (fun (s : BinaryCofan X Y) ↦
          (ofHom
              {
                toFun :=
                  Sum.elim
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          carrier) s.inl) :
                      (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
                        (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u))
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          carrier) s.inr) :
                      (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
                        (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) :
                          Type u)),
                continuous_toFun := ⋯ } :
            of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ of (↑s.1 : Type u)))
        s =
    s.inl
have refine_2 : ∀ (x : (↑X : Type u)),
  Eq (α := (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y := s.pt)
            (ofHom { toFun := Sum.inl, continuous_toFun := sorry : C((↑X : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫
              (fun (s : BinaryCofan X Y) ↦
                  (ofHom
                      {
                        toFun :=
                          Sum.elim
                            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                  (CC := carrier) s.inl) :
                              (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
                                (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) :
                                  Type u))
                            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                  (CC := carrier) s.inr) :
                              (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
                                (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) :
                                  Type u)),
                        continuous_toFun := sorry } :
                    of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ of (↑s.1 : Type u)))
                s) :
          (a : (↑X : Type u)) → (↑s.pt : Type u))
        x :
      (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) s.inl :
          (a : (↑X : Type u)) → (↑s.pt : Type u))
        x :
      (↑s.pt : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
J : Type v
inst : Category.{w, v} J
X Y : TopCat
s : BinaryCofan X Y
⊢ ofHom { toFun := Sum.inr, continuous_toFun := ⋯ : C((↑Y : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫
      (fun (s : BinaryCofan X Y) ↦
          (ofHom
              {
                toFun :=
                  Sum.elim
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          carrier) s.inl) :
                      (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
                        (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u))
                    (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                          carrier) s.inr) :
                      (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
                        (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) :
                          Type u)),
                continuous_toFun := ⋯ } :
            of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ of (↑s.1 : Type u)))
        s =
    s.inr
have refine_3 : ∀ (x : (↑Y : Type u)),
  Eq (α := (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) (Y := s.pt)
            (ofHom { toFun := Sum.inr, continuous_toFun := sorry : C((↑Y : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫
              (fun (s : BinaryCofan X Y) ↦
                  (ofHom
                      {
                        toFun :=
                          Sum.elim
                            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                  (CC := carrier) s.inl) :
                              (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
                                (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) :
                                  Type u))
                            (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                  (CC := carrier) s.inr) :
                              (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
                                (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) :
                                  Type u)),
                        continuous_toFun := sorry } :
                    of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ of (↑s.1 : Type u)))
                s) :
          (a : (↑Y : Type u)) → (↑s.pt : Type u))
        x :
      (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) s.inr :
          (a : (↑Y : Type u)) → (↑s.pt : Type u))
        x :
      (↑s.pt : Type u))
Tactic: ext
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
J : Type v
inst : Category.{w, v} J
X Y : TopCat
s : BinaryCofan X Y
m : of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ s.pt
h₁ : ofHom { toFun := Sum.inl, continuous_toFun := ⋯ : C((↑X : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫ m = s.inl
h₂ : ofHom { toFun := Sum.inr, continuous_toFun := ⋯ : C((↑Y : Type u), (↑X : Type u) ⊕ (↑Y : Type u)) } ≫ m = s.inr
⊢ m =
    (fun (s : BinaryCofan X Y) ↦
        (ofHom
            {
              toFun :=
                Sum.elim
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) s.inl) :
                    (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
                      (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) : Type u))
                  (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                        carrier) s.inr) :
                    (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
                      (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) : Type u)),
              continuous_toFun := ⋯ } :
          of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ of (↑s.1 : Type u)))
      s
have refine_4 : ∀ (x : (↑X : Type u)),
  Eq (α := (↑s.pt : Type u))
    ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := carrier) m :
          (a : (↑(of ((↑X : Type u) ⊕ (↑Y : Type u))) : Type u)) → (↑s.pt : Type u))
        (Sum.inl x) :
      (↑s.pt : Type u))
    ((@ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) carrier _ _
            (of ((↑X : Type u) ⊕ (↑Y : Type u))) s.pt
            ((fun (s : BinaryCofan X Y) ↦
                (ofHom
                    {
                      toFun :=
                        Sum.elim
                          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                (CC := carrier) s.inl) :
                            (a : (↑((pair X Y).obj { as := WalkingPair.left }) : Type u)) →
                              (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.left }) :
                                Type u))
                          (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                                (CC := carrier) s.inr) :
                            (a : (↑((pair X Y).obj { as := WalkingPair.right }) : Type u)) →
                              (↑(((Functor.const (Discrete WalkingPair)).obj s.pt).obj { as := WalkingPair.right }) :
                                Type u)),
                      continuous_toFun := sorry } :
                  of ((↑X : Type u) ⊕ (↑Y : Type u)) ⟶ of (↑s.1 : Type u)))
              s) :
          (a : (↑(of ((↑X : Type u) ⊕ (↑Y : Type u))) : Type u)) → (↑s.pt : Type u))
        (Sum.inl x) :
      (↑s.pt : Type u))
Tactic: ext (x | x)
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
⊢ IsCompl (α := Set (↑c.pt : Type u))
    (range (ι := (↑X : Type u))
      (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
        (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
          (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }) :
              C((↑X : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑X : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))
    (range (ι := (↑Y : Type u))
      (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
        (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
          (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
              C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))
have mp : Eq (α := Set (↑c.pt : Type u))
  (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
    (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
      (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
    (range (ι := (↑X : Type u))
      (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.left }) :
            C((↑X : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
        (a : (↑X : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))
  (range (ι := (↑Y : Type u))
      (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
        (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
          (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
              C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))ᶜ
Tactic: rw [Set.range_comp, ← eq_compl_iff_isCompl]
-- Lean 4 proof step from Mathlib.Topology.Category.TopCat.Limits.Products (goal)
Goal:
X Y : TopCat
c : BinaryCofan X Y
h : IsColimit c
| (range (ι := (↑Y : Type u))
      (Function.comp (β := (↑(X.binaryCofan Y).pt : Type u))
        (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
          (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
        (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
              C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
          (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))ᶜ
have rw : (Set.image (α := (↑(X.binaryCofan Y).pt : Type u))
    (⇑(Hom.hom (h.coconePointUniqueUpToIso (X.binaryCofanIsColimit Y)).inv) :
      (a : (↑(X.binaryCofan Y).pt : Type u)) → (↑c.pt : Type u))
    (range (ι := (↑Y : Type u))
      (⇑(Hom.hom ((X.binaryCofan Y).ι.app { as := WalkingPair.right }) :
            C((↑Y : Type u), (↑(X.binaryCofan Y).pt : Type u))) :
        (a : (↑Y : Type u)) → (↑(X.binaryCofan Y).pt : Type u))))ᶜ
Tactic: rw [Set.range_comp]