mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Topology.Homotopy.Basic

Goal state before:
pp: case pos.e_6.e_fst
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ ⟨2 * (1 - ↑t) - 1, ⋯⟩ = σ ⟨2 * ↑t, ⋯⟩

Tactic:
apply Subtype.ext

Goal state after:
case pos.e_6.e_fst
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f₀ f₁ f₂ : C(X, Y)
F : f₀.Homotopy f₁
G : f₁.Homotopy f₂
t : ↑I
snd✝ : X
h₁ : ¬1 - ↑t ≤ 1 / 2
h₂ : ↑t ≤ 1 / 2
⊢ ↑⟨2 * (1 - ↑t) - 1, ⋯⟩ = ↑(σ ⟨2 * ↑t, ⋯⟩)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X₁ X₂ Y : TopCat
f : C(↑X₁, ↑Y)
g : C(↑X₂, ↑Y)
x₀ x₁ : ↑X₁
x₂ x₃ : ↑X₂
p : Path x₀ x₁
q : Path x₂ x₃
hfg : ∀ (t : ↑I), f (p t) = g (q t)
⊢ (π.map (TopCat.ofHom f)).map ⟦p⟧ = hcast ⋯ ≫ (π.map (TopCat.ofHom g)).map ⟦q⟧ ≫ hcast ⋯

Tactic:
rw [conj_eqToHom_iff_heq
    ((πₘ (TopCat.ofHom f)).map ⟦p⟧) ((πₘ (TopCat.ofHom g)).map ⟦q⟧)
    (FundamentalGroupoid.ext <| start_path hfg)
    (FundamentalGroupoid.ext <| end_path hfg)]
  exact heq_path_of_eq_image hfg

Goal state after:
Module: Mathlib.CategoryTheory.Localization.CalculusOfFractions.OfAdjunction

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w✝ : W s
f : T ⟶ Y
this✝ : IsIso (G.map s)
this : s ≫ adj.unit.app X = adj.unit.app T ≫ F.map (G.map s)
⊢ f ≫ adj.unit.app Y = adj.unit.app T ≫ F.map (G.map s) ≫ inv (F.map (G.map s)) ≫ F.map (G.map f)

Tactic:
IsIso.hom_inv_id_assoc,

Goal state after:
C₁ : Type u_1
C₂ : Type u_2
inst✝² : Category.{v_1, u_1} C₁
inst✝¹ : Category.{v_2, u_2} C₂
G : C₁ ⥤ C₂
F : C₂ ⥤ C₁
adj : G ⊣ F
W : MorphismProperty C₁
inst✝ : W.IsMultiplicative
hW : W.IsInvertedBy G
hW' : W.functorCategory C₁ adj.unit
X Y T : C₁
s : T ⟶ X
w✝ : W s
f : T ⟶ Y
this✝ : IsIso (G.map s)
this : s ≫ adj.unit.app X = adj.unit.app T ≫ F.map (G.map s)
⊢ f ≫ adj.unit.app Y = adj.unit.app T ≫ F.map (G.map f)
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
⊢ (weakEquivalences (HoCat C)).IsInvertedBy HoCat.bifibrantResolution

Tactic:
by
    intro X Y f hf
    obtain ⟨X, rfl⟩ := toHoCat_obj_surjective X
    obtain ⟨Y, rfl⟩ := toHoCat_obj_surjective Y
    obtain ⟨f, rfl⟩ := toHoCat.map_surjective f
    rw [← weakEquivalence_iff, weakEquivalence_toHoCat_map_iff] at hf
    rw [HoCat.bifibrantResolution_map]
    apply Localization.inverts _ (weakEquivalences _)
    rw [← weakEquivalence_iff]
    infer_instance

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

Goal state before:
pp: case refine_1
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
hA : A ≤ Λ[n + 1, i]
h : Set.range ⇑(stdSimplex.asOrderHom (stdSimplex.objEquiv.symm (SimplexCategory.δ i))) ∪ {i} ≠ Set.univ
⊢ Set.range ⇑(ConcreteCategory.hom (SimplexCategory.δ i)) ∪ {i} = Set.univ

Tactic:
SimplexCategory.coe_δ,

Goal state after:
case refine_1
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
hA : A ≤ Λ[n + 1, i]
h : Set.range ⇑(stdSimplex.asOrderHom (stdSimplex.objEquiv.symm (SimplexCategory.δ i))) ∪ {i} ≠ Set.univ
⊢ Set.range i.succAbove ∪ {i} = Set.univ
Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits

Goal state before:
pp: X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
⊢ IsColimit ((PushoutCocone.mk (homOfLE ⋯) (homOfLE ⋯) ⋯).map ((evaluation SimplexCategoryᵒᵖ (Type u)).obj n))

Tactic:
by
        have h : Lattice.BicartSq (A₁.obj n) (A₂.obj n) (A₃.obj n) (A₄.obj n) :=
          { sup_eq := by
              rw [← sq.sup_eq]
              rfl
            inf_eq := by
              rw [← sq.inf_eq]
              rfl }
        exact (Types.isPushout_of_bicartSq h).isColimit

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

Goal state before:
pp: case refine_2
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
⊢ A ≤ Λ[n + 1, i]

Tactic:
rw [Subcomplex.le_iff_contains_nonDegenerate]
    intro d x hx
    by_cases! hd : d < n
    · simp [horn_obj_eq_univ i d]
    · obtain ⟨⟨S, hS⟩, rfl⟩ := stdSimplex.nonDegenerateEquiv'.symm.surjective x
      dsimp at hS
      simp only [stdSimplex.nonDegenerateEquiv'_symm_mem_iff_face_le] at hx ⊢
      obtain hd | rfl := hd.lt_or_eq
      · obtain rfl : S = .univ := by
          rw [← Finset.card_eq_iff_eq_univ, Fintype.card_fin]
          exact le_antisymm (card_finset_fin_le S) (by lia)
        exact (h (le_trans (by simp) hx)).elim
      · replace hS : Sᶜ.card = 1 := by
          have := S.card_compl_add_card
          rw [Fintype.card_fin] at this
          lia
        obtain ⟨j, rfl⟩ : ∃ j, S = {j}ᶜ := by
          rw [Finset.card_eq_one] at hS
          obtain ⟨j, hS⟩ := hS
          exact ⟨j, by simp [← hS]⟩
        exact face_le_horn _ _ (by rintro rfl; tauto)

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

Goal state before:
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:
obtain rfl := (mono_iff_injective f).1 inferInstance h'

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₁ : X₁
x₂ : X₂
⊢ (ConcreteCategory.hom (inl f g)) x₁ = (ConcreteCategory.hom (inr f g)) x₂ ↔
    ∃ s, (ConcreteCategory.hom f) s = x₁ ∧ (ConcreteCategory.hom g) s = x₂

Tactic:
refine (Pushout.quot_mk_eq_iff f g (Sum.inl x₁) (Sum.inr x₂)).trans ?_

Goal state after:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₁ : X₁
x₂ : X₂
⊢ Rel' f g (Sum.inl x₁) (Sum.inr x₂) ↔ ∃ s, (ConcreteCategory.hom f) s = x₁ ∧ (ConcreteCategory.hom g) s = x₂
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
⊢ (ConcreteCategory.hom (X.map (tr (intervalEdge j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f) =
    (ConcreteCategory.hom (X.map ((tr (subinterval j l hjl) ⋯ ?h).op ≫ (tr (diag l) ⋯ ⋯).op)))
      (sx.spineToSimplex m ?h f)

pp: case h
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ m ≤ n + 1

Tactic:
← op_comp,

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
⊢ (ConcreteCategory.hom (X.map (tr (intervalEdge j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f) =
    (ConcreteCategory.hom (X.map (tr (diag l) ⋯ ⋯ ≫ tr (subinterval j l hjl) ⋯ ?h).op)) (sx.spineToSimplex m ?h f)

case h
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ m ≤ n + 1
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
h : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := h })
i : Fin m
⊢ (ConcreteCategory.hom (((trunc (n + 1) 1 ⋯).obj X).map (tr (SimplexCategory.δ 0) Path₁._proof_1 Path₁._proof_5).op))
      ((ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ h).op)) Δ) =
    (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ i.succ) ⋯ h).op)) Δ

Tactic:
simp [← δ_zero_mkOfSucc, tr_comp]
    rfl

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
a : ℕ
hₐ : a ≤ n + 1
φ : { obj := ⦋a⦌, property := hₐ } ⟶ { obj := ⦋m⦌, property := hₘ }
i : Fin (a + 1)
⊢ (ConcreteCategory.hom (X.map (φ.op ≫ (tr (⦋0⦌.const ⦋a⦌ i) ⋯ hₐ).op))) Δ =
    (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ((Hom.toOrderHom φ.hom) i)) ⋯ hₘ).op)) Δ

Tactic:
← op_comp,

Goal state after:
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
a : ℕ
hₐ : a ≤ n + 1
φ : { obj := ⦋a⦌, property := hₐ } ⟶ { obj := ⦋m⦌, property := hₘ }
i : Fin (a + 1)
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋a⦌ i) ⋯ hₐ ≫ φ).op)) Δ =
    (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ((Hom.toOrderHom φ.hom) i)) ⋯ hₘ).op)) Δ
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : i.castSucc < j
⊢ (ConcreteCategory.hom (X.map ((tr (SimplexCategory.δ j) ⋯ ⋯).op ≫ (tr (⦋0⦌.const ⦋m⦌ i) ⋯ ⋯).op)))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.vertex i.castSucc

Tactic:
← op_comp,

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : i.castSucc < j
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ i) ⋯ ⋯ ≫ tr (SimplexCategory.δ j) ⋯ ⋯).op))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.vertex i.castSucc
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := ⋯
hlt : ksucc < j
⊢ (horn.spineId i h₀ hₙ).arrow k.castSucc =
    ⟨(ConcreteCategory.hom (Δ[n + 2].map (mkOfSucc k).op)) ↑(horn.face i j hj), ⋯⟩

Tactic:
apply Subtype.ext

Goal state after:
case h.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := ⋯
hlt : ksucc < j
⊢ ↑((horn.spineId i h₀ hₙ).arrow k.castSucc) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 2].map (mkOfSucc k).op)) ↑(horn.face i j hj), ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : j ≤ i.castSucc
⊢ (ConcreteCategory.hom (X.map ((tr (SimplexCategory.δ j) ⋯ ⋯).op ≫ (tr (⦋0⦌.const ⦋m⦌ i) ⋯ ⋯).op)))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.vertex i.succ

Tactic:
← op_comp,

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin (m + 1)
j : Fin (m + 2)
hij : j ≤ i.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ i) ⋯ ⋯ ≫ tr (SimplexCategory.δ j) ⋯ ⋯).op))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.vertex i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : i.succ.castSucc < j
⊢ (ConcreteCategory.hom (X.map ((tr (SimplexCategory.δ j) ⋯ ⋯).op ≫ (tr (mkOfSucc i) ⋯ ⋯).op)))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.castSucc

Tactic:
← op_comp,

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : i.succ.castSucc < j
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ ⋯ ≫ tr (SimplexCategory.δ j) ⋯ ⋯).op))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hᵥ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin (l + 1)
⊢ (ConcreteCategory.hom (X.map ((tr (subinterval j l h) ⋯ hₘ).op ≫ (tr (⦋0⦌.const ⦋l⦌ i) ⋯ ⋯).op))) Δ =
    Path.vertex
      { vertex := fun i ↦ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ,
        arrow := fun i ↦ (X.spine m hₘ Δ).arrow ⟨j + ↑i, ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }
      i

Tactic:
← op_comp,

Goal state after:
case hᵥ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin (l + 1)
⊢ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋l⦌ i) ⋯ ⋯ ≫ tr (subinterval j l h) ⋯ hₘ).op)) Δ =
    Path.vertex
      { vertex := fun i ↦ (ConcreteCategory.hom (X.map (tr (⦋0⦌.const ⦋m⦌ ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ,
        arrow := fun i ↦ (X.spine m hₘ Δ).arrow ⟨j + ↑i, ⋯⟩, arrow_src := ⋯, arrow_tgt := ⋯ }
      i
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := ⋯
hgt : j < ksucc
⊢ (horn.spineId i h₀ hₙ).arrow k.succ = ⟨(ConcreteCategory.hom (Δ[n + 2].map (mkOfSucc k).op)) ↑(horn.face i j hj), ⋯⟩

Tactic:
apply Subtype.ext

Goal state after:
case h.inr.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := ⋯
hgt : j < ksucc
⊢ ↑((horn.spineId i h₀ hₙ).arrow k.succ) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 2].map (mkOfSucc k).op)) ↑(horn.face i j hj), ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map ((tr (SimplexCategory.δ j) ⋯ ⋯).op ≫ (tr (mkOfSucc i) ⋯ ⋯).op)))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.succ

Tactic:
← op_comp,

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ ⋯ ≫ tr (SimplexCategory.δ j) ⋯ ⋯).op))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case hₐ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin l
⊢ (ConcreteCategory.hom (X.map ((tr (subinterval j l h) ⋯ hₘ).op ≫ (tr (mkOfSucc i) ⋯ ⋯).op))) Δ =
    Path.arrow
      { vertex := fun i ↦ (X.spine m hₘ Δ).vertex ⟨j + ↑i, ⋯⟩,
        arrow := fun i ↦ (ConcreteCategory.hom (X.map (tr (mkOfSucc ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ, arrow_src := ⋯,
        arrow_tgt := ⋯ }
      i

Tactic:
← op_comp,

Goal state after:
case hₐ
n : ℕ
X : Truncated (n + 1)
m : ℕ
hₘ : m ≤ n + 1
j l : ℕ
h : j + l ≤ m
Δ : X.obj (op { obj := ⦋m⦌, property := hₘ })
i : Fin l
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ ⋯ ≫ tr (subinterval j l h) ⋯ hₘ).op)) Δ =
    Path.arrow
      { vertex := fun i ↦ (X.spine m hₘ Δ).vertex ⟨j + ↑i, ⋯⟩,
        arrow := fun i ↦ (ConcreteCategory.hom (X.map (tr (mkOfSucc ⟨j + ↑i, ⋯⟩) ⋯ hₘ).op)) Δ, arrow_src := ⋯,
        arrow_tgt := ⋯ }
      i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map ((tr (SimplexCategory.δ j) ⋯ ⋯).op ≫ (tr (mkOfSucc i) ⋯ ⋯).op)))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i) 2 ⋯)

Tactic:
← op_comp,

Goal state after:
n : ℕ
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ ⋯ ≫ tr (SimplexCategory.δ j) ⋯ ⋯).op))
      (sx.spineToSimplex (m + 1) ⋯ f) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i) 2 ⋯)
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
⊢ (ConcreteCategory.hom (X.map (intervalEdge j l hjl).op)) (sx.spineToSimplex f) =
    (ConcreteCategory.hom (X.map ((subinterval j l hjl).op ≫ (diag l).op))) (sx.spineToSimplex f)

Tactic:
← op_comp,

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ (ConcreteCategory.hom (X.map (intervalEdge j l hjl).op)) (sx.spineToSimplex f) =
    (ConcreteCategory.hom (X.map (diag l ≫ subinterval j l hjl).op)) (sx.spineToSimplex f)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Path

Goal state before:
pp: case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ (ConcreteCategory.hom (X.map ((δ 0).op ≫ (mkOfSucc i).op))) x = ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i

Tactic:
← op_comp,

Goal state after:
case succ
X : SSet
m : ℕ
x : X _⦋m + 1 + 1⦌
i : Fin (m + 1)
⊢ (ConcreteCategory.hom (X.map (mkOfSucc i ≫ δ 0).op)) x = ((X.spine (m + 1 + 1) x).interval 1 (m + 1) ⋯).arrow i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
⊢ (ConcreteCategory.hom (X.map ((δ j).op ≫ (⦋0⦌.const ⦋n⦌ i).op))) (sx.spineToSimplex f) = f.vertex i.castSucc

Tactic:
← op_comp,

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : i.castSucc < j
⊢ (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋n⦌ i ≫ δ j).op)) (sx.spineToSimplex f) = f.vertex i.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
⊢ (ConcreteCategory.hom (X.map ((δ j).op ≫ (⦋0⦌.const ⦋n⦌ i).op))) (sx.spineToSimplex f) = f.vertex i.succ

Tactic:
← op_comp,

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path (n + 1)
i : Fin (n + 1)
j : Fin (n + 2)
h : j ≤ i.castSucc
⊢ (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋n⦌ i ≫ δ j).op)) (sx.spineToSimplex f) = f.vertex i.succ
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := ⋯
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := ⋯
m : Fin (1 + 1)
⊢ ((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow m =
    ⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc m).op)) ↑triangle, ⋯⟩

Tactic:
apply Subtype.ext

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := ⋯
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := ⋯
m : Fin (1 + 1)
⊢ ↑(((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow m) =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc m).op)) ↑triangle, ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p✝ : X.Path n
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 0)) (p.arrow 0) =
    (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋n⦌ 0).op)) (spineToSimplex h (p.interval 1 n ⋯))

Tactic:
rw [p.arrow_tgt 0]
      exact Path.congr_vertex (spine_spineToSimplex h (p.interval 1 n)).symm 0

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

Goal state before:
pp: case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := ⋯
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
⊢ ⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (diag 2).op)) ↑triangle, ⋯⟩ =
    ⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc k).op)) ↑(horn.face i j hj), ⋯⟩

Tactic:
apply Subtype.ext

Goal state after:
case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := ⋯
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
⊢ ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (diag 2).op)) ↑triangle, ⋯⟩ =
    ↑⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc k).op)) ↑(horn.face i j hj), ⋯⟩
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
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ (λ_ (X'' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f' ▷ X'' ⟶[V] Y) ≫
        (λ_ ((X' ⟶[V] X'') ⊗ X'' ⟶[V] Y)).inv ≫
          𝟙_ V ◁ eComp V X' X'' Y ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y =
    (λ_ (X'' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f' ▷ X'' ⟶[V] Y) ≫
        eComp V X' X'' Y ≫ (λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y

Tactic:
id_whiskerLeft_assoc,

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
X X' X'' : C
f : X ⟶ X'
f' : X' ⟶ X''
Y : C
⊢ (λ_ (X'' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f' ▷ X'' ⟶[V] Y) ≫
        (λ_ ((X' ⟶[V] X'') ⊗ X'' ⟶[V] Y)).inv ≫
          (λ_ ((X' ⟶[V] X'') ⊗ X'' ⟶[V] Y)).hom ≫
            eComp V X' X'' Y ≫ (λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y =
    (λ_ (X'' ⟶[V] Y)).inv ≫
      ((eHomEquiv V) f' ▷ X'' ⟶[V] Y) ≫
        eComp V X' X'' Y ≫ (λ_ (X' ⟶[V] Y)).inv ≫ ((eHomEquiv V) f ▷ X' ⟶[V] Y) ≫ eComp V X X' Y
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
D : Type u₂
inst✝¹ : EnrichedCategory V D
inst✝ : BraidedCategory V
F G : EnrichedFunctor V C D
X✝ Y✝ : Vᵒᵖ
f : X✝ ⟶ Y✝
σ : GradedNatTrans ((Center.ofBraided V).obj (unop X✝)) F G
X Y : C
⊢ (((Center.ofBraided V).obj (unop Y✝)).snd.β (X ⟶[V] Y)).hom ≫
      (F.map X Y ⊗ₘ f.unop ≫ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)

Tactic:
have p := σ.naturality X Y

Goal state after:
V : Type v
inst✝⁴ : Category.{w, v} V
inst✝³ : MonoidalCategory V
C : Type u₁
inst✝² : EnrichedCategory V C
D : Type u₂
inst✝¹ : EnrichedCategory V D
inst✝ : BraidedCategory V
F G : EnrichedFunctor V C D
X✝ Y✝ : Vᵒᵖ
f : X✝ ⟶ Y✝
σ : GradedNatTrans ((Center.ofBraided V).obj (unop X✝)) F G
X Y : C
p :
  (((Center.ofBraided V).obj (unop X✝)).snd.β (X ⟶[V] Y)).hom ≫
      (F.map X Y ⊗ₘ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
⊢ (((Center.ofBraided V).obj (unop Y✝)).snd.β (X ⟶[V] Y)).hom ≫
      (F.map X Y ⊗ₘ f.unop ≫ σ.app Y) ≫ eComp V (F.obj X) (F.obj Y) (G.obj Y) =
    (f.unop ≫ σ.app X ⊗ₘ G.map X Y) ≫ eComp V (F.obj X) (G.obj X) (G.obj Y)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: case mp
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
y₁ : Y₁.obj m
y₂ : Y₂.obj m
⊢ (y₁, y₂) ∈ (range (f₁ ⊗ₘ f₂)).obj m → (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m

Tactic:
rintro ⟨⟨x₁, x₂⟩, h⟩
    rw [Prod.eq_iff_fst_eq_snd_eq] at h
    exact ⟨⟨x₁, h.1⟩, ⟨x₂, h.2⟩⟩

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

Goal state before:
pp: case cast
n : ℕ
i✝ : Fin (n + 1)
⊢ δ i✝.castSucc ≫ Fin.lastCases (σ (Fin.last n)) (fun i ↦ σ i) i✝.castSucc = 𝟙 (mk n)

Tactic:
simp only [Fin.lastCases_castSucc]
      exact δ_comp_σ_self

Goal state after: