awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
⊢ (ofSimplex x).image f =
    ofSimplex (n := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x)
have a : (ofSimplex x).image f ≤
  ofSimplex (n := n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
      x)
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
a :
  (ofSimplex x).image f ≤
    ofSimplex (n := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x)
⊢ (ofSimplex x).image f =
    ofSimplex (n := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x)
have a₁ : ofSimplex (n := n)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
      x) ≤
  (ofSimplex x).image f
Tactic: apply le_antisymm
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
⊢ (ofSimplex x).image f ≤
    ofSimplex (n := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x)
have a : Membership.mem (α := (fun (X : Type u) ↦ X) (Y _⦋n⦌)) (γ := Set ((fun (X : Type u) ↦ X) (Y _⦋n⦌)))
  (Subfunctor.obj
    (ofSimplex (n := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x))
    (Opposite.op ⦋n⦌))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
      x :
    (fun (X : Type u) ↦ X) (Y _⦋n⦌))
Tactic: rw [image_le_iff, ofSimplex_le_iff, preimage_obj, Set.mem_preimage]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
n : ℕ
x : X _⦋n⦌
f : X ⟶ Y
⊢ ofSimplex (n := n)
      ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
          (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
        x) ≤
    (ofSimplex x).image f
have a : Membership.mem (α := Y _⦋n⦌) (γ := Set (Y _⦋n⦌)) (((ofSimplex x).image f).obj (Opposite.op ⦋n⦌))
  ((ConcreteCategory.hom (FC := TypeCat.Fun) (f.app (Opposite.op ⦋n⦌)) :
        (a : (fun (X : Type u) ↦ X) (X _⦋n⦌)) → (fun (X : Type u) ↦ X) (Y _⦋n⦌))
      x :
    (fun (X : Type u) ↦ X) (Y _⦋n⦌))
Tactic: rw [ofSimplex_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
⊢ range (A.ι ≫ f) ≤ A.image f
have rw : range (A.ι ≫ f) ≤ range (A.ι ≫ f)
Tactic: rw [image_eq_range]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
⊢ Epi (A.toImage f)
have rw : range (A.toImage f) = ⊤
Tactic: rw [← range_eq_top_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
⊢ range (A.toImage f) = ⊤
have apply : ⊤ ≤ range (A.toImage f)
Tactic: apply le_antisymm (by simp)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
f : X ⟶ Y
S T : X.Subcomplex
h : S ≤ T
⊢ LE.le.{u} (α := Y.Subcomplex) ((fun (S : X.Subcomplex) ↦ S.image f) S) ((fun (S : X.Subcomplex) ↦ S.image f) T)
have rw : S ≤ preimage ((fun (S : X.Subcomplex) ↦ S.image f) T) f
Tactic: rw [image_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
f : X ⟶ Y
S T : X.Subcomplex
h : S ≤ T
⊢ T ≤ preimage ((fun (S : X.Subcomplex) ↦ S.image f) T) f
have rw : T.image f ≤ T.image f
Tactic: rw [← image_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
B : X.Subcomplex
f : Y ⟶ X
⊢ B.preimage f = ⊤ ↔ range f ≤ B
have rw : B.preimage f = ⊤ ↔ image ⊤ f ≤ B
Tactic: rw [← image_top, image_le_iff, top_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
B : X.Subcomplex
f : Y ⟶ X
rw : B.preimage f = ⊤ ↔ image ⊤ f ≤ B
⊢ B.preimage f = ⊤ ↔ range f ≤ B
have rw₁ : B.preimage f = ⊤ ↔ ⊤ ≤ B.preimage f
Tactic: rw [← image_top, image_le_iff, top_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
B : X.Subcomplex
f : Y ⟶ X
rw : B.preimage f = ⊤ ↔ image ⊤ f ≤ B
rw₁ : B.preimage f = ⊤ ↔ ⊤ ≤ B.preimage f
⊢ B.preimage f = ⊤ ↔ range f ≤ B
have rw₂ : B.preimage f = ⊤ ↔ B.preimage f = ⊤
Tactic: rw [← image_top, image_le_iff, top_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
B : X.Subcomplex
f : Y ⟶ X
⊢ (B.preimage f).image f ≤ B
have rw : B.preimage f ≤ B.preimage f
Tactic: rw [image_le_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
f : X ⟶ Y
B : Y.Subcomplex
inst : IsIso f
⊢ (B.preimage f).image f = B
have apply : B ≤ (B.preimage f).image f
Tactic: apply le_antisymm (B.image_preimage_le f)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst : IsIso f
⊢ A.preimage (inv f) = A.image f
have obj : ∀ (x : SimplexCategoryᵒᵖ) (x_1 : Y.obj x), x_1 ∈ (A.preimage (inv f)).obj x ↔ x_1 ∈ (A.image f).obj x
Tactic: ext _ x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex (goal)
Goal:
X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
inst : IsIso f
x_1 : SimplexCategoryᵒᵖ
x : Y.obj x_1
⊢ x ∈ (A.preimage (inv f)).obj x_1 ↔ x ∈ (A.image f).obj x_1
have obj : Membership.mem (α := X.obj x_1) (A.obj x_1)
    ((ConcreteCategory.hom (FC := TypeCat.Fun) (inv (f.app x_1)) : (a : Y.obj x_1) → X.obj x_1) x : X.obj x_1) ↔
  ∃ x_2 ∈ A.obj x_1, (ConcreteCategory.hom (FC := TypeCat.Fun) (f.app x_1) : (a : X.obj x_1) → Y.obj x_1) x_2 = x
Tactic: simp only [preimage_obj, NatIso.isIso_inv_app, Set.mem_preimage, image_obj, Set.mem_image]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits (hypothesis)
Goal:
X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
n : SimplexCategoryᵒᵖ
⊢ IsColimit (F :=
    ((CompleteLattice.MulticoequalizerDiagram.multispanIndex h).map toSSetFunctor).multispan ⋙
      Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u)) n)
    (Functor.mapCocone (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u)) n)
      ((CompleteLattice.MulticoequalizerDiagram.multicofork h).map toSSetFunctor))
have h' : CompleteLattice.MulticoequalizerDiagram (A.obj n) (fun (i : ι) ↦ (U i).obj n) fun (i j : ι) ↦ (V i j).obj n
Tactic: have h' : CompleteLattice.MulticoequalizerDiagram (A.obj n) (fun i ↦ (U i).obj n)
        (fun i j ↦ (V i j).obj n) :=
      { eq_inf := by simp [h.eq_inf]
        iSup_eq := by simp [← h.iSup_eq] }
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits (goal)
Goal:
X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
inst : LinearOrder ι
i j : ι
⊢ (CompleteLattice.MulticoequalizerDiagram.multispanIndex h).left (i, j) =
    (CompleteLattice.MulticoequalizerDiagram.multispanIndex h).left (j, i)
have dsimp : V i j = V j i
Tactic: dsimp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits (goal)
Goal:
X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
inst : LinearOrder ι
i j : ι
⊢ V i j = V j i
have rw : U i ⊓ U j = V j i
Tactic: rw [h.eq_inf, h.eq_inf, inf_comm]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits (goal)
Goal:
X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
inst : LinearOrder ι
i j : ι
rw : U i ⊓ U j = V j i
⊢ V i j = V j i
have rw₁ : U i ⊓ U j = U j ⊓ U i
Tactic: rw [h.eq_inf, h.eq_inf, inf_comm]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits (goal)
Goal:
X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
inst : LinearOrder ι
i j : ι
rw : U i ⊓ U j = V j i
rw₁ : U i ⊓ U j = U j ⊓ U i
⊢ V i j = V j i
have rw₂ : U j ⊓ U i = U j ⊓ U i
Tactic: rw [h.eq_inf, h.eq_inf, inf_comm]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits (goal)
Goal:
X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
⊢ A₂.obj n ⊔ A₃.obj n = A₄.obj n
have rw : A₂.obj n ⊔ A₃.obj n = (A₂ ⊔ A₃).obj n
Tactic: rw [← sq.sup_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits (goal)
Goal:
X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
⊢ A₂.obj n ⊓ A₃.obj n = A₁.obj n
have rw : A₂.obj n ⊓ A₃.obj n = (A₂ ⊓ A₃).obj n
Tactic: rw [← sq.inf_eq]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits (hypothesis)
Goal:
X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
⊢ IsColimit (F :=
    span (X := Functor.obj (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u)) n) A₁.toSSet)
      (CategoryTheory.Functor.map (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u)) n) (homOfLE ⋯))
      (CategoryTheory.Functor.map (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u)) n) (homOfLE ⋯)))
    (PushoutCocone.map (PushoutCocone.mk (homOfLE ⋯) (homOfLE ⋯) ⋯)
      (Functor.obj (evaluation SimplexCategoryᵒᵖ (Type u)) n))
have h : Lattice.BicartSq (A₁.obj n) (A₂.obj n) (A₃.obj n) (A₄.obj n)
Tactic: have h : Lattice.BicartSq (A₁.obj n) (A₂.obj n) (A₃.obj n) (A₄.obj n) :=
          { sup_eq := by
              rw [← sq.sup_eq]
              rfl
            inf_eq := by
              rw [← sq.inf_eq]
              rfl }
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
n m : SimplexCategory
f : n ⟶ m
⊢ Eq (α := (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u) → (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
    (Function.comp (β := (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      (⇑m.toTopHomeo :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (SSet.toTop.map (SSet.stdSimplex.map f))) :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) →
          (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u)))
    (Function.comp (β := (↑(_root_.stdSimplex ℝ ((fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n)) : Type))
      (stdSimplex.map
        (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f) :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m))
      (⇑n.toTopHomeo :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (n.len + 1))) : Type)))
have h : ∀ (x : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)),
  Eq (α := (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
    (Function.comp (β := (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      (⇑m.toTopHomeo :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
      (⇑(ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
            (SSet.toTop.map (SSet.stdSimplex.map f))) :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) →
          (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      x)
    (Function.comp (β := (↑(_root_.stdSimplex ℝ ((fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n)) : Type))
      (stdSimplex.map
        (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f) :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m))
      (⇑n.toTopHomeo :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) → (↑(_root_.stdSimplex ℝ (Fin (n.len + 1))) : Type))
      x)
Tactic: ext x : 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
n m : SimplexCategory
f : n ⟶ m
⊢ Eq (α :=
    (↑(_root_.stdSimplex ℝ ((fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n)) : Type) →
      (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
    (Function.comp (β := (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
      (⇑m.toTopHomeo.symm :
        (a : (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type)) → (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      (stdSimplex.map
        (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f) :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m)))
    (Function.comp (β := (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u))
      (⇑(TopCat.Hom.hom (SSet.toTop.map (SSet.stdSimplex.map f))) :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) →
          (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      (⇑n.toTopHomeo.symm :
        (a : (↑(_root_.stdSimplex ℝ (Fin (n.len + 1))) : Type)) → (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)))
have h : ∀ (x : (↑(_root_.stdSimplex ℝ ((fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n)) : Type)),
  Eq (α := (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
    (Function.comp (β := (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type))
      (⇑m.toTopHomeo.symm :
        (a : (↑(_root_.stdSimplex ℝ (Fin (m.len + 1))) : Type)) → (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      (stdSimplex.map
        (⇑(ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) f) :
          (a : (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) n) → (fun (X : SimplexCategory) ↦ Fin (X.len + 1)) m))
      x)
    (Function.comp (β := (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u))
      (⇑(TopCat.Hom.hom (SSet.toTop.map (SSet.stdSimplex.map f))) :
        (a : (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u)) →
          (↑(SSet.toTop.obj (SSet.stdSimplex.obj m)) : Type u))
      (⇑n.toTopHomeo.symm :
        (a : (↑(_root_.stdSimplex ℝ (Fin (n.len + 1))) : Type)) → (↑(SSet.toTop.obj (SSet.stdSimplex.obj n)) : Type u))
      x)
Tactic: ext x : 1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
X : TopCat
x : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u))
⊢ (fun (x : (↑X : Type u)) ↦
        { toFun := fun (x_1 : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) ↦ x, continuous_toFun := ⋯ :
          C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u)) })
      ((fun (f : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u))) ↦ f.toFun default) x) =
    x
have h : ∀ (x_1 : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)),
  Eq (α := (↑X : Type u))
    (((fun (x : (↑X : Type u)) ↦
              { toFun := fun (x_2 : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) ↦ x,
                continuous_toFun := sorry : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u)) })
            ((fun (f : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u))) ↦ f.toFun default)
              x) :
          (a : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) → (↑X : Type u))
        x_1 :
      (↑X : Type u))
    ((x : (a : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) → (↑X : Type u)) x_1 : (↑X : Type u))
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
X : TopCat
x_1 : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u))
x : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)
⊢ Eq (α := (↑X : Type u))
    (((fun (x : (↑X : Type u)) ↦
              { toFun := fun (x_2 : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) ↦ x,
                continuous_toFun := ⋯ : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u)) })
            ((fun (f : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u))) ↦ f.toFun default)
              x_1) :
          (a : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) → (↑X : Type u))
        x :
      (↑X : Type u))
    ((x_1 : (a : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) → (↑X : Type u)) x : (↑X : Type u))
have h : Eq (α := (↑X : Type u))
  (((fun (x : (↑X : Type u)) ↦
            { toFun := fun (x_2 : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) ↦ x, continuous_toFun := sorry :
              C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u)) })
          ((fun (f : C((↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type), (↑X : Type u))) ↦ f.toFun default)
            x_1) :
        (a : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) → (↑X : Type u))
      default :
    (↑X : Type u))
  ((x_1 : (a : (↑(stdSimplex ℝ (Fin ((unop (op ⦋0⦌)).len + 1))) : Type)) → (↑X : Type u)) default : (↑X : Type u))
Tactic: obtain rfl := Subsingleton.elim x default
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (hypothesis)
Goal:
X : TopCat
f : SSet.toTop.obj Δ[0] ⟶ X
⊢ Eq (α := Δ[0] ⟶ TopCat.toSSet.obj X)
    ((sSetTopAdj.homEquiv Δ[0] X : (a : SSet.toTop.obj Δ[0] ⟶ X) → Δ[0] ⟶ TopCat.toSSet.obj X) f :
      Δ[0] ⟶ TopCat.toSSet.obj X)
    (SSet.const
        ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑X : Type u)) → TopCat.toSSet.obj X _⦋0⦌)
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  f :
                (a : (↑(SSet.toTop.obj Δ[0]) : Type u)) → (↑X : Type u))
              default :
            (↑X : Type u))) :
      Δ[0] ⟶ TopCat.toSSet.obj X)
have this : Eq (α := Functor.obj (𝟭 SSet) Δ[0] ⟶ (SSet.toTop ⋙ TopCat.toSSet).obj Δ[0]) (sSetTopAdj.unit.app Δ[0])
  (SSet.const
    ((Equiv.symm TopCat.toSSetObj₀Equiv :
        (a : (↑(SSet.toTop.obj Δ[0]) : Type u)) → TopCat.toSSet.obj (SSet.toTop.obj Δ[0]) _⦋0⦌)
      default))
Tactic: have : sSetTopAdj.unit.app Δ[0] =
      SSet.const (TopCat.toSSetObj₀Equiv.symm default) :=
    SSet.yonedaEquiv.injective (TopCat.toSSetObj₀Equiv.injective (by subsingleton))
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
X : TopCat
f : SSet.toTop.obj Δ[0] ⟶ X
this :
  Eq (α := Functor.obj (𝟭 SSet) Δ[0] ⟶ (SSet.toTop ⋙ TopCat.toSSet).obj Δ[0]) (sSetTopAdj.unit.app Δ[0])
    (SSet.const
      ((Equiv.symm TopCat.toSSetObj₀Equiv :
          (a : (↑(SSet.toTop.obj Δ[0]) : Type u)) → TopCat.toSSet.obj (SSet.toTop.obj Δ[0]) _⦋0⦌)
        default))
⊢ Eq (α := Δ[0] ⟶ TopCat.toSSet.obj X)
    ((sSetTopAdj.homEquiv Δ[0] X : (a : SSet.toTop.obj Δ[0] ⟶ X) → Δ[0] ⟶ TopCat.toSSet.obj X) f :
      Δ[0] ⟶ TopCat.toSSet.obj X)
    (SSet.const
        ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑X : Type u)) → TopCat.toSSet.obj X _⦋0⦌)
          ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                  f :
                (a : (↑(SSet.toTop.obj Δ[0]) : Type u)) → (↑X : Type u))
              default :
            (↑X : Type u))) :
      Δ[0] ⟶ TopCat.toSSet.obj X)
have rw : Eq (α := Δ[0] ⟶ TopCat.toSSet.obj X)
  (SSet.const
        ((Equiv.symm TopCat.toSSetObj₀Equiv :
            (a : (↑(SSet.toTop.obj Δ[0]) : Type u)) → TopCat.toSSet.obj (SSet.toTop.obj Δ[0]) _⦋0⦌)
          default) ≫
      TopCat.toSSet.map f :
    Δ[0] ⟶ TopCat.toSSet.obj X)
  (SSet.const
      ((Equiv.symm (X.toSSetObjEquiv (op ⦋0⦌)) :
          (a : C((↑(stdSimplex ℝ (Fin (0 + 1))) : Type), (↑X : Type u))) → TopCat.toSSet.obj X _⦋0⦌)
        {
          toFun := fun (x : (↑(stdSimplex ℝ (Fin (HAdd.hAdd (α := ℕ) 0 1))) : Type)) ↦
            (ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC :=
                  TopCat.carrier) f :
                (a : (↑(SSet.toTop.obj Δ[0]) : Type u)) → (↑X : Type u))
              default,
          continuous_toFun := sorry }) :
    Δ[0] ⟶ TopCat.toSSet.obj X)
Tactic: rw [Adjunction.homEquiv_unit, TopCat.toSSetObj₀Equiv_symm_apply, this]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplicialSet.TopAdj (goal)
Goal:
⊢ Eq (α := Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
    (stdSimplex.δ 1 ≫
      (sSetTopAdj.homEquiv Δ[1] TopCat.I : (a : toTop.obj Δ[1] ⟶ TopCat.I) → Δ[1] ⟶ TopCat.toSSet.obj TopCat.I)
        (TopCat.isoOfHomeo
            (Homeomorph.trans ⦋1⦌.toTopHomeo
              (stdSimplexHomeomorphUnitInterval.trans (Homeomorph.symm Homeomorph.ulift)))).hom)
    (SSet.const ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u)) → TopCat.toSSet.obj TopCat.I _⦋0⦌) 0))
have rw : Eq (α := Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
  (SSet.const
      ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u)) → TopCat.toSSet.obj TopCat.I _⦋0⦌)
        ((ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u))) (CC := TopCat.carrier)
                (toTop.map (stdSimplex.δ 1) ≫
                  (TopCat.isoOfHomeo
                      (Homeomorph.trans ⦋1⦌.toTopHomeo
                        (stdSimplexHomeomorphUnitInterval.trans (Homeomorph.symm Homeomorph.ulift)))).hom) :
              (a : (↑(toTop.obj Δ[0]) : Type u)) → (↑TopCat.I : Type u))
            default :
          (↑TopCat.I : Type u))) :
    Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
  (SSet.const ((Equiv.symm TopCat.toSSetObj₀Equiv : (a : (↑TopCat.I : Type u)) → TopCat.toSSet.obj TopCat.I _⦋0⦌) 0) :
    Δ[0] ⟶ TopCat.toSSet.obj TopCat.I)
Tactic: rw [← Adjunction.homEquiv_naturality_left, sSetTopAdj_homEquiv_stdSimplex_zero]