mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
F : SSet ⥤ C
⊢ { app := fun R ↦ Sigma.ι (fun x ↦ R) (stdSimplex.objEquiv.symm (𝟙 ⦋n⦌)), naturality := ⋯ }.app
        (((evaluation SSet C).obj Δ[n]).obj F) ≫
      ((evaluation SSet C).obj Δ[n]).map
        ({ app := fun F ↦ { app := fun S ↦ Sigma.desc fun α ↦ F.map (yonedaEquiv.symm α), naturality := ⋯ },
              naturality := ⋯ }.app
          F) =
    𝟙 (((evaluation SSet C).obj Δ[n]).obj F)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n + 1⦌
⊢ X.ιChainComplex x ≫ (X.chainComplex R).d (n + 1) n =
    ∑ i, (-1) ^ ↑i • X.ιChainComplex ((ConcreteCategory.hom (SimplicialObject.δ X i)) x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X Y : SSet
f : X ⟶ Y
R : C
n : ℕ
x : X _⦋n⦌
⊢ X.ιChainComplex x ≫ (chainComplexMap f R).f n = Y.ιChainComplex ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
X : SSet
R : C
inst✝ : CategoryWithHomology C
n : ℕ
⊢ SSet.homologyMap (𝟙 X) R n = 𝟙 (X.homology R n)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj X₂)
inst✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj Y₂)
h : IsInitial X₁
⊢ IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) (𝟙 ((F.obj Y₁).obj X₂))
    ((IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h).to ((F.obj Y₁).obj X₂))

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Basic

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
X Y Z : SSet
f : X ⟶ Y
g : Y ⟶ Z
R : C
inst✝ : CategoryWithHomology C
n : ℕ
⊢ SSet.homologyMap (f ≫ g) R n = SSet.homologyMap f R n ≫ SSet.homologyMap g R n

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
i : Fin (d + 1 + 1)
hx : IsIndex x ⋯ i
⊢ i ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty

Goal state before:
pp: X : SSet
inst✝ : X.Nonempty
⊢ Classical.arbitrary (X _⦋0⦌) ∈ X.nonDegenerate 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty

Goal state before:
pp: X : SSet
x✝ : X.HasDimensionLT 0
x : X _⦋0⦌
⊢ x ∈ X.nonDegenerate 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty

Goal state before:
pp: X : SSet
⊢ ¬X.Nonempty ↔ X.HasDimensionLT 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty

Goal state before:
pp: X : SSet
hX : IsEmpty (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty (X.obj n)
x✝³ : SSet
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (X.map x✝ ≫ ↾fun x ↦ isEmptyElim x) = (↾fun x ↦ isEmptyElim x) ≫ x✝³.map x✝

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty

Goal state before:
pp: X : SSet
hX : IsEmpty (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty (X.obj n)
x✝¹ : SSet
x✝ : X ⟶ x✝¹
⊢ x✝ = { app := fun x ↦ ↾fun x_1 ↦ isEmptyElim x_1, naturality := ⋯ }

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty

Goal state before:
pp: X : SSet
hX : ¬X.Nonempty
⊢ IsInitial X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero

Goal state before:
pp: X : SSet
motive : X.π₀ → Prop
mk : ∀ (x : X _⦋0⦌), motive (π₀.mk x)
x : X.π₀
⊢ motive x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero

Goal state before:
pp: X Y Z : SSet
T : Type u_1
f : X _⦋0⦌ → T
hf : ∀ ⦃x₀ x₁ : X _⦋0⦌⦄ (x : Edge x₀ x₁), f x₀ = f x₁
⊢ ∀ (a b : X _⦋0⦌), π₀Rel a b → f a = f b

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero

Goal state before:
pp: X : SSet
x : X.π₀
⊢ mapπ₀ (𝟙 X) x = x

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero

Goal state before:
pp: X Y Z : SSet
f : X ⟶ Y
g : Y ⟶ Z
x : X.π₀
⊢ mapπ₀ (f ≫ g) x = mapπ₀ g (mapπ₀ f x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero

Goal state before:
pp: X Y Z : SSet
⊢ SimplicialObject.δ X 1 ≫ ↾π₀.mk = SimplicialObject.δ X 0 ≫ ↾π₀.mk

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero

Goal state before:
pp: X Y Z : SSet
s : Cofork (SimplicialObject.δ X 1) (SimplicialObject.δ X 0)
x₀ x₁ : X _⦋0⦌
e : Edge x₀ x₁
⊢ (ConcreteCategory.hom s.π) x₀ = (ConcreteCategory.hom s.π) x₁

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero

Goal state before:
pp: X Y Z : SSet
s : Cofork (SimplicialObject.δ X 1) (SimplicialObject.δ X 0)
m : coforkπ₀.pt ⟶ s.pt
hm : coforkπ₀.π ≫ m = s.π
⊢ m = ↾π₀.lift ⇑(ConcreteCategory.hom s.π) ⋯

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero

Goal state before:
pp: X Y Z : SSet
⊢ SSet.evaluation.map (SimplexCategory.δ 1).op ≫ toπ₀NatTrans =
    SSet.evaluation.map (SimplexCategory.δ 0).op ≫ toπ₀NatTrans

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
        (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom) ≫
      pushout.desc ((initialIsInitial.ofIso (zeroMul initialIsInitial).symm).to X.left) (ρ_ X.left).hom ⋯ ≫
        (ρ_ X.left).inv ≫
          pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
            (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom) =
    pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
        (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom) ≫
      𝟙 (X □ Arrow.mk (initial.to (𝟙_ C))).left

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero

Goal state before:
pp: X : SSet
x✝ : X.IsPreconnected ∧ X.Nonempty
left✝ : X.IsPreconnected
right✝ : X.Nonempty
⊢ X.Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.PiZero

Goal state before:
pp: X : SSet
⊢ X.IsConnected ↔ Nonempty (Unique X.π₀)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
⊢ ∃ s,
    x.toS = { dim := s.d + 1, simplex := (s.x.cast ⋯).simplex } ∨
      x.toS =
        { dim := s.d,
          simplex :=
            (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) s.index.castSucc)) (s.x.cast ⋯).simplex }

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj X₁)
inst✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.obj Y₁)
h : IsInitial X₂
⊢ IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) ((IsInitial.isInitialObj (F.obj Y₁) X₂ h).to ((F.obj X₁).obj Y₂))
    (𝟙 ((F.obj X₁).obj Y₂))

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁✝ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝ f₂✝
f₁ f₁' : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ (F.map f₁.hom).app f₂.left ≫ (F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
        (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom) ≫
      { hom := pushout.desc ((initialIsInitial.ofIso (zeroMul initialIsInitial).symm).to X.left) (ρ_ X.left).hom ⋯,
            inv :=
              (ρ_ X.left).inv ≫
                pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
                  (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom),
            hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        X.hom =
    pushout.inr (((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left)
        (((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom) ≫
      (X □ Arrow.mk (initial.to (𝟙_ C))).hom ≫ (ρ_ X.right).hom

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ (X □ Arrow.mk (initial.to (𝟙_ C))) ≅ X

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
x : X _⦋0⦌
⊢ X.ιChainComplex x ≫ fromChainComplexXZero X R = Sigma.ι (fun x ↦ R) (mk x)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPullbacks C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalClosed C
X : Arrow C
T : C
t : IsTerminal T
W : C
this✝ : IsIso ((MonoidalClosed.pre X.hom).app T)
this :
  IsPullback (𝟙 (X.left ⟹ W)) ((IsTerminal.isTerminalObj (ihom X.right) T t).from (X.left ⟹ W))
    ((ihom X.left).map (t.from W)) ((MonoidalClosed.pre X.hom).app T)
⊢ (((Iso.refl
              ((MonoidalClosed.internalHom.obj (Opposite.op (Opposite.unop (Opposite.op X)).right)).obj
                (Arrow.mk (t.from W)).left)).hom ≫
          (MonoidalClosed.pre X.hom).app W) ≫
        this.isoPullback.hom) ≫
      pullback.fst ((ihom X.left).map (t.from W)) ((MonoidalClosed.pre X.hom).app T) =
    (PullbackObjObj.ofHasPullback MonoidalClosed.internalHom (Opposite.unop (Opposite.op X)).hom
          (Arrow.mk (t.from W)).hom).π ≫
      pullback.fst ((ihom X.left).map (t.from W)) ((MonoidalClosed.pre X.hom).app T)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
hn : n ≠ 1
⊢ ¬(ComplexShape.down ℕ).Rel n 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPullbacks C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
X : Arrow C
I : C
i : IsInitial I
W : C
this✝ : IsIso ((ihom I).map X.hom)
this :
  IsPullback ((isTerminalTensorUnit.ofIso (powZero i).symm).from (W ⟹ X.right)) (𝟙 (W ⟹ X.right)) ((ihom I).map X.hom)
    ((MonoidalClosed.pre (i.to W)).app X.right)
⊢ (((Iso.refl
              ((MonoidalClosed.internalHom.obj
                    (Opposite.op (Opposite.unop (Opposite.op (Arrow.mk (i.to W)))).right)).obj
                X.left)).hom ≫
          (ihom W).map X.hom) ≫
        this.isoPullback.hom) ≫
      pullback.snd ((ihom I).map X.hom) ((MonoidalClosed.pre (i.to W)).app X.right) =
    (PullbackObjObj.ofHasPullback MonoidalClosed.internalHom (Opposite.unop (Opposite.op (Arrow.mk (i.to W)))).hom
          X.hom).π ≫
      pullback.snd ((ihom I).map X.hom) ((MonoidalClosed.pre (i.to W)).app X.right)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
⊢ (X.chainComplex R).d n 0 ≫ fromChainComplexXZero X R = 0

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁✝ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝ f₂✝
f₁ f₁' : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ (𝟭 C₃).map
        (⋯.desc ((F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl)
          ((F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr) ⋯) ≫
      (Arrow.mk sq₁₂'.ι).hom =
    (Arrow.mk sq₁₂.ι).hom ≫ (𝟭 C₃).map ((F.map (Arrow.Hom.right sq)).app f₂.right)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ (parallelPair ((sigmaConst.obj R).map (SimplicialObject.δ X 1) - (sigmaConst.obj R).map (SimplicialObject.δ X 0))
            0).map
        WalkingParallelPairHom.right ≫
      (Iso.refl
          ((parallelPair
                ((sigmaConst.obj R).map (SimplicialObject.δ X 1) - (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                0).obj
            WalkingParallelPair.one)).hom =
    (-Iso.refl
            ((parallelPair
                  ((sigmaConst.obj R).map (SimplicialObject.δ X 1) - (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                  0).obj
              WalkingParallelPair.zero)).hom ≫
      (parallelPair ((X.chainComplex R).d 1 0) 0).map WalkingParallelPairHom.right

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
f₁ : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
⊢ sq₁₂.mapArrowLeft sq₁₂ (𝟙 f₁) = 𝟙 (Arrow.mk sq₁₂.ι)

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
f₁ f₁' : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
f₁'' : Arrow C₁
sq₁₂'' : F.PushoutObjObj f₁''.hom f₂.hom
sq : f₁ ⟶ f₁'
sq' : f₁' ⟶ f₁''
⊢ sq₁₂.mapArrowLeft sq₁₂' sq ≫ sq₁₂'.mapArrowLeft sq₁₂'' sq' = sq₁₂.mapArrowLeft sq₁₂'' (sq ≫ sq')

Tactic:
by

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝² : Category.{v₁, u₁} C₁
inst✝¹ : Category.{v₂, u₂} C₂
inst✝ : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁✝¹ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂✝¹ : X₂ ⟶ Y₂
sq✝ : F.PushoutObjObj f₁✝¹ f₂✝¹
f₁✝ f₁' : Arrow C₁
f₂✝ : Arrow C₂
sq₁₂✝ : F.PushoutObjObj f₁✝.hom f₂✝.hom
sq₁₂'✝ : F.PushoutObjObj f₁'.hom f₂✝.hom
f₁ : Arrow C₁
f₂ f₂' : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
⊢ (F.map f₁.hom).app f₂.left ≫ (F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ IsColimit (CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ (HomologicalComplex.sc' (X.chainComplex R) 1 0 0).g = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin ((Opposite.unop (Opposite.op ⦋n⦌)).len + 1)
h : j₁ ≤ j₂
⊢ (fun j ↦ if j.castSucc < i then 0 else 1) j₁ ≤ (fun j ↦ if j.castSucc < i then 0 else 1) j₂

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R T : C
f : T ⟶ (X.chainComplex R).X 0
⊢ f ≫ (HomologicalComplex.sc' (X.chainComplex R) 1 0 0).g = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : i ≤ j.castSucc
⊢ (ConcreteCategory.hom (SimplicialObject.δ Δ[1] j)) (objMk₁ i) = objMk₁ (i.castPred ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
X : SSet
R : C
inst✝ : CategoryWithHomology C
⊢ (ComplexShape.down ℕ).prev 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : j.castSucc < i
⊢ (ConcreteCategory.hom (SimplicialObject.δ Δ[1] j)) (objMk₁ i) = objMk₁ (i.pred ⋯)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
X : SSet
R : C
inst✝ : CategoryWithHomology C
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
X : SSet
R : C
inst✝ : CategoryWithHomology C
x : X _⦋0⦌
⊢ (ComplexShape.down ℕ).next 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
⊢ (ConcreteCategory.hom (SimplicialObject.σ Δ[1] j)) (objMk₁ i) = objMk₁ i.castSucc

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
X : SSet
R : C
inst✝ : CategoryWithHomology C
x : X _⦋0⦌
⊢ X.ιChainComplex x ≫ (X.chainComplex R).d 0 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
X : SSet
R : C
inst✝ : CategoryWithHomology C
x : X _⦋0⦌
⊢ HomologicalComplex.liftCycles (X.chainComplex R) (X.ιChainComplex x) 0
        liftCycles_ιChainComplex_homologyπ_homology₀Iso_hom._proof_1 ⋯ ≫
      HomologicalComplex.homologyπ (X.chainComplex R) 0 ≫ (X.homology₀Iso R).hom =
    Sigma.ι (fun x ↦ R) (π₀.mk x)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplexOne

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
⊢ (ConcreteCategory.hom (SimplicialObject.σ Δ[1] j)) (objMk₁ i) = objMk₁ i.succ

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasCoproducts C
inst✝¹ : Preadditive C
X : SSet
R : C
inst✝ : CategoryWithHomology C
x : X _⦋0⦌
⊢ HomologicalComplex.liftCycles (X.chainComplex R) (X.ιChainComplex x) 0
        liftCycles_ιChainComplex_homologyπ_homology₀Iso_hom._proof_1 ⋯ ≫
      HomologicalComplex.homologyπ (X.chainComplex R) 0 ≫ X.homology₀ε R =
    𝟙 R

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCoproducts C
inst✝² : Preadditive C
X : SSet
R : C
inst✝¹ : CategoryWithHomology C
inst✝ : X.IsConnected
x : X.π₀ := Classical.arbitrary X.π₀
⊢ (Sigma.ι (fun x ↦ R) x ≫ Sigma.desc fun x ↦ 𝟙 R) = 𝟙 R

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCoproducts C
inst✝² : Preadditive C
X : SSet
R : C
inst✝¹ : CategoryWithHomology C
inst✝ : X.IsConnected
x : X.π₀ := Classical.arbitrary X.π₀
y : X.π₀
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasCoproducts C
inst✝² : Preadditive C
X : SSet
R : C
inst✝¹ : CategoryWithHomology C
inst✝ : X.IsConnected
⊢ IsIso (X.homology₀ε R)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d✝ m : ℕ
k : Fin (m + 1)
n d : ℕ
is it : Fin (d + 1)
s : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
hs₁ : s ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
hs₂ : s ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
hs : IsIndex (Subcomplex.N.mk s hs₁ hs₂) ⋯ is.succ
t : (Δ[m + 1] ⊗ Δ[n]) _⦋d + 1⦌
ht₁ : t ∈ (Δ[m + 1] ⊗ Δ[n]).nonDegenerate (d + 1)
ht₂ : t ∉ (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).obj (Opposite.op ⦋d + 1⦌)
ht : IsIndex (Subcomplex.N.mk t ht₁ ht₂) ⋯ it.succ
h₂ :
  (pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs } <
    (pairingCore k n).type₁ { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }
h₁ : ¬Subcomplex.N.mk s hs₁ hs₂ = Subcomplex.N.mk t ht₁ ht₂
i : Fin (d + 2)
hf : Mono (SimplexCategory.δ i)
hδ :
  (ConcreteCategory.hom ((Δ[m + 1] ⊗ Δ[n]).map (SimplexCategory.δ i).op))
      ((pairingCore k n).type₁
          { x := Subcomplex.N.mk t ht₁ ht₂, d := d, hd := ⋯, index := it, isIndex := ht }).simplex =
    ((pairingCore k n).type₂ { x := Subcomplex.N.mk s hs₁ hs₂, d := d, hd := ⋯, index := is, isIndex := hs }).simplex
⊢ { dim := hs.δ.dim, simplex := hs.δ.simplex } =
    { dim := d,
      simplex :=
        (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) ((Subcomplex.N.mk t ht₁ ht₂).cast ⋯).simplex }

Tactic:
by

Goal state after: