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

Goal state before:
pp: case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : ↑I
hx : x ∈ {1}
⊢ { toFun := fun x ↦ p ⟨↑(σ (t, x).1) * ↑(t, x).2 + ↑(t, x).1 * ↑(f (t, x).2), ⋯⟩, continuous_toFun := ⋯ } x =
    p.toContinuousMap x

Tactic:
Set.mem_singleton_iff

Goal state after:
case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
f : ↑I → ↑I
hf : Continuous f
hf₀ : f 0 = 0
hf₁ : f 1 = 1
t x : ↑I
hx : x = 1
⊢ { toFun := fun x ↦ p ⟨↑(σ (t, x).1) * ↑(t, x).2 + ↑(t, x).1 * ↑(f (t, x).2), ⋯⟩, continuous_toFun := ⋯ } x =
    p.toContinuousMap x
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: case inr
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
t x : ↑I
hx : x ∈ {1}
⊢ { toFun := fun x ↦ F ((t, x).1, σ (t, x).2), continuous_toFun := ⋯ } x = p.symm.toContinuousMap x

Tactic:
Set.mem_singleton_iff

Goal state after:
case inr
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
t x : ↑I
hx : x = 1
⊢ { toFun := fun x ↦ F ((t, x).1, σ (t, x).2), continuous_toFun := ⋯ } x = p.symm.toContinuousMap x
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: case inr
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 ∈ {1}
⊢ { toFun := fun x ↦ (⇑f ∘ ⇑F) (t, x), continuous_toFun := ⋯ } x = (p.map ⋯).toContinuousMap x

Tactic:
Set.mem_singleton_iff

Goal state after:
case inr
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 = 1
⊢ { toFun := fun x ↦ (⇑f ∘ ⇑F) (t, x), continuous_toFun := ⋯ } x = (p.map ⋯).toContinuousMap x
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) p) ≫ hcast ⋯) ≫
        ⟦H.evalAt x₁⟧ =
      H.diagonalPath' p ∧
    ⟦H.evalAt x₀⟧ ≫
        hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) p) ≫ hcast ⋯ =
      H.diagonalPath' p

Tactic:
H.evalAt_eq

Goal state after:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) p) ≫ hcast ⋯) ≫
        ⟦H.evalAt x₁⟧ =
      H.diagonalPath' p ∧
    (hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x₀))) ≫ hcast ⋯) ≫
        hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) p) ≫ hcast ⋯ =
      H.diagonalPath' p
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) p) ≫ hcast ⋯) ≫
        ⟦H.evalAt x₁⟧ =
      H.diagonalPath' p ∧
    (hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x₀))) ≫ hcast ⋯) ≫
        hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) p) ≫ hcast ⋯ =
      H.diagonalPath' p

Tactic:
H.evalAt_eq

Goal state after:
X Y : TopCat
f g : C(↑X, ↑Y)
H : f.Homotopy g
x₀ x₁ : ↑X
p : fromTop x₀ ⟶ fromTop x₁
⊢ (hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 0 })) p) ≫ hcast ⋯) ≫
        hcast ⋯ ≫
          (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop (fromTop x₁).as))) ≫ hcast ⋯ =
      H.diagonalPath' p ∧
    (hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI uhpath01 (𝟙 (fromTop x₀))) ≫ hcast ⋯) ≫
        hcast ⋯ ≫ (π.map (TopCat.ofHom H.uliftMap)).map (prodToProdTopI (𝟙 (fromTop { down := 1 })) p) ≫ hcast ⋯ =
      H.diagonalPath' p
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: case pos.left
x : ↑I × ↑I
h✝ : ↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1 * 2 * ↑x.2

Tactic:
apply mul_nonneg <;> grind

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

Goal state before:
pp: case neg.left
x : ↑I × ↑I
h✝ : ¬↑x.2 ≤ 1 / 2
⊢ 0 ≤ ↑x.1 * (2 - 2 * ↑x.2)

Tactic:
apply mul_nonneg <;> grind

Goal state after:
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)
this : WeakEquivalence (h.p ≫ pullback.snd p g)
⊢ (sq'.lift ≫ h.p ≫ pullback.fst p g) ≫ p = g

Tactic:
by
                rw [assoc, assoc, pullback.condition, reassoc_of% sq'.fac_right]

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

Goal state before:
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:
obtain ⟨i, q, rfl⟩ := SimplexCategory.eq_comp_δ_of_not_surjective f (fun hf ↦ by
      rw [← SimplexCategory.epi_iff_surjective] at hf
      have : n + 1 ≤ m := SimplexCategory.len_le_of_epi f
      lia)
    apply face_singleton_compl_le_boundary i
    rw [stdSimplex.face_singleton_compl, stdSimplex.objEquiv_symm_comp,
      ← Subcomplex.ofSimplex_le_iff]
    apply Subcomplex.ofSimplex_map_le

Goal state after:
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom (c₁.ι.app j ≫ φ)) x = (hom (f.app j ≫ c₂.ι.app j)) x
⊢ Function.Injective ⇑(hom φ)

Tactic:
simp only [Functor.const_obj_obj, comp_apply] at hφ

Goal state after:
J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
⊢ Function.Injective ⇑(hom φ)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) s✝)) = Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) s✝))

pp: case inr_inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
s✝ : S
⊢ Quot.mk (Rel f g) (Sum.inr ((ConcreteCategory.hom g) s✝)) = Quot.mk (Rel f g) (Sum.inl ((ConcreteCategory.hom f) s✝))

Tactic:
· apply Quot.sound
      apply Rel.inl_inr

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

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

Tactic:
· symm
      apply Quot.sound
      apply Rel.inl_inr

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

Goal state before:
pp: X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
ht : Function.Injective ⇑(ConcreteCategory.hom t)
⊢ IsPullback t l r b

Tactic:
isPullback_iff

Goal state after:
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
ht : Function.Injective ⇑(ConcreteCategory.hom t)
⊢ t ≫ r = l ≫ b ∧
    (∀ (x₁ y₁ : (fun X ↦ X) X₁),
        (ConcreteCategory.hom t) x₁ = (ConcreteCategory.hom t) y₁ ∧
            (ConcreteCategory.hom l) x₁ = (ConcreteCategory.hom l) y₁ →
          x₁ = y₁) ∧
      ∀ (x₂ : (fun X ↦ X) X₂) (x₃ : (fun X ↦ X) X₃),
        (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom b) x₃ →
          ∃ x₁, (ConcreteCategory.hom t) x₁ = x₂ ∧ (ConcreteCategory.hom l) x₁ = x₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case commf
⊢ (stdSimplex.faceSingletonIso 0).hom ≫ Subcomplex.homOfLE ⋯ = stdSimplex.δ 1 ≫ (stdSimplex.facePairIso 0 1 ⋯).hom

pp: case commg
⊢ (stdSimplex.faceSingletonIso 0).hom ≫ Subcomplex.homOfLE ⋯ = stdSimplex.δ 1 ≫ (stdSimplex.facePairIso 0 2 ⋯).hom

pp: case comminl
⊢ (stdSimplex.facePairIso 0 1 ⋯).hom ≫ Subcomplex.homOfLE ⋯ = ι₀₁ ≫ (Iso.refl Λ[2, 0].toSSet).hom

pp: case comminr
⊢ (stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯ = ι₀₂ ≫ (Iso.refl Λ[2, 0].toSSet).hom

Tactic:
all_goals decide

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

Goal state before:
pp: case commf
⊢ (stdSimplex.faceSingletonIso 1).hom ≫ Subcomplex.homOfLE ⋯ = stdSimplex.δ 0 ≫ (stdSimplex.facePairIso 0 1 ⋯).hom

pp: case commg
⊢ (stdSimplex.faceSingletonIso 1).hom ≫ Subcomplex.homOfLE ⋯ = stdSimplex.δ 1 ≫ (stdSimplex.facePairIso 1 2 ⋯).hom

pp: case comminl
⊢ (stdSimplex.facePairIso 0 1 ⋯).hom ≫ Subcomplex.homOfLE ⋯ = ι₀₁ ≫ (Iso.refl Λ[2, 1].toSSet).hom

pp: case comminr
⊢ (stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯ = ι₁₂ ≫ (Iso.refl Λ[2, 1].toSSet).hom

Tactic:
all_goals decide

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

Goal state before:
pp: case commf
⊢ (stdSimplex.faceSingletonIso 2).hom ≫ Subcomplex.homOfLE ⋯ = stdSimplex.δ 0 ≫ (stdSimplex.facePairIso 0 2 ⋯).hom

pp: case commg
⊢ (stdSimplex.faceSingletonIso 2).hom ≫ Subcomplex.homOfLE ⋯ = stdSimplex.δ 0 ≫ (stdSimplex.facePairIso 1 2 ⋯).hom

pp: case comminl
⊢ (stdSimplex.facePairIso 0 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯ = ι₀₂ ≫ (Iso.refl Λ[2, 2].toSSet).hom

pp: case comminr
⊢ (stdSimplex.facePairIso 1 2 ⋯).hom ≫ Subcomplex.homOfLE ⋯ = ι₁₂ ≫ (Iso.refl Λ[2, 2].toSSet).hom

Tactic:
all_goals decide

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j k : ↑{i}ᶜ
⊢ stdSimplex.face {↑j, ↑k}ᶜ = stdSimplex.face {↑j}ᶜ ⊓ stdSimplex.face {↑k}ᶜ

Tactic:
stdSimplex.face_inter_face

Goal state after:
n : ℕ
i : Fin (n + 1)
j k : ↑{i}ᶜ
⊢ stdSimplex.face {↑j, ↑k}ᶜ = stdSimplex.face ({↑j}ᶜ ⊓ {↑k}ᶜ)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ ((t i d).app (op ⦋n⦌) ≫ ↾fun x ↦ ⟨↑x, ⋯⟩) = (l i d).app (op ⦋n⦌) ≫ (b i d).app (op ⦋n⦌) ∧
    (∀ (x₁ y₁ : (fun X ↦ X) (sigmaBoundary i d _⦋n⦌)),
        (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) x₁ = (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) y₁ ∧
            (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) x₁ = (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) y₁ →
          x₁ = y₁) ∧
      ∀ (x₂ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))) (x₃ : (fun X ↦ X) (sigmaStdSimplex i d _⦋n⦌)),
        (ConcreteCategory.hom (↾fun x ↦ ⟨↑x, ⋯⟩)) x₂ = (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₃ →
          ∃ x₁,
            (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) x₁ = x₂ ∧
              (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) x₁ = x₃

Tactic:
refine ⟨NatTrans.congr_app (w i d) _,
      fun x₁ x₂ ⟨_, h⟩ ↦ injective_of_mono ((l i d).app (op ⦋n⦌)) h,
      fun ⟨x, hx⟩ y h ↦ ?_⟩

Goal state after:
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : (fun X ↦ X) ↑(((skeletonOfMono i) d).obj (op ⦋n⦌))
y : (fun X ↦ X) (sigmaStdSimplex i d _⦋n⦌)
x : Y _⦋n⦌
hx : x ∈ ((skeletonOfMono i) d).obj (op ⦋n⦌)
h : (ConcreteCategory.hom (↾fun x ↦ ⟨↑x, ⋯⟩)) ⟨x, hx⟩ = (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) y
⊢ ∃ x₁,
    (ConcreteCategory.hom ((t i d).app (op ⦋n⦌))) x₁ = ⟨x, hx⟩ ∧ (ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) x₁ = y
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

Tactic:
exact range_r_app_union_range_b_app _ _ _

Goal state after:
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) := k.succ.castSucc
hlt : ksucc < j
⊢ (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋1⦌))) ((horn.spineId i h₀ hₙ).arrow k.castSucc) =
    (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋1⦌)))
      ⟨(ConcreteCategory.hom (Δ[n + 2].map (mkOfSucc k).op)) ↑(horn.face i j hj), ⋯⟩

Tactic:
apply congr_arg

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.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) := k.succ.castSucc
hgt : 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 + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)

Tactic:
rw [← spine_arrow, spine_δ_arrow_gt sx _ hgt]

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) := k.succ.castSucc
hgt : j < ksucc
⊢ ((horn.spineId i h₀ hₙ).map σ₀).arrow k.succ =
    (ConcreteCategory.hom (Λ[n + 2, i].toSSet.map (mkOfSucc k).op ≫ σ₀.app (Opposite.op ⦋1⦌))) (horn.face i j hj)
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) := k.succ.castSucc
hgt : j < ksucc
⊢ (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋1⦌))) ((horn.spineId i h₀ hₙ).arrow k.succ) =
    (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋1⦌)))
      ⟨(ConcreteCategory.hom (Δ[n + 2].map (mkOfSucc k).op)) ↑(horn.face i j hj), ⋯⟩

Tactic:
apply congr_arg

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.HornColimits

Goal state before:
pp: X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ ι₁ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = f₁

Tactic:
rw [← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 1).inv, ← Category.assoc,
    horn.faceSingletonComplIso_inv_ι]

Goal state after:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ horn.faceι 2 1 ι₁._proof_1 ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = (stdSimplex.faceSingletonComplIso 1).inv ≫ f₁
Module: Mathlib.CategoryTheory.Monoidal.Types.Coyoneda

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| ((λ_ (𝟙_ C)).inv ≫ (f ⊗ₘ g) ⊗ₘ h) ≫ (α_ X Y Z).hom

Tactic:
← Category.id_comp h,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : MonoidalCategory C
X Y Z : C
h : 𝟙_ C ⟶ Z
f : 𝟙_ C ⟶ X
g : 𝟙_ C ⟶ Y
| ((λ_ (𝟙_ C)).inv ≫ (f ⊗ₘ g) ⊗ₘ 𝟙 (𝟙_ C) ≫ h) ≫ (α_ X Y Z).hom
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) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
m : Fin (1 + 1)
⊢ (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋1⦌))) (((horn.spineId i h₀ hₙ).interval (↑k) 2 ⋯).arrow m) =
    (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋1⦌)))
      ⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc m).op)) ↑triangle, ⋯⟩

Tactic:
apply congr_arg

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.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
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
⊢ (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋1⦌)))
      ⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (diag 2).op)) ↑triangle, ⋯⟩ =
    (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋1⦌)))
      ⟨(ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc k).op)) ↑(horn.face i j hj), ⋯⟩

Tactic:
apply congr_arg

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.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ G✝ : C ⥤ D
F G A : C ⥤ Type w
a : F.HomObj G A
X Y : C
f : X ⟶ Y
⊢ ((F ⊗ A).map f ≫
      ↾fun x ↦
        match x with
        | (x, y) => (ConcreteCategory.hom (a.app Y y)) x) =
    (↾fun x ↦
        match x with
        | (x, y) => (ConcreteCategory.hom (a.app X y)) x) ≫
      G.map f

Tactic:
ext ⟨x, y⟩

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ G✝ : C ⥤ D
F G A : C ⥤ Type w
a : F.HomObj G A
X Y : C
f : X ⟶ Y
x : F.obj X
y : A.obj X
⊢ (ConcreteCategory.hom
          ((F ⊗ A).map f ≫
            ↾fun x ↦
              match x with
              | (x, y) => (ConcreteCategory.hom (a.app Y y)) x)).toFun
      (x, y) =
    (ConcreteCategory.hom
          ((↾fun x ↦
              match x with
              | (x, y) => (ConcreteCategory.hom (a.app X y)) x) ≫
            G.map f)).toFun
      (x, y)
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 : TransportEnrichment F (ForgetEnrichment V D)
⊢ ForgetEnrichment.homOf W (eId W (ForgetEnrichment.to V X)) = 𝟙 (ForgetEnrichment.of W X)

Tactic:
simp [ForgetEnrichment.to]

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

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

Tactic:
by
  rw [← preimage_β_hom, preimage_image_of_isIso]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y : SimplexCategory
h : WithInitial.of x = WithInitial.of y
⊢ x.len = y.len

Tactic:
injection h with h; rw [h]

Goal state after: