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

Goal state before:
pp: X Y Z : Truncated 2
xyz : X.HomotopyCategory × Y.HomotopyCategory × Z.HomotopyCategory
⊢ (Functor.currying₃.functor.map
          (mkNatIso
              (fun x ↦
                mkNatIso
                  (fun y ↦
                    mkNatIso
                      (fun z ↦
                        Iso.refl
                          ((((Functor.curry₃.obj
                                        ((prod.associativity X.HomotopyCategory Y.HomotopyCategory
                                              Z.HomotopyCategory).inverse ⋙
                                          (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                                            inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                                    (mk x)).obj
                                (mk y)).obj
                            (mk z)))
                      ⋯)
                  ⋯)
              ⋯).hom).app
      xyz =
    𝟙
      (((prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse ⋙
            (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙ inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom).obj
        xyz)

Tactic:
]

Goal state after:
X Y Z : Truncated 2
xyz : X.HomotopyCategory × Y.HomotopyCategory × Z.HomotopyCategory
⊢ (Functor.currying₃.functor.map
          (mkNatIso
              (fun x ↦
                mkNatIso
                  (fun y ↦
                    mkNatIso
                      (fun z ↦
                        Iso.refl
                          ((((Functor.curry₃.obj
                                        ((prod.associativity X.HomotopyCategory Y.HomotopyCategory
                                              Z.HomotopyCategory).inverse ⋙
                                          (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                                            inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                                    (mk x)).obj
                                (mk y)).obj
                            (mk z)))
                      ⋯)
                  ⋯)
              ⋯).hom).app
      xyz =
    𝟙
      (((prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse ⋙
            (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙ inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom).obj
        xyz)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X Y Z : Truncated 2
xyz : (X.HomotopyCategory × Y.HomotopyCategory) × Z.HomotopyCategory
⊢ 𝟙 ((mapHomotopyCategory (α_ X Y Z).hom).obj ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj xyz.1, xyz.2))) ≫
      (mapHomotopyCategory (α_ X Y Z).hom).map
          ((inverse (X ⊗ Y) Z).map (Prod.mkHom ((inverse X Y).map (𝟙 xyz.1)) (𝟙 xyz.2))) ≫
        𝟙
            ((mapHomotopyCategory (α_ X Y Z).hom).obj
              ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj (xyz.1.1, xyz.1.2), xyz.2))) ≫
          𝟙
            (((prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse ⋙
                  (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                    inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom).obj
              (xyz.1.1, xyz.1.2, xyz.2)) =
    𝟙 ((mapHomotopyCategory (α_ X Y Z).hom).obj ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj xyz.1, xyz.2)))

Tactic:
]

Goal state after:
X Y Z : Truncated 2
xyz : (X.HomotopyCategory × Y.HomotopyCategory) × Z.HomotopyCategory
⊢ 𝟙 ((mapHomotopyCategory (α_ X Y Z).hom).obj ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj xyz.1, xyz.2))) ≫
      (mapHomotopyCategory (α_ X Y Z).hom).map
          ((inverse (X ⊗ Y) Z).map (Prod.mkHom ((inverse X Y).map (𝟙 xyz.1)) (𝟙 xyz.2))) ≫
        𝟙
            ((mapHomotopyCategory (α_ X Y Z).hom).obj
              ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj (xyz.1.1, xyz.1.2), xyz.2))) ≫
          𝟙
            (((prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse ⋙
                  (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                    inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom).obj
              (xyz.1.1, xyz.1.2, xyz.2)) =
    𝟙 ((mapHomotopyCategory (α_ X Y Z).hom).obj ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj xyz.1, xyz.2)))
Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory

Goal state before:
pp: n m : SemiSimplexCategory
f : n ⟶ m
⊢ Function.Injective ⇑(SimplexCategory.Hom.toOrderHom (toSimplexCategory.map f))

Tactic:
]

Goal state after:
n m : SemiSimplexCategory
f : n ⟶ m
⊢ Function.Injective ⇑(SimplexCategory.Hom.toOrderHom (toSimplexCategory.map f))
Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory

Goal state before:
pp: n m : SemiSimplexCategory
f : toSimplexCategory.obj n ⟶ toSimplexCategory.obj m
inst✝ : Mono f
⊢ Mono f

Tactic:
]

Goal state after:
n m : SemiSimplexCategory
f : toSimplexCategory.obj n ⟶ toSimplexCategory.obj m
inst✝ : Mono f
⊢ Mono f
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

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

Tactic:
]

Goal state after:
n : ℕ
j i : Fin (n + 2)
h✝ : i.castSucc ≤ j.castSucc
h : i ≤ j
⊢ δ j ≫ toMk₁ i.castSucc = toMk₁ i
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
j i : Fin (n + 2)
h✝ : i.castSucc ≤ j.castSucc
h : i ≤ j
k : Fin (⦋n⦌.len + 1)
⊢ (j.succAbove k).castSucc < i.castSucc ↔ k.castSucc < i

Tactic:
]

Goal state after:
n : ℕ
j i : Fin (n + 2)
h✝ : i.castSucc ≤ j.castSucc
h : i ≤ j
k : Fin (⦋n⦌.len + 1)
⊢ (j.succAbove k).castSucc < i.castSucc ↔ k.castSucc < i
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
⊢ δ j ≫ toMk₁ i.succ = toMk₁ i

Tactic:
]

Goal state after:
n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
⊢ δ j ≫ toMk₁ i.succ = toMk₁ i
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
k : Fin (⦋n⦌.len + 1)
⊢ (j.succAbove k).castSucc < i.succ ↔ k.castSucc < i

Tactic:
]

Goal state after:
n : ℕ
j i : Fin (n + 2)
h : j.castSucc < i.succ
k : Fin (⦋n⦌.len + 1)
⊢ (j.succAbove k).castSucc < i.succ ↔ k.castSucc < i
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X Y Z : Truncated 2
xyz : (X.HomotopyCategory × Y.HomotopyCategory) × Z.HomotopyCategory
⊢ 𝟙 ((mapHomotopyCategory (α_ X Y Z).hom).obj ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj xyz.1, xyz.2))) =
    𝟙 ((mapHomotopyCategory (α_ X Y Z).hom).obj ((inverse (X ⊗ Y) Z).obj ((inverse X Y).obj xyz.1, xyz.2)))

Tactic:
]

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

Goal state before:
pp: case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₂)) x
this : (ConcreteCategory.hom (X.map α.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α)) x
⊢ (ConcreteCategory.hom (X.map ((inclusion 2).op.map (Hom.right β₁))))
      ((ConcreteCategory.hom (X.map α.hom)) (lift sx s x)) =
    (ConcreteCategory.hom (s.π.app α₁)) x

Tactic:
]

Goal state after:
case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₂)) x
this : (ConcreteCategory.hom (X.map α.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α)) x
⊢ (ConcreteCategory.hom (X.map ((inclusion 2).op.map (Hom.right β₁))))
      ((ConcreteCategory.hom (X.map α.hom)) (lift sx s x)) =
    (ConcreteCategory.hom (s.π.app α₁)) x
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
⊢ 1 = 1

pp: case neg.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
⊢ i ≤ (j.predAbove k).castSucc

Tactic:
]

Goal state after:
case neg.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
⊢ i ≤ (j.predAbove k).castSucc
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
hk' : k ≤ j.castSucc
⊢ i ≤ k

Tactic:
]

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
hk' : k ≤ j.castSucc
⊢ i ≤ k
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₂)) x
this : (ConcreteCategory.hom (X.map α.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α)) x
⊢ (ConcreteCategory.hom (X.map α₁.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₁)) x

Tactic:
rw [← StructuredArrow.w β₁, Functor.map_comp_apply]

Goal state after:
case succ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₂)) x
this : (ConcreteCategory.hom (X.map α.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α)) x
⊢ (ConcreteCategory.hom (X.map ((inclusion 2).op.map (Hom.right β₁))))
      ((ConcreteCategory.hom (X.map α.hom)) (lift sx s x)) =
    (ConcreteCategory.hom (s.π.app α₁)) x
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
⊢ 0 = 0

pp: case neg.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
⊢ (j.predAbove k).castSucc < i

Tactic:
]

Goal state after:
case neg.h
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
⊢ (j.predAbove k).castSucc < i
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
hk' : j.castSucc < k
⊢ k ≤ i

Tactic:
]

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
hk' : j.castSucc < k
⊢ k ≤ i
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
hk' : k ≤ j.castSucc
⊢ (k.castPred ⋯).castSucc < i

Tactic:
]

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
hk' : k ≤ j.castSucc
⊢ (k.castPred ⋯).castSucc < i
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ 0 = (ConcreteCategory.hom f) i

Tactic:
]

Goal state after:
case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ 0 = (ConcreteCategory.hom f) i
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
x : Finset β
h : x ∈ (fun s ↦ Finset.image f s) '' K.faces
⊢ x.Nonempty ∧ ∀ ⦃b : Finset β⦄, b ⊆ x → b.Nonempty → b ∈ (fun s ↦ Finset.image f s) '' K.faces

Tactic:
simp only [Set.mem_image] at h ⊢

Goal state after:
ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
x : Finset β
h : ∃ x_1 ∈ K.faces, Finset.image f x_1 = x
⊢ x.Nonempty ∧ ∀ ⦃b : Finset β⦄, b ⊆ x → b.Nonempty → ∃ x ∈ K.faces, Finset.image f x = b
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case left
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty

Tactic:
]

Goal state after:
case left
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case left
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty

Tactic:
]

Goal state after:
case left
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case left
ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty

Tactic:
]

Goal state after:
case left
ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case hᵥ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin (i + 1)
⊢ (X.spine i
          ((ConcreteCategory.hom (X.map f.op))
            (sx.spineToSimplex
              { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
                arrow := fun i ↦
                  (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
                arrow_src := ⋯, arrow_tgt := ⋯ }))).vertex
      k =
    (X.spine i ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk f.op))) x)).vertex k

Tactic:
]

Goal state after:
case hᵥ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin (i + 1)
⊢ (X.spine i
          ((ConcreteCategory.hom (X.map f.op))
            (sx.spineToSimplex
              { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
                arrow := fun i ↦
                  (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
                arrow_src := ⋯, arrow_tgt := ⋯ }))).vertex
      k =
    (X.spine i ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk f.op))) x)).vertex k
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right.inl
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
L : AbstractSimplicialComplex ι
hL : L ∈ upperBounds x✝
a✝ : Finset ι
ht : a✝ ∈ ⋃ K ∈ x✝, K.faces
⊢ a✝ ∈ (fun K ↦ K.faces) L

Tactic:
simp only [Set.mem_iUnion] at ht
        obtain ⟨K, hK, htK⟩ := ht
        exact hL hK htK

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

Goal state before:
pp: case hᵥ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin (i + 1)
⊢ Path.vertex
      { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
        arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
        arrow_src := ⋯, arrow_tgt := ⋯ }
      ((Hom.toOrderHom f) k) =
    (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋i⦌ k).op)) ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk f.op))) x)

Tactic:
]

Goal state after:
case hᵥ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin (i + 1)
⊢ Path.vertex
      { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
        arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
        arrow_src := ⋯, arrow_tgt := ⋯ }
      ((Hom.toOrderHom f) k) =
    (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋i⦌ k).op)) ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk f.op))) x)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case hₐ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin i
⊢ (ConcreteCategory.hom (X.map (op f ≫ (mkOfSucc k).op)))
      (sx.spineToSimplex
        { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
          arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
          arrow_src := ⋯, arrow_tgt := ⋯ }) =
    (ConcreteCategory.hom (X.map (mkOfSucc k).op)) ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))) x)

Tactic:
]

Goal state after:
case hₐ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin i
⊢ (ConcreteCategory.hom (X.map (op f ≫ (mkOfSucc k).op)))
      (sx.spineToSimplex
        { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i).op))) x,
          arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
          arrow_src := ⋯, arrow_tgt := ⋯ }) =
    (ConcreteCategory.hom (X.map (mkOfSucc k).op)) ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))) x)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y : SimplexCategory
h : x = y
⊢ y.len = y.len

Tactic:
]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: case left.left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₁.len + 1)
h : ↑(Fin.castAdd (x₂.len + 1) i✝¹) ≤ ↑(Fin.castAdd (x₂.len + 1) i✝)
⊢ ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.castAdd (x₂.len + 1) i✝¹)) ≤
    ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.castAdd (x₂.len + 1) i✝))

Tactic:
]

Goal state after:
case left.left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₁.len + 1)
h : ↑(Fin.castAdd (x₂.len + 1) i✝¹) ≤ ↑(Fin.castAdd (x₂.len + 1) i✝)
⊢ ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.castAdd (x₂.len + 1) i✝¹)) ≤
    ↑((fun i ↦
          Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
            (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
        (Fin.castAdd (x₂.len + 1) i✝))