awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
x : C((↑(stdSimplex ℝ (Fin ((Opposite.unop (Opposite.op ⦋1⦌)).len + 1))) : Type), (↑X : Type u))
⊢ (fun (f : I ⟶ X) ↦
        ((Hom.hom f).comp
            (↑stdSimplexHomeomorphI :
              C((↑(stdSimplex ℝ (Fin ((Opposite.unop (Opposite.op ⦋1⦌)).len + 1))) : Type), (↑I : Type u))) :
          C((↑(stdSimplex ℝ (Fin ((Opposite.unop (Opposite.op ⦋1⦌)).len + 1))) : Type), (↑X : Type u))))
      ((fun (f : C((↑(stdSimplex ℝ (Fin ((Opposite.unop (Opposite.op ⦋1⦌)).len + 1))) : Type), (↑X : Type u))) ↦
          (ofHom
              (f.comp
                (↑stdSimplexHomeomorphI.symm :
                  C(ULift.{u, 0} (↑unitInterval : Type),
                    (↑(stdSimplex ℝ (Fin ((Opposite.unop (Opposite.op ⦋1⦌)).len + 1))) : Type)))) :
            of (ULift.{u, 0} (↑unitInterval : Type)) ⟶ of (↑X : Type u)))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
x : I ⟶ X
⊢ (fun (f : C((↑(stdSimplex ℝ (Fin ((Opposite.unop (Opposite.op ⦋1⦌)).len + 1))) : Type), (↑X : Type u))) ↦
        (ofHom
            (f.comp
              (↑stdSimplexHomeomorphI.symm :
                C(ULift.{u, 0} (↑unitInterval : Type),
                  (↑(stdSimplex ℝ (Fin ((Opposite.unop (Opposite.op ⦋1⦌)).len + 1))) : Type)))) :
          of (ULift.{u, 0} (↑unitInterval : Type)) ⟶ of (↑X : Type u)))
      ((fun (f : I ⟶ X) ↦
          ((Hom.hom f).comp
              (↑stdSimplexHomeomorphI :
                C((↑(stdSimplex ℝ (Fin ((Opposite.unop (Opposite.op ⦋1⦌)).len + 1))) : Type), (↑I : Type u))) :
            C((↑(stdSimplex ℝ (Fin ((Opposite.unop (Opposite.op ⦋1⦌)).len + 1))) : Type), (↑X : Type u))))
        x) =
    x

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
s : toSSet.obj X _⦋1⦌
⊢ Eq (α := (↑X : Type u))
    ((@CategoryTheory.ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
            carrier _ _ I X ((toSSetObj₁Equiv : (a : toSSet.obj X _⦋1⦌) → I ⟶ X) s) :
          (a : (↑I : Type u)) → (↑X : Type u))
        0 :
      (↑X : Type u))
    ((toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryTheory.SimplicialObject.δ (toSSet.obj X) 1) :
              (a : (fun (X : Type u) ↦ X) (toSSet.obj X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (toSSet.obj X _⦋0⦌))
            s :
          (fun (X : Type u) ↦ X) (toSSet.obj X _⦋0⦌)) :
      (↑X : Type u))

Tactic:
simp [toSSetObj₀Equiv, toSSetObj₁Equiv,
    Subsingleton.elim (default : stdSimplex ℝ (Fin 1)) (stdSimplex.vertex 0)]

Premises used: Inhabited.default, stdSimplex.vertex, TopCat.toSSetObj₀Equiv, TopCat.toSSetObj₁Equiv, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
s : toSSet.obj X _⦋1⦌
⊢ Eq (α := (↑X : Type u))
    ((@CategoryTheory.ConcreteCategory.hom _ instCategory (fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
            carrier _ _ I X ((toSSetObj₁Equiv : (a : toSSet.obj X _⦋1⦌) → I ⟶ X) s) :
          (a : (↑I : Type u)) → (↑X : Type u))
        1 :
      (↑X : Type u))
    ((toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryTheory.SimplicialObject.δ (toSSet.obj X) 0) :
              (a : (fun (X : Type u) ↦ X) (toSSet.obj X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (toSSet.obj X _⦋0⦌))
            s :
          (fun (X : Type u) ↦ X) (toSSet.obj X _⦋0⦌)) :
      (↑X : Type u))

Tactic:
simp [toSSetObj₀Equiv, toSSetObj₁Equiv,
    Subsingleton.elim (default : stdSimplex ℝ (Fin 1)) (stdSimplex.vertex 0)]

Premises used: Inhabited.default, stdSimplex.vertex, TopCat.toSSetObj₀Equiv, TopCat.toSSetObj₁Equiv, Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
f : I ⟶ X
⊢ Eq (α := (↑X : Type u))
    ((toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryTheory.SimplicialObject.δ (toSSet.obj X) 1) :
              (a : (fun (X : Type u) ↦ X) (toSSet.obj X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (toSSet.obj X _⦋0⦌))
            ((Equiv.symm toSSetObj₁Equiv : (a : I ⟶ X) → toSSet.obj X _⦋1⦌) f : toSSet.obj X _⦋1⦌) :
          (fun (X : Type u) ↦ X) (toSSet.obj X _⦋0⦌)) :
      (↑X : Type u))
    ((toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
        ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌)
            ((CategoryTheory.ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                    (CC := carrier) f :
                  (a : (↑I : Type u)) → (↑X : Type u))
                0 :
              (↑X : Type u)) :
          toSSet.obj X _⦋0⦌) :
      (↑X : Type u))

Tactic:
simp [← toSSetObj₁Equiv_apply_zero]

Premises used: TopCat.toSSetObj₁Equiv_apply_zero
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
f : I ⟶ X
⊢ Eq (α := (↑X : Type u))
    ((toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
        ((CategoryTheory.ConcreteCategory.hom (FC := TypeCat.Fun) (CategoryTheory.SimplicialObject.δ (toSSet.obj X) 0) :
              (a : (fun (X : Type u) ↦ X) (toSSet.obj X _⦋0 + 1⦌)) → (fun (X : Type u) ↦ X) (toSSet.obj X _⦋0⦌))
            ((Equiv.symm toSSetObj₁Equiv : (a : I ⟶ X) → toSSet.obj X _⦋1⦌) f : toSSet.obj X _⦋1⦌) :
          (fun (X : Type u) ↦ X) (toSSet.obj X _⦋0⦌)) :
      (↑X : Type u))
    ((toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
        ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌)
            ((CategoryTheory.ConcreteCategory.hom (FC := fun (X Y : TopCat.{u}) ↦ C((↑X : Type u), (↑Y : Type u)))
                    (CC := carrier) f :
                  (a : (↑I : Type u)) → (↑X : Type u))
                1 :
              (↑X : Type u)) :
          toSSet.obj X _⦋0⦌) :
      (↑X : Type u))

Tactic:
simp [← toSSetObj₁Equiv_apply_one]

Premises used: TopCat.toSSetObj₁Equiv_apply_one
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
x y : (↑X : Type u)
x_1 :
  SSet.Edge (X := toSSet.obj X) ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x)
    ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) y)
⊢ (fun (p : X.Path x y) ↦ SSet.Edge.mk ((Equiv.symm toSSetObj₁Equiv : (a : I ⟶ X) → toSSet.obj X _⦋1⦌) p.hom) ⋯ ⋯)
      ((fun
            (e :
              SSet.Edge (X := toSSet.obj X) ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x)
                ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) y)) ↦
          { hom := (toSSetObj₁Equiv : (a : toSSet.obj X _⦋1⦌) → I ⟶ X) e.edge, hom₀ := ⋯, hom₁ := ⋯ : X.Path x y })
        x_1) =
    x_1

Tactic:
aesop
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
x y : (↑X : Type u)
x_1 : X.Path x y
⊢ (fun
          (e :
            SSet.Edge (X := toSSet.obj X) ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x)
              ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) y)) ↦
        { hom := (toSSetObj₁Equiv : (a : toSSet.obj X _⦋1⦌) → I ⟶ X) e.edge, hom₀ := ⋯, hom₁ := ⋯ : X.Path x y })
      ((fun (p : X.Path x y) ↦ SSet.Edge.mk ((Equiv.symm toSSetObj₁Equiv : (a : I ⟶ X) → toSSet.obj X _⦋1⦌) p.hom) ⋯ ⋯)
        x_1) =
    x_1

Tactic:
aesop
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
x y : toSSet.obj X _⦋0⦌
e : SSet.Edge x y
obtain :
  ∀ (x : (↑X : Type u)) (e : SSet.Edge ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x) y),
    Eq (α := ZerothHomotopy (↑X : Type u))
      (Function.comp (α := toSSet.obj X _⦋0⦌) ZerothHomotopy.mk
        ((⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u)) : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
        ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x : toSSet.obj X _⦋0⦌))
      ((ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))) y)
⊢ Eq (α := ZerothHomotopy (↑X : Type u))
    ((ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))) x)
    ((ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))) y)

Tactic:
obtain ⟨x, rfl⟩ := toSSetObj₀Equiv.symm.surjective x

Premises used: TopCat.toSSetObj₀Equiv, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
y : toSSet.obj X _⦋0⦌
x : (↑X : Type u)
e : SSet.Edge ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x) y
obtain :
  ∀ (y : (↑X : Type u))
    (e :
      SSet.Edge (X := toSSet.obj X) ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x)
        ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) y)),
    Eq (α := ZerothHomotopy (↑X : Type u))
      (Function.comp (α := toSSet.obj X _⦋0⦌) ZerothHomotopy.mk
        ((⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u)) : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
        ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x : toSSet.obj X _⦋0⦌))
      (Function.comp (α := toSSet.obj X _⦋0⦌) ZerothHomotopy.mk
        ((⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u)) : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
        ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) y : toSSet.obj X _⦋0⦌))
⊢ Eq (α := ZerothHomotopy (↑X : Type u))
    (Function.comp (α := toSSet.obj X _⦋0⦌) ZerothHomotopy.mk
      ((⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u)) : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
      ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x : toSSet.obj X _⦋0⦌))
    ((ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))) y)

Tactic:
obtain ⟨y, rfl⟩ := toSSetObj₀Equiv.symm.surjective y

Premises used: TopCat.toSSetObj₀Equiv, Equiv.surjective, Equiv.symm, rfl
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
x y : (↑X : Type u)
e :
  SSet.Edge (X := toSSet.obj X) ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x)
    ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) y)
⊢ Eq (α := ZerothHomotopy (↑X : Type u))
    (Function.comp (α := toSSet.obj X _⦋0⦌) ZerothHomotopy.mk
      ((⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u)) : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
      ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x : toSSet.obj X _⦋0⦌))
    (Function.comp (α := toSSet.obj X _⦋0⦌) ZerothHomotopy.mk
      ((⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u)) : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
      ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) y : toSSet.obj X _⦋0⦌))

Tactic:
ZerothHomotopy.sound (pathEquiv (toSSetObjEdgeEquiv e))

Premises used: TopCat.pathEquiv, ZerothHomotopy.mk, DFunLike.coe, TopCat.toSSetObjEdgeEquiv, ZerothHomotopy.sound
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
x y : (↑X : Type u)
e :
  SSet.Edge (X := toSSet.obj X) ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x)
    ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) y)
⊢ Eq (α := ZerothHomotopy (↑X : Type u))
    (Function.comp (α := toSSet.obj X _⦋0⦌) ZerothHomotopy.mk
      ((⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u)) : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
      ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x : toSSet.obj X _⦋0⦌))
    (Function.comp (α := toSSet.obj X _⦋0⦌) ZerothHomotopy.mk
      ((⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u)) : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))
      ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) y : toSSet.obj X _⦋0⦌))

Tactic:
exact ZerothHomotopy.sound (pathEquiv (toSSetObjEdgeEquiv e))

Premises used: TopCat.pathEquiv, DFunLike.coe, TopCat.toSSetObjEdgeEquiv, ZerothHomotopy.sound
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
x : ZerothHomotopy (↑X : Type u)
mk :
  ∀ (x : (↑X : Type u)),
    Eq (α := ZerothHomotopy (↑X : Type u))
      (SSet.π₀.lift (X := toSSet.obj X)
        (ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))) ⋯
        (ZerothHomotopy.lift (SSet.π₀.mk ∘ (⇑(Equiv.symm toSSetObj₀Equiv) : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌)) ⋯
          (ZerothHomotopy.mk x)))
      (ZerothHomotopy.mk x)
⊢ SSet.π₀.lift (X := toSSet.obj X) (ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))) ⋯
      (ZerothHomotopy.lift (SSet.π₀.mk ∘ (⇑(Equiv.symm toSSetObj₀Equiv) : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌)) ⋯
        x) =
    x

Tactic:
induction x
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
x : (↑X : Type u)
⊢ Eq (α := ZerothHomotopy (↑X : Type u))
    (SSet.π₀.lift (X := toSSet.obj X) (ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u)))
      ⋯
      (ZerothHomotopy.lift (SSet.π₀.mk ∘ (⇑(Equiv.symm toSSetObj₀Equiv) : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌)) ⋯
        (ZerothHomotopy.mk x)))
    (ZerothHomotopy.mk x)

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
x : (toSSet.obj X).π₀
mk :
  ∀ (x : toSSet.obj X _⦋0⦌),
    ZerothHomotopy.lift (SSet.π₀.mk ∘ (⇑(Equiv.symm toSSetObj₀Equiv) : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌)) ⋯
        (SSet.π₀.lift (ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))) ⋯
          (SSet.π₀.mk x)) =
      SSet.π₀.mk x
⊢ ZerothHomotopy.lift (SSet.π₀.mk ∘ (⇑(Equiv.symm toSSetObj₀Equiv) : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌)) ⋯
      (SSet.π₀.lift (ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))) ⋯ x) =
    x

Tactic:
induction x
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
x : toSSet.obj X _⦋0⦌
⊢ ZerothHomotopy.lift (SSet.π₀.mk ∘ (⇑(Equiv.symm toSSetObj₀Equiv) : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌)) ⋯
      (SSet.π₀.lift (ZerothHomotopy.mk ∘ (⇑toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u))) ⋯
        (SSet.π₀.mk x)) =
    SSet.π₀.mk x

Tactic:
simp
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
x : (↑X : Type u)
⊢ Eq (α := (toSSet.obj X).π₀)
    ((zerothHomotopyEquiv : (a : ZerothHomotopy (↑X : Type u)) → (toSSet.obj X).π₀) (ZerothHomotopy.mk x) :
      (toSSet.obj X).π₀)
    (SSet.π₀.mk ((Equiv.symm toSSetObj₀Equiv : (a : (↑X : Type u)) → toSSet.obj X _⦋0⦌) x) : (toSSet.obj X).π₀)

Tactic:
rfl

Premises used: ZerothHomotopy.lift, SSet.π₀.mk, rfl
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
x : toSSet.obj X _⦋0⦌
⊢ Eq (α := ZerothHomotopy (↑X : Type u))
    ((Equiv.symm zerothHomotopyEquiv : (a : (toSSet.obj X).π₀) → ZerothHomotopy (↑X : Type u)) (SSet.π₀.mk x) :
      ZerothHomotopy (↑X : Type u))
    (ZerothHomotopy.mk ((toSSetObj₀Equiv : (a : toSSet.obj X _⦋0⦌) → (↑X : Type u)) x) : ZerothHomotopy (↑X : Type u))

Tactic:
rfl

Premises used: SSet.π₀.lift, ZerothHomotopy.mk, rfl
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
inst : PathConnectedSpace.{u} (↑X : Type u)
rw : Subsingleton.{u + 1} (ZerothHomotopy (↑X : Type u)) ∧ Nonempty.{u + 1} (ZerothHomotopy (↑X : Type u))
⊢ Nonempty.{u + 1} (Unique (ZerothHomotopy (↑X : Type u)))

Tactic:
rw [unique_iff_subsingleton_and_nonempty]

Premises used: unique_iff_subsingleton_and_nonempty
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
inst : PathConnectedSpace.{u} (↑X : Type u)
left : Subsingleton.{u + 1} (ZerothHomotopy (↑X : Type u))
right : Nonempty.{u + 1} (ZerothHomotopy (↑X : Type u))
⊢ Subsingleton.{u + 1} (ZerothHomotopy (↑X : Type u)) ∧ Nonempty.{u + 1} (ZerothHomotopy (↑X : Type u))

Tactic:
constructor
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
inst : PathConnectedSpace.{u} (↑X : Type u)
⊢ Subsingleton.{u + 1} (ZerothHomotopy (↑X : Type u))

Tactic:
infer_instance
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
inst : PathConnectedSpace.{u} (↑X : Type u)
⊢ Nonempty.{u + 1} (ZerothHomotopy (↑X : Type u))

Tactic:
infer_instance
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
inst : PathConnectedSpace.{u} (↑X : Type u)
this : Unique (ZerothHomotopy (↑X : Type u)) := Nonempty.some ⋯
rw : Nonempty.{u + 1} (Unique (toSSet.obj X).π₀)
⊢ SSet.IsConnected.{u} (toSSet.obj X)

Tactic:
rw [SSet.isConnected_iff_nonempty_unique]

Premises used: SSet.isConnected_iff_nonempty_unique
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
inst : PathConnectedSpace.{u} (↑X : Type u)
this : Unique (ZerothHomotopy (↑X : Type u)) := Nonempty.some ⋯
⊢ Nonempty.{u + 1} (Unique (toSSet.obj X).π₀)

Tactic:
⟨zerothHomotopyEquiv.symm.unique⟩

Premises used: TopCat.zerothHomotopyEquiv, Equiv.unique, Nonempty.intro, Equiv.symm
-- Module: Mathlib.Topology.Homotopy.TopCat.ZerothHomotopy
Goal:
X : TopCat
inst : PathConnectedSpace.{u} (↑X : Type u)
this : Unique (ZerothHomotopy (↑X : Type u)) := Nonempty.some ⋯
⊢ Nonempty.{u + 1} (Unique (toSSet.obj X).π₀)

Tactic:
exact ⟨zerothHomotopyEquiv.symm.unique⟩
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
mp : Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G) → ∀ᶠ (i : ι) in L, p i ↔ q
mpr : (∀ᶠ (i : ι) in L, p i ↔ q) → Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G)
⊢ Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G) ↔ ∀ᶠ (i : ι) in L, p i ↔ q

Tactic:
constructor
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G)
pos : ∀ (hq : q), ∀ᶠ (i : ι) in L, p i ↔ q
neg : ∀ (hq : ¬q), ∀ᶠ (i : ι) in L, p i ↔ q
⊢ ∀ᶠ (i : ι) in L, p i ↔ q

Tactic:
by_cases hq : q
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G)
hq : q
⊢ Tendsto (fun (i : ι) ↦ if p i then a else b) L F

Tactic:
simp only [hq, ite_true] at h

Premises used: ite_true
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : q
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L F
h₁ :
  ∀ (i : ι) (hi : Membership.mem (γ := Set ι) (Set.preimage (β := β) (fun (i : ι) ↦ if p i then a else b) {b}ᶜ) i),
    p i ↔ q
⊢ ∀ᶠ (i : ι) in L, p i ↔ q

Tactic:
filter_upwards [mem_map.mp (h hbF)] with i hi

Premises used: Iff.mp, Filter.mem_map
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : q
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L F
i : ι
hi : Membership.mem (γ := Set ι) (Set.preimage (β := β) (fun (i : ι) ↦ if p i then a else b) {b}ᶜ) i
⊢ p i ∧ ¬a = b

Tactic:
simp only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff,
        ite_eq_right_iff, not_forall, exists_prop] at hi

Premises used: exists_prop, Set.mem_singleton_iff, ite_eq_right_iff, Set.preimage_compl, Classical.not_forall, Set.mem_compl_iff, Set.mem_preimage
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : q
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L F
i : ι
hi : p i ∧ ¬a = b
h₁ h₂ : p i → ¬a = b → (p i ↔ q)
h₃ : p i → ¬a = b → p i → q
h₄ : p i → ¬a = b → q → p i
h₅ h₆ h₇ : p i → ¬a = b → p i → q
h₈ h₉ h₁₀ : p i → ¬a = b → q → p i
⊢ p i ↔ q

Tactic:
tauto
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L (if q then F else G)
hq : ¬q
⊢ Tendsto (fun (i : ι) ↦ if p i then a else b) L G

Tactic:
simp only [hq, ite_false] at h

Premises used: ite_false
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : ¬q
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L G
h₁ :
  ∀ (i : ι) (hi : Membership.mem (γ := Set ι) (Set.preimage (β := β) (fun (i : ι) ↦ if p i then a else b) {a}ᶜ) i),
    p i ↔ q
⊢ ∀ᶠ (i : ι) in L, p i ↔ q

Tactic:
filter_upwards [mem_map.mp (h haG)] with i hi

Premises used: Iff.mp, Filter.mem_map
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : ¬q
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L G
i : ι
hi : Membership.mem (γ := Set ι) (Set.preimage (β := β) (fun (i : ι) ↦ if p i then a else b) {a}ᶜ) i
⊢ ¬p i ∧ ¬b = a

Tactic:
simp only [Set.preimage_compl, Set.mem_compl_iff, Set.mem_preimage, Set.mem_singleton_iff,
        ite_eq_left_iff, not_forall, exists_prop] at hi

Premises used: ite_eq_left_iff, exists_prop, Set.mem_singleton_iff, Set.preimage_compl, Classical.not_forall, Set.mem_compl_iff, Set.mem_preimage
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
hq : ¬q
h : Tendsto (fun (i : ι) ↦ if p i then a else b) L G
i : ι
hi : ¬p i ∧ ¬b = a
h₁ h₂ : ¬p i → ¬b = a → (p i ↔ q)
h₃ : ¬p i → ¬b = a → p i → q
h₄ : ¬p i → ¬b = a → q → p i
h₅ : ¬p i → ¬b = a → p i → q
h₆ : ¬p i → ¬b = a → q → p i
⊢ p i ↔ q

Tactic:
tauto
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
h₁ : ∀ (i : ι) (hi : p i ↔ q), (if q then a else b) = if p i then a else b
⊢ EventuallyEq.{u_3, u_4} (β := β) L (fun (x : ι) ↦ if q then a else b) fun (i : ι) ↦ if p i then a else b

Tactic:
filter_upwards [h] with i hi
-- Module: Mathlib.Topology.IndicatorConstPointwise
Goal:
ι : Type u_3
L : Filter ι
β : Type u_4
p : ι → Prop
inst : DecidablePred p
q : Prop
inst_1 : Decidable q
a b : β
F G : Filter β
haG : {a}ᶜ ∈ G
hbF : {b}ᶜ ∈ F
haF : 𝓟 {a} ≤ F
hbG : 𝓟 {b} ≤ G
h : ∀ᶠ (i : ι) in L, p i ↔ q
i : ι
hi : p i ↔ q
⊢ (if q then a else b) = if p i then a else b

Tactic:
simp only [hi]