mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ ((s.cofan Δ).inj A ≫ s.desc Δ fun B_1 ↦ if h : B_1 = B then eqToHom ⋯ else 0) = 0

Tactic:
ι_desc,

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A B : IndexSet Δ
h : B ≠ A
⊢ (if h : A = B then eqToHom ⋯ else 0) = 0
Module: Mathlib.AlgebraicTopology.DoldKan.GammaCompN

Goal state before:
pp: case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
A : Splitting.IndexSet (op ⦋n⦌)
⊢ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫
      ((Γ₀.splitting X).desc (op ⦋n⦌) fun A ↦ 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A) ≫
        PInfty.f n =
    ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫ PInfty.f n

Tactic:
rw [Splitting.ι_desc_assoc, assoc]

Goal state after:
case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : ChainComplex C ℕ
n : ℕ
A : Splitting.IndexSet (op ⦋n⦌)
⊢ 𝟙 (X.X (unop A.fst).len) ≫ ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫ PInfty.f n =
    ((Γ₀.splitting X).cofan (op ⦋n⦌)).inj A ≫ PInfty.f n
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
n m : ℕ
i : ⦋m⦌ ⟶ ⦋n⦌
hi : Mono i
h₁ : ⦋m⦌.len ≠ n
h₂ : ¬Isδ₀ i
h : ⦋n⦌ = ⦋m⦌
⊢ False

Tactic:
rw [← h] at h₁
        exact h₁ rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ PInfty.f (m + k + 1 + 1) ≫ X.map ((i ≫ SimplexCategory.δ j₂) ≫ SimplexCategory.δ 0).op = 0

Tactic:
rw [assoc, ← SimplexCategory.δ_comp_δ'' (Fin.zero_le _)]

Goal state after:
case pos
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
m k : ℕ
h₁ : ⦋m⦌.len ≠ m + k + 1 + 1
j₂ : Fin (m + k + 2)
i : ⦋m⦌ ⟶ ⦋m + k⦌
⊢ PInfty.f (m + k + 1 + 1) ≫ X.map (i ≫ SimplexCategory.δ (Fin.castLT 0 ⋯) ≫ SimplexCategory.δ j₂.succ).op = 0
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
f : C(X, Y)
t x : ↑I
hx : x ∈ {0, 1}
⊢ { toFun := fun x ↦ (⇑f ∘ ⇑F) (t, x), continuous_toFun := ⋯ } x = (p.map ⋯).toContinuousMap x

Tactic:
by
    rcases hx with hx | hx
    · simp [hx]
    · rw [Set.mem_singleton_iff] at hx
      simp [hx]

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f
⊢ weakEquivalences (BifibrantObject C) f

Tactic:
weakEquivalence_iff

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : BifibrantObject C
f : X ⟶ Y
hf : weakEquivalences (BifibrantObject C) f
⊢ weakEquivalences (BifibrantObject C) f
Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (cofibrations C).HasFactorization (trivialFibrations C)
inst✝⁵ : HasPushouts C
inst✝⁴ : (cofibrations C).IsStableUnderComposition
inst✝³ : (cofibrations C).IsStableUnderCobaseChange
h✝ : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (pushout.desc p g ⋯) :=
  (cofibrations C).factorizationData (trivialFibrations C) (pushout.desc p g ⋯)
sq' : CommSq (𝟙 X) (pushout.inl f i ≫ h.i) p h.p
h₁ : WeakEquivalence ((pushout.inl f i ≫ h.i) ≫ h.p)
h₂ : Cofibration (pushout.inl f i ≫ h.i)
⊢ WeakEquivalence (pushout.inl f i ≫ h.i)

Tactic:
weakEquivalence_iff

Goal state after:
C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (cofibrations C).HasFactorization (trivialFibrations C)
inst✝⁵ : HasPushouts C
inst✝⁴ : (cofibrations C).IsStableUnderComposition
inst✝³ : (cofibrations C).IsStableUnderCobaseChange
h✝ : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence i] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence p
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (cofibrations C).MapFactorizationData (trivialFibrations C) (pushout.desc p g ⋯) :=
  (cofibrations C).factorizationData (trivialFibrations C) (pushout.desc p g ⋯)
sq' : CommSq (𝟙 X) (pushout.inl f i ≫ h.i) p h.p
h₁ : weakEquivalences C ((pushout.inl f i ≫ h.i) ≫ h.p)
h₂ : Cofibration (pushout.inl f i ≫ h.i)
⊢ weakEquivalences C (pushout.inl f i ≫ h.i)
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
X₁ X₂ : CofibrantObject C
f : X₁ ⟶ X₂
inst✝ : WeakEquivalence f
⊢ WeakEquivalence (bifibrantResolutionMap f)

Tactic:
weakEquivalence_iff

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
X₁ X₂ : CofibrantObject C
f : X₁ ⟶ X₂
inst✝ : WeakEquivalence f
⊢ weakEquivalences (BifibrantObject C) (bifibrantResolutionMap f)
Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (trivialCofibrations C).HasFactorization (fibrations C)
inst✝⁵ : HasPullbacks C
inst✝⁴ : (fibrations C).IsStableUnderComposition
inst✝³ : (fibrations C).IsStableUnderBaseChange
h✝ : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (pullback.lift f i ⋯) :=
  (trivialCofibrations C).factorizationData (fibrations C) (pullback.lift f i ⋯)
sq' : CommSq h.i i (h.p ≫ pullback.snd p g) (𝟙 B)
h₁ : WeakEquivalence (h.i ≫ h.p ≫ pullback.snd p g)
h₂ : Fibration (h.p ≫ pullback.snd p g)
⊢ WeakEquivalence (h.p ≫ pullback.snd p g)

Tactic:
weakEquivalence_iff

Goal state after:
C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (trivialCofibrations C).HasFactorization (fibrations C)
inst✝⁵ : HasPullbacks C
inst✝⁴ : (fibrations C).IsStableUnderComposition
inst✝³ : (fibrations C).IsStableUnderBaseChange
h✝ : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
h : (trivialCofibrations C).MapFactorizationData (fibrations C) (pullback.lift f i ⋯) :=
  (trivialCofibrations C).factorizationData (fibrations C) (pullback.lift f i ⋯)
sq' : CommSq h.i i (h.p ≫ pullback.snd p g) (𝟙 B)
h₁ : weakEquivalences C (h.i ≫ h.p ≫ pullback.snd p g)
h₂ : Fibration (h.p ≫ pullback.snd p g)
⊢ weakEquivalences C (h.p ≫ pullback.snd p g)
Module: Mathlib.AlgebraicTopology.ModelCategory.JoyalTrick

Goal state before:
pp: C : Type u_1
inst✝¹¹ : Category.{v_1, u_1} C
inst✝¹⁰ : CategoryWithCofibrations C
inst✝⁹ : CategoryWithFibrations C
inst✝⁸ : CategoryWithWeakEquivalences C
inst✝⁷ : (weakEquivalences C).HasTwoOutOfThreeProperty
inst✝⁶ : (trivialCofibrations C).HasFactorization (fibrations C)
inst✝⁵ : HasPullbacks C
inst✝⁴ : (fibrations C).IsStableUnderComposition
inst✝³ : (fibrations C).IsStableUnderBaseChange
h : ∀ {A B X Y : C} (i : A ⟶ B) (p : X ⟶ Y) [Cofibration i] [WeakEquivalence p] [Fibration p], HasLiftingProperty i p
A B X Y : C
i : A ⟶ B
p : X ⟶ Y
inst✝² : Cofibration i
inst✝¹ : Fibration p
inst✝ : WeakEquivalence i
f : A ⟶ X
g : B ⟶ Y
sq : CommSq f i p g
⊢ sq.HasLift

Tactic:
by
    let h := factorizationData (trivialCofibrations C) (fibrations C)
      (pullback.lift f i sq.w)
    have sq' : CommSq h.i i (h.p ≫ pullback.snd _ _) (𝟙 B) := .mk
    have h₁ : WeakEquivalence (h.i ≫ h.p ≫ pullback.snd p g) := by simpa
    have h₂ := comp_mem _ _ _ h.hp ((fibrations C).of_isPullback
      (IsPullback.of_hasPullback p g) (mem_fibrations p))
    rw [← fibration_iff] at h₂
    have : WeakEquivalence (h.p ≫ pullback.snd p g) := by
      rw [weakEquivalence_iff] at h₁ ⊢
      exact of_precomp _ _ _ h.hi.2 h₁
    exact ⟨⟨{ l := sq'.lift ≫ h.p ≫ pullback.fst p g
              fac_right := by
                rw [assoc, assoc, pullback.condition, reassoc_of% sq'.fac_right] }⟩⟩

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ Λ[n, i].toSSet.HasDimensionLT n

Tactic:
rw [horn_eq_iSup, hasDimensionLT_iSup_iff]
  intro i
  exact stdSimplex.hasDimensionLT_face _ _ (by simp [Finset.card_compl])

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

Goal state before:
pp: n : ℕ
⊢ ∂Δ[n].toSSet.HasDimensionLT n

Tactic:
rw [boundary_eq_iSup, hasDimensionLT_iSup_iff]
  intro i
  exact stdSimplex.hasDimensionLT_face _ _ (by simp [Finset.card_compl])

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

Goal state before:
pp: case zero
m : ℕ
h : m < 0
f : unop (op ⦋m⦌) ⟶ ⦋0⦌
⊢ stdSimplex.objEquiv.symm f ∈ ∂Δ[0].obj (op ⦋m⦌)

pp: case succ
m n : ℕ
h : m < n + 1
f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
⊢ stdSimplex.objEquiv.symm f ∈ ∂Δ[n + 1].obj (op ⦋m⦌)

Tactic:
· simp at h

Goal state after:
case succ
m n : ℕ
h : m < n + 1
f : unop (op ⦋m⦌) ⟶ ⦋n + 1⦌
⊢ stdSimplex.objEquiv.symm f ∈ ∂Δ[n + 1].obj (op ⦋m⦌)
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
S₁ S₂ S₃ S₄ : Set X
h : Lattice.BicartSq S₁ S₂ S₃ S₄
⊢ (MultispanShape.ofLinearOrder Bool).fst default ≠ (MultispanShape.ofLinearOrder Bool).snd default

Tactic:
by tauto

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr_inl.inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inl ((ConcreteCategory.hom f) s✝))

pp: case inr_inl.inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ w✝¹ w✝ : S
h : (ConcreteCategory.hom g) w✝¹ = (ConcreteCategory.hom g) w✝
h' : (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) w✝¹
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inl ((ConcreteCategory.hom f) w✝))

Tactic:
· apply Rel'.inr_inl

Goal state after:
case inr_inl.inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ w✝¹ w✝ : S
h : (ConcreteCategory.hom g) w✝¹ = (ConcreteCategory.hom g) w✝
h' : (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) w✝¹
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inl ((ConcreteCategory.hom f) w✝))
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: ⊢ IsPushout (stdSimplex.δ 0) (stdSimplex.δ 1) ι₀₁ ι₁₂

Tactic:
apply sq.{u}.isPushout.of_iso' (stdSimplex.faceSingletonIso _)
    (stdSimplex.facePairIso _ _ (by simp)) (stdSimplex.facePairIso _ _ (by simp))
    (Iso.refl _)
  all_goals decide

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ (sx.spineEquiv l ⋯) ((ConcreteCategory.hom (X.map (tr (subinterval j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f)) =
    (sx.spineEquiv l ⋯) (sx.spineToSimplex l ⋯ (f.interval j l hjl))

Tactic:
dsimp only [spineEquiv, Equiv.coe_fn_mk]

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ X.spine l ⋯ ((ConcreteCategory.hom (X.map (tr (subinterval j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f)) =
    X.spine l ⋯ (sx.spineToSimplex l ⋯ (f.interval j l hjl))
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ (sx.spineEquiv l) ((ConcreteCategory.hom (X.map (subinterval j l hjl).op)) (sx.spineToSimplex f)) =
    (sx.spineEquiv l) (sx.spineToSimplex (f.interval j l hjl))

Tactic:
dsimp only [spineEquiv, Equiv.coe_fn_mk]

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ X.spine l ((ConcreteCategory.hom (X.map (subinterval j l hjl).op)) (sx.spineToSimplex f)) =
    X.spine l (sx.spineToSimplex (f.interval j l hjl))
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝³ : Category.{w, v} V
inst✝² : MonoidalCategory V
C : Type u₁
D : Type u₂
inst✝¹ : EnrichedCategory V C
inst✝ : EnrichedCategory V D
F G : EnrichedFunctor V C D
h_obj : ∀ (X : C), F.obj X = G.obj X
h_map : ∀ (X Y : C), F.map X Y ≫ eqToHom ⋯ = G.map X Y
⊢ F = G

Tactic:
match F, G with
  | mk F_obj F_map _ _, mk G_obj G_map _ _ =>
    obtain rfl : F_obj = G_obj := funext fun X ↦ h_obj X
    congr
    ext X Y
    simpa using h_map X Y

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

Goal state before:
pp: x✝¹ : SSet
x✝ : x✝¹ ⟶ Δ[0]
⊢ x✝ = SSet.const (obj₀Equiv.symm 0)

Tactic:
ext ⟨n⟩

Goal state after:
x✝² : SSet
x✝¹ : x✝² ⟶ Δ[0]
n : SimplexCategory
x✝ : x✝².obj (Opposite.op n)
⊢ (ConcreteCategory.hom (x✝¹.app (Opposite.op n))).toFun x✝ =
    (ConcreteCategory.hom ((SSet.const (obj₀Equiv.symm 0)).app (Opposite.op n))).toFun x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: case mpr
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
x₁ : X₁.obj m
x₂ : X₂.obj m
⊢ ((ConcreteCategory.hom (f₁.app m)) x₁, (ConcreteCategory.hom (f₂.app m)) x₂) ∈ (range (f₁ ⊗ₘ f₂)).obj m

Tactic:
exact ⟨⟨x₁, x₂⟩, rfl⟩

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F (ForgetEnrichment V D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf W
      ((Functor.LaxMonoidal.ε F ≫
          F.map (λ_ (𝟙_ V)).inv ≫ F.map (ForgetEnrichment.homTo V f ⊗ₘ ForgetEnrichment.homTo V g)) ≫
        F.map (eComp V (ForgetEnrichment.to V X✝) (ForgetEnrichment.to V Y✝) (ForgetEnrichment.to V Z✝))) =
    ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V f)) ≫
      ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V g))

Tactic:
← Functor.LaxMonoidal.left_unitality_inv,

Goal state after:
V : Type u'
inst✝¹⁰ : Category.{v', u'} V
inst✝⁹ : MonoidalCategory V
C : Type u
inst✝⁸ : Category.{v, u} C
inst✝⁷ : EnrichedOrdinaryCategory V C
W✝ : Type u''
inst✝⁶ : Category.{v'', u''} W✝
inst✝⁵ : MonoidalCategory W✝
F✝ : V ⥤ W✝
inst✝⁴ : F✝.LaxMonoidal
W : Type u''
inst✝³ : Category.{v'', u''} W
inst✝² : MonoidalCategory W
F : V ⥤ W
inst✝¹ : F.LaxMonoidal
D : Type u
inst✝ : EnrichedCategory V D
e : (v : V) → (𝟙_ V ⟶ v) ≃ (𝟙_ W ⟶ F.obj v)
h : ∀ (v : V) (f : 𝟙_ V ⟶ v), (e v) f = Functor.LaxMonoidal.ε F ≫ F.map f
X✝ Y✝ Z✝ : TransportEnrichment F (ForgetEnrichment V D)
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ ForgetEnrichment.homOf W
      ((Functor.LaxMonoidal.ε F ≫
          ((λ_ (F.obj (𝟙_ V))).inv ≫ Functor.LaxMonoidal.ε F ▷ F.obj (𝟙_ V) ≫ Functor.LaxMonoidal.μ F (𝟙_ V) (𝟙_ V)) ≫
            F.map (ForgetEnrichment.homTo V f ⊗ₘ ForgetEnrichment.homTo V g)) ≫
        F.map (eComp V (ForgetEnrichment.to V X✝) (ForgetEnrichment.to V Y✝) (ForgetEnrichment.to V Z✝))) =
    ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V f)) ≫
      ForgetEnrichment.homOf W (Functor.LaxMonoidal.ε F ≫ F.map (ForgetEnrichment.homTo V g))
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_of.inl
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
e : x✝ = y✝
h✝ : i = eqToHom e
⊢ (∃ (h : x✝ = z✝), i ≫ u = eqToHom h) ∨ x✝.len < z✝.len

Tactic:
apply Or.inr

Goal state after:
case comp_of.inl
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
e : x✝ = y✝
h✝ : i = eqToHom e
⊢ x✝.len < z✝.len
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_of.inr
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
h' : x✝.len < y✝.len
⊢ (∃ (h : x✝ = z✝), i ≫ u = eqToHom h) ∨ x✝.len < z✝.len

Tactic:
apply Or.inr

Goal state after:
case comp_of.inr
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
h' : x✝.len < y✝.len
⊢ x✝.len < z✝.len
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'.succ ≫ σ i.castSucc = σ i ≫ δ i'

Tactic:
δ_comp_σ_of_gt h

Goal state after:
n : ℕ
i' : Fin (n + 2)
i : Fin (n + 1)
h✝ : i.castSucc.succ ≤ i'.succ
h : i.castSucc < i'
⊢ σ i ≫ δ i' = σ i ≫ δ i'
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

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

Tactic:
by
  induction n generalizing x with
  | zero => cases hf with
    | of _ h => cases h; exact factor_δ_σ _ _
    | id => exact ⟨_, _, _, P_σ.σ i, P_δ.id_mem _, by simp⟩
    | comp_of j f hf hg =>
      obtain ⟨k⟩ := hg
      obtain ⟨rfl, rfl⟩ | hf' := eq_or_len_le_of_P_δ hf
      · simpa using factor_δ_σ i k
      · simp at hf'
  | succ n hn =>
    cases hf with
    | of _ h => cases h; exact factor_δ_σ _ _
    | id n => exact ⟨_, _, _, P_σ.σ i, P_δ.id_mem _, by simp⟩
    | comp_of f g hf hg =>
      obtain ⟨k⟩ := hg
      obtain ⟨rfl, rfl⟩ | h' := eq_or_len_le_of_P_δ hf
      · simpa using factor_δ_σ i k
      · obtain h'' | ⟨j, j', h''⟩ := switch_δ_σ i k
        · exact ⟨_, _, _, P_σ.id_mem _, hf, by simp [h'']⟩
        · obtain ⟨z, e, m, he, hm, fac⟩ := hn j f hf
          exact ⟨z, e, m ≫ δ j', he, P_δ.comp_mem _ _ hm (P_δ.δ j'),
            by simp [h'', reassoc_of% fac]⟩

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

Goal state before:
pp: case id
x y : SimplexCategoryGenRel
n : ℕ
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), 𝟙 (mk n) = e ≫ m

Tactic:
use (mk n), (𝟙 (mk n)), (𝟙 (mk n)), P_σ.id_mem _, P_δ.id_mem _

Goal state after:
case h
x y : SimplexCategoryGenRel
n : ℕ
⊢ 𝟙 (mk n) = 𝟙 (mk n) ≫ 𝟙 (mk n)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
⊢ Nonempty (P_σ.MapFactorizationData P_δ f)

Tactic:
obtain ⟨z, e, m, he, hm, fac⟩ := exists_P_σ_P_δ_factorization f
    exact ⟨⟨z, e, m, fac.symm, he, hm⟩⟩

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₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
⊢ ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ (a :: L) ⋯))) ⟨j, hj⟩) =
    simplicialEvalσ (a :: L) j

Tactic:
set a₀ := hL.head

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₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
⊢ ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ (a :: L) ⋯))) ⟨j, hj⟩) =
    simplicialEvalσ (a :: L) j
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

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

Tactic:
dsimp only [spineEquiv, Equiv.coe_fn_mk]

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