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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
⊢ ∀ (n : ℕ),
    (Γ₀.splitting K[X]).φ
        (((N₁ ⋙ Γ₂).obj X).p ≫
          { app := fun Δ ↦ (Γ₀.splitting K[X]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op,
              naturality := ⋯ } ≫
            ((toKaroubi (SimplicialObject C)).obj X).p)
        n =
      (Γ₀.splitting K[X]).φ
        { app := fun Δ ↦ (Γ₀.splitting K[X]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op, naturality := ⋯ }
        n

Tactic:
intro n

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X : SimplicialObject C
n : ℕ
⊢ (Γ₀.splitting K[X]).φ
      (((N₁ ⋙ Γ₂).obj X).p ≫
        { app := fun Δ ↦ (Γ₀.splitting K[X]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op,
            naturality := ⋯ } ≫
          ((toKaroubi (SimplicialObject C)).obj X).p)
      n =
    (Γ₀.splitting K[X]).φ
      { app := fun Δ ↦ (Γ₀.splitting K[X]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op, naturality := ⋯ } n
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
f : X ⟶ Y
⊢ ∀ (n : ℕ),
    (Γ₀.splitting K[X]).φ
        ((N₁ ⋙ Γ₂).map f ≫
            {
              f :=
                { app := fun Δ ↦ (Γ₀.splitting K[Y]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ Y.map A.e.op,
                  naturality := ⋯ },
              comm := ⋯ }).f
        n =
      (Γ₀.splitting K[X]).φ
        ({
              f :=
                { app := fun Δ ↦ (Γ₀.splitting K[X]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op,
                  naturality := ⋯ },
              comm := ⋯ } ≫
            (toKaroubi (SimplicialObject C)).map f).f
        n

Tactic:
intro n

Goal state after:
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X Y : SimplicialObject C
f : X ⟶ Y
n : ℕ
⊢ (Γ₀.splitting K[X]).φ
      ((N₁ ⋙ Γ₂).map f ≫
          {
            f :=
              { app := fun Δ ↦ (Γ₀.splitting K[Y]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ Y.map A.e.op,
                naturality := ⋯ },
            comm := ⋯ }).f
      n =
    (Γ₀.splitting K[X]).φ
      ({
            f :=
              { app := fun Δ ↦ (Γ₀.splitting K[X]).desc Δ fun A ↦ PInfty.f (unop A.fst).len ≫ X.map A.e.op,
                naturality := ⋯ },
            comm := ⋯ } ≫
          (toKaroubi (SimplicialObject C)).map f).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
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ (((Functor.whiskeringLeft (SimplicialObject C) (Karoubi (SimplicialObject C)) (Karoubi (SimplicialObject C))).obj
              (toKaroubi (SimplicialObject C))).preimage
          (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans)).app
      P =
    (N₂ ⋙ Γ₂).map P.decompId_i ≫ (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans).app P.X ≫ P.decompId_p

Tactic:
simp only [whiskeringLeft_obj_preimage_app, Functor.id_map]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X✝ Y✝ : Split C
Φ : X✝ ⟶ Y✝
⊢ (nondegComplexFunctor ⋙ toKaroubi (ChainComplex C ℕ)).map Φ ≫ Y✝.s.toKaroubiNondegComplexIsoN₁.hom =
    X✝.s.toKaroubiNondegComplexIsoN₁.hom ≫ (forget C ⋙ N₁).map Φ

Tactic:
ext n
    dsimp
    simp only [assoc, PInfty_f_idem_assoc]
    erw [← Split.cofan_inj_naturality_symm_assoc Φ (Splitting.IndexSet.id (op ⦋n⦌))]
    rw [PInfty_f_naturality]

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

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
X✝ Y✝ : Split C
Φ : X✝ ⟶ Y✝
⊢ (nondegComplexFunctor ⋙ toKaroubi (ChainComplex C ℕ)).map Φ ≫ Y✝.s.toKaroubiNondegComplexIsoN₁.hom =
    X✝.s.toKaroubiNondegComplexIsoN₁.hom ≫ (forget C ⋙ N₁).map Φ

Tactic:
by
    ext n
    dsimp
    simp only [assoc, PInfty_f_idem_assoc]
    erw [← Split.cofan_inj_naturality_symm_assoc Φ (Splitting.IndexSet.id (op ⦋n⦌))]
    rw [PInfty_f_naturality]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : LocallySmall.{w, v, u} C
⊢ LocallySmall.{w, v, u} (HoCat C)

Tactic:
by
  dsimp [HoCat]
  infer_instance

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

Goal state before:
pp: case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
h : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj ⟶ X.obj
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 X.obj)
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 Y.obj)
⊢ F.map f ≫ F.map (homMk g') = 𝟙 (F.obj X)

pp: case refine_2.refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
h : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj ⟶ X.obj
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 X.obj)
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 Y.obj)
⊢ F.map (homMk g') ≫ F.map f = 𝟙 (F.obj Y)

Tactic:
all_goals
      rw [← F.map_comp, ← F.map_id]
      apply h
      assumption

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

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ {X_1 Y : FundamentalGroupoid X} (f : Path.Homotopic.Quotient X_1.as Y.as),
    Path.Homotopic.Quotient.trans ⟦Path.refl X_1.as⟧ f = f

Tactic:
rintro _ _ ⟨f⟩

Goal state after:
case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : FundamentalGroupoid X
f✝ : Path.Homotopic.Quotient X✝.as Y✝.as
f : Path X✝.as Y✝.as
⊢ Path.Homotopic.Quotient.trans ⟦Path.refl X✝.as⟧ (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f) =
    Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ {X_1 Y : FundamentalGroupoid X} (f : Path.Homotopic.Quotient X_1.as Y.as), f.trans ⟦Path.refl Y.as⟧ = f

Tactic:
rintro _ _ ⟨f⟩

Goal state after:
case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : FundamentalGroupoid X
f✝ : Path.Homotopic.Quotient X✝.as Y✝.as
f : Path X✝.as Y✝.as
⊢ Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f) ⟦Path.refl Y✝.as⟧ =
    Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ {X_1 Y : FundamentalGroupoid X} (f : Path.Homotopic.Quotient X_1.as Y.as),
    (Quotient.lift (fun f ↦ ⟦f.symm⟧) ⋯ f).trans f = ⟦Path.refl Y.as⟧

Tactic:
rintro _ _ ⟨f⟩

Goal state after:
case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : FundamentalGroupoid X
f✝ : Path.Homotopic.Quotient X✝.as Y✝.as
f : Path X✝.as Y✝.as
⊢ (Quotient.lift (fun f ↦ ⟦f.symm⟧) ⋯ (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f)).trans
      (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f) =
    ⟦Path.refl Y✝.as⟧
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
⊢ ∀ {X_1 Y : FundamentalGroupoid X} (f : Path.Homotopic.Quotient X_1.as Y.as),
    f.trans (Quotient.lift (fun f ↦ ⟦f.symm⟧) ⋯ f) = ⟦Path.refl X_1.as⟧

Tactic:
rintro _ _ ⟨f⟩

Goal state after:
case mk
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ : X
X✝ Y✝ : FundamentalGroupoid X
f✝ : Path.Homotopic.Quotient X✝.as Y✝.as
f : Path X✝.as Y✝.as
⊢ Path.Homotopic.Quotient.trans (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f)
      (Quotient.lift (fun f ↦ ⟦f.symm⟧) ⋯ (Quot.mk (⇑(Path.Homotopic.setoid X✝.as Y✝.as)) f)) =
    ⟦Path.refl X✝.as⟧
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case mp
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ y₁ : X₁
⊢ Rel' f g (Sum.inl x₁) (Sum.inl y₁) →
    x₁ = y₁ ∨
      ∃ x₀ y₀,
        ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
          x₁ = (ConcreteCategory.hom f) x₀ ∧ y₁ = (ConcreteCategory.hom f) y₀

Tactic:
rintro (_ | ⟨_, _, h⟩)

Goal state after:
case mp.refl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₁ : X₁
⊢ x₁ = x₁ ∨
    ∃ x₀ y₀,
      ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
        x₁ = (ConcreteCategory.hom f) x₀ ∧ x₁ = (ConcreteCategory.hom f) y₀

case mp.inl_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
⊢ (ConcreteCategory.hom f) x₀✝ = (ConcreteCategory.hom f) y₀✝ ∨
    ∃ x₀ y₀,
      ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
        (ConcreteCategory.hom f) x₀✝ = (ConcreteCategory.hom f) x₀ ∧
          (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) y₀
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
h : ∃ i, ofHoms (fun i_1 ↦ Λ[i + 1, i_1].ι) f✝
⊢ monomorphisms SSet f✝

Tactic:
obtain ⟨n, ⟨i⟩⟩ := h

Goal state after:
n : ℕ
X Y : SSet
i : Fin (n + 2)
⊢ monomorphisms SSet Λ[n + 1, i].ι
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
⊢ ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ ⊤.obj (op ⦋n⦌) → ↑x ∈ (⨆ n, X.skeleton n).obj (op ⦋n⦌)

Tactic:
intro n

Goal state after:
X : SSet
n : ℕ
⊢ ∀ (x : ↑(X.nonDegenerate n)), ↑x ∈ ⊤.obj (op ⦋n⦌) → ↑x ∈ (⨆ n, X.skeleton n).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
⊢ ∀ (i_1 : ℕ), Y.skeleton i_1 ≤ ⨆ n, (skeletonOfMono i) n

Tactic:
intro n

Goal state after:
X Y : SSet
i : X ⟶ Y
n : ℕ
⊢ Y.skeleton n ≤ ⨆ n, (skeletonOfMono i) n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case refine_2
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
c : Cell i d
y : Δ[d] _⦋n⦌
hx :
  ↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)) ∈
    ((skeletonOfMono i) d).obj (op ⦋n⦌)
⊢ ↑((ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaBoundary.app (op ⦋n⦌))) ⟨y, ⋯⟩)) =
    ↑⟨↑((ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋n⦌))) y)), hx⟩

Tactic:
exact congr($(c.ι_t_ι_eq_ι_l_b_ι).app _ ⟨y, _⟩)

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

Goal state before:
pp: case refine_2
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ Set.range ⇑(ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (r i d))) ⊔
      Set.range ⇑(ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (b i d))) =
    Set.univ

pp: case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ ∀ (x₃ y₃ : evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.obj (sigmaStdSimplex i d)),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (l i d))) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (l i d))) →
        (ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (b i d))) x₃ =
            (ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (b i d))) y₃ →
          x₃ = y₃

Tactic:
· exact range_r_app_union_range_b_app _ _ _

Goal state after:
case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ ∀ (x₃ y₃ : evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.obj (sigmaStdSimplex i d)),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (l i d))) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (l i d))) →
        (ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (b i d))) x₃ =
            (ConcreteCategory.hom (evaluation SimplexCategoryᵒᵖ (Type u) _⦋n⦌.map (b i d))) y₃ →
          x₃ = y₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
i : Fin (m + 1)
f : X.Path m
⊢ (X.spine m h (sx.spineToSimplex m h f)).vertex i = f.vertex i

Tactic:
spine_spineToSimplex_apply

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
i : Fin (m + 1)
f : X.Path m
⊢ f.vertex i = f.vertex i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
i : Fin m
f : X.Path m
⊢ (X.spine m h (sx.spineToSimplex m h f)).arrow i = f.arrow i

Tactic:
spine_spineToSimplex_apply

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
i : Fin m
f : X.Path m
⊢ f.arrow i = f.arrow i
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
⊢ 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))

Tactic:
spine_spineToSimplex_apply

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)) =
    f.interval j l hjl
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
⊢ ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ X),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ X j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)

Tactic:
intro n

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
⊢ ∀ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ X),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ X j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1)
f : X.Path n
⊢ (X.spine n (sx.spineToSimplex f)).vertex i = f.vertex i

Tactic:
spine_spineToSimplex_apply

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1)
f : X.Path n
⊢ f.vertex i = f.vertex i
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin n
f : X.Path n
⊢ (X.spine n (sx.spineToSimplex f)).arrow i = f.arrow i

Tactic:
spine_spineToSimplex_apply

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin n
f : X.Path n
⊢ f.arrow i = f.arrow i
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
⊢ (X.spine n (sx.spineToSimplex f)).interval j l hjl = f.interval j l hjl

Tactic:
spine_spineToSimplex_apply

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ f.interval j l hjl = f.interval j l hjl
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) := k.succ.castSucc
heq : j = ksucc
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀))) =
    (ConcreteCategory.hom (Λ[n + 1 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
let triangle : (Λ[n + 3, i] : SSet.{u}) _⦋2⦌ :=
        horn.primitiveTriangle i h₀ hₙ k (by grind)
      /- The interval spanning from `k` to `k + 2` is equivalently the spine
      of the triangle with vertices `k`, `k + 1`, and `k + 2`. -/
      have hi : ((horn.spineId i h₀ hₙ).map σ₀).interval k 2 (by grind) =
          X.spine 2 (σ₀.app _ triangle) := by
        ext m
        dsimp [spine_arrow, Path.map_interval, Path.map_arrow]
        rw [← dsimp% σ₀.naturality_apply]
        apply congr_arg
        apply Subtype.ext
        ext a : 1
        fin_cases a <;> fin_cases m <;> rfl
      rw [← spine_arrow, spine_δ_arrow_eq sx _ heq, hi]
      simp only [spineToDiagonal, diagonal, spineToSimplex_spine_apply]
      rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality, types_comp_apply]
      dsimp
      apply congr_arg
      apply Subtype.ext
      ext z : 1
      dsimp [horn.face]
      rw [dsimp% Subcomplex.yonedaEquiv_coe, Subfunctor.lift_ι, stdSimplex.map_apply,
        Quiver.Hom.unop_op, stdSimplex.map_apply, Quiver.Hom.unop_op]
      dsimp [CosimplicialObject.δ]
      rw [SSet.yonedaEquiv_map]
      simp only [Equiv.apply_symm_apply, triangle]
      rw [mkOfSucc_δ_eq heq]
      fin_cases z <;> rfl

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
⊢ X.Quasicategory

Tactic:
apply quasicategory_of_filler X
  intro n i σ₀ h₀ hₙ
  use sx.spineToSimplex <| Path.map (horn.spineId i h₀ hₙ) σ₀
  intro j hj
  apply sx.spineInjective
  ext k
  dsimp only [spineEquiv, spine_arrow, Function.comp_apply, Equiv.coe_fn_mk]
  rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality]
  let ksucc := k.succ.castSucc
  obtain hlt | hgt | heq : ksucc < j ∨ j < ksucc ∨ j = ksucc := by lia
  · rw [← spine_arrow, spine_δ_arrow_lt sx _ hlt]
    dsimp only [Path.map_arrow, spine_arrow, Fin.coe_eq_castSucc]
    dsimp
    apply congr_arg
    apply Subtype.ext
    dsimp [horn.face, CosimplicialObject.δ]
    rw [dsimp% Subcomplex.yonedaEquiv_coe, Subfunctor.lift_ι, stdSimplex.map_apply,
      Quiver.Hom.unop_op, SSet.yonedaEquiv_map, Equiv.apply_symm_apply,
      mkOfSucc_δ_lt hlt]
    rfl
  · rw [← spine_arrow, spine_δ_arrow_gt sx _ hgt]
    dsimp
    apply congr_arg
    apply Subtype.ext
    dsimp [horn.face, CosimplicialObject.δ]
    rw [dsimp% Subcomplex.yonedaEquiv_coe, Subfunctor.lift_ι, stdSimplex.map_apply,
      Quiver.Hom.unop_op, SSet.yonedaEquiv_map, Equiv.apply_symm_apply,
      mkOfSucc_δ_gt hgt]
    rfl
  · obtain _ | n := n
    · /- The only inner horn of `Δ[2]` does not contain the diagonal edge. -/
      obtain rfl : k = 0 := by omega
      fin_cases i <;> contradiction
    · /- We construct the triangle in the standard simplex as a 2-simplex in
      the horn. While the triangle is not contained in the inner horn `Λ[2, 1]`,
      it suffices to inhabit `Λ[n + 3, i] _⦋2⦌`. -/
      let triangle : (Λ[n + 3, i] : SSet.{u}) _⦋2⦌ :=
        horn.primitiveTriangle i h₀ hₙ k (by grind)
      /- The interval spanning from `k` to `k + 2` is equivalently the spine
      of the triangle with vertices `k`, `k + 1`, and `k + 2`. -/
      have hi : ((horn.spineId i h₀ hₙ).map σ₀).interval k 2 (by grind) =
          X.spine 2 (σ₀.app _ triangle) := by
        ext m
        dsimp [spine_arrow, Path.map_interval, Path.map_arrow]
        rw [← dsimp% σ₀.naturality_apply]
        apply congr_arg
        apply Subtype.ext
        ext a : 1
        fin_cases a <;> fin_cases m <;> rfl
      rw [← spine_arrow, spine_δ_arrow_eq sx _ heq, hi]
      simp only [spineToDiagonal, diagonal, spineToSimplex_spine_apply]
      rw [← types_comp_apply (σ₀.app _) (X.map _), ← σ₀.naturality, types_comp_apply]
      dsimp
      apply congr_arg
      apply Subtype.ext
      ext z : 1
      dsimp [horn.face]
      rw [dsimp% Subcomplex.yonedaEquiv_coe, Subfunctor.lift_ι, stdSimplex.map_apply,
        Quiver.Hom.unop_op, stdSimplex.map_apply, Quiver.Hom.unop_op]
      dsimp [CosimplicialObject.δ]
      rw [SSet.yonedaEquiv_map]
      simp only [Equiv.apply_symm_apply, triangle]
      rw [mkOfSucc_δ_eq heq]
      fin_cases z <;> rfl

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a✝ b✝ c✝ d✝ e✝ : CatEnriched C
f : a✝ ⟶ b✝
g : b✝ ⟶ c✝
h : c✝ ⟶ d✝
i : d✝ ⟶ e✝
⊢ hComp (eqToIso ⋯).hom (𝟙 i) ≫ (eqToIso ⋯).hom ≫ hComp (𝟙 f) (eqToIso ⋯).hom = (eqToIso ⋯).hom ≫ (eqToIso ⋯).hom

Tactic:
generalize_proofs h1 h2 h3 h4; revert h1 h2 h3 h4
    generalize (f ≫ g) ≫ h = x, (g ≫ h) ≫ i = w
    rintro rfl _ rfl _; simp

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 U' : C
⊢ 𝟙 ((X.fst ⊗ Y.fst) ⊗ U ⊗ U') ⊗≫
      X.fst ◁ (Y.snd.β U).hom ▷ U' ⊗≫
        ((X.fst ⊗ U) ◁ (Y.snd.β U').hom ≫ (X.snd.β U).hom ▷ (U' ⊗ Y.fst)) ⊗≫
          U ◁ (X.snd.β U').hom ▷ Y.fst ⊗≫ 𝟙 ((U ⊗ U') ⊗ X.fst ⊗ Y.fst) =
    (α_ (X.fst ⊗ Y.fst) U U').inv ≫
      ((α_ 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' ≫
        (α_ U (X.fst ⊗ Y.fst) U').hom ≫
          U ◁
              ((α_ 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 U' (X.fst ⊗ Y.fst)).inv

Tactic:
rw [whisker_exchange]; monoidal

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₁ Y₂ : Center C
f : Y₁ ⟶ Y₂
U : C
⊢ 𝟙 ((X.fst ⊗ Y₁.fst) ⊗ U) ⊗≫
      X.fst ◁ (Y₁.snd.β U).hom ⊗≫ ((X.fst ⊗ U) ◁ f.f ≫ (X.snd.β U).hom ▷ Y₂.fst) ⊗≫ 𝟙 (U ⊗ X.fst ⊗ Y₂.fst) =
    ((α_ 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.fst ◁ f.f

Tactic:
rw [whisker_exchange]; monoidal

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

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
motive : {x y : FreeRefl V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk : ∀ {x y z : V} (f : mk x ⟶ mk y) (g : y ⟶ z), motive f → motive (f ≫ homMk g)
x y : FreeRefl V
f : x ⟶ y
⊢ motive f

Tactic:
induction x using induction with

Goal state after:
case mk
V : Type u_1
inst✝ : ReflQuiver V
motive : {x y : FreeRefl V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk : ∀ {x y z : V} (f : mk x ⟶ mk y) (g : y ⟶ z), motive f → motive (f ≫ homMk g)
y : FreeRefl V
x : V
f : mk x ⟶ y
⊢ motive f
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝ : ReflQuiver V
motive : {x y : FreeRefl V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk : ∀ {x y z : V} (f : mk x ⟶ mk y) (g : y ⟶ z), motive f → motive (f ≫ homMk g)
x y : FreeRefl V
f : x ⟶ y
⊢ motive f

Tactic:
induction x using induction with | _ x

Goal state after:
case mk
V : Type u_1
inst✝ : ReflQuiver V
motive : {x y : FreeRefl V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk : ∀ {x y z : V} (f : mk x ⟶ mk y) (g : y ⟶ z), motive f → motive (f ≫ homMk g)
y : FreeRefl V
x : V
f : mk x ⟶ y
⊢ motive f