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

Goal state before:
pp: case «0»
n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] ((fun i ↦ i) ⟨0, ⋯⟩).castSucc

pp: case «1»
n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] ((fun i ↦ i) ⟨1, ⋯⟩).castSucc

Tactic:
·

Goal state after:
case «0»
n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] ((fun i ↦ i) ⟨0, ⋯⟩).castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: case mk.succ
n : ℕ
X Y : Truncated (n + 1)
inst✝ : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := ⋯ })),
    (ConcreteCategory.hom (f.app (op { obj := ⦋1⦌, property := ⋯ }))) x =
      (ConcreteCategory.hom (g.app (op { obj := ⦋1⦌, property := ⋯ }))) x
m : ℕ
hm : ⦋m + 1⦌.len ≤ n + 1
x : X.obj (op { obj := ⦋m + 1⦌, property := hm })
⊢ (ConcreteCategory.hom (f.app (op { obj := ⦋m + 1⦌, property := hm }))).toFun x =
    (ConcreteCategory.hom (g.app (op { obj := ⦋m + 1⦌, property := hm }))).toFun x

Tactic:
·

Goal state after:
case mk.succ
n : ℕ
X Y : Truncated (n + 1)
inst✝ : Y.IsStrictSegal
f g : X ⟶ Y
h :
  ∀ (x : X.obj (op { obj := ⦋1⦌, property := ⋯ })),
    (ConcreteCategory.hom (f.app (op { obj := ⦋1⦌, property := ⋯ }))) x =
      (ConcreteCategory.hom (g.app (op { obj := ⦋1⦌, property := ⋯ }))) x
m : ℕ
hm : ⦋m + 1⦌.len ≤ n + 1
x : X.obj (op { obj := ⦋m + 1⦌, property := hm })
⊢ (ConcreteCategory.hom (f.app (op { obj := ⦋m + 1⦌, property := hm }))).toFun x =
    (ConcreteCategory.hom (g.app (op { obj := ⦋m + 1⦌, property := hm }))).toFun x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case «1»
n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] ((fun i ↦ i) ⟨1, ⋯⟩).castSucc

Tactic:
·

Goal state after:
case «1»
n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 1) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] ((fun i ↦ i) ⟨1, ⋯⟩).castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case «0»
n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] ((fun i ↦ i) ⟨0, ⋯⟩).succ

pp: case «1»
n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] ((fun i ↦ i) ⟨1, ⋯⟩).succ

Tactic:
·

Goal state after:
case «0»
n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] ((fun i ↦ i) ⟨0, ⋯⟩).succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case «1»
n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] ((fun i ↦ i) ⟨1, ⋯⟩).succ

Tactic:
·

Goal state after:
case «1»
n✝ : ℕ
X✝ : Truncated (n✝ + 1)
m n : ℕ
X : Truncated (n + 1)
p q : X.Path 1
h : p.vertex 1 = q.vertex 0
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      (![p.arrow 0, q.arrow 0] ((fun i ↦ i) ⟨1, ⋯⟩)) =
    ![p.vertex 0, p.vertex 1, q.vertex 1] ((fun i ↦ i) ⟨1, ⋯⟩).succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
f : X.Path m
j l : ℕ
h : j + l ≤ m
i : Fin (l + 1)
⊢ j + ↑i < m + 1

Tactic:
by lia

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
f : X.Path m
j l : ℕ
h : j + l ≤ m
i : Fin l
⊢ j + ↑i < m

Tactic:
by lia

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ l ≤ n + 1

Tactic:
by lia

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
⊢ ksucc < j ∨ j < ksucc ∨ j = ksucc

Tactic:
by lia

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

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

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

pp: case h.inr.inr
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 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 (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
·

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

Goal state before:
pp: case «1»
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₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

pp: case «2»
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₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
·

Goal state after:
case «1»
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₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
k : Fin (m + 1)
⊢ (ConcreteCategory.hom (Y.map (tr (mkOfSucc k) ⋯ ⋯).op)) (sy.spineToSimplex (m + 1) ⋯ (f.map σ)) =
    (ConcreteCategory.hom (X.map (tr (mkOfSucc k) ⋯ ⋯).op ≫ σ.app (op { obj := ⦋1⦌, property := ⋯ })))
      (sx.spineToSimplex (m + 1) ⋯ f)

Tactic:
simp [-NatTrans.naturality]

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

Goal state before:
pp: case «2»
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₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
·

Goal state after:
case «2»
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₁
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨1, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨3, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
      | 2, hi => ⋯.elim
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
⊢ l ≤ n + 1

Tactic:
by lia

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

Goal state before:
pp: case hᵥ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin (l + 1)
⊢ (X.spine l ⋯ ((ConcreteCategory.hom (X.map (tr (subinterval j l h) ⋯ hₘ).op)) Δ)).vertex i =
    ((X.spine m hₘ Δ).interval j l h).vertex i

pp: case hₐ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin l
⊢ (X.spine l ⋯ ((ConcreteCategory.hom (X.map (tr (subinterval j l h) ⋯ hₘ).op)) Δ)).arrow i =
    ((X.spine m hₘ Δ).interval j l h).arrow i

Tactic:
·

Goal state after:
case hᵥ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin (l + 1)
⊢ (X.spine l ⋯ ((ConcreteCategory.hom (X.map (tr (subinterval j l h) ⋯ hₘ).op)) Δ)).vertex i =
    ((X.spine m hₘ Δ).interval j l h).vertex i
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

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

pp: case h.inr.inr
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 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 (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
·

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

Goal state before:
pp: case hₐ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin l
⊢ (X.spine l ⋯ ((ConcreteCategory.hom (X.map (tr (subinterval j l h) ⋯ hₘ).op)) Δ)).arrow i =
    ((X.spine m hₘ Δ).interval j l h).arrow i

Tactic:
·

Goal state after:
case hₐ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin l
⊢ (X.spine l ⋯ ((ConcreteCategory.hom (X.map (tr (subinterval j l h) ⋯ hₘ).op)) Δ)).arrow i =
    ((X.spine m hₘ Δ).interval j l h).arrow i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X✝ : Truncated (n + 1)
sx✝ : X✝.StrictSegal
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
⊢ 2 ≤ n + 1 + 1

Tactic:
by lia

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

Goal state before:
pp: n : ℕ
X✝ : Truncated (n + 1)
sx✝ : X✝.StrictSegal
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
⊢ ↑i + 2 ≤ m + 1

Tactic:
by lia

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

Goal state before:
pp: case h.inr.inr
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 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 (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
·

Goal state after:
case h.inr.inr
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 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 (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hᵥ
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
i : Fin (0 + 1)
⊢ f.vertex i = g.vertex i

pp: case hₐ
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
i : Fin 0
⊢ f.arrow i = g.arrow i

Tactic:
·

Goal state after:
case hᵥ
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
i : Fin (0 + 1)
⊢ f.vertex i = g.vertex i
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hₐ
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
i : Fin 0
⊢ f.arrow i = g.arrow i

Tactic:
·

Goal state after:
case hₐ
X : SSet
f g : X.Path 0
h : f.vertex 0 = g.vertex 0
i : Fin 0
⊢ f.arrow i = g.arrow i
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)

pp: case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 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 (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
·

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
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)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case zero
X : SSet
x : X _⦋0 + 1⦌
⊢ X.spine 0 ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) = (X.spine (0 + 1) x).interval 1 0 ⋯

pp: case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
⊢ X.spine (m + 1) ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) = (X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯

Tactic:
·

Goal state after:
case zero
X : SSet
x : X _⦋0 + 1⦌
⊢ X.spine 0 ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) = (X.spine (0 + 1) x).interval 1 0 ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
⊢ X.spine (m + 1) ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) = (X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯

Tactic:
·

Goal state after:
case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
⊢ X.spine (m + 1) ((ConcreteCategory.hom (SimplicialObject.δ X 0)) x) = (X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 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 (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
·

Goal state after:
case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 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 (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: X : SSet
n j l : ℕ
h : j + l ≤ n
Δ : X _⦋n⦌
⊢ n ≤ n + 1

Tactic:
by lia

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: case h_map
C : Type u
inst✝ : Category.{v, u} C
x✝ : ↑chosenTerminal ⥤ C
⊢ autoParam
    (∀ (X Y : ↑chosenTerminal) (f : X ⟶ Y),
      ((Functor.const ↑chosenTerminal).obj ((fun F ↦ F.obj { down := { as := () } }) x✝)).map f =
        eqToHom ⋯ ≫ x✝.map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

pp: case h_obj
C : Type u
inst✝ : Category.{v, u} C
x✝ : ↑chosenTerminal ⥤ C
⊢ ∀ (X : ↑chosenTerminal),
    ((Functor.const ↑chosenTerminal).obj ((fun F ↦ F.obj { down := { as := () } }) x✝)).obj X = x✝.obj X

Tactic:
·

Goal state after:
case h_map
C : Type u
inst✝ : Category.{v, u} C
x✝ : ↑chosenTerminal ⥤ C
⊢ autoParam
    (∀ (X Y : ↑chosenTerminal) (f : X ⟶ Y),
      ((Functor.const ↑chosenTerminal).obj ((fun F ↦ F.obj { down := { as := () } }) x✝)).map f =
        eqToHom ⋯ ≫ x✝.map f ≫ eqToHom ⋯)
    Functor.ext._auto_1