mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.InducedMaps

Goal state before:
pp: X✝ : Type u_1
Y✝ : Type u_2
inst✝³ : TopologicalSpace X✝
inst✝² : TopologicalSpace Y✝
f g : C(X✝, Y✝)
X : Type u_3
Y : Type u_4
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hequiv : X ≃ₕ Y
⊢ ↑(π.obj (TopCat.of X)) ≌ ↑(π.obj (TopCat.of Y))

Tactic:
apply CategoryTheory.Equivalence.mk (map hequiv.toFun) (map hequiv.invFun)
  · simpa only [FundamentalGroupoid.map_id, FundamentalGroupoid.map_comp]
      using (asIso (homotopicMapsNatIso hequiv.left_inv.some)).symm
  · simpa only [FundamentalGroupoid.map_id, FundamentalGroupoid.map_comp]
      using asIso (homotopicMapsNatIso hequiv.right_inv.some)

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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f g : X ⟶ Y
h✝ : homRel C f g
P : PathObject Y.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject C ⥤ (weakEquivalences (CofibrantObject C)).Localization := (weakEquivalences (CofibrantObject C)).Q
⊢ AreEqualizedByLocalization (weakEquivalences (CofibrantObject C)) f g

Tactic:
rw [areEqualizedByLocalization_iff L]

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
X Y : CofibrantObject C
f g : X ⟶ Y
h✝ : homRel C f g
P : PathObject Y.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
L : CofibrantObject C ⥤ (weakEquivalences (CofibrantObject C)).Localization := (weakEquivalences (CofibrantObject C)).Q
⊢ L.map f = L.map g
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: 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 : (weakEquivalences (BifibrantObject C)).IsInvertedBy F
K L : BifibrantObject C
f g : K ⟶ L
h✝ : homRel C f g
P : PathObject L.obj
left✝ : P.IsVeryGood
h : P.RightHomotopy f.hom g.hom
this : IsCofibrant P.P
⊢ weakEquivalences (BifibrantObject C) (homMk P.ι)

Tactic:
rw [← weakEquivalence_iff, weakEquivalence_iff_of_objectProperty]
      exact inferInstanceAs (WeakEquivalence P.ι)

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ (weakEquivalences (Over S)).IsStableUnderRetracts

Tactic:
rw [weakEquivalences_over_def, MorphismProperty.over_eq_inverseImage]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ ((weakEquivalences C).inverseImage (Over.forget S)).IsStableUnderRetracts
Module: Mathlib.AlgebraicTopology.ModelCategory.Over

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).HasTwoOutOfThreeProperty
⊢ (weakEquivalences (Over S)).HasTwoOutOfThreeProperty

Tactic:
rw [weakEquivalences_over_def, MorphismProperty.over_eq_inverseImage]

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithWeakEquivalences C
inst✝ : (weakEquivalences C).HasTwoOutOfThreeProperty
⊢ ((weakEquivalences C).inverseImage (Over.forget S)).HasTwoOutOfThreeProperty
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: case neg.inl
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 Finset.univ ≤ Λ[n + 1, i]

Tactic:
exact (h (le_trans (by simp) hx)).elim

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), stdSimplex.δ j ≫ φ = f j hj

Tactic:
obtain ⟨φ, hφ, _⟩ := hf.exists_lift (terminal.from _) (terminal.from _) (by simp)

Goal state after:
X : SSet
n : ℕ
i : Fin (n + 2)
f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ X)
inst✝ : X.KanComplex
hf : horn.IsCompatible f
φ : Δ[n + 1] ⟶ X
hφ : ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
right✝ : φ ≫ terminal.from X = terminal.from Δ[n + 1]
⊢ ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
⊢ sy.spineToSimplex (f.map σ) = (ConcreteCategory.hom (σ.app (Opposite.op ⦋n + 1⦌))) (sx.spineToSimplex f)

Tactic:
apply sy.spineInjective

Goal state after:
X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
⊢ (sy.spineEquiv (n + 1)) (sy.spineToSimplex (f.map σ)) =
    (sy.spineEquiv (n + 1)) ((ConcreteCategory.hom (σ.app (Opposite.op ⦋n + 1⦌))) (sx.spineToSimplex f))
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ CatEnriched.hComp (eqToHom ⋯) (eqToHom ⋯) ≫
      CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ ≫ 𝟙 (homEquiv h')) ≍
    CatEnriched.hComp (𝟙 (homEquiv f) ≫ Hom.base η ≫ 𝟙 (homEquiv f'))
      (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
CatEnriched.eqToHom_hComp_eqToHom

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ eqToHom ⋯ ≫
      CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ ≫ 𝟙 (homEquiv h')) ≍
    CatEnriched.hComp (𝟙 (homEquiv f) ≫ Hom.base η ≫ 𝟙 (homEquiv f'))
      (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ eqToHom ⋯ ≫
      CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫
        CatEnriched.hComp (eqToHom ⋯) (eqToHom ⋯) ≍
    CatEnriched.hComp (𝟙 (homEquiv f) ≫ Hom.base η ≫ 𝟙 (homEquiv f'))
      (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
CatEnriched.eqToHom_hComp_eqToHom

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫ eqToHom ⋯ ≍
    CatEnriched.hComp (𝟙 (homEquiv f) ≫ Hom.base η ≫ 𝟙 (homEquiv f'))
      (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫ eqToHom ⋯ ≍
    CatEnriched.hComp (eqToHom ⋯) (eqToHom ⋯) ≫
      CatEnriched.hComp (Hom.base η ≫ 𝟙 (homEquiv f')) (CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
CatEnriched.eqToHom_hComp_eqToHom

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫ eqToHom ⋯ ≍
    eqToHom ⋯ ≫
      CatEnriched.hComp (Hom.base η ≫ 𝟙 (homEquiv f')) (CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫ eqToHom ⋯ ≍
    eqToHom ⋯ ≫
      CatEnriched.hComp (Hom.base η) (CatEnriched.hComp (Hom.base θ) (Hom.base κ)) ≫
        CatEnriched.hComp (eqToHom ⋯) (eqToHom ⋯)

Tactic:
CatEnriched.eqToHom_hComp_eqToHom

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
⊢ eqToHom ⋯ ≫ CatEnriched.hComp (CatEnriched.hComp (Hom.base η) (Hom.base θ)) (Hom.base κ) ≫ eqToHom ⋯ ≍
    eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (CatEnriched.hComp (Hom.base θ) (Hom.base κ)) ≫ eqToHom ⋯
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V W : Truncated 2
f : V ⟶ W
⊢ ∀ (x y : Cat.FreeRefl (OneTruncation₂ V)) (f₁ f₂ : x ⟶ y),
    OneTruncation₂.HoRel₂ V f₁ f₂ →
      (((oneTruncation₂ ⋙ Cat.freeRefl).map f).toFunctor ⋙ quotientFunctor W).map f₁ =
        (((oneTruncation₂ ⋙ Cat.freeRefl).map f).toFunctor ⋙ quotientFunctor W).map f₂

Tactic:
rintro _ _ _ _ ⟨h⟩
      exact CategoryTheory.Quotient.sound _ ⟨h.map f⟩

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

Goal state before:
pp: ⊢ default ⟶ default

Tactic:
exact 𝟙rq instUniqueOneTruncation₂DeltaZero.default

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

Goal state before:
pp: x y : SimplexCategoryGenRel
n✝ : ℕ
z : SimplexCategoryGenRel
e : mk n✝ ⟶ z
he : P_σ e
n : ℕ
j : Fin (n + 1 + 1)
X Y : SimplexCategoryGenRel
i : Fin (n + 1 + 2)
f : z ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
j' : Fin (n + 1)
j'' : Fin (n + 2)
h' : δ i ≫ σ j = σ j' ≫ δ j''
w✝¹ : SimplexCategoryGenRel
w✝ : z ⟶ w✝¹
m₁ : w✝¹ ⟶ mk n
he₁ : P_σ w✝
hm₁ : P_δ m₁
h₁ : f ≫ σ j' = w✝ ≫ m₁
⊢ (e ≫ f ≫ δ i) ≫ σ j = (e ≫ w✝) ≫ m₁ ≫ δ j''

Tactic:
simp [← reassoc_of% h₁, h']

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

Goal state before:
pp: x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i j : Fin (x₁.len + 1 + (x₂.len + 1))
h : i ≤ j
⊢ (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      i ≤
    (fun i ↦
        Fin.addCases (fun i ↦ Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom f₁) i))
          (fun i ↦ Fin.natAdd (y₁.len + 1) ((SimplexCategory.Hom.toOrderHom f₂) i)) i)
      j

Tactic:
by
        cases i using Fin.addCases <;>
        cases j using Fin.addCases <;>
        rw [Fin.le_def] at h ⊢ <;>
        simp at h ⊢ <;>
        grind only [OrderHom.apply_mono]

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

Goal state before:
pp: x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
⊢ inl (WithInitial.of x₁) (WithInitial.of x₂) ≫ (f₁ ⊗ₘ f₂) = f₁ ≫ inl (WithInitial.of y₁) (WithInitial.of y₂)

Tactic:
change inl' _ _ ≫ tensorHomOf _ _ = WithInitial.down f₁ ≫ inl' _ _

Goal state after:
x₁✝ y₁✝ x₂✝ y₂✝ : AugmentedSimplexCategory
f₁✝ : x₁✝ ⟶ y₁✝
f₂✝ : x₂✝ ⟶ y₂✝
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : WithInitial.of x₁ ⟶ WithInitial.of y₁
f₂ : WithInitial.of x₂ ⟶ WithInitial.of y₂
⊢ inl' x₁ x₂ ≫ tensorHomOf f₁ f₂ = WithInitial.down f₁ ≫ inl' y₁ y₂
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : i.castSucc < j
⊢ i.predAbove j < x

pp: case neg
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : j ≤ i.castSucc
⊢ i.predAbove j < x

Tactic:
· rwa [Fin.predAbove_of_castSucc_lt _ _ h, ← Fin.succ_lt_succ_iff,
            Fin.succ_pred]

Goal state after:
case neg
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : j ≤ i.castSucc
⊢ i.predAbove j < x
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ (II.δ i).unop = (σ i).op.unop

Tactic:
by ext : 3; apply II.map'_succAboveOrderEmb

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.PairingCore
inst✝ : P.IsProper
⊢ P.IsRegular ↔ Nonempty (P.RankFunction ℕ)

Tactic:
by
  rw [← isRegular_pairing_iff, Pairing.isRegular_iff_nonempty_rankFunction]
  exact (P.rankFunctionEquiv ℕ).symm.nonempty_congr

Goal state after:
Module: Mathlib.CategoryTheory.Presentable.Retracts

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
X Y : C
h : Retract Y X
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
inst✝ : IsCardinalPresentable X κ
J : Type w
x✝¹ : SmallCategory J
x✝ : IsCardinalFiltered J κ
F : J ⥤ C
c : Cocone F
hc : IsColimit c
this✝ : EssentiallySmall.{w, w, w} J
this : IsFiltered J
j : J
f₁ f₂ : (fun X ↦ X) ((F ⋙ coyoneda.obj (Opposite.op Y)).obj j)
hf :
  (ConcreteCategory.hom (((coyoneda.obj (Opposite.op Y)).mapCocone c).ι.app j)) f₁ =
    (ConcreteCategory.hom (((coyoneda.obj (Opposite.op Y)).mapCocone c).ι.app j)) f₂
⊢ ∃ k f,
    (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op Y)).map f)) f₁ =
      (ConcreteCategory.hom ((F ⋙ coyoneda.obj (Opposite.op Y)).map f)) f₂

Tactic:
· dsimp at f₁ f₂ hf ⊢
      obtain ⟨k, u, hj⟩ := IsCardinalPresentable.exists_eq_of_isColimit'
        κ hc (h.r ≫ f₁) (h.r ≫ f₂) (by simp [hf])
      exact ⟨k, u, by simpa [← cancel_epi h.r] using hj⟩

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
⊢ c.horn ≤ (f.filtration j).preimage c.map

Tactic:
← Subcomplex.image_le_iff,

Goal state after:
case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
⊢ c.horn.image c.map ≤ f.filtration j
Module: Mathlib.CategoryTheory.ExtremalEpi

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasEqualizers C
hf : ∀ ⦃Z : C⦄ (p : X ⟶ Z) (i : Z ⟶ Y), p ≫ i = f → ∀ [Mono i], IsIso i
Z : C
p q : Y ⟶ Z
h : f ≫ p = f ≫ q
this : IsIso (equalizer.ι p q)
⊢ equalizer.ι p q ≫ p = equalizer.ι p q ≫ q

Tactic:
equalizer.condition

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasEqualizers C
hf : ∀ ⦃Z : C⦄ (p : X ⟶ Z) (i : Z ⟶ Y), p ≫ i = f → ∀ [Mono i], IsIso i
Z : C
p q : Y ⟶ Z
h : f ≫ p = f ≫ q
this : IsIso (equalizer.ι p q)
⊢ equalizer.ι p q ≫ q = equalizer.ι p q ≫ q
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
⊢ range (c.horn.ι ≫ c.map) ≤ f.filtration j

Tactic:
by
    simp [← image_top, image_le_iff, preimage_comp, c.preimage_filtration_map]

Goal state after:
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: κ : Cardinal.{w}
C : Type u
inst✝ : Category.{v, u} C
hC : HasCardinalLT (Arrow C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
f₁ : C ↪ Ω := ⋯.some
f₂ : (X Y : C) → (X ⟶ Y) ↪ Ω := fun X Y ↦ ⋯.some
e : C ≃ ↑(Set.range ⇑f₁) := Equiv.ofInjective ⇑f₁ ⋯
h : CoreSmallCategoryOfSet Ω C :=
  { obj := Set.range ⇑f₁, hom := fun X Y ↦ Set.range ⇑(f₂ (e.symm X) (e.symm Y)), objEquiv := e.symm,
    homEquiv := fun {x x_1} ↦ (Equiv.ofInjective ⇑(f₂ (e.symm x) (e.symm x_1)) ⋯).symm }
⊢ ∃ S, Nonempty (categoryFamily κ S ≌ C)

Tactic:
refine ⟨⟨h.smallCategoryOfSet, ?_⟩, ⟨h.equivalence⟩⟩

Goal state after:
κ : Cardinal.{w}
C : Type u
inst✝ : Category.{v, u} C
hC : HasCardinalLT (Arrow C) κ
Ω : Type w := κ.ord.ToType
ι : Arrow C ↪ Ω
h₁ : Cardinal.lift.{w, u} (Cardinal.mk C) ≤ Cardinal.lift.{u, w} (Cardinal.mk Ω)
h₂ : ∀ (X Y : C), Cardinal.lift.{w, v} (Cardinal.mk (X ⟶ Y)) ≤ Cardinal.lift.{v, w} (Cardinal.mk Ω)
f₁ : C ↪ Ω := ⋯.some
f₂ : (X Y : C) → (X ⟶ Y) ↪ Ω := fun X Y ↦ ⋯.some
e : C ≃ ↑(Set.range ⇑f₁) := Equiv.ofInjective ⇑f₁ ⋯
h : CoreSmallCategoryOfSet Ω C :=
  { obj := Set.range ⇑f₁, hom := fun X Y ↦ Set.range ⇑(f₂ (e.symm X) (e.symm Y)), objEquiv := e.symm,
    homEquiv := fun {x x_1} ↦ (Equiv.ofInjective ⇑(f₂ (e.symm x) (e.symm x_1)) ⋯).symm }
⊢ HasCardinalLT (Arrow ↑h.smallCategoryOfSet.obj) κ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ f.mapN (Cell.type₁ f c) = { dim := (↑(P.p c.s)).dim, simplex := (↑(P.p c.s)).simplex }

Tactic:
dsimp only [Cell.type₁, mapN]
  rw [← S.cast_eq_self _ (P.dim_p c.s)]
  dsimp
  rw [S.ext_iff, c.ι_b_app_apply]
  apply yonedaEquiv_symm_app_id

Goal state after:
Module: Mathlib.CategoryTheory.Functor.KanExtension.Dense

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝³ : Category.{v₁, u₁} C
inst✝² : Category.{v₂, u₂} D
C' : Type u₃
inst✝¹ : Category.{v₃, u₃} C'
F : C ⥤ D
inst✝ : F.IsDense
Y Z : D
f : (restrictedULiftYoneda F).obj Y ⟶ (restrictedULiftYoneda F).obj Z
⊢ ∃ a, (restrictedULiftYoneda F).map a = f

Tactic:
let c : Cocone (CostructuredArrow.proj F Y ⋙ F) :=
      { pt := Z
        ι :=
          { app g := ((f.app (op g.left)) (ULift.up g.hom)).down
            naturality g₁ g₂ φ := by
              simpa [uliftFunctor, uliftYoneda,
                restrictedULiftYoneda, ← ULift.down_inj] using
                ((f.naturality_apply φ.left.op) (ULift.up g₂.hom)).symm } }
    refine ⟨(F.denseAt Y).desc c, ?_⟩
    ext ⟨X⟩ ⟨x⟩
    have := (F.denseAt Y).fac c (.mk x)
    dsimp [c] at this
    simpa using ULift.down_injective this

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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
⊢ IsFinitelyPresentable X

Tactic:
by
  obtain ⟨Y, _, _, p, _⟩ := exists_epi_from_isCardinalPresentable X
  obtain ⟨Z, _, _, q, _⟩ := exists_epi_from_isCardinalPresentable (pullback p p)
  have := Cardinal.fact_isRegular_aleph0.{u}
  have := IsRegularEpiCategory.regularEpiOfEpi p
  apply +allowSynthFailures isCardinalPresentable_of_isColimit' _
      (isCoequalizerEpiComp ((EffectiveEpi.getStruct p).isColimitCoforkOfIsPullback
        (IsPullback.of_hasPullback p p)) q) _
  · exact hasCardinalLT_of_finite _ _ (by rfl)
  · rintro (_ | _) <;> dsimp <;> infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
⊢ modelCategoryQuillen.J.rlp.llp Λ[n, i].ι

Tactic:
exact le_llp_rlp _ _ (modelCategoryQuillen.horn_ι_mem_J n i)

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case refine_2
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d + 1
l : Fin (d + 1)
hl : IsIndex x hd l.succ
y : Fin (d + 1)
hy : y ∈ finset hl.δ ⋯
⊢ l ≤ y

Tactic:
· simp only [mem_finset_iff, Monoidal.tensorObj_obj, S.cast_dim,
      S.cast_simplex_rfl, prod_δ_fst, stdSimplex.δ_apply] at hy
    by_contra!
    rw [Fin.succAbove_of_castSucc_lt _ _ (by grind)] at hy
    grind [(hl.succ_le_simplex_fst_iff y.castSucc).1 hy.symm.le]

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj

Goal state before:
pp: C₁ : Type u₁
C₂ : Type u₂
C₃ : Type u₃
inst✝⁴ : Category.{v₁, u₁} C₁
inst✝³ : Category.{v₂, u₂} C₂
inst✝² : Category.{v₃, u₃} C₃
F : C₁ ⥤ C₂ ⥤ C₃
G : C₁ᵒᵖ ⥤ C₃ ⥤ C₂
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
sq : F.PushoutObjObj f₁ f₂
inst✝¹ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj X₂)
inst✝ : PreservesColimitsOfShape (Discrete PEmpty.{1}) (F.flip.obj Y₂)
h : IsInitial X₁
⊢ IsPushout ((F.map f₁).app X₂) ((F.obj X₁).map f₂) (𝟙 ((F.obj Y₁).obj X₂))
    ((IsInitial.isInitialObj (F.flip.obj Y₂) X₁ h).to ((F.obj Y₁).obj X₂))

Tactic:
by
    let hX₂ := IsInitial.isInitialObj (F.flip.obj X₂) _ h
    let hY₂ := IsInitial.isInitialObj (F.flip.obj Y₂) _ h
    apply +allowSynthFailures IsPushout.of_vert_isIso
    · exact isIso_of_isInitial hX₂ hY₂ _
    · exact ⟨hX₂.hom_ext _ _⟩

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

Goal state before:
pp: case refine_2
X : SSet
x✝¹ : SimplexCategoryᵒᵖ
n : ℕ
x✝ : SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌)
m : ℕ
f : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)
property✝ : Epi f
x y :
  SimplicialObject.Splitting.summand (fun n ↦ ↑(X.nonDegenerate n)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋m⦌, ⟨f, property✝⟩⟩
h :
  (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋m⦌, ⟨f, property✝⟩⟩ x =
    (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋m⦌, ⟨f, property✝⟩⟩ y
⊢ x = y

pp: case refine_3
X : SSet
x✝² : SimplexCategoryᵒᵖ
n : ℕ
x✝¹ x✝ : SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌)
m : ℕ
f : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)
property✝¹ : Epi f
x :
  SimplicialObject.Splitting.summand (fun n ↦ ↑(X.nonDegenerate n)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩
p : ℕ
g : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋p⦌)
property✝ : Epi g
y :
  SimplicialObject.Splitting.summand (fun n ↦ ↑(X.nonDegenerate n)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋p⦌, ⟨g, property✝⟩⟩
h :
  (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩ x =
    (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋p⦌, ⟨g, property✝⟩⟩ y
⊢ ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩ = ⟨Opposite.op ⦋p⦌, ⟨g, property✝⟩⟩

Tactic:
· exact unique_nonDegenerate_simplex _ _ _ _ rfl _ _ h

Goal state after:
case refine_3
X : SSet
x✝² : SimplexCategoryᵒᵖ
n : ℕ
x✝¹ x✝ : SimplicialObject.Splitting.IndexSet (Opposite.op ⦋n⦌)
m : ℕ
f : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋m⦌)
property✝¹ : Epi f
x :
  SimplicialObject.Splitting.summand (fun n ↦ ↑(X.nonDegenerate n)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩
p : ℕ
g : Opposite.unop (Opposite.op ⦋n⦌) ⟶ Opposite.unop (Opposite.op ⦋p⦌)
property✝ : Epi g
y :
  SimplicialObject.Splitting.summand (fun n ↦ ↑(X.nonDegenerate n)) (Opposite.op ⦋n⦌) ⟨Opposite.op ⦋p⦌, ⟨g, property✝⟩⟩
h :
  (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩ x =
    (SimplicialObject.Splitting.cofan' (fun n ↦ ↑(X.nonDegenerate n)) X (fun n ↦ ↾Subtype.val)
            (Opposite.op ⦋n⦌)).cofanTypes.inj
      ⟨Opposite.op ⦋p⦌, ⟨g, property✝⟩⟩ y
⊢ ⟨Opposite.op ⦋m⦌, ⟨f, property✝¹⟩⟩ = ⟨Opposite.op ⦋p⦌, ⟨g, property✝⟩⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: m✝ : ℕ
k✝ : Fin (m✝ + 1)
n✝ : ℕ
x✝ : (Λ[m✝ + 1, k✝.castSucc].unionProd ∂Δ[n✝]).N
d m : ℕ
k : Fin m
n : ℕ
x : (pairingCore k.succ n).ι
⊢ (pairingCore k.succ n).index x ≠ Fin.last ((pairingCore k.succ n).dim x + 1)

Tactic:
dsimp [pairingCore]
    simp

Goal state after: