mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m₁ a : ℕ
L : List ℕ
h_rec :
  ∀ {m : ℕ},
    IsAdmissible (m + 1) L →
      ∀ j < m + 1,
        ∀ (hm₁ : m + L.length + 1 = m₁), standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)
m : ℕ
hL : IsAdmissible (m + 1) (a :: L)
j : ℕ
hj : j < m + 1
hm₁ : m + (a :: L).length + 1 = m₁
h✝ : ¬j < a
this✝ : ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j
this : a < m + 2
⊢ σ (Fin.ofNat (m + 2) a) ≫ σ (Fin.ofNat (m + 1) j) = σ (Fin.ofNat (m + 1 + 1) (j + 1)) ≫ σ (Fin.ofNat (m + 1) a)

Tactic:
by

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
⊢ (Functor.curry.obj (inverse X Y ⋙ functor X Y)).map (homMk e) ≫
      (mkNatIso (fun y ↦ Iso.refl (((Functor.curry.obj (inverse X Y ⋙ functor X Y)).obj (mk x₁)).obj (mk y))) ⋯).hom =
    (mkNatIso (fun y ↦ Iso.refl (((Functor.curry.obj (inverse X Y ⋙ functor X Y)).obj (mk x₀)).obj (mk y))) ⋯).hom ≫
      (Functor.curry.obj (𝟭 (X.HomotopyCategory × Y.HomotopyCategory))).map (homMk e)

Tactic:
by

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
⊢ { toFunctor := functor X Y } ≫ { toFunctor := inverse X Y } = 𝟙 (Cat.of (X ⊗ Y).HomotopyCategory)

Tactic:
by

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
⊢ { toFunctor := inverse X Y } ≫ { toFunctor := functor X Y } = 𝟙 (Cat.of (X.HomotopyCategory × Y.HomotopyCategory))

Tactic:
by

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

Goal state before:
pp: 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
t : Fin (1 + 1)
⊢ (α.hom ≫ (mkOfSucc 1).op).unop = α₀.hom.unop

Tactic:
by

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

Goal state before:
pp: m : ℕ
L : List ℕ
hL : IsAdmissible (m + 1) L
j : ℕ
hj : j < m + 1
m₁ : ℕ
hm₁ : m + L.length + 1 = m₁
⊢ standardσ (simplicialInsert j L) ⋯ = standardσ L ⋯ ≫ σ (Fin.ofNat (m + 1) j)

Tactic:
by

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

Goal state before:
pp: m✝ : ℕ
L✝ : List ℕ
x y : SimplexCategoryGenRel
f : x ⟶ y
hf : P_σ f
L : List ℕ
m b : ℕ
h₁ : mk m = y
h₂ : x = mk (m + b)
h : L.length = b
⊢ y.1 + L.length = x.1

Tactic:
by

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
f : X ⟶ X'
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
⊢ (Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).map (homMk e) ≫
      (mkNatIso
          (fun y ↦
            Iso.refl
              (((Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                    (mk x₁)).obj
                (mk y)))
          ⋯).hom =
    (mkNatIso
          (fun y ↦
            Iso.refl
              (((Functor.curry.obj ((mapHomotopyCategory f).prod (𝟭 Y.HomotopyCategory) ⋙ inverse X' Y)).obj
                    (mk x₀)).obj
                (mk y)))
          ⋯).hom ≫
      (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (f ▷ Y))).map (homMk e)

Tactic:
by

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

Goal state before:
pp: x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
L₁ : List ℕ
b₁ : ℕ
h' : L₁.length = b₁
h₁' : mk (m + 1) = mk (m + 1)
g : mk (m + 1 + b₁) ⟶ mk (m + 1)
hg : degeneracies.multiplicativeClosure g
hL₁ : IsAdmissible (m + 1) L₁
e₁ : g = standardσ L₁ ⋯
⊢ mk (m + 1 + b₁) = mk (m + (b₁ + 1))

Tactic:
by

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
g : Y ⟶ Y'
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
⊢ (Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).map (homMk e) ≫
      (mkNatIso
          (fun y ↦
            Iso.refl
              (((Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                    (mk x₁)).obj
                (mk y)))
          ⋯).hom =
    (mkNatIso
          (fun y ↦
            Iso.refl
              (((Functor.curry.obj ((𝟭 X.HomotopyCategory).prod (mapHomotopyCategory g) ⋙ inverse X Y')).obj
                    (mk x₀)).obj
                (mk y)))
          ⋯).hom ≫
      (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (X ◁ g))).map (homMk e)

Tactic:
by

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

Goal state before:
pp: x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
L₁ : List ℕ
b₁ : ℕ
h' : L₁.length = b₁
h₁' : mk (m + 1) = mk (m + 1)
g : mk (m + 1 + b₁) ⟶ mk (m + 1)
hg : degeneracies.multiplicativeClosure g
hL₁ : IsAdmissible (m + 1) L₁
e₁ : g = standardσ L₁ ⋯
⊢ (simplicialInsert (↑k) L₁).length = b₁ + 1

Tactic:
by

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

Goal state before:
pp: x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
L₁ : List ℕ
b₁ : ℕ
h' : L₁.length = b₁
h₁' : mk (m + 1) = mk (m + 1)
g : mk (m + 1 + b₁) ⟶ mk (m + 1)
hg : degeneracies.multiplicativeClosure g
hL₁ : IsAdmissible (m + 1) L₁
e₁ : g = standardσ L₁ ⋯
⊢ IsAdmissible m (simplicialInsert (↑k) L₁)

Tactic:
by

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

Goal state before:
pp: x y : SimplexCategoryGenRel
f : x ⟶ y
m : ℕ
k : Fin (m + 1)
L₁ : List ℕ
h₁' : mk (m + 1) = mk (m + 1)
hL₁ : IsAdmissible (m + 1) L₁
hg : degeneracies.multiplicativeClosure (standardσ L₁ ⋯)
⊢ m + L₁.length + 1 + [].length = m + 1 + L₁.length

Tactic:
by

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y₀ y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge y₀ y₁
⊢ ((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x)).map (homMk e) ≫
      (Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x)).obj (mk y₁))).hom =
    (Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x)).obj (mk y₀))).hom ≫
      ((Functor.curry.obj (CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory)).obj (mk x)).map (homMk e)

Tactic:
by

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

Goal state before:
pp: x y : SimplexCategoryGenRel
f : x ⟶ y
hf : P_σ f
⊢ ∃ L m b, ∃ (h₁ : mk m = y) (h₂ : x = mk (m + b)) (h : L.length = b), IsAdmissible m L ∧ f = standardσ L ⋯

Tactic:
by

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

Goal state before:
pp: m : ℕ
L : List ℕ
hL : IsAdmissible m L
k : ℕ
hk : k < L.length
⊢ simplicialEvalσ L L[k] = simplicialEvalσ L (L[k] + 1)

Tactic:
by

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
⊢ (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).map (homMk e) ≫
      (mkNatIso
          (fun y ↦
            Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x₁)).obj (mk y)))
          ⋯).hom =
    (mkNatIso
          (fun y ↦
            Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x₀)).obj (mk y)))
          ⋯).hom ≫
      (Functor.curry.obj (CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory)).map (homMk e)

Tactic:
by

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

Goal state before:
pp: m : ℕ
L : List ℕ
hL : IsAdmissible m L
j : ℕ
hj₁ : j < m + L.length
hj₂ : simplicialEvalσ L j = simplicialEvalσ L (j + 1)
⊢ j ∈ L

Tactic:
by

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

Goal state before:
pp: m : ℕ
L : List ℕ
hL : IsAdmissible m L
j : ℕ
hj : j ∈ L
⊢ j < m + L.length ∧ simplicialEvalσ L j = simplicialEvalσ L (j + 1)

Tactic:
by

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

Goal state before:
pp: m : ℕ
L : List ℕ
hL : IsAdmissible m L
j : ℕ
⊢ j ∈ L ↔ j < m + L.length ∧ simplicialEvalσ L j = simplicialEvalσ L (j + 1)

Tactic:
by

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
⊢ (Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).map (homMk e) ≫
      (mkNatIso
          (fun y ↦
            Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).obj (mk x₁)).obj (mk y)))
          ⋯).hom =
    (mkNatIso
          (fun y ↦
            Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (snd X Y))).obj (mk x₀)).obj (mk y)))
          ⋯).hom ≫
      (Functor.curry.obj (CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory)).map (homMk e)

Tactic:
by

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

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
n : ℕ
hn : n < d
i : Fin (n + 2)
⊢ { len := n }.len ≤ d

Tactic:
by

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

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
n : ℕ
hn : n < d
i : Fin (n + 2)
⊢ { len := n + 1 }.len ≤ d

Tactic:
by

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

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
n : ℕ
hn : n < d
i : Fin (n + 1)
⊢ { len := n + 1 }.len ≤ d

Tactic:
by

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

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
n : ℕ
hn : n < d
i : Fin (n + 1)
⊢ { len := n }.len ≤ d

Tactic:
by

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

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = 0
⊢ a = 0

Tactic:
by

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

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
b : ℕ
hb : b ≤ d
ha : 0 ≤ d
f : { obj := { len := 0 }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : 0 + b = 0
⊢ b = 0

Tactic:
by

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

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
ha hb : 0 ≤ d
f : { obj := { len := 0 }, property := ha } ⟶ { obj := { len := 0 }, property := hb }
h : 0 + 0 = 0
⊢ f = 𝟙 { obj := { len := 0 }, property := ha }

Tactic:
by

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

Goal state before:
pp: X Y : Truncated 2
inst✝¹ : Unique (X.obj (Opposite.op { obj := ⦋0⦌, property := Edge.tensor._proof_1 }))
inst✝ : Subsingleton (X.obj (Opposite.op { obj := ⦋1⦌, property := isoTerminal._proof_1 }))
⊢ CategoryTheory.Prod.snd (↑Cat.chosenTerminal) Y.HomotopyCategory =
    (isoTerminal X).inv.toFunctor.prod (𝟭 Y.HomotopyCategory) ⋙ inverse X Y ⋙ mapHomotopyCategory (snd X Y)

Tactic:
by

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

Goal state before:
pp: X Y : Truncated 2
inst✝¹ : Unique (Y.obj (Opposite.op { obj := ⦋0⦌, property := Edge.tensor._proof_1 }))
inst✝ : Subsingleton (Y.obj (Opposite.op { obj := ⦋1⦌, property := isoTerminal._proof_1 }))
⊢ CategoryTheory.Prod.fst X.HomotopyCategory ↑Cat.chosenTerminal =
    (𝟭 X.HomotopyCategory).prod (isoTerminal Y).inv.toFunctor ⋙ inverse X Y ⋙ mapHomotopyCategory (fst X Y)

Tactic:
by

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

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b + 1 ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b + 1 }, property := hb }
h : a + (b + 1) = c + 1
h₁ : ¬Function.Surjective ⇑(Hom.toOrderHom f.hom)
i : Fin (b + 2)
g' : { obj := { len := a }, property := ha }.obj ⟶ { len := b }
hf' : f = Hom.tr g' ha ⋯ ≫ Hom.tr (SimplexCategory.δ i) ⋯ hb
⊢ a + b = c

Tactic:
by

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

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b + 1 ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b + 1 }, property := hb }
h : a + (b + 1) = c + 1
h₁ : ¬Function.Surjective ⇑(Hom.toOrderHom f.hom)
i : Fin (b + 2)
g' : { obj := { len := a }, property := ha }.obj ⟶ { len := b }
hf' : f = Hom.tr g' ha ⋯ ≫ Hom.tr (SimplexCategory.δ i) ⋯ hb
⊢ b < d

Tactic:
by

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

Goal state before:
pp: case neg.succ
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b + 1 ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b + 1 }, property := hb }
h : a + (b + 1) = c + 1
h₁ : ¬Function.Surjective ⇑(Hom.toOrderHom f.hom)
i : Fin (b + 2)
g' : { obj := { len := a }, property := ha }.obj ⟶ { len := b }
hf' : f = Hom.tr g' ha ⋯ ≫ Hom.tr (SimplexCategory.δ i) ⋯ hb
⊢ W (Hom.tr g' ha ⋯ ≫ Hom.tr (SimplexCategory.δ i) ⋯ hb)

Tactic:
exact W.comp_mem _ _ (hc _ _ _ _ _ (by lia))
          (δ_mem _ (by lia) _)

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
z₀ z₁ : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge z₀ z₁
⊢ (((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)).map
        (homMk e) ≫
      (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 =
    (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 ≫
      (((Functor.curry₃.obj ((𝟭 X.HomotopyCategory).prod (inverse Y Z) ⋙ inverse X (Y ⊗ Z))).obj (mk x)).obj (mk y)).map
        (homMk e)

Tactic:
by

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y₀ y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge y₀ y₁
⊢ ((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)).map
        (homMk e) ≫
      (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 =
    (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 ≫
      ((Functor.curry₃.obj ((𝟭 X.HomotopyCategory).prod (inverse Y Z) ⋙ inverse X (Y ⊗ Z))).obj (mk x)).map (homMk e)

Tactic:
by

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

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
b : ℕ
hb : b ≤ d
a : ℕ
ha : a + 1 ≤ d
f : { obj := { len := a + 1 }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + 1 + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : ¬Function.Injective ⇑(Hom.toOrderHom f.hom)
i : Fin (a + 1)
g' : { len := a } ⟶ { obj := { len := b }, property := hb }.obj
hf' : f = Hom.tr (SimplexCategory.σ i) ha ⋯ ≫ Hom.tr g' ⋯ hb
⊢ a < d

Tactic:
by

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

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
b : ℕ
hb : b ≤ d
a : ℕ
ha : a + 1 ≤ d
f : { obj := { len := a + 1 }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + 1 + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : ¬Function.Injective ⇑(Hom.toOrderHom f.hom)
i : Fin (a + 1)
g' : { len := a } ⟶ { obj := { len := b }, property := hb }.obj
hf' : f = Hom.tr (SimplexCategory.σ i) ha ⋯ ≫ Hom.tr g' ⋯ hb
⊢ a + b = c

Tactic:
by

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
⊢ (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)).map
        (homMk e) ≫
      (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 =
    (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 ≫
      (Functor.curry₃.obj ((𝟭 X.HomotopyCategory).prod (inverse Y Z) ⋙ inverse X (Y ⊗ Z))).map (homMk e)

Tactic:
by

Goal state after: