mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : C
e✝ : X✝ ≅ Y✝
X Y : C
e : X ≅ Y
⊢ r.degHom (e.hom ≫ e.inv) ≤ r.deg Y

Tactic:
]

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X✝ Y✝ : C
e✝ : X✝ ≅ Y✝
X Y : C
e : X ≅ Y
⊢ r.degHom (e.hom ≫ e.inv) ≤ r.deg Y
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : P = ⊤
⊢ P f

Tactic:
]

Goal state after:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : P = ⊤
⊢ P f
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : P = ⊤
⊢ ⊤ f

Tactic:
]

Goal state after:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : P = ⊤
⊢ ⊤ f
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : P = ⊤
⊢ P f

Tactic:
]

Goal state after:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : P = ⊤
⊢ P f
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : P = ⊤
⊢ ⊤ f

Tactic:
]

Goal state after:
P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f : a ⟶ b
this : P = ⊤
⊢ ⊤ f
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_of.inl.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
i : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure i
e : x✝ = mk n✝
h✝ : i = eqToHom e
⊢ (mk n✝).len < (mk (n✝ + 1)).len

Tactic:
]

Goal state after:
case comp_of.inl.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
i : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure i
e : x✝ = mk n✝
h✝ : i = eqToHom e
⊢ (mk n✝).len < (mk (n✝ + 1)).len
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case inl
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i.succ ≤ i'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'

Tactic:
]

Goal state after:
case inl
n : ℕ
i : Fin (n + 2)
i' : Fin (n + 3)
h : i.succ ≤ i'
⊢ δ i' ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i' ≫ σ i = σ j ≫ δ j'
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case inl.inl
n : ℕ
i i' : Fin (n + 2)
h✝ : i.succ ≤ i'.succ
h : i < i'
⊢ δ i'.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.succ ≫ σ i = σ j ≫ δ j'

Tactic:
]

Goal state after:
case inl.inl
n : ℕ
i i' : Fin (n + 2)
h✝ : i.succ ≤ i'.succ
h : i < i'
⊢ δ i'.succ ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.succ ≫ σ i = σ j ≫ δ j'
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h✝ : i.castSucc.succ ≤ i'.succ
h : i.castSucc < i'
⊢ σ i ≫ δ i' = σ i ≫ δ i'

Tactic:
]

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

Goal state before:
pp: case inr.inr
n : ℕ
i i' : Fin (n + 2)
h : i' < i
⊢ δ i'.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.castSucc ≫ σ i = σ j ≫ δ j'

Tactic:
]

Goal state after:
case inr.inr
n : ℕ
i i' : Fin (n + 2)
h : i' < i
⊢ δ i'.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.castSucc ≫ σ i = σ j ≫ δ j'
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case inr.inr
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h : i' ≤ i.castSucc
⊢ δ i'.castSucc ≫ σ i.succ = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.castSucc ≫ σ i.succ = σ j ≫ δ j'

Tactic:
]

Goal state after:
case inr.inr
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h : i' ≤ i.castSucc
⊢ δ i'.castSucc ≫ σ i.succ = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.castSucc ≫ σ i.succ = σ j ≫ δ j'
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h : i' ≤ i.castSucc
⊢ σ i ≫ δ i' = σ i ≫ δ i'

Tactic:
]

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

Goal state before:
pp: case cons_cons
x✝ y✝ : ℕ
xs✝ : List ℕ
a✝ :
  ∀ {m : ℕ},
    IsAdmissible m xs✝ ↔ List.IsChain (fun x1 x2 ↦ x1 < x2) xs✝ ∧ ∀ (k : ℕ) (h : k < xs✝.length), xs✝[k] ≤ m + k
IH :
  ∀ (y : ℕ) {m : ℕ},
    IsAdmissible m (y :: xs✝) ↔
      List.IsChain (fun x1 x2 ↦ x1 < x2) (y :: xs✝) ∧ ∀ (k : ℕ) (h : k < (y :: xs✝).length), (y :: xs✝)[k] ≤ m + k
m : ℕ
⊢ IsAdmissible m (x✝ :: y✝ :: xs✝) ↔
    List.IsChain (fun x1 x2 ↦ x1 < x2) (x✝ :: y✝ :: xs✝) ∧
      ∀ (k : ℕ) (h : k < (x✝ :: y✝ :: xs✝).length), (x✝ :: y✝ :: xs✝)[k] ≤ m + k

Tactic:
simp_rw [isAdmissible_cons_cons_iff, IH, List.length_cons, and_assoc,
      List.isChain_cons_cons, and_assoc, and_congr_right_iff, and_comm]

Goal state after:
case cons_cons
x✝ y✝ : ℕ
xs✝ : List ℕ
a✝ :
  ∀ {m : ℕ},
    IsAdmissible m xs✝ ↔ List.IsChain (fun x1 x2 ↦ x1 < x2) xs✝ ∧ ∀ (k : ℕ) (h : k < xs✝.length), xs✝[k] ≤ m + k
IH :
  ∀ (y : ℕ) {m : ℕ},
    IsAdmissible m (y :: xs✝) ↔
      List.IsChain (fun x1 x2 ↦ x1 < x2) (y :: xs✝) ∧ ∀ (k : ℕ) (h : k < (y :: xs✝).length), (y :: xs✝)[k] ≤ m + k
m : ℕ
⊢ x✝ < y✝ →
    List.IsChain (fun x1 x2 ↦ x1 < x2) (y✝ :: xs✝) →
      ((x✝ ≤ m ∧ ∀ (k : ℕ) (h : k < xs✝.length + 1), (y✝ :: xs✝)[k] ≤ m + 1 + k) ↔
        ∀ (k : ℕ) (h : k < xs✝.length + 1 + 1), (x✝ :: y✝ :: xs✝)[k] ≤ m + k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m : ℕ
L : List ℕ
⊢ (List.Pairwise (fun x1 x2 ↦ x1 < x2) L ∧ ∀ (k : ℕ) (h : k < L.length), L[k] ≤ m + k) ↔
    List.Pairwise (fun x1 x2 ↦ x1 < x2) L ∧ ∀ (k : ℕ) (h : k < L.length), L[k] ≤ m + k

Tactic:
]

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
⊢ m + L.length ≤ m + L.length

Tactic:
]

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

Goal state before:
pp: X Y : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := Edge.tensor._proof_1 })
ex : Edge x₀ x₁
y₀ y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := Edge.tensor._proof_1 })
ey : Edge y₀ y₁
⊢ homMk (ex.tensor ey) = homMk (ex.tensor ey)

Tactic:
]

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
⊢ ∀ ⦃x y : (X ⊗ Y).obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })⦄ (e : Edge x y),
    (functor X Y ⋙ inverse X Y).map (homMk e) ≫ (Iso.refl ((functor X Y ⋙ inverse X Y).obj (mk y))).hom =
      (Iso.refl ((functor X Y ⋙ inverse X Y).obj (mk x))).hom ≫ (𝟭 (X ⊗ Y).HomotopyCategory).map (homMk e)

Tactic:
rintro ⟨x₀, y₀⟩ ⟨x₁, y₁⟩ e

Goal state after:
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 })
x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge (x₀, y₀) (x₁, y₁)
⊢ (functor X Y ⋙ inverse X Y).map (homMk e) ≫ (Iso.refl ((functor X Y ⋙ inverse X Y).obj (mk (x₁, y₁)))).hom =
    (Iso.refl ((functor X Y ⋙ inverse X Y).obj (mk (x₀, y₀)))).hom ≫ (𝟭 (X ⊗ Y).HomotopyCategory).map (homMk e)
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 })
x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
ex : Edge x₀ x₁
ey : Edge y₀ y₁
⊢ homMk (ex.tensor ey) = homMk (ex.tensor ey)

Tactic:
]

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
⊢ (mk m).1 + b = (mk (m + b)).1

Tactic:
]

Goal state after:
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
⊢ (mk m).1 + b = (mk (m + b)).1
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₁
⊢ homMk (Edge.id x) =
    𝟙
        (mk
          ((ConcreteCategory.hom
              (fst (X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
                (Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))))
            (x, y₀))) ≫
      𝟙 (mk x)

Tactic:
]

Goal state after:
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₁
⊢ homMk (Edge.id x) =
    𝟙
        (mk
          ((ConcreteCategory.hom
              (fst (X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
                (Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))))
            (x, y₀))) ≫
      𝟙 (mk x)
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:
induction hf with
  | id n =>
    use [], n.len, 0, rfl, rfl, rfl, IsAdmissible.nil _
    rfl
  | of f hf =>
    cases hf with | @σ m k =>
    use [k.val], m, 1, rfl, rfl, rfl, IsAdmissible.singleton k.is_le
    simp [standardσ]
  | @comp_of _ j x' g g' hg hg' h_rec =>
    cases hg' with | @σ m k =>
    obtain ⟨L₁, m₁, b₁, h₁', rfl, h', hL₁, e₁⟩ := h_rec
    obtain rfl : m₁ = m + 1 := congrArg (fun x ↦ x.len) h₁'
    use simplicialInsert k.val L₁, m, b₁ + 1, rfl, by grind, by grind, by grind
    subst_vars
    have := standardσ (m₁ := m + 1 + L₁.length) [] (by grind) ≫=
      (standardσ_simplicialInsert L₁ hL₁ k k.prop _ rfl).symm
    simp_all [Fin.ofNat_eq_cast, Fin.cast_val_eq_self, standardσ_comp_standardσ_assoc,
      standardσ_comp_standardσ]

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) ⋙
      CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory

Tactic:
]

Goal state after:
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) ⋙
      CategoryTheory.Prod.snd X.HomotopyCategory Y.HomotopyCategory
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 ⋙
      CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory

Tactic:
]

Goal state after:
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 ⋙
      CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory
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:
]

Goal state after:
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)
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₁
⊢ (mapHomotopyCategory (α_ X Y Z).hom).map
      ((inverse (X ⊗ Y) Z).map (Prod.mkHom (𝟙 ((inverse X Y).obj (mk x, mk y))) (homMk e))) =
    homMk ((Edge.id x).tensor ((Edge.id y).tensor e))

Tactic:
]

Goal state after:
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₁
⊢ (mapHomotopyCategory (α_ X Y Z).hom).map
      ((inverse (X ⊗ Y) Z).map (Prod.mkHom (𝟙 ((inverse X Y).obj (mk x, mk y))) (homMk e))) =
    homMk ((Edge.id x).tensor ((Edge.id y).tensor e))
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₁
z : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ homMk ((Edge.id x).tensor (e.tensor (Edge.id z))) = homMk ((Edge.id x).tensor (e.tensor (Edge.id z)))

Tactic:
]

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
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
⊢ W (Hom.tr (SimplexCategory.σ i) ha ⋯ ≫ Hom.tr g' ⋯ hb)

Tactic:
]

Goal state after:
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
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
⊢ W (Hom.tr (SimplexCategory.σ i) ha ⋯ ≫ Hom.tr g' ⋯ hb)
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: case pos
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 ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Epi f.hom
h₂ : Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f

Tactic:
]

Goal state after:
case pos
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 ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Epi f.hom
h₂ : Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: case pos
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 ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Epi f.hom
h₂ : Mono f.hom
⊢ W f

Tactic:
]

Goal state after:
case pos
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 ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Epi f.hom
h₂ : Mono f.hom
⊢ W f