mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X Y✝ : C
inst✝¹ : IsCofibrant X
Y : C
inst✝ : IsFibrant Y
h✝¹ : IsCofibrant Y
this✝ : ∀ (X : C) [IsCofibrant X], IsFibrant X → Function.Bijective (rightHomotopyClassToHom L)
h✝ : ¬IsFibrant X
X' : C
i : X ⟶ X'
left✝¹ : Cofibration i
left✝ : WeakEquivalence i
right✝ : IsFibrant X'
x✝ : IsCofibrant X'
hX' : Function.Bijective (rightHomotopyClassToHom L)
this : IsIso (L.map i)
f : X' ⟶ Y
⊢ (rightHomotopyClassToHom L ∘ fun g ↦ g.precomp i) (RightHomotopyClass.mk f) =
    (⇑((asIso (L.map i)).homCongr (Iso.refl (L.obj Y))).symm ∘ rightHomotopyClassToHom L) (RightHomotopyClass.mk f)

Tactic:
simp

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✝⁶ : (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)
⊢ sq.HasLift

Tactic:
have : WeakEquivalence (pushout.inl f i ≫ h.i) := by
      rw [weakEquivalence_iff] at h₁ ⊢
      exact of_postcomp _ _ _ h.hp.2 h₁

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₁ : WeakEquivalence ((pushout.inl f i ≫ h.i) ≫ h.p)
h₂ : Cofibration (pushout.inl f i ≫ h.i)
this : WeakEquivalence (pushout.inl f i ≫ h.i)
⊢ sq.HasLift
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₂
⊢ ι.map (f ≫ X₂.iBifibrantResolutionObj) ≫
      terminal.from (ι.obj (BifibrantObject.ιCofibrantObject.obj X₂.bifibrantResolutionObj)) =
    X₁.iBifibrantResolutionObj.hom ≫ terminal.from (BifibrantObject.ιCofibrantObject.obj X₁.bifibrantResolutionObj).obj

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X : CofibrantObject C
⊢ toHoCat.map X.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map (BifibrantObject.toHoCat.map (bifibrantResolutionMap (𝟙 X))) =
    toHoCat.map X.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map (𝟙 (BifibrantObject.toHoCat.obj X.bifibrantResolutionObj))

Tactic:
simp

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X₁ X₂ X₃ : CofibrantObject C
f : X₁ ⟶ X₂
g : X₂ ⟶ X₃
⊢ toHoCat.map X₁.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map (BifibrantObject.toHoCat.map (bifibrantResolutionMap (f ≫ g))) =
    toHoCat.map X₁.iBifibrantResolutionObj ≫
      BifibrantObject.HoCat.ιCofibrantObject.map
        (BifibrantObject.toHoCat.map (bifibrantResolutionMap f) ≫
          BifibrantObject.toHoCat.map (bifibrantResolutionMap g))

Tactic:
simp

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 : HoCat C
f : X ⟶ Y
⊢ weakEquivalences (HoCat C) f → IsIso (HoCat.bifibrantResolution.map f)

Tactic:
hf

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ModelCategory C
X Y : HoCat C
f : X ⟶ Y
hf : weakEquivalences (HoCat C) f
⊢ IsIso (HoCat.bifibrantResolution.map f)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x' y' : X
p : Path.Homotopic.Quotient x' y'
⊢ eqToHom ⋯ ≫ p ≫ eqToHom ⋯ = p.cast ⋯ ⋯

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: case id
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MulticospanShape
d : MulticospanIndex J C
c : Multifork d
F : C ⥤ D
a : WalkingMulticospan J
⊢ (d.map F).multicospan.map (WalkingMulticospan.Hom.id a) ≫
      (match a with
        | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom =
    (match a with
        | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom ≫
      (d.multicospan ⋙ F).map (WalkingMulticospan.Hom.id a)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: case fst
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MulticospanShape
d : MulticospanIndex J C
c : Multifork d
F : C ⥤ D
b✝ : J.R
⊢ (d.map F).multicospan.map (WalkingMulticospan.Hom.fst b✝) ≫
      (match WalkingMulticospan.right b✝ with
        | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom =
    (match WalkingMulticospan.left (J.fst b✝) with
        | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom ≫
      (d.multicospan ⋙ F).map (WalkingMulticospan.Hom.fst b✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: case snd
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MulticospanShape
d : MulticospanIndex J C
c : Multifork d
F : C ⥤ D
b✝ : J.R
⊢ (d.map F).multicospan.map (WalkingMulticospan.Hom.snd b✝) ≫
      (match WalkingMulticospan.right b✝ with
        | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom =
    (match WalkingMulticospan.left (J.snd b✝) with
        | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
        | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom ≫
      (d.multicospan ⋙ F).map (WalkingMulticospan.Hom.snd b✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MulticospanShape
d : MulticospanIndex J C
c : Multifork d
F : C ⥤ D
i : J.L
⊢ (Iso.refl ((Cone.postcompose (d.multicospanMapIso F).inv).obj (F.mapCone c)).pt).hom ≫
      (c.map F).π.app (WalkingMulticospan.left i) =
    ((Cone.postcompose (d.multicospanMapIso F).inv).obj (F.mapCone c)).π.app (WalkingMulticospan.left i)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
i : C
x : A.toFunctor.obj i
⊢ ↑x ∈ (Subfunctor.equalizer f g).obj i ↔ (ConcreteCategory.hom (f.app i)) x = (ConcreteCategory.hom (g.app i)) x

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: case id
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
X✝ : WalkingMultispan J
⊢ (d.map F).multispan.map (WalkingMultispan.Hom.id X✝) ≫
      (match X✝ with
        | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom =
    (match X✝ with
        | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom ≫
      (d.multispan ⋙ F).map (WalkingMultispan.Hom.id X✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: case fst
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
a✝ : J.L
⊢ (d.map F).multispan.map (WalkingMultispan.Hom.fst a✝) ≫
      (match WalkingMultispan.right (J.fst a✝) with
        | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom =
    (match WalkingMultispan.left a✝ with
        | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom ≫
      (d.multispan ⋙ F).map (WalkingMultispan.Hom.fst a✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: case snd
C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
a✝ : J.L
⊢ (d.map F).multispan.map (WalkingMultispan.Hom.snd a✝) ≫
      (match WalkingMultispan.right (J.snd a✝) with
        | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom =
    (match WalkingMultispan.left a✝ with
        | WalkingMultispan.left a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.left a))
        | WalkingMultispan.right a => Iso.refl ((d.map F).multispan.obj (WalkingMultispan.right a))).hom ≫
      (d.multispan ⋙ F).map (WalkingMultispan.Hom.snd a✝)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MultispanShape
d : MultispanIndex J C
c : Multicofork d
F : C ⥤ D
i : J.R
⊢ ((Cocone.precompose (d.multispanMapIso F).symm.inv).obj (F.mapCocone c)).ι.app (WalkingMultispan.right i) ≫
      (Iso.refl ((Cocone.precompose (d.multispanMapIso F).symm.inv).obj (F.mapCocone c)).pt).hom =
    (c.map F).ι.app (WalkingMultispan.right i)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
U✝ V✝ : SimplexCategoryᵒᵖ
φ : U✝ ⟶ V✝
s : Δ[n].obj U✝
hs : s ∈ {s | Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i} ≠ Set.univ}
h : ∀ (x : Fin (n + 1)), x ∈ Set.range ⇑(stdSimplex.asOrderHom ((ConcreteCategory.hom (Δ[n].map φ)) s)) ∪ {i}
⊢ ∀ (x : Fin (n + 1)), x ∈ Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i}

Tactic:
intro j

Goal state after:
n : ℕ
i : Fin (n + 1)
U✝ V✝ : SimplexCategoryᵒᵖ
φ : U✝ ⟶ V✝
s : Δ[n].obj U✝
hs : s ∈ {s | Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i} ≠ Set.univ}
h : ∀ (x : Fin (n + 1)), x ∈ Set.range ⇑(stdSimplex.asOrderHom ((ConcreteCategory.hom (Δ[n].map φ)) s)) ∪ {i}
j : Fin (n + 1)
⊢ j ∈ Set.range ⇑(stdSimplex.asOrderHom s) ∪ {i}
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
r : J.R
z : d.multispan.obj (WalkingMultispan.right r)
⊢ d.multispan.ιColimitType (WalkingMultispan.right r) z = d.multispan.ιColimitType (WalkingMultispan.right r) z

Tactic:
simp

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

Goal state before:
pp: J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
hc : c.IsColimit
i : J.R
z : d.right i
⊢ c.ι (WalkingMultispan.right i) z =
    d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i) z)

Tactic:
simp

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

Goal state before:
pp: n d : ℕ
s : Δ[n] _⦋d⦌
⊢ s ∈ (⨆ i, stdSimplex.face {i}ᶜ).obj (op ⦋d⦌) ↔ ∃ j, j ∉ Set.range ⇑s

Tactic:
simp

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

Goal state before:
pp: n : ℕ
⊢ ∂Δ[n] ≤ ⊤

Tactic:
simp

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

Goal state before:
pp: n : ℕ
h : ⊤ ≤ ∂Δ[n]
⊢ stdSimplex.objMk OrderHom.id ∈ ⊤.obj (op ⦋n⦌)

Tactic:
simp

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

Goal state before:
pp: n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
hd✝ : n ≤ d
hd : n < d
hS : Finset.univ.card = d + 1
hx : stdSimplex.face Finset.univ ≤ A
⊢ stdSimplex.face {i}ᶜ ≤ stdSimplex.face Finset.univ

Tactic:
simp

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

Goal state before:
pp: n : ℕ
A : Δ[n].Subcomplex
h : A ≠ ⊤
hi : n ≤ n
ha : objEquiv.symm (𝟙 (unop (op ⦋n⦌))) ∈ A.obj (op ⦋n⦌)
⊢ A ≤ ⊤

Tactic:
simp

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
⊢ {i}ᶜ ≠ Finset.univ ∧ {i}ᶜ ≠ {j}ᶜ ↔ ¬i = j

Tactic:
simp

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

Goal state before:
pp: n : ℕ
i k : Fin (n + 3)
m : SimplexCategoryᵒᵖ
⊢ stdSimplex.obj₀Equiv.symm k ∈ Λ[n + 2, i].obj (op ⦋0⦌)

Tactic:
simp

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Set

Goal state before:
pp: case hsurj
J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
⊢ ∀ (x : (functorToTypes.mapCocone (colimitCocone F).cocone).pt),
    ∃ i xi, x = (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) xi

pp: case hinj
J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
⊢ ∀ (i j : J) (xi : (fun X ↦ X) ((F ⋙ functorToTypes).obj i)) (xj : (fun X ↦ X) ((F ⋙ functorToTypes).obj j)),
    (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) xi =
        (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((F ⋙ functorToTypes).map f)) xi = (ConcreteCategory.hom ((F ⋙ functorToTypes).map g)) xj

Tactic:
· rintro ⟨x, hx⟩
      simp only [colimitCocone_cocone_pt, iSup_eq_iUnion, mem_iUnion] at hx
      obtain ⟨i, hi⟩ := hx
      exact ⟨i, ⟨x, hi⟩, rfl⟩

Goal state after:
case hinj
J : Type w
inst✝¹ : Category.{w', w} J
X : Type u
inst✝ : IsFilteredOrEmpty J
F : J ⥤ Set X
⊢ ∀ (i j : J) (xi : (fun X ↦ X) ((F ⋙ functorToTypes).obj i)) (xj : (fun X ↦ X) ((F ⋙ functorToTypes).obj j)),
    (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app i)) xi =
        (ConcreteCategory.hom ((functorToTypes.mapCocone (colimitCocone F).cocone).ι.app j)) xj →
      ∃ k f g,
        (ConcreteCategory.hom ((F ⋙ functorToTypes).map f)) xi = (ConcreteCategory.hom ((F ⋙ functorToTypes).map g)) xj
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j h) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j h)
⊢ ∀ (a : Fin (n + 1 + 1)), ¬a = i → yonedaEquiv (stdSimplex.δ a) ∈ (Subfunctor.equalizer σ₁ σ₂).obj (op ⦋n⦌)

Tactic:
intro j

Goal state after:
n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j h) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j h)
j : Fin (n + 1 + 1)
⊢ ¬j = i → yonedaEquiv (stdSimplex.δ j) ∈ (Subfunctor.equalizer σ₁ σ₂).obj (op ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
hf : horn.IsCompatible f
Y : SSet
p : X ⟶ Y
inst✝ : Fibration p
b : Δ[n + 1] ⟶ Y
comm : ∀ (j : Fin (n + 2)) (hj : j ≠ i), f j hj ≫ p = stdSimplex.δ j ≫ b
sq : CommSq hf.desc Λ[n + 1, i].ι p b
⊢ sq.lift ≫ p = b

Tactic:
simp

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

Goal state before:
pp: S : SSet
inst✝ : S.KanComplex
n : ℕ
i : Fin (n + 2)
σ₀ : Λ[n + 1, i].toSSet ⟶ S
⊢ σ₀ ≫ terminal.from S = Λ[n + 1, i].ι ≫ terminal.from Δ[n + 1]

Tactic:
simp

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

Goal state before:
pp: S : SSet
inst✝ : S.KanComplex
n : ℕ
i : Fin (n + 2)
σ₀ : Λ[n + 1, i].toSSet ⟶ S
sq' : CommSq σ₀ Λ[n + 1, i].ι (terminal.from S) (terminal.from Δ[n + 1])
⊢ σ₀ = Λ[n + 1, i].ι ≫ sq'.lift

Tactic:
simp

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
inst✝ : X.KanComplex
hf : horn.IsCompatible f
⊢ ∀ (j : Fin (n + 2)) (hj : j ≠ i), f j hj ≫ terminal.from X = stdSimplex.δ j ≫ terminal.from Δ[n + 1]

Tactic:
simp

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

Goal state before:
pp: Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
X✝ Y✝ : SSet
g✝ : X✝ ⟶ Y✝
⊢ J g✝ → HasLiftingProperty g✝ (terminal.from Z)

Tactic:
hf

Goal state after:
Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
X✝ Y✝ : SSet
g✝ : X✝ ⟶ Y✝
hf : J g✝
⊢ HasLiftingProperty g✝ (terminal.from Z)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
h₁ : Function.Injective ⇑(ConcreteCategory.hom f)
x₁ : X₁
x₂ : X₂
⊢ ∀ (j : WalkingSpan),
    c.ι.app j ≫ (hc.coconePointUniqueUpToIso (Pushout.isColimitCocone f g)).hom = (Pushout.cocone f g).ι.app j

Tactic:
simp

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
inst✝ : Mono f
⊢ ∀ (j : WalkingSpan),
    c.ι.app j ≫ (hc.coconePointUniqueUpToIso (Pushout.isColimitCocone f g)).hom = (Pushout.cocone f g).ι.app j

Tactic:
simp

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
x : (span t l).obj none
⊢ (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom (h.cocone.ι.app none)) x

Tactic:
simp

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
x : (span t l).obj none
⊢ (ConcreteCategory.hom r) ((ConcreteCategory.hom t) x) = (ConcreteCategory.hom (t ≫ r)) x
Module: Mathlib.AlgebraicTopology.Quasicategory.Basic

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

Tactic:
intro j

Goal state after:
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
      (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
j : Fin (n + 1 + 2)
⊢ ∀ (h : j ≠ i),
    (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h) =
      (ConcreteCategory.hom ((Λ[n + 2, i].ι ≫ yonedaEquiv.symm σ).app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
Module: Mathlib.AlgebraicTopology.Quasicategory.Basic

Goal state before:
pp: S X : SSet
t : Limits.IsTerminal X
h : ∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → HasLiftingProperty Λ[n, i].ι (t.from S)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h0 : 0 < i
hn : i < Fin.last (n + 2)
this : HasLiftingProperty Λ[n + 2, i].ι (t.from S) := h h0 hn
⊢ σ₀ = Λ[n + 2, i].ι ≫ ⋯.lift

Tactic:
simp

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

Goal state before:
pp: ⊢ 2 ≠ 0

Tactic:
simp

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

Goal state before:
pp: ⊢ 1 ≠ 0

Tactic:
simp

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

Goal state before:
pp: ⊢ 0 < 1

Tactic:
simp

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

Goal state before:
pp: ⊢ 0 < 2

Tactic:
simp

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

Goal state before:
pp: ⊢ 2 ≠ 1

Tactic:
simp

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

Goal state before:
pp: ⊢ 0 ≠ 1

Tactic:
simp

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

Goal state before:
pp: X : SSet
⊢ ⨆ n, X.skeleton n ≤ ⊤

Tactic:
simp

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

Goal state before:
pp: ⊢ 1 < 2

Tactic:
simp

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

Goal state before:
pp: ⊢ 1 ≠ 2

Tactic:
simp

Goal state after: