mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
v : V
⊢ FreeRefl.homMk (F.map (𝟙rq v)) = 𝟙 (FreeRefl.mk (F.obj v))

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
X : ReflQuiv
⊢ ∀ (v : ↑X),
    (freeReflMap (𝟙 X)).toCatHom.toFunctor.obj (FreeRefl.mk v) = (𝟙 (of (FreeRefl ↑X))).toFunctor.obj (FreeRefl.mk v)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
X : ReflQuiv
⊢ ∀ {v w : ↑X} (f : v ⟶ w),
    (freeReflMap (𝟙 X)).toCatHom.toFunctor.map (FreeRefl.homMk f) =
      eqToHom ⋯ ≫ (𝟙 (of (FreeRefl ↑X))).toFunctor.map (FreeRefl.homMk f) ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
X Y Z : ReflQuiv
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ (v : ↑X),
    (freeReflMap (f ≫ g)).toCatHom.toFunctor.obj (FreeRefl.mk v) =
      ((freeReflMap f).toCatHom ≫ (freeReflMap g).toCatHom).toFunctor.obj (FreeRefl.mk v)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : Type u_2
inst✝ : ReflQuiver W
F : V ⥤rq W
X Y Z : ReflQuiv
f : X ⟶ Y
g : Y ⟶ Z
⊢ ∀ {v w : ↑X} (f_1 : v ⟶ w),
    (freeReflMap (f ≫ g)).toCatHom.toFunctor.map (FreeRefl.homMk f_1) =
      eqToHom ⋯ ≫ ((freeReflMap f).toCatHom ≫ (freeReflMap g).toCatHom).toFunctor.map (FreeRefl.homMk f_1) ≫ eqToHom ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝² : ReflQuiver W
inst✝¹ : ReflQuiver V
C : Type u_3
inst✝ : Category.{v_1, u_3} C
F : V ⥤rq W
G : W ⥤rq C
⊢ ∀ (v : V),
    (homEquiv.symm (F ⋙rq G)).obj (Cat.FreeRefl.mk v) = (Cat.freeReflMap F ⋙ homEquiv.symm G).obj (Cat.FreeRefl.mk v)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
W : Type u_2
inst✝² : ReflQuiver W
inst✝¹ : ReflQuiver V
C : Type u_3
inst✝ : Category.{v_1, u_3} C
F : V ⥤rq W
G : W ⥤rq C
⊢ ∀ {v w : V} (f : v ⟶ w),
    (homEquiv.symm (F ⋙rq G)).map (Cat.FreeRefl.homMk f) =
      eqToHom ⋯ ≫ (Cat.freeReflMap F ⋙ homEquiv.symm G).map (Cat.FreeRefl.homMk f) ≫ eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
V : Cᵒᵖ ⥤ Type w
X Y Z : C
α : X ⟶ Y
β : Y ⟶ Z
φ : (fun X ↦ X) (V.obj (op Z))
⊢ (ConcreteCategory.hom (V.map α.op)) ((ConcreteCategory.hom (V.map β.op)) φ) =
    (ConcreteCategory.hom (V.map (α ≫ β).op)) φ

Tactic:
simp

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
i : ℕ
hij : i ≤ i
hj : i ≤ n
this : mkOfLe ⟨i, ⋯⟩ ⟨i, ⋯⟩ ⋯ = ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩
⊢ (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1).hom ≫ (inclusion 2).op.map (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op =
    (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_3).hom

Tactic:
simp

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hij : i ≤ i
hj : i ≤ n
this : mkOfLe ⟨i, ⋯⟩ ⟨i, ⋯⟩ ⋯ = ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩
⊢ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩).op ≫ (⦋1⦌.const ⦋0⦌ 0).op = (⦋1⦌.const ⦋n⦌ ⟨i, ⋯⟩).op
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
⊢ (morphismPropertyHomMk V).multiplicativeClosure ≤ ⊤

Tactic:
simp

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

Goal state before:
pp: V : Truncated 2
x y : V.HomotopyCategory
f : x.as ⟶ y.as
x✝ : ⊤ ((quotientFunctor V).map f)
⊢ ⊤ f

Tactic:
simp

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

Goal state before:
pp: V : Truncated 2
W : MorphismProperty V.HomotopyCategory
inst✝ : W.IsMultiplicative
hW : ∀ {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} (e : Edge x y), W (homMk e)
⊢ W ≤ ⊤

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Functor.CurryingThree

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₁₂ : Type u_3
C₃ : Type u_4
C₂₃ : Type u_5
D₁ : Type u_6
D₂ : Type u_7
D₃ : Type u_8
E : Type u_9
inst✝⁸ : Category.{v_1, u_1} C₁
inst✝⁷ : Category.{v_2, u_2} C₂
inst✝⁶ : Category.{v_3, u_4} C₃
inst✝⁵ : Category.{v_4, u_3} C₁₂
inst✝⁴ : Category.{v_5, u_5} C₂₃
inst✝³ : Category.{v_6, u_6} D₁
inst✝² : Category.{v_7, u_7} D₂
inst✝¹ : Category.{v_8, u_8} D₃
inst✝ : Category.{v_9, u_9} E
X✝ Y✝ : C₁ ⥤ C₂ ⥤ C₃ ⥤ E
f : X✝ ⟶ Y✝
x✝¹ x✝ : C₁
g : x✝¹ ⟶ x✝
⊢ X✝.flip₂₃.map g ≫ { app := fun Y ↦ { app := fun Z ↦ ((f.app x✝).app Z).app Y, naturality := ⋯ }, naturality := ⋯ } =
    { app := fun Y ↦ { app := fun Z ↦ ((f.app x✝¹).app Z).app Y, naturality := ⋯ }, naturality := ⋯ } ≫ Y✝.flip₂₃.map g

Tactic:
ext
      simp only [flip₂₃_obj_obj_obj, NatTrans.comp_app, flip₂₃_map_app_app]
      simp [← NatTrans.comp_app]

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

Goal state before:
pp: V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F G : V.HomotopyCategory ⥤ D
φ : (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })) → F.obj (mk x) ⟶ G.obj (mk x)
hφ :
  ∀ ⦃x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })⦄ (e : Edge x y),
    F.map (homMk e) ≫ φ y = φ x ≫ G.map (homMk e)
x✝¹ x✝ : V.HomotopyCategory
f : x✝¹ ⟶ x✝
this : (MorphismProperty.naturalityProperty fun x ↦ φ x.1.as) = ⊤
⊢ ⊤ f

Tactic:
simp

Goal state after:
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: case pos
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
f : X ⟶ Y
hf : W₁ f
hf' : MorphismProperty.identities C f
⊢ r.deg Y ≤ r.deg X

pp: case neg
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
f : X ⟶ Y
hf : W₁ f
hf' : ¬MorphismProperty.identities C f
⊢ r.deg Y ≤ r.deg X

Tactic:
· cases hf'
    rfl

Goal state after:
case neg
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
f : X ⟶ Y
hf : W₁ f
hf' : ¬MorphismProperty.identities C f
⊢ r.deg Y ≤ r.deg X
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: case pos
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
f : X ⟶ Y
hf : W₂ f
hf' : MorphismProperty.identities C f
⊢ r.deg X ≤ r.deg Y

pp: case neg
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
f : X ⟶ Y
hf : W₂ f
hf' : ¬MorphismProperty.identities C f
⊢ r.deg X ≤ r.deg Y

Tactic:
· cases hf'
    rfl

Goal state after:
case neg
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
f : X ⟶ Y
hf : W₂ f
hf' : ¬MorphismProperty.identities C f
⊢ r.deg X ≤ r.deg Y
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V W x✝ : Truncated 2
⊢ ∀ (x : x✝.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })),
    (mapHomotopyCategory (𝟙 x✝)).toCatHom.toFunctor.obj (HomotopyCategory.mk x) =
      (𝟙 (Cat.of x✝.HomotopyCategory)).toFunctor.obj (HomotopyCategory.mk x)

Tactic:
simp

Goal state after:
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
f : X ⟶ Y
fac : W₁.MapFactorizationData W₂ f
this : Subsingleton (W₁.MapFactorizationData W₂ f)
⊢ ∃ (h : fac.Z = fac.Z), fac.i = fac.i ≫ eqToHom ⋯ ∧ fac.p = eqToHom h ≫ fac.p

Tactic:
simp

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

Goal state before:
pp: V W X✝ Y✝ Z✝ : Truncated 2
x✝¹ : X✝ ⟶ Y✝
x✝ : Y✝ ⟶ Z✝
⊢ ∀ (x : X✝.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })),
    (mapHomotopyCategory (x✝¹ ≫ x✝)).toCatHom.toFunctor.obj (HomotopyCategory.mk x) =
      ((mapHomotopyCategory x✝¹).toCatHom ≫ (mapHomotopyCategory x✝).toCatHom).toFunctor.obj (HomotopyCategory.mk x)

Tactic:
simp

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
⊢ ⟨i, ⋯⟩ ≤ ⟨i + k, ⋯⟩

Tactic:
simp

Goal state after:
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 : C
⊢ 𝟙 X ≫ 𝟙 X = 𝟙 X

Tactic:
simp

Goal state after:
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 ≫ e.hom = e.hom

Tactic:
simp

Goal state after:
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
⊢ e.hom ≫ 𝟙 Y = e.hom

Tactic:
simp

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
⊢ ⟨i, ⋯⟩ ≤ ⟨i + k, ⋯⟩

Tactic:
simp

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

Goal state before:
pp: ⊢ generators.multiplicativeClosure ≤ ⊤

Tactic:
simp

Goal state after:
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
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
⊢ generators.multiplicativeClosure f → P f

Tactic:
hf

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
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
hf : generators.multiplicativeClosure f
⊢ 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
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
⊢ generators.multiplicativeClosure' f → P f

Tactic:
hf

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
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
hf : generators.multiplicativeClosure' f
⊢ P f
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
⊢ i ≤ i + k

Tactic:
simp

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

Goal state before:
pp: case of.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
n✝ : ℕ
i✝ : Fin (n✝ + 2)
⊢ (mk n✝).len < (mk (n✝ + 1)).len

Tactic:
simp

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

Goal state before:
pp: case h
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
⊢ 𝟙 x✝ = eqToHom ⋯

Tactic:
simp

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

Goal state before:
pp: i : Fin (0 + 1)
⊢ 𝟙 (mk (0 + 1)) ≫ σ i = σ i ≫ 𝟙 (mk 0)

Tactic:
simp

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

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

Tactic:
simp

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

Goal state before:
pp: case h
x y : SimplexCategoryGenRel
n : ℕ
⊢ 𝟙 (mk n) = 𝟙 (mk n) ≫ 𝟙 (mk n)

Tactic:
simp

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

Goal state before:
pp: x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 2)
z : SimplexCategoryGenRel
e : mk n ⟶ z
m : z ⟶ mk n'
he : P_σ e
hm : P_δ m
⊢ (e ≫ m) ≫ δ j = e ≫ m ≫ δ j

Tactic:
simp

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

Goal state before:
pp: x y : SimplexCategoryGenRel
n n' : ℕ
j : Fin (n' + 1)
e : mk n ⟶ mk (n' + 1)
he : P_σ e
⊢ (e ≫ 𝟙 (mk (n' + 1))) ≫ σ j = (e ≫ σ j) ≫ 𝟙 (mk n')

Tactic:
simp

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

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

Tactic:
simp

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

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

Tactic:
induction L using List.twoStepInduction generalizing m with

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

Goal state before:
pp: case nil
L₁ : List ℕ
m₁ m₃ : ℕ
h : m₃ + L₁.length = m₁
h' : m₃ + [].length = m₃
⊢ standardσ L₁ h ≫ standardσ [] h' = standardσ ([] ++ L₁) ⋯

Tactic:
simp

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

Goal state before:
pp: case cons
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₁ m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hk : m₂ + (a :: L).length = m₁
hj : j < m₁ + 1
⊢ ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ (a :: L) hk))) ⟨j, hj⟩) =
    simplicialEvalσ (a :: L) j

Tactic:
simp only [List.length_cons] at hk

Goal state after:
case cons
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₁ m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hk : m₂ + (L.length + 1) = m₁
hj : j < m₁ + 1
⊢ ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ (a :: L) hk))) ⟨j, hj⟩) =
    simplicialEvalσ (a :: L) j
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 })
⊢ ∀ (x_1 : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })),
    homMk ((Edge.id x).tensor (Edge.id x_1)) = 𝟙 (mk (x, x_1))

Tactic:
simp

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

Goal state before:
pp: case pos
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
⊢ standardσ (j :: a :: L) ⋯ = standardσ (a :: L) ⋯ ≫ σ (Fin.ofNat (m + 1) j)

Tactic:
simp

Goal state after:
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
⊢ ∀ (j k : ℕ), j < k + 1 → ↑(Fin.ofNat (k + 1) j) = j

Tactic:
simp

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₁
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ ((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).app
      (mk y) =
    ((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)).app
      (mk y)

Tactic:
simp

Goal state after:
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₁
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ homMk ((e.map f).tensor (Edge.id y)) ≫
      𝟙 (mk ((ConcreteCategory.hom (f.app (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))) x₁, y)) =
    𝟙 (mk ((ConcreteCategory.hom (f.app (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))) x₀, y)) ≫
      homMk ((e.map f).tensor (Edge.id y))
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₁
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
⊢ ((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).app
      (mk y) =
    ((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)).app
      (mk y)

Tactic:
simp

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