mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case pos
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
hx : IsType₂ x
⊢ ∃ 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 }

pp: case neg
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
hx : ¬IsType₂ x
⊢ ∃ 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:
·

Goal state after:
case pos
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
hx : IsType₂ x
⊢ ∃ 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 }
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_1
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))).left ≅ X.left

pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ Iso.hom ?refine_1 ≫ X.hom = (X □ Arrow.mk (initial.to (𝟙_ C))).hom ≫ (ρ_ X.right).hom

Tactic:
·

Goal state after:
case refine_1
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))).left ≅ X.left
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case neg
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
hx : ¬IsType₂ x
⊢ ∃ 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:
·

Goal state after:
case neg
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
hx : ¬IsType₂ x
⊢ ∃ 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 }
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case inst
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₁
hX₂ : IsInitial ((F.flip.obj X₂).obj X₁) := ⋯
hY₂ : IsInitial ((F.flip.obj Y₂).obj X₁) := ⋯
⊢ IsIso ((F.obj X₁).map f₂)

pp: case sq
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₁
hX₂ : IsInitial ((F.flip.obj X₂).obj X₁) := ⋯
hY₂ : IsInitial ((F.flip.obj Y₂).obj X₁) := ⋯
⊢ CommSq ((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:
·

Goal state after:
case inst
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₁
hX₂ : IsInitial ((F.flip.obj X₂).obj X₁) := ⋯
hY₂ : IsInitial ((F.flip.obj Y₂).obj X₁) := ⋯
⊢ IsIso ((F.obj X₁).map f₂)
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_1.refine_1
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))).left ⟶ X.left

pp: case refine_1.refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ ?refine_1.refine_1 ≫
      (ρ_ 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) =
    𝟙 (X □ Arrow.mk (initial.to (𝟙_ C))).left

pp: case refine_1.refine_3
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ ((ρ_ 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)) ≫
      ?refine_1.refine_1 =
    𝟙 X.left

Tactic:
·

Goal state after:
case refine_1.refine_1
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))).left ⟶ X.left
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case neg.zero
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
hd : x.dim = 0
i : Fin (0 + 1)
hx : IsIndex x ⋯ i
⊢ ∃ 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 }

pp: case neg.succ
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
⊢ ∃ 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:
·

Goal state after:
case neg.zero
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
hd : x.dim = 0
i : Fin (0 + 1)
hx : IsIndex x ⋯ i
⊢ ∃ 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 }
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_1.refine_1.refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ ((curriedTensor C).obj X.right).obj (Arrow.mk (initial.to (𝟙_ C))).left ⟶ X.left

pp: case refine_1.refine_1.refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ ((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left ≫ ?refine_1.refine_1.refine_1 =
    ((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom ≫ (ρ_ X.left).hom

Tactic:
·

Goal state after:
case refine_1.refine_1.refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ ((curriedTensor C).obj X.right).obj (Arrow.mk (initial.to (𝟙_ C))).left ⟶ X.left
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case sq
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₁
hX₂ : IsInitial ((F.flip.obj X₂).obj X₁) := ⋯
hY₂ : IsInitial ((F.flip.obj Y₂).obj X₁) := ⋯
⊢ CommSq ((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:
·

Goal state after:
case sq
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₁
hX₂ : IsInitial ((F.flip.obj X₂).obj X₁) := ⋯
hY₂ : IsInitial ((F.flip.obj Y₂).obj X₁) := ⋯
⊢ CommSq ((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₂))
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

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

Tactic:
·

Goal state after:
case refine_1.refine_1.refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ ((curriedTensor C).map X.hom).app (Arrow.mk (initial.to (𝟙_ C))).left ≫
      (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).to X.left =
    ((curriedTensor C).obj X.left).map (Arrow.mk (initial.to (𝟙_ C))).hom ≫ (ρ_ X.left).hom
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case neg.succ
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
⊢ ∃ 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:
·

Goal state after:
case neg.succ
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
⊢ ∃ 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 }
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty

Goal state before:
pp: case refine_1
X : SSet
x✝ : IsEmpty (X _⦋0⦌)
n : ℕ
hn : 0 ≤ n
⊢ X.degenerate n = ⊤

pp: case refine_2
X : SSet
x✝ : X.HasDimensionLT 0
x : X _⦋0⦌
⊢ False

Tactic:
·

Goal state after:
case refine_1
X : SSet
x✝ : IsEmpty (X _⦋0⦌)
n : ℕ
hn : 0 ≤ n
⊢ X.degenerate n = ⊤
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty

Goal state before:
pp: case refine_2
X : SSet
x✝ : X.HasDimensionLT 0
x : X _⦋0⦌
⊢ False

Tactic:
·

Goal state after:
case refine_2
X : SSet
x✝ : X.HasDimensionLT 0
x : X _⦋0⦌
⊢ False
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_1.refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ 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) =
    𝟙 (X □ Arrow.mk (initial.to (𝟙_ C))).left

pp: case refine_1.refine_3
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ ((ρ_ 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.desc ((initialIsInitial.ofIso (zeroMul initialIsInitial).symm).to X.left) (ρ_ X.left).hom ⋯ =
    𝟙 X.left

Tactic:
·

Goal state after:
case refine_1.refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ 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) =
    𝟙 (X □ Arrow.mk (initial.to (𝟙_ C))).left
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case inst
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₂
hX₁ : IsInitial ((F.obj X₁).obj X₂) := ⋯
hY₁ : IsInitial ((F.obj Y₁).obj X₂) := ⋯
⊢ IsIso ((F.map f₁).app X₂)

pp: case sq
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₂
hX₁ : IsInitial ((F.obj X₁).obj X₂) := ⋯
hY₁ : IsInitial ((F.obj Y₁).obj X₂) := ⋯
⊢ CommSq ((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:
·

Goal state after:
case inst
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₂
hX₁ : IsInitial ((F.obj X₁).obj X₂) := ⋯
hY₁ : IsInitial ((F.obj Y₁).obj X₂) := ⋯
⊢ IsIso ((F.map f₁).app X₂)
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: case sq
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₂
hX₁ : IsInitial ((F.obj X₁).obj X₂) := ⋯
hY₁ : IsInitial ((F.obj Y₁).obj X₂) := ⋯
⊢ CommSq ((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:
·

Goal state after:
case sq
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₂
hX₁ : IsInitial ((F.obj X₁).obj X₂) := ⋯
hY₁ : IsInitial ((F.obj Y₁).obj X₂) := ⋯
⊢ CommSq ((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₂))
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_1.refine_3
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ ((ρ_ 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.desc ((initialIsInitial.ofIso (zeroMul initialIsInitial).symm).to X.left) (ρ_ X.left).hom ⋯ =
    𝟙 X.left

Tactic:
·

Goal state after:
case refine_1.refine_3
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ ((ρ_ 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.desc ((initialIsInitial.ofIso (zeroMul initialIsInitial).symm).to X.left) (ρ_ X.left).hom ⋯ =
    𝟙 X.left
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ { 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 =
    (X □ Arrow.mk (initial.to (𝟙_ C))).hom ≫ (ρ_ X.right).hom

Tactic:
·

Goal state after:
case refine_2
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ { 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 =
    (X □ Arrow.mk (initial.to (𝟙_ C))).hom ≫ (ρ_ X.right).hom
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
  simp [π₀.fromChainComplexXZero, ιChainComplex]

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

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

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

Tactic:
·

Goal state after:
case pos
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
hn : n ≠ 1
⊢ (X.chainComplex R).d n 0 ≫ fromChainComplexXZero X R = 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

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

Tactic:
·

Goal state after:
case neg
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
hn : n = 1
⊢ (X.chainComplex R).d n 0 ≫ fromChainComplexXZero X R = 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: case refine_1
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 ≅
    parallelPair ((X.chainComplex R).d 1 0) 0

pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
⊢ (Cocone.precompose (Iso.inv ?refine_1)).obj
      (Preadditive.cokernelCoforkOfCofork (Cofork.ofπ ((sigmaConst.obj R).map (↾π₀.mk)) ⋯)) ≅
    CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) ⋯

Tactic:
·

Goal state after:
case refine_1
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 ≅
    parallelPair ((X.chainComplex R).d 1 0) 0