awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
h_fst :
  (ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)
h_snd :
  (ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)
⊢ ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI = TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I

Tactic:
apply CartesianMonoidalCategory.hom_ext

Premises used: CategoryTheory.CartesianMonoidalCategory.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
⊢ (ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.fst (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
Goal:
X : TopCat
⊢ (ι₁ ≫ TopCat.toSSet.obj X ◁ toSSetObjI) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I) =
    (TopCat.toSSet.map TopCat.ι₁ ≫ Functor.OplaxMonoidal.δ TopCat.toSSet X TopCat.I) ≫
      SemiCartesianMonoidalCategory.snd (TopCat.toSSet.obj X) (TopCat.toSSet.obj TopCat.I)

Tactic:
simp [← Functor.map_comp]

Premises used: CategoryTheory.Functor.map_comp
-- Module: Mathlib.AlgebraicTopology.SingularHomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
⊢ Functor.Additive (D := TopCat ⥤ ChainComplex.{v, u, 0} C ℕ)
    (SSet.chainComplexFunctor C ⋙
      Functor.obj (Functor.whiskeringLeft TopCat SSet (ChainComplex.{v, u, 0} C ℕ)) TopCat.toSSet)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SingularHomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
inst_3 : HasPullbacks.{v, u} C
X : C
X_1 Y : TopCat
f : X_1 ⟶ Y
h : Mono f
dsimp :
  Mono (C := ChainComplex.{v, u, 0} C ℕ) (X :=
    Functor.obj (alternatingFaceMapComplex C)
      (Functor.obj (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X))
        (TopCat.toSSet.obj X_1)))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C)
      (CategoryTheory.Functor.map (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X))
        (TopCat.toSSet.map f)))
⊢ Mono (C := ChainComplex.{v, u, 0} C ℕ) (X := Functor.obj (Functor.obj (singularChainComplexFunctor C) X) X_1)
    (CategoryTheory.Functor.map (Functor.obj (singularChainComplexFunctor C) X) f)

Tactic:
dsimp [singularChainComplexFunctor, SSet.chainComplexFunctor]

Premises used: SSet.chainComplexFunctor, AlgebraicTopology.singularChainComplexFunctor
-- Module: Mathlib.AlgebraicTopology.SingularHomology.Basic
Goal:
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasCoproducts.{w, v, u} C
inst_3 : Preadditive.{v, u} C
n : ℕ
inst_4 : HasPullbacks.{v, u} C
X : C
X_1 Y : TopCat
f : X_1 ⟶ Y
h : Mono f
inst :
  Mono (C := SimplicialObject.{v, u} C) (X :=
    Functor.obj (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X))
      (TopCat.toSSet.obj X_1))
    (CategoryTheory.Functor.map (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X))
      (TopCat.toSSet.map f))
⊢ Mono (C := ChainComplex.{v, u, 0} C ℕ) (X :=
    Functor.obj (alternatingFaceMapComplex C)
      (Functor.obj (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X))
        (TopCat.toSSet.obj X_1)))
    (CategoryTheory.Functor.map (alternatingFaceMapComplex C)
      (CategoryTheory.Functor.map (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X))
        (TopCat.toSSet.map f)))

Tactic:
apply +allowSynthFailures Functor.map_mono

Premises used: CategoryTheory.Functor.map_mono
-- Module: Mathlib.AlgebraicTopology.SingularHomology.Basic
Goal:
C : Type u
inst_1 : Category.{v, u} C
inst_2 : HasCoproducts.{w, v, u} C
inst_3 : Preadditive.{v, u} C
n : ℕ
inst_4 : HasPullbacks.{v, u} C
X : C
X_1 Y : TopCat
f : X_1 ⟶ Y
h : Mono f
inst :
  Functor.PreservesMonomorphisms (D := SimplicialObject.{v, u} C)
    (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X))
⊢ Mono (C := SimplicialObject.{v, u} C) (X :=
    Functor.obj (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X))
      (TopCat.toSSet.obj X_1))
    (CategoryTheory.Functor.map (Functor.obj (SimplicialObject.whiskering (Type w) C) (Functor.obj sigmaConst X))
      (TopCat.toSSet.map f))

Tactic:
apply +allowSynthFailures Functor.map_mono

Premises used: CategoryTheory.Functor.map_mono
-- Module: Mathlib.AlgebraicTopology.SingularHomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
inst_3 : HasPullbacks.{v, u} C
X : C
X_1 Y : TopCat
f : X_1 ⟶ Y
h : Mono f
⊢ Functor.PreservesMonomorphisms (C := SimplexCategoryᵒᵖ ⥤ Type w) (D :=
    CategoryTheory.Functor.{0, v, 0, u} SimplexCategoryᵒᵖ C)
    (Functor.obj (Functor.whiskeringRight SimplexCategoryᵒᵖ (Type w) C) (Functor.obj sigmaConst X))

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.SingularHomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
R : C
⊢ Eq.{v + 1} (α :=
    R ⟶
      sigmaObj.{w, v, u}
        fun
          (x :
            TopCat.toSSet.obj
                (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌) ↦
        R)
    (Sigma.ι.{w, v, u} (β :=
        TopCat.toSSet.obj (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌)
        (C := C)
        (fun
            (x :
              TopCat.toSSet.obj
                  (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌) ↦
          R)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (TopCat.toSSet.map (toTopSimplex.hom.app ⦋n⦌)) (Opposite.op ⦋n⦌)) :
              (a : TopCat.toSSet.obj (toTop.obj Δ[n]) _⦋n⦌) →
                TopCat.toSSet.obj
                    (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌)
            ((ConcreteCategory.hom (FC := TypeCat.Fun) (NatTrans.app (sSetTopAdj.unit.app Δ[n]) (Opposite.op ⦋n⦌)) :
                  (a : Δ[n] _⦋n⦌) → TopCat.toSSet.obj (toTop.obj Δ[n]) _⦋n⦌)
                ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) : Δ[n] _⦋n⦌) :
              TopCat.toSSet.obj (toTop.obj Δ[n]) _⦋n⦌) :
          TopCat.toSSet.obj (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌) :
      R ⟶
        sigmaObj.{w, v, u}
          fun
            (x :
              TopCat.toSSet.obj
                  (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌) ↦
          R)
    (Sigma.ι.{w, v, u} (β :=
        TopCat.toSSet.obj (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌)
        (C := C)
        (fun
            (x :
              TopCat.toSSet.obj
                  (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌) ↦
          R)
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
                (NatTrans.app (sSetTopAdj.unit.app Δ[n]) (Opposite.op ⦋n⦌) ≫
                  NatTrans.app (TopCat.toSSet.map (toTopSimplex.hom.app ⦋n⦌)) (Opposite.op ⦋n⦌)) :
              (a : Δ[n] _⦋n⦌) →
                TopCat.toSSet.obj
                    (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌)
            ((Equiv.symm stdSimplex.objEquiv : (a : ⦋n⦌ ⟶ ⦋n⦌) → Δ[n] _⦋n⦌) (𝟙 ⦋n⦌) : Δ[n] _⦋n⦌) :
          TopCat.toSSet.obj (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌) :
      R ⟶
        sigmaObj.{w, v, u}
          fun
            (x :
              TopCat.toSSet.obj
                  (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) _⦋n⦌) ↦
          R)

Tactic:
rfl
-- Module: Mathlib.AlgebraicTopology.SingularHomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
F : CategoryTheory.Functor.{w, v, w + 1, u} TopCat C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
⊢ Eq (α := F.obj (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) ⟶ F.obj X)
    (CategoryStruct.comp (Y :=
        sigmaObj.{w, v, u} fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦
          F.obj (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))))
        (Sigma.ι.{w, v, u} (C := C)
          (fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦
            F.obj (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))))
          i)
        (CategoryStruct.comp (Y := sigmaObj.{w, v, u} fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦ F.obj (toTop.obj Δ[n]))
          (Limits.Sigma.map fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦ F.map (toTopSimplex.inv.app ⦋n⦌))
          (𝟙 (sigmaObj.{w, v, u} fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦ F.obj (toTop.obj Δ[n])) ≫
            (𝟙 (sigmaObj.{w, v, u} fun (x : TopCat.toSSet.obj X _⦋n⦌) ↦ F.obj (toTop.obj Δ[n])) ≫
                (Sigma.desc fun (α : TopCat.toSSet.obj X _⦋n⦌) ↦
                    F.map
                      (toTop.map
                        ((Equiv.symm SSet.yonedaEquiv : (a : TopCat.toSSet.obj X _⦋n⦌) → Δ[n] ⟶ TopCat.toSSet.obj X)
                          α))) ≫
                  𝟙 (F.obj (toTop.obj (TopCat.toSSet.obj X)))) ≫
              (NatTrans.app (Adjunction.counit (Adjunction.whiskerLeft C sSetTopAdj)) F).app X)) :
      F.obj (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) ⟶ F.obj X)
    (F.map
        (toTopSimplex.inv.app ⦋n⦌ ≫
          toTop.map ((Equiv.symm SSet.yonedaEquiv : (a : TopCat.toSSet.obj X _⦋n⦌) → Δ[n] ⟶ TopCat.toSSet.obj X) i) ≫
            sSetTopAdj.counit.app X) :
      F.obj (TopCat.uliftFunctor.obj (TopCat.of (↑(_root_.stdSimplex ℝ (Fin (n + 1))) : Type))) ⟶ F.obj X)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SingularHomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
F : CategoryTheory.Functor.{w, v, w + 1, u} TopCat C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
e_a :
  toTopSimplex.inv.app ⦋n⦌ ≫
      toTop.map ((Equiv.symm SSet.yonedaEquiv : (a : TopCat.toSSet.obj X _⦋n⦌) → Δ[n] ⟶ TopCat.toSSet.obj X) i) ≫
        sSetTopAdj.counit.app X =
    i.down
⊢ F.map
      (toTopSimplex.inv.app ⦋n⦌ ≫
        toTop.map ((Equiv.symm SSet.yonedaEquiv : (a : TopCat.toSSet.obj X _⦋n⦌) → Δ[n] ⟶ TopCat.toSSet.obj X) i) ≫
          sSetTopAdj.counit.app X) =
    F.map i.down

Tactic:
congr 1
-- Module: Mathlib.AlgebraicTopology.SingularHomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
F : CategoryTheory.Functor.{w, v, w + 1, u} TopCat C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
e_a :
  ULift.down
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (sSetTopAdj.unit.app (TopCat.toSSet.obj X)) (Opposite.op ⦋n⦌)) :
            (a : TopCat.toSSet.obj X _⦋n⦌) → TopCat.toSSet.obj (toTop.obj (TopCat.toSSet.obj X)) _⦋n⦌)
          i) ≫
      sSetTopAdj.counit.app X =
    i.down
⊢ toTopSimplex.inv.app ⦋n⦌ ≫
      toTop.map ((Equiv.symm SSet.yonedaEquiv : (a : TopCat.toSSet.obj X _⦋n⦌) → Δ[n] ⟶ TopCat.toSSet.obj X) i) ≫
        sSetTopAdj.counit.app X =
    i.down

Tactic:
rw [← reassoc_of% sSetTopAdj_unit_app_app_down]

Premises used: sSetTopAdj_unit_app_app_down
-- Module: Mathlib.AlgebraicTopology.SingularHomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
F : CategoryTheory.Functor.{w, v, w + 1, u} TopCat C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
⊢ ULift.down
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (sSetTopAdj.unit.app (TopCat.toSSet.obj X)) (Opposite.op ⦋n⦌)) :
            (a : TopCat.toSSet.obj X _⦋n⦌) → TopCat.toSSet.obj (toTop.obj (TopCat.toSSet.obj X)) _⦋n⦌)
          i) ≫
      sSetTopAdj.counit.app X =
    i.down

Tactic:
congr(($(sSetTopAdj.right_triangle_components X).app (.op ⦋n⦌) i).down)

Premises used: congrArg, CategoryTheory.ConcreteCategory.hom, id, SimplexCategory.mk, Opposite.op, sSetTopAdj, CategoryTheory.Adjunction.right_triangle_components, DFunLike.coe, ULift.down, CategoryTheory.NatTrans.app
-- Module: Mathlib.AlgebraicTopology.SingularHomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
F : CategoryTheory.Functor.{w, v, w + 1, u} TopCat C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
⊢ ULift.down
        ((ConcreteCategory.hom (FC := TypeCat.Fun)
              (NatTrans.app (sSetTopAdj.unit.app (TopCat.toSSet.obj X)) (Opposite.op ⦋n⦌)) :
            (a : TopCat.toSSet.obj X _⦋n⦌) → TopCat.toSSet.obj (toTop.obj (TopCat.toSSet.obj X)) _⦋n⦌)
          i) ≫
      sSetTopAdj.counit.app X =
    i.down

Tactic:
exact congr(($(sSetTopAdj.right_triangle_components X).app (.op ⦋n⦌) i).down)
-- Module: Mathlib.AlgebraicTopology.SingularHomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
R : C
X : TopCat
inst_3 : TotallyDisconnectedSpace.{w} (↑X : Type w)
hn : n ≠ 0
⊢ HomologicalComplex.ExactAt.{v, u, 0} (Functor.obj (Functor.obj (singularChainComplexFunctor C) R) X) n

Tactic:
have := hasCoproducts_shrink.{0, w} (C := C)
  have : HasZeroObject C := ⟨_, initialIsInitial.isZero⟩
  .of_iso (ChainComplex.alternatingConst_exactAt _ _ hn)
    (singularChainComplexFunctorIsoOfTotallyDisconnectedSpace C R X).symm

Premises used: HomologicalComplex.ExactAt.of_iso, CategoryTheory.Limits.HasZeroObject.mk, CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.IsInitial.isZero, Exists.intro, CategoryTheory.Iso.symm, CategoryTheory.Limits.hasCoproducts_shrink, ChainComplex.alternatingConst_exactAt, AlgebraicTopology.singularChainComplexFunctorIsoOfTotallyDisconnectedSpace, CategoryTheory.Limits.sigmaObj, CategoryTheory.Limits.initial
-- Module: Mathlib.AlgebraicTopology.SingularHomology.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
n : ℕ
R : C
X : TopCat
inst_3 : TotallyDisconnectedSpace.{w} (↑X : Type w)
inst_4 : CategoryWithHomology.{v, u} C
hn : n ≠ 0
⊢ IsZero.{v, u} (Functor.obj.{w, v, w + 1, u} (Functor.obj (singularHomologyFunctor C n) R) X)

Tactic:
have := hasCoproducts_shrink.{0, w} (C := C)
  have : HasZeroObject C := ⟨_, initialIsInitial.isZero⟩
  (singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace C n R X hn).isZero_homology

Premises used: AlgebraicTopology.singularChainComplexFunctor_exactAt_of_totallyDisconnectedSpace, Set.Mem, CategoryTheory.Limits.HasZeroObject.mk, CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.IsInitial.isZero, CategoryTheory.ShortComplex.homology, Exists.intro, CategoryTheory.Limits.hasCoproducts_shrink, HomologicalComplex.ExactAt.isZero_homology, HomologicalComplex.homology, CategoryTheory.Limits.initial
-- Module: Mathlib.AlgebraicTopology.SingularHomology.HomologyZero
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasCoproducts.{w, v, u} C
inst_2 : Preadditive.{v, u} C
inst_3 : CategoryWithHomology.{v, u} C
X : TopCat
R : C
inst_4 : PathConnectedSpace.{w} (↑X : Type w)
⊢ IsIso.{v, u} (X := Functor.obj.{w, v, w + 1, u} (Functor.obj (singularHomologyFunctor C 0) R) X)
    (X.singularHomology₀ε R)

Tactic:
inferInstanceAs (IsIso ((toSSet.obj X).homology₀ε R))

Premises used: _private.0.TopCat.instIsIsoSingularHomology₀εOfPathConnectedSpaceCarrier._proof_1
-- Module: Mathlib.AlgebraicTopology.SingularHomology.HomotopyInvariance
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : Preadditive.{v, u} C
inst_2 : HasCoproducts.{w, v, u} C
X Y : TopCat
f g : X ⟶ Y
inst_3 : CategoryWithHomology.{v, u} C
H : Homotopy f g
R : C
n : ℕ
⊢ Eq.{v + 1} (α :=
    homology.{v, u, 0} (Functor.obj (Functor.obj (singularChainComplexFunctor C) R) X) n ⟶
      homology.{v, u, 0} (Functor.obj (Functor.obj (singularChainComplexFunctor C) R) Y) n)
    (homologyMap (CategoryTheory.Functor.map (Functor.obj (singularChainComplexFunctor C) R) f) n)
    (homologyMap (CategoryTheory.Functor.map (Functor.obj (singularChainComplexFunctor C) R) g) n)

Tactic:
(H.singularChainComplexFunctorObjMap R).homologyMap_eq n

Premises used: Homotopy.homologyMap_eq, TopCat.Homotopy.singularChainComplexFunctorObjMap
-- Module: Mathlib.AlgebraicTopology.SingularSet
Goal:
⊢ SSet.toTop.IsLeftAdjoint

Tactic:
sSetTopAdj.isLeftAdjoint

Premises used: sSetTopAdj, CategoryTheory.Adjunction.isLeftAdjoint
-- Module: Mathlib.AlgebraicTopology.SingularSet
Goal:
⊢ TopCat.toSSet.IsRightAdjoint

Tactic:
sSetTopAdj.isRightAdjoint

Premises used: CategoryTheory.Adjunction.isRightAdjoint, sSetTopAdj
-- Module: Mathlib.AlgebraicTopology.SingularSet
Goal:
⊢ SSet.toTop.IsLeftKanExtension SSet.toTopSimplex.inv

Tactic:
inferInstanceAs (Functor.IsLeftKanExtension _
    (SSet.stdSimplex.{u}.leftKanExtensionUnit SimplexCategory.toTop.{u}))

Premises used: _private.0.instIsLeftKanExtensionSimplexCategoryTopCatSSetToTopInvFunctorToTopSimplex._proof_1
-- Module: Mathlib.AlgebraicTopology.SingularSet
Goal:
S : SSet
m : SimplexCategoryᵒᵖ
a : S.obj m
cat_disch cat_disch₁ cat_disch₂ cat_disch₃ :
  Eq (α := Functor.obj (Functor.obj yoneda (SSet.toTop.obj S)) (SimplexCategory.toTop.{u_1}.op.obj m))
    (ULift.down
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((sSetTopAdj.unit.app S).app m) :
          (a : (fun (X : Type u_1) ↦ X) (((𝟭 SSet).obj S).obj m)) →
            (fun (X : Type u_1) ↦ X) (((SSet.toTop ⋙ TopCat.toSSet).obj S).obj m))
        a))
    (SSet.toTopSimplex.inv.app (Opposite.unop m) ≫
      SSet.toTop.map
        ((Equiv.symm SSet.yonedaEquiv :
            (a : S.obj (Opposite.op (Opposite.unop m))) → SSet.stdSimplex.obj (Opposite.unop m) ⟶ S)
          a))
⊢ Eq (α := Functor.obj (Functor.obj yoneda (SSet.toTop.obj S)) (SimplexCategory.toTop.{u_1}.op.obj m))
    (ULift.down
      ((ConcreteCategory.hom (FC := TypeCat.Fun) ((sSetTopAdj.unit.app S).app m) :
          (a : (fun (X : Type u_1) ↦ X) (((𝟭 SSet).obj S).obj m)) →
            (fun (X : Type u_1) ↦ X) (((SSet.toTop ⋙ TopCat.toSSet).obj S).obj m))
        a))
    (SSet.toTopSimplex.inv.app (Opposite.unop m) ≫
      SSet.toTop.map
        ((Equiv.symm SSet.yonedaEquiv :
            (a : S.obj (Opposite.op (Opposite.unop m))) → SSet.stdSimplex.obj (Opposite.unop m) ⟶ S)
          a))

Tactic:
cat_disch
-- Module: Mathlib.AlgebraicTopology.TopologicalSimplex
Goal:
n : SimplexCategory
⊢ Nonempty (↑(stdSimplex ℝ (Fin (n.len + 1))) : Type)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.TopologicalSimplex
Goal:
n : SimplexCategory
⊢ Nonempty.{u + 1} (↑(toTop.{u}.obj n) : Type u)

Tactic:
inferInstanceAs (Nonempty (ULift _))

Premises used: _private.0.SimplexCategory.instNonemptyCarrierObjTopCatToTop._proof_1
-- Module: Mathlib.AlgebraicTopology.TopologicalSimplex
Goal:
n : SimplexCategory
⊢ PathConnectedSpace (↑(stdSimplex ℝ (Fin (n.len + 1))) : Type)

Tactic:
infer_instance
-- Module: Mathlib.AlgebraicTopology.TopologicalSimplex
Goal:
n : SimplexCategory
⊢ PathConnectedSpace.{u} (↑(toTop.{u}.obj n) : Type u)

Tactic:
ULift.up_surjective.pathConnectedSpace continuous_uliftUp

Premises used: continuous_uliftUp, Function.Surjective.pathConnectedSpace, ULift.up_surjective
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : PartialOrder S
v : AbsoluteValue R S
⊢ v.IsEquiv v

Tactic:
fun _ _ ↦ .rfl

Premises used: Iff.rfl, AbsoluteValue.IsEquiv
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : PartialOrder S
v w : AbsoluteValue R S
h : v.IsEquiv w
⊢ w.IsEquiv v

Tactic:
fun _ _ ↦ (h _ _).symm

Premises used: Iff.symm, AbsoluteValue.IsEquiv
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : PartialOrder S
v w u : AbsoluteValue R S
h₁ : v.IsEquiv w
h₂ : w.IsEquiv u
⊢ v.IsEquiv u

Tactic:
fun _ _ ↦ (h₁ _ _).trans (h₂ _ _)

Premises used: Iff.trans, AbsoluteValue.IsEquiv
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : PartialOrder S
v w : AbsoluteValue R S
h : v.IsEquiv w
x y : R
⊢ LE.le.{u_2} (α := S) ((v : (a : R) → S) x : S) ((v : (a : R) → S) y : S) ↔
    LE.le.{u_2} (α := S) ((w : (a : R) → S) x : S) ((w : (a : R) → S) y : S)

Tactic:
h ..
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : PartialOrder S
v w : AbsoluteValue R S
h : v.IsEquiv w
x y : R
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) ((v : (a : R) → S) y : S) ↔
    LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) ((w : (a : R) → S) y : S)

Tactic:
lt_iff_lt_of_le_iff_le' (h y x) (h x y)

Premises used: lt_iff_lt_of_le_iff_le'
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : PartialOrder S
v w : AbsoluteValue R S
h : v.IsEquiv w
x y : R
⊢ Eq.{u_2 + 1} (α := S) ((v : (a : R) → S) x : S) ((v : (a : R) → S) y : S) ↔
    Eq.{u_2 + 1} (α := S) ((w : (a : R) → S) x : S) ((w : (a : R) → S) y : S)

Tactic:
simp [le_antisymm_iff, h x y, h y x]

Premises used: le_antisymm_iff
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : PartialOrder S
v w : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : Nontrivial R
h : v.IsEquiv w
x : R
⊢ LT.lt.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ LT.lt.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)

Tactic:
simpa only [map_one] using h.lt_iff_lt (y := 1)

Premises used: AbsoluteValue.IsEquiv.lt_iff_lt, map_one
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : PartialOrder S
v w : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : Nontrivial R
h : v.IsEquiv w
x : R
⊢ LT.lt.{u_2} (α := S) (1 : S) ((v : (a : R) → S) x : S) ↔ LT.lt.{u_2} (α := S) (1 : S) ((w : (a : R) → S) x : S)

Tactic:
simpa only [map_one] using h.lt_iff_lt (x := 1)

Premises used: AbsoluteValue.IsEquiv.lt_iff_lt, map_one
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : PartialOrder S
v w : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : Nontrivial R
h : v.IsEquiv w
x : R
⊢ LE.le.{u_2} (α := S) ((v : (a : R) → S) x : S) (1 : S) ↔ LE.le.{u_2} (α := S) ((w : (a : R) → S) x : S) (1 : S)

Tactic:
simpa only [map_one] using h x 1

Premises used: map_one, OfNat.ofNat
-- Module: Mathlib.Analysis.AbsoluteValue.Equivalence
Goal:
R : Type u_1
inst : Semiring R
S : Type u_2
inst_1 : Semiring S
inst_2 : PartialOrder S
v w : AbsoluteValue R S
inst_3 : IsDomain S
inst_4 : Nontrivial R
h : v.IsEquiv w
x : R
⊢ LE.le.{u_2} (α := S) (1 : S) ((v : (a : R) → S) x : S) ↔ LE.le.{u_2} (α := S) (1 : S) ((w : (a : R) → S) x : S)

Tactic:
simpa only [map_one] using h 1 x

Premises used: map_one, OfNat.ofNat