mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
⊢ { f := { f := fun n ↦ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n, comm' := ⋯ }, comm := ⋯ } ≫
      { f := { f := fun n ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }, comm := ⋯ } =
    𝟙 ((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex)

Tactic:
ext n

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ ({ f := { f := fun n ↦ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n, comm' := ⋯ }, comm := ⋯ } ≫
            { f := { f := fun n ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }, comm := ⋯ }).f.f
      n =
    (𝟙 ((toKaroubi (ChainComplex C ℕ)).obj s.nondegComplex)).f.f n
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
⊢ { f := { f := fun n ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }, comm := ⋯ } ≫
      { f := { f := fun n ↦ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n, comm' := ⋯ }, comm := ⋯ } =
    𝟙 (N₁.obj X)

Tactic:
ext n

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
n : ℕ
⊢ ({ f := { f := fun n ↦ s.πSummand (IndexSet.id (op ⦋n⦌)), comm' := ⋯ }, comm := ⋯ } ≫
            { f := { f := fun n ↦ (s.cofan (op ⦋n⦌)).inj (IndexSet.id (op ⦋n⦌)) ≫ PInfty.f n, comm' := ⋯ },
              comm := ⋯ }).f.f
      n =
    (𝟙 (N₁.obj X)).f.f n
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂N₂.natTrans.app P) = 𝟙 (N₂.obj P)

Tactic:
ext n

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
n : ℕ
⊢ (N₂Γ₂.inv.app (N₂.obj P) ≫ N₂.map (Γ₂N₂.natTrans.app P)).f.f n = (𝟙 (N₂.obj P)).f.f n
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X✝ Y✝ : Split C
Φ : X✝ ⟶ Y✝
⊢ (nondegComplexFunctor ⋙ toKaroubi (ChainComplex C ℕ)).map Φ ≫ Y✝.s.toKaroubiNondegComplexIsoN₁.hom =
    X✝.s.toKaroubiNondegComplexIsoN₁.hom ≫ (forget C ⋙ N₁).map Φ

Tactic:
ext n

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X✝ Y✝ : Split C
Φ : X✝ ⟶ Y✝
n : ℕ
⊢ ((nondegComplexFunctor ⋙ toKaroubi (ChainComplex C ℕ)).map Φ ≫ Y✝.s.toKaroubiNondegComplexIsoN₁.hom).f.f n =
    (X✝.s.toKaroubiNondegComplexIsoN₁.hom ≫ (forget C ⋙ N₁).map Φ).f.f n
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Product

Goal state before:
pp: I : Type u
X : I → TopCat
⊢ CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X = 𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))

Tactic:
apply CategoryTheory.Functor.ext

Goal state after:
case h_map
I : Type u
X : I → TopCat
⊢ autoParam
    (∀ (X_1 Y : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))) (f : X_1 ⟶ Y),
      (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).map f =
        CategoryTheory.eqToHom ⋯ ≫ (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).map f ≫ CategoryTheory.eqToHom ⋯)
    CategoryTheory.Functor.ext._auto_1

case h_obj
I : Type u
X : I → TopCat
⊢ ∀ (X_1 : ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))),
    (CategoryTheory.Functor.pi' (proj X) ⋙ piToPiTop X).obj X_1 = (𝟭 ↑(π.obj (TopCat.of ((i : I) → ↑(X i))))).obj X_1
Module: Mathlib.Topology.Homotopy.Contractible

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : ContractibleSpace X
inst✝ : ContractibleSpace Y
hX : X ≃ₕ Unit
hY : Y ≃ₕ Unit
⊢ ContractibleSpace (X × Y)

Tactic:
refine ⟨⟨(hX.prodCongr hY).trans ?_⟩⟩

Goal state after:
X : Type u_1
Y : Type u_2
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : ContractibleSpace X
inst✝ : ContractibleSpace Y
hX : X ≃ₕ Unit
hY : Y ≃ₕ Unit
⊢ Unit × Unit ≃ₕ Unit
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: Y : Type u_2
inst✝ : TopologicalSpace Y
h : PathConnectedSpace Y ∧ ∀ (x y : Y), Subsingleton (Path.Homotopic.Quotient x y)
⊢ SimplyConnectedSpace Y

Tactic:
cases h; rw [simply_connected_iff_unique_homotopic]
    exact ⟨inferInstance, fun x y => ⟨uniqueOfSubsingleton ⟦PathConnectedSpace.somePath x y⟧⟩⟩

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : G ⊣ F
j✝ : C₁
⊢ (isomorphisms C₂).inverseImage G (adj.unit.app j✝)

Tactic:
simp only [Functor.id_obj, inverseImage_iff, isomorphisms.iff]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : G ⊣ F
j✝ : C₁
⊢ IsIso (G.map (adj.unit.app j✝))
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : F ⊣ G
j✝ : C₁
⊢ (isomorphisms C₂).inverseImage G (adj.counit.app j✝)

Tactic:
simp only [Functor.id_obj, inverseImage_iff, isomorphisms.iff]

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
inst✝¹ : F.Full
inst✝ : F.Faithful
adj : F ⊣ G
j✝ : C₁
⊢ IsIso (G.map (adj.counit.app j✝))
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithWeakEquivalences C
X Y : Over S
f : X ⟶ Y
inst✝ : WeakEquivalence f
⊢ WeakEquivalence (Over.Hom.left f)

Tactic:
by
  rwa [← weakEquivalences_over_iff]

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
inst✝ : LinearOrder ι
i j : ι
⊢ (CompleteLattice.MulticoequalizerDiagram.multispanIndex h).left (i, j) =
    (CompleteLattice.MulticoequalizerDiagram.multispanIndex h).left (j, i)

Tactic:
dsimp
        rw [h.eq_inf, h.eq_inf, inf_comm]

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

Goal state before:
pp: case pos
n i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
h : 0 < n + 2
hS : {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩} = univ
this : Fin.last (n + 3) ∈ univ
⊢ False

Tactic:
rw [← hS] at this

Goal state after:
case pos
n i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
h : 0 < n + 2
hS : {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩} = univ
this : Fin.last (n + 3) ∈ {⟨i, hi⟩, ⟨0, ⋯⟩, ⟨0 + 1, ⋯⟩, ⟨0 + 2, ⋯⟩}
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case neg
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
hS : {⟨i, hi⟩, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩} = univ
hk : ¬k = 0
this : 0 ∈ univ
⊢ False

Tactic:
rw [← hS] at this

Goal state after:
case neg
n k : ℕ
h : k < n + 2
i : ℕ
hi : i < n + 4
h₀ : 0 < ⟨i, hi⟩
hₙ : ⟨i, hi⟩ < Fin.last (n + 3)
hS : {⟨i, hi⟩, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩} = univ
hk : ¬k = 0
this : 0 ∈ {⟨i, hi⟩, ⟨k, ⋯⟩, ⟨k + 1, ⋯⟩, ⟨k + 2, ⋯⟩}
⊢ False
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: case refine_1
X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
h : innerHornInclusions f✝
⊢ (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι) f✝

pp: case refine_2
X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
h : (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι) f✝
⊢ innerHornInclusions f✝

Tactic:
· obtain @⟨n, i, h0, hn⟩ := h
    simp only [iSup_iff, ofHoms_iff, Subtype.exists, exists_prop]
    use n, i

Goal state after:
case refine_2
X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
h : (⨆ n, ofHoms fun p ↦ Λ[n + 2, ↑p].ι) f✝
⊢ innerHornInclusions f✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
⊢ ⊤ ≤ Subcomplex.range (r i d) ⊔ Subcomplex.range (b i d)

Tactic:
rintro ⟨n⟩ ⟨x, hx⟩ _

Goal state after:
X Y : SSet
i : X ⟶ Y
d : ℕ
n : SimplexCategory
x : Y.obj (op n)
hx : x ∈ ((skeletonOfMono i) (d + 1)).obj (op n)
a✝ : ⟨x, hx⟩ ∈ ⊤.obj (op n)
⊢ ⟨x, hx⟩ ∈ (Subcomplex.range (r i d) ⊔ Subcomplex.range (b i d)).obj (op n)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
x₁ x₂ : sigmaStdSimplex i d _⦋n⦌
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
⊢ x₂ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) →
    (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₁ = (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₂ → x₁ = x₂

Tactic:
hx₂

Goal state after:
case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
x₁ x₂ : sigmaStdSimplex i d _⦋n⦌
hx₁ : x₁ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
hx₂ : x₂ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌)))
⊢ (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₁ = (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₂ → x₁ = x₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ι₁ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₁

Tactic:
by
  rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 1).inv, ← Category.assoc,
    horn.faceSingletonComplIso_inv_ι]
  exact (horn.isColimit 2).fac _ (.right ⟨1, by simp⟩)

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inr.zero
X : SSet
sx : X.StrictSegal
i : Fin (0 + 3)
σ₀ : Λ[0 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (0 + 2)
j : Fin (0 + 3)
hj : j ≠ i
k : Fin (0 + 1)
ksucc : Fin (0 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[0 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
obtain rfl : k = 0 := by omega

Goal state after:
case h.inr.inr.zero
X : SSet
sx : X.StrictSegal
i : Fin (0 + 3)
σ₀ : Λ[0 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (0 + 2)
j : Fin (0 + 3)
hj : j ≠ i
ksucc : Fin (0 + 1 + 1 + 1) := (Fin.succ 0).castSucc
heq : j = ksucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc 0).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[0 + 2, i].toSSet.map (mkOfSucc 0).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
⊢ (ConcreteCategory.hom (Y.map (mkOfSucc k).op)) (sy.spineToSimplex (f.map σ)) =
    (ConcreteCategory.hom (σ.app (Opposite.op ⦋n + 1⦌) ≫ Y.map (mkOfSucc k).op)) (sx.spineToSimplex f)

Tactic:
← σ.naturality,

Goal state after:
X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
⊢ (ConcreteCategory.hom (Y.map (mkOfSucc k).op)) (sy.spineToSimplex (f.map σ)) =
    (ConcreteCategory.hom (X.map (mkOfSucc k).op ≫ σ.app (Opposite.op ⦋1⦌))) (sx.spineToSimplex f)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p : X.Path n
⊢ { s // X.spine n s = p }

Tactic:
induction n with

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
s : X _⦋n⦌
⊢ spineToSimplex h (X.spine n s) = s

Tactic:
induction n with

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

Goal state before:
pp: V : Truncated 2
x y : V.HomotopyCategory
h : x.as.as = y.as.as
⊢ x = y

Tactic:
by
  obtain ⟨x, rfl⟩ := x.mk_surjective
  obtain ⟨y, rfl⟩ := y.mk_surjective
  obtain rfl : x = y := h
  rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g h : Edge x y
hgh : HomotopicL g h
hfg : f.CompStruct (Edge.id y) g
⊢ HomotopicL f h

Tactic:
rcases hgh with ⟨hgh⟩

Goal state after:
X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g h : Edge x y
hfg : f.CompStruct (Edge.id y) g
hgh : g.CompStruct (Edge.id y) h
⊢ HomotopicL f h
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g h : Edge x y
hgh : HomotopicR g h
hfg : (Edge.id x).CompStruct f g
⊢ HomotopicR f h

Tactic:
rcases hgh with ⟨hgh⟩

Goal state after:
X : Truncated 2
inst✝ : X.Quasicategory₂
x y : X.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
f g h : Edge x y
hfg : (Edge.id x).CompStruct f g
hgh : (Edge.id x).CompStruct g h
⊢ HomotopicR f h
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ mk (n + 1) ⟶ mk n

Tactic:
induction i using Fin.lastCases with
    | last => exact σ (Fin.last n)
    | cast i => exact σ i

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case id
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
⊢ (∃ (h : x✝ = x✝), 𝟙 x✝ = eqToHom h) ∨ x✝.len < x✝.len

Tactic:
left; use rfl; simp

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case zero.of.δ
i : Fin (0 + 1)
i✝ : Fin (0 + 2)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i✝ ≫ σ i = e ≫ m

Tactic:
exact factor_δ_σ _ _

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case succ.of.δ
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
i✝ : Fin (n + 1 + 2)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i✝ ≫ σ i = e ≫ m

Tactic:
exact factor_δ_σ _ _

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: case cons
a : ℕ
t : List ℕ
H :
  ∀ (L₁ : List ℕ) {m₁ m₂ m₃ : ℕ} (h : m₂ + L₁.length = m₁) (h' : m₃ + t.length = m₂),
    standardσ L₁ h ≫ standardσ t h' = standardσ (t ++ L₁) ⋯
L₁ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + (a :: t).length = m₂
⊢ standardσ L₁ h ≫ standardσ (a :: t) h' = standardσ (a :: t ++ L₁) ⋯

Tactic:
dsimp at h' ⊢
    obtain rfl : m₂ = (m₃ + t.length) + 1 := by grind
    simp [reassoc_of% (H L₁ (m₁ := m₁) (m₂ := m₃ + t.length + 1) (m₃ := m₃ + 1)
      (by grind) (by grind))]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
h : i ≤ j.castSucc
⊢ δ j ≫ toMk₁ i = toMk₁ (i.castPred ⋯)

Tactic:
by
  obtain ⟨i, rfl⟩ := Fin.eq_castSucc_of_ne_last
    (Fin.ne_last_of_lt (lt_of_le_of_lt h j.castSucc_lt_succ))
  simp only [Fin.castSucc_le_castSucc_iff] at h
  rw [Fin.castPred_castSucc]
  refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)
  change toMk₁ i.castSucc (j.succAbove k) = _
  dsimp
  rw [Fin.eq_iff_eq_zero_iff, toMk₁_apply_eq_zero_iff, toMk₁_apply_eq_zero_iff]
  grind [Fin.succAbove]

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
x y : A.N
⊢ x.toN = y.toN ↔ { dim := x.dim, simplex := x.simplex } = { dim := y.dim, simplex := y.simplex }

Tactic:
SSet.N.ext_iff

Goal state after:
X : SSet
A : X.Subcomplex
x y : A.N
⊢ x.toS = y.toS ↔ { dim := x.dim, simplex := x.simplex } = { dim := y.dim, simplex := y.simplex }
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.IsUniquelyCodimOneFace

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
⊢ (ConcreteCategory.hom (SimplicialObject.δ X (hxy.index hd))) (y.cast ⋯).simplex = (x.cast hd).simplex

Tactic:
apply δ_index

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

Goal state before:
pp: case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
h : x ∈ P.II
⊢ ∃ y, x = ↑y ∨ x = ↑(P.p y)

Tactic:
· exact ⟨⟨_, h⟩, Or.inl rfl⟩

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
h : { dim := (↑s).dim, simplex := ((↑s).cast ⋯).simplex } = { dim := (↑t).dim, simplex := ((↑t).cast ⋯).simplex }
⊢ (↑s).toN = (↑t).toN

Tactic:
SSet.N.ext_iff

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
h : { dim := (↑s).dim, simplex := ((↑s).cast ⋯).simplex } = { dim := (↑t).dim, simplex := ((↑t).cast ⋯).simplex }
⊢ (↑s).toS = (↑t).toS
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
h :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim, simplex := ((↑t).cast ⋯).simplex }
⊢ ((↑(P.p s)).cast ⋯).toN = (↑t).toN

Tactic:
SSet.N.ext_iff

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s t : ↑P.II
h :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim, simplex := ((↑t).cast ⋯).simplex }
⊢ ((↑(P.p s)).cast ⋯).toS = (↑t).toS
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝¹ x✝ : h.ι
hst : (h.type₁ x✝¹).toN = (h.type₁ x✝).toN
⊢ { dim := h.dim x✝¹ + 1, simplex := h.simplex x✝¹ } = { dim := h.dim x✝ + 1, simplex := h.simplex x✝ }

Tactic:
SSet.N.ext_iff

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝¹ x✝ : h.ι
hst : (h.type₁ x✝¹).toS = (h.type₁ x✝).toS
⊢ { dim := h.dim x✝¹ + 1, simplex := h.simplex x✝¹ } = { dim := h.dim x✝ + 1, simplex := h.simplex x✝ }
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
s t : h.ι
hst : (h.type₂ s).toN = (h.type₂ t).toN
⊢ { dim := h.dim s, simplex := (ConcreteCategory.hom (SimplicialObject.δ X (h.index s))) (h.simplex s) } =
    { dim := h.dim t, simplex := (ConcreteCategory.hom (SimplicialObject.δ X (h.index t))) (h.simplex t) }

Tactic:
SSet.N.ext_iff

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
s t : h.ι
hst : (h.type₂ s).toS = (h.type₂ t).toS
⊢ { dim := h.dim s, simplex := (ConcreteCategory.hom (SimplicialObject.δ X (h.index s))) (h.simplex s) } =
    { dim := h.dim t, simplex := (ConcreteCategory.hom (SimplicialObject.δ X (h.index t))) (h.simplex t) }
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x : A.N
s : h.ι
h✝ : x.toS = { dim := h.dim s + 1, simplex := h.simplex s }
⊢ x.toN = (h.type₁ s).toN

Tactic:
SSet.N.ext_iff

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
x : A.N
s : h.ι
h✝ : x.toS = { dim := h.dim s + 1, simplex := h.simplex s }
⊢ x.toS = (h.type₁ s).toS
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x : A.N
s : h.ι
h✝ : x.toS = { dim := h.dim s, simplex := (ConcreteCategory.hom (SimplicialObject.δ X (h.index s))) (h.simplex s) }
⊢ x.toN = (h.type₂ s).toN

Tactic:
SSet.N.ext_iff

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
x : A.N
s : h.ι
h✝ : x.toS = { dim := h.dim s, simplex := (ConcreteCategory.hom (SimplicialObject.δ X (h.index s))) (h.simplex s) }
⊢ x.toS = (h.type₂ s).toS
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -∑ x, α x + -∑ x, β x + H.h 0 ≫ Y.δ 0

Tactic:
let γ₂ (x : Fin (n + 1) × Fin (n + 2)) := (x.2.succ, x.1.castSucc)

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
⊢ H.h (Fin.last (n + 1)) ≫ Y.δ (Fin.last (n + 1 + 1)) = -∑ x, α x + -∑ x, β x + H.h 0 ≫ Y.δ 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h : (↑c.s).simplex ∈ (↑(P.p c'.s)).subcomplex.obj (op ⦋(↑c.s).dim⦌)
⊢ P.AncestralRel c.s c'.s

Tactic:
refine ⟨fun hxy ↦ ?_, lt_of_le_of_ne ?_ ((P.ne _ _).symm)⟩

Goal state after:
case refine_1
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h : (↑c.s).simplex ∈ (↑(P.p c'.s)).subcomplex.obj (op ⦋(↑c.s).dim⦌)
hxy : c.s = c'.s
⊢ False

case refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝ : LinearOrder ι
f : P.RankFunction ι
j : ι
c : f.Cell j
i : ι
c' : f.Cell i
hi : f.rank c'.s < f.rank c.s
h : (↑c.s).simplex ∈ (↑(P.p c'.s)).subcomplex.obj (op ⦋(↑c.s).dim⦌)
⊢ ↑c.s ≤ ↑(P.p c'.s)