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

Goal state before:
pp: case zero.one.zero
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x✝¹ : zero ⟶ one
x✝ : one ⟶ zero
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ zero) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y zero))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) zero x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) zero x)
      zero (x✝¹ ≫ x✝) =
    WalkingIso.rec (motive := fun {x} ↦ (x ⟶ one) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y one))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) one x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) one x)
        zero x✝¹ ≫
      WalkingIso.rec (motive := fun {x} ↦ (x ⟶ zero) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y zero))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) zero x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) zero x)
        one x✝

Tactic:
simp

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

Goal state before:
pp: case zero.one.one
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x✝¹ : zero ⟶ one
x✝ : one ⟶ one
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ one) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y one))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) one x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) one x)
      zero (x✝¹ ≫ x✝) =
    WalkingIso.rec (motive := fun {x} ↦ (x ⟶ one) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y one))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) one x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) one x)
        zero x✝¹ ≫
      WalkingIso.rec (motive := fun {x} ↦ (x ⟶ one) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y one))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) one x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) one x)
        one x✝

Tactic:
simp

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

Goal state before:
pp: case one.zero.zero
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x✝¹ : one ⟶ zero
x✝ : zero ⟶ zero
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ zero) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y zero))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) zero x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) zero x)
      one (x✝¹ ≫ x✝) =
    WalkingIso.rec (motive := fun {x} ↦ (x ⟶ zero) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y zero))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) zero x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) zero x)
        one x✝¹ ≫
      WalkingIso.rec (motive := fun {x} ↦ (x ⟶ zero) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y zero))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) zero x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) zero x)
        zero x✝

Tactic:
simp

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

Goal state before:
pp: case one.zero.one
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x✝¹ : one ⟶ zero
x✝ : zero ⟶ one
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ one) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y one))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) one x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) one x)
      one (x✝¹ ≫ x✝) =
    WalkingIso.rec (motive := fun {x} ↦ (x ⟶ zero) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y zero))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) zero x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) zero x)
        one x✝¹ ≫
      WalkingIso.rec (motive := fun {x} ↦ (x ⟶ one) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y one))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) one x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) one x)
        zero x✝

Tactic:
simp

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

Goal state before:
pp: case one.one.zero
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x✝¹ : one ⟶ one
x✝ : one ⟶ zero
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ zero) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y zero))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) zero x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) zero x)
      one (x✝¹ ≫ x✝) =
    WalkingIso.rec (motive := fun {x} ↦ (x ⟶ one) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y one))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) one x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) one x)
        one x✝¹ ≫
      WalkingIso.rec (motive := fun {x} ↦ (x ⟶ zero) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y zero))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) zero x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) zero x)
        one x✝

Tactic:
simp

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

Goal state before:
pp: case one.one.one
C : Type u
inst✝ : Category.{v, u} C
X Y : C
e : X ≅ Y
x✝¹ x✝ : one ⟶ one
⊢ WalkingIso.rec (motive := fun {x} ↦ (x ⟶ one) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y one))
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y)) (fun x ↦ 𝟙 X)
          (fun x ↦ e.hom) one x)
      (fun x ↦
        WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y)) (fun x ↦ e.inv)
          (fun x ↦ 𝟙 Y) one x)
      one (x✝¹ ≫ x✝) =
    WalkingIso.rec (motive := fun {x} ↦ (x ⟶ one) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y one))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) one x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) one x)
        one x✝¹ ≫
      WalkingIso.rec (motive := fun {x} ↦ (x ⟶ one) → (WalkingIso.rec X Y x ⟶ WalkingIso.rec X Y one))
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (zero ⟶ y) → (WalkingIso.rec X Y zero ⟶ WalkingIso.rec X Y y))
            (fun x ↦ 𝟙 X) (fun x ↦ e.hom) one x)
        (fun x ↦
          WalkingIso.rec (motive := fun {y} ↦ (one ⟶ y) → (WalkingIso.rec X Y one ⟶ WalkingIso.rec X Y y))
            (fun x ↦ e.inv) (fun x ↦ 𝟙 Y) one x)
        one x✝

Tactic:
simp

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₂
pt : C₃
inl : (F.obj Y₁).obj X₂ ⟶ pt
inr : (F.obj X₁).obj Y₂ ⟶ pt
isPushout : IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) inl inr
⊢ (F.map f₁).app X₂ ≫ (F.obj Y₁).map f₂ = (F.obj X₁).map f₂ ≫ (F.map f₁).app Y₂

Tactic:
simp

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₂
inst✝ : HasPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂)
⊢ (F.map f₁).app X₂ ≫ (F.obj Y₁).map f₂ = (F.obj X₁).map f₂ ≫ (F.map f₁).app Y₂

Tactic:
simp

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' : C₁ ⥤ C₂ ⥤ C₃
e : F ≅ F'
⊢ (F.map f₁).app X₂ ≫ ((e.app Y₁).app X₂).hom = ((e.app X₁).app X₂).hom ≫ (F'.map f₁).app X₂

Tactic:
simp

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' : C₁ ⥤ C₂ ⥤ C₃
e : F ≅ F'
⊢ (F.obj X₁).map f₂ ≫ ((e.app X₁).app Y₂).hom = ((e.app X₁).app X₂).hom ≫ (F'.obj X₁).map f₂

Tactic:
simp

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' : C₁ ⥤ C₂ ⥤ C₃
e : F ≅ F'
⊢ sq.inl ≫ (Iso.refl sq.pt).hom = ((e.app Y₁).app X₂).hom ≫ (e.inv.app Y₁).app X₂ ≫ sq.inl

Tactic:
simp

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' : C₁ ⥤ C₂ ⥤ C₃
e : F ≅ F'
⊢ sq.inr ≫ (Iso.refl sq.pt).hom = ((e.app X₁).app Y₂).hom ≫ (e.inv.app X₁).app Y₂ ≫ sq.inr

Tactic:
simp

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
n : ℕ
F : SSet ⥤ C
⊢ (Sigma.ι (fun x ↦ F.obj Δ[n]) (stdSimplex.objEquiv.symm (𝟙 ⦋n⦌)) ≫ Sigma.desc fun α ↦ F.map (yonedaEquiv.symm α)) =
    𝟙 (F.obj Δ[n])

Tactic:
simp

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⦌
⊢ (Sigma.ι (fun x ↦ R) x ≫
      Sigma.desc fun a ↦ 𝟙 R ≫ Sigma.ι (fun x ↦ R) ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) a)) =
    Sigma.ι (fun x ↦ R) ((ConcreteCategory.hom (f.app (Opposite.op ⦋n⦌))) x)

Tactic:
simp

Goal state after:
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:
obtain ⟨i, rfl⟩ := Fin.eq_succ_of_ne_zero (i := i) (by rintro rfl; simp at hx)

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)
hx : IsIndex x ⋯ i.succ
⊢ ∃ 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: X : SSet
inst✝ : X.Nonempty
⊢ Classical.arbitrary (X _⦋0⦌) ∈ X.nonDegenerate 0

Tactic:
simp

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:
simp

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:
simp

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

Goal state before:
pp: case mk
X : SSet
x✝ : X _⦋0⦌
⊢ mapπ₀ (𝟙 X) (π₀.mk x✝) = π₀.mk x✝

Tactic:
simp

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

Goal state before:
pp: case mk
X Y Z : SSet
f : X ⟶ Y
g : Y ⟶ Z
x✝ : X _⦋0⦌
⊢ mapπ₀ (f ≫ g) (π₀.mk x✝) = mapπ₀ g (mapπ₀ f (π₀.mk x✝))

Tactic:
simp

Goal state after:
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:
simp

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:
simp

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:
simp

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:
simp

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
hn : n ≠ 1
⊢ ¬1 = n
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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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:
simp

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) ≫ Sigma.ι (fun x ↦ R) x = Sigma.ι (fun x ↦ R) x ≫ 𝟙 (∐ fun x ↦ R)

Tactic:
simp

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₃
pt : C₂
fst : pt ⟶ (G.obj (op X₁)).obj X₃
snd : pt ⟶ (G.obj (op Y₁)).obj Y₃
isPullback : IsPullback fst snd ((G.obj (op X₁)).map f₃) ((G.map f₁.op).app Y₃)
⊢ (G.map f₁.op).app X₃ ≫ (G.obj (op X₁)).map f₃ = (G.obj (op Y₁)).map f₃ ≫ (G.map f₁.op).app Y₃

Tactic:
simp

Goal state after: