mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G H : C ⥤ Type (max w v u)
f : G ⟶ H
x✝¹ : C
x✝ : ((𝟭 (C ⥤ Type (max w v u))).obj G).obj x✝¹
⊢ (ConcreteCategory.hom
          (((𝟭 (C ⥤ Type (max w v u))).map f ≫ (functorHomEquiv F H ((tensorLeft F).obj H)).invFun (𝟙 (F ⊗ H))).app
            x✝¹)).toFun
      x✝ =
    (ConcreteCategory.hom
          (((functorHomEquiv F G ((tensorLeft F).obj G)).invFun (𝟙 (F ⊗ G)) ≫ (tensorLeft F ⋙ rightAdj F).map f).app
            x✝¹)).toFun
      x✝

Tactic:
dsimp

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G H : C ⥤ Type (max w v u)
f : G ⟶ H
x✝¹ : C
x✝ : ((𝟭 (C ⥤ Type (max w v u))).obj G).obj x✝¹
⊢ (ConcreteCategory.hom ((f ≫ (functorHomEquiv F H (F ⊗ H)).symm (𝟙 (F ⊗ H))).app x✝¹)) x✝ =
    (ConcreteCategory.hom (((functorHomEquiv F G (F ⊗ G)).symm (𝟙 (F ⊗ G)) ≫ (rightAdj F).map (F ◁ f)).app x✝¹)) x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: K : SSet
x : K _⦋0⦌
Δ Δ' : SimplexCategoryᵒᵖ
f : Δ ⟶ Δ'
⊢ (ConcreteCategory.hom
          ((𝟙_ SSet).map f ≫ ↾fun x_1 ↦ (ConcreteCategory.hom (K.map ((Opposite.unop Δ').const ⦋0⦌ 0).op)) x)).toFun
      PUnit.unit =
    (ConcreteCategory.hom
          ((↾fun x_1 ↦ (ConcreteCategory.hom (K.map ((Opposite.unop Δ).const ⦋0⦌ 0).op)) x) ≫ K.map f)).toFun
      PUnit.unit

Tactic:
dsimp

Goal state after:
K : SSet
x : K _⦋0⦌
Δ Δ' : SimplexCategoryᵒᵖ
f : Δ ⟶ Δ'
⊢ (ConcreteCategory.hom (K.map ((Opposite.unop Δ').const ⦋0⦌ 0).op)) x =
    (ConcreteCategory.hom (K.map f)) ((ConcreteCategory.hom (K.map ((Opposite.unop Δ).const ⦋0⦌ 0).op)) x)
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ : Center C
f : X₁ ⟶ X₂
Y : Center C
U : C
⊢ 𝟙 ((X₁.fst ⊗ Y.fst) ⊗ U) ⊗≫
      (f.f ▷ (Y.fst ⊗ U) ≫ X₂.fst ◁ (Y.snd.β U).hom) ⊗≫ (X₂.snd.β U).hom ▷ Y.fst ⊗≫ 𝟙 (U ⊗ X₂.fst ⊗ Y.fst) =
    𝟙 ((X₁.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X₁.fst ◁ (Y.snd.β U).hom ⊗≫ (f.f ▷ U ≫ (X₂.snd.β U).hom) ▷ Y.fst ⊗≫ 𝟙 (U ⊗ X₂.fst ⊗ Y.fst)

Tactic:
← whisker_exchange

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁ X₂ : Center C
f : X₁ ⟶ X₂
Y : Center C
U : C
⊢ 𝟙 ((X₁.fst ⊗ Y.fst) ⊗ U) ⊗≫
      (X₁.fst ◁ (Y.snd.β U).hom ≫ f.f ▷ (U ⊗ Y.fst)) ⊗≫ (X₂.snd.β U).hom ▷ Y.fst ⊗≫ 𝟙 (U ⊗ X₂.fst ⊗ Y.fst) =
    𝟙 ((X₁.fst ⊗ Y.fst) ⊗ U) ⊗≫
      X₁.fst ◁ (Y.snd.β U).hom ⊗≫ (f.f ▷ U ≫ (X₂.snd.β U).hom) ▷ Y.fst ⊗≫ 𝟙 (U ⊗ X₂.fst ⊗ Y.fst)
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C✝ : Type u₁
inst✝² : EnrichedCategory V C✝
C : Type v
inst✝¹ : EnrichedCategory (Type v) C
D : Type v
inst✝ : EnrichedCategory (Type v) D
F G : EnrichedFunctor (Type v) C D
α : Type vᵒᵖ
σ : (yoneda.obj (enrichedFunctorTypeEquivFunctor F ⟶ enrichedFunctorTypeEquivFunctor G)).obj α
X Y : C
⊢ (((Center.ofBraided (Type v)).obj (unop α)).snd.β (X ⟶[Type v] Y)).hom ≫
      (F.map X Y ⊗ₘ ↾fun x ↦ ((TypeCat.Hom.hom σ) x).app Y) ≫ eComp (Type v) (F.obj X) (F.obj Y) (G.obj Y) =
    ((↾fun x ↦ ((TypeCat.Hom.hom σ) x).app X) ⊗ₘ G.map X Y) ≫ eComp (Type v) (F.obj X) (G.obj X) (G.obj Y)

Tactic:
ext ⟨x, f⟩; exact (σ.hom x).naturality f

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

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : X.obj n
y : Y.obj n
⊢ (x, y) ∈ (⊤.prod T ⊓ S.prod ⊤).obj n ↔ (x, y) ∈ (S.prod T).obj n

Tactic:
change _ ∧ _ ↔ _

Goal state after:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : X.obj n
y : Y.obj n
⊢ (x, y) ∈ (⊤.prod T).obj n ∧ (x, y) ∈ (S.prod ⊤).obj n ↔ (x, y) ∈ (S.prod T).obj n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : Y.obj n
y : X.obj n
⊢ (x, y) ∈ ((S.unionProd T).preimage (β_ Y X).hom).obj n ↔ (x, y) ∈ (T.unionProd S).obj n

Tactic:
dsimp

Goal state after:
X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
n : SimplexCategoryᵒᵖ
x : Y.obj n
y : X.obj n
⊢ (x, y) ∈ ((S.unionProd T).preimage (β_ Y X).hom).obj n ↔ (x, y) ∈ (T.unionProd S).obj n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ (S.unionProd T).preimage (β_ Y X).hom = T.unionProd S

Tactic:
by
  ext n ⟨x, y⟩
  dsimp
  simp only [mem_unionProd_iff, preimage_obj, Monoidal.tensorObj_obj,
    dsimp% Set.mem_preimage (f := (β_ Y X).hom.app n)]
  tauto

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

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ (S.unionProd T).preimage (β_ X Y).inv = T.unionProd S

Tactic:
apply preimage_β_hom

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Center

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U : C
⊢ (X.snd.β Y.fst).hom ▷ U ≫ ((Y ⊗ X).snd.β U).hom = ((X ⊗ Y).snd.β U).hom ≫ U ◁ (X.snd.β Y.fst).hom

Tactic:
dsimp

Goal state after:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X Y : Center C
U : C
⊢ (X.snd.β Y.fst).hom ▷ U ≫
      (α_ Y.fst X.fst U).hom ≫
        Y.fst ◁ (X.snd.β U).hom ≫ (α_ Y.fst U X.fst).inv ≫ (Y.snd.β U).hom ▷ X.fst ≫ (α_ U Y.fst X.fst).hom =
    ((α_ X.fst Y.fst U).hom ≫
        X.fst ◁ (Y.snd.β U).hom ≫ (α_ X.fst U Y.fst).inv ≫ (X.snd.β U).hom ▷ Y.fst ≫ (α_ U X.fst Y.fst).hom) ≫
      U ◁ (X.snd.β Y.fst).hom
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: C : Type u
inst✝ : Category.{max u v, u} C
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ (Cat.FreeRefl.quotientFunctor C ⋙ (adj.counit.app (Cat.of C)).toFunctor).map f.toPath =
    eqToHom ⋯ ≫ (pathComposition C).map f.toPath ≫ eqToHom ⋯

Tactic:
dsimp

Goal state after:
C : Type u
inst✝ : Category.{max u v, u} C
x✝¹ x✝ : C
f : x✝¹ ⟶ x✝
⊢ (adj.counit.app (Cat.of C)).toFunctor.map ((Cat.FreeRefl.quotientFunctor C).map f.toPath) =
    𝟙 ((adj.counit.app (Cat.of C)).toFunctor.obj ((Cat.FreeRefl.quotientFunctor C).obj x✝¹)) ≫
      composePath f.toPath ≫ 𝟙 x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : Fin n
⊢ (ConcreteCategory.hom
        (((Truncated.trunc (0 + 1) 1 ⋯).obj ((truncation 1).obj X)).map
          (Hom.tr (SimplexCategory.δ 0) Truncated.Path₁._proof_1 Truncated.Path₁._proof_5).op))
      ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x) =
    (ConcreteCategory.hom
        (s.π.app
          (StructuredArrow.mk
            (((inclusion 2).obj (unop (op { obj := ⦋0⦌, property := lift._proof_2 }))).const ⦋n⦌ i.succ).op)))
      x

Tactic:
dsimp

Goal state after:
X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : Fin n
⊢ (ConcreteCategory.hom
        (((Truncated.trunc 1 1 ⋯).obj ((truncation 1).obj X)).map
          (Hom.tr (SimplexCategory.δ 0) Truncated.Path₁._proof_1 Truncated.Path₁._proof_5).op))
      ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x) =
    (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ i.succ).op))) x
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 j : ℕ
hij : i ≤ j
hj : j ≤ n
k : ℕ
hk : 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

Tactic:
revert i j

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
⊢ ∀ (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
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 ⟶
  strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
| (ConcreteCategory.hom (s.π.app (strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) fac_aux₁._proof_1))) x

Tactic:
dsimp

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, ⋯⟩
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1 ⟶
  strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
| (ConcreteCategory.hom (s.π.app (strArrowMk₂ (⦋1⦌.const ⦋n⦌ ⟨i, ⋯⟩) fac_aux₁._proof_1))) x
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✝
hf : r.degHom f = r.deg X✝
X Y : C
i : X✝ ⟶ Y✝
hi : W₂ i
h : r.degHom f = r.deg X✝
hp : W₁ (𝟙 X✝)
fac : 𝟙 X✝ ≫ i = f
⊢ i = f

Tactic:
by simpa using fac

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✝
hf : r.degHom f = r.deg Y✝
X Y : C
p : X✝ ⟶ Y✝
hp : W₁ p
h : r.degHom f = r.deg Y✝
hi : W₂ (𝟙 Y✝)
fac : p ≫ 𝟙 Y✝ = f
⊢ p = f

Tactic:
by simpa using fac

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
⊢ (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

Tactic:
let β₀ : α ⟶ α₀ := StructuredArrow.homMk ((Hom.tr (mkOfSucc 1)).op) (Quiver.Hom.unop_inj
        (by ext x; fin_cases x <;> rfl))

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 ⋯
⊢ (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
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)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
h'' : δ k ≫ σ i = 𝟙 (mk (n + 1))
⊢ (f ≫ δ k) ≫ σ i = 𝟙 x ≫ f

Tactic:
simp [h'']

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

Goal state before:
pp: case succ.comp_of.inr.inl
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)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
h'' : δ k ≫ σ i = 𝟙 (mk (n + 1))
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Tactic:
exact ⟨_, _, _, P_σ.id_mem _, hf, by simp [h'']⟩

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 })
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₁
⊢ (functor X Y ⋙ inverse X Y).map (homMk (ex.tensor ey)) ≫
      (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 (ex.tensor ey))

Tactic:
dsimp

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 })
ex : Edge x₀ x₁
ey : Edge y₀ y₁
⊢ (inverse X Y).map (homMk ex, homMk ey) ≫ 𝟙 (mk (x₁, y₁)) = 𝟙 (mk (x₀, y₀)) ≫ homMk (ex.tensor ey)
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:
dsimp

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

Tactic:
dsimp

Goal state after:
X X' Y Y' Z : Truncated 2
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 (Edge.id y) ≫
      𝟙
        (mk
          ((ConcreteCategory.hom
              (snd (X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
                (Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))))
            (x₁, y))) =
    𝟙
        (mk
          ((ConcreteCategory.hom
              (snd (X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
                (Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))))
            (x₀, y))) ≫
      𝟙 (mk y)
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:
dsimp

Goal state after:
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
n : ℕ
hn : n < d
i : Fin (n + 2)
⊢ n ≤ d
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:
dsimp

Goal state after:
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
n : ℕ
hn : n < d
i : Fin (n + 2)
⊢ n + 1 ≤ d
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:
dsimp

Goal state after:
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)
⊢ n + 1 ≤ d
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:
dsimp

Goal state after:
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)
⊢ n ≤ d
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:
dsimp

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).map (Prod.mkHom (𝟙 (mk x)) (𝟙 (mk y)))) (homMk e))) ≫
      𝟙
        ((((Functor.curry₃.obj
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                  (mk x)).obj
              (mk y)).obj
          (mk z₁)) =
    𝟙
        ((((Functor.curry₃.obj
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                  (mk x)).obj
              (mk y)).obj
          (mk z₀)) ≫
      (inverse X (Y ⊗ Z)).map (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (𝟙 (mk y), homMk e)))