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

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
⊢ (localizerMorphism C).IsLocalizedEquivalence

Tactic:
let Hcof := (weakEquivalences (HoCat C)).Localization
  let Lcofπ : HoCat C ⥤ Hcof := (weakEquivalences (CofibrantObject.HoCat C)).Q
  let Lcof : CofibrantObject C ⥤ Hcof := toHoCat ⋙ Lcofπ
  let H := (weakEquivalences C).Localization
  let L : C ⥤ H := (weakEquivalences C).Q
  let F := (localizerMorphism C).localizedFunctor Lcof L
  let eF : ι ⋙ L ≅ Lcof ⋙ F := CatCommSq.iso (localizerMorphism C).functor Lcof L F
  let eF' : HoCat.toLocalization L ≅ Lcofπ ⋙ F :=
    CategoryTheory.Quotient.natIsoLift _
      (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ associator _ _ _)
  let G : H ⥤ Hcof := (HoCat.localizerMorphismResolution C).localizedFunctor L Lcofπ
  let eG : HoCat.resolution ⋙ Lcofπ ≅ L ⋙ G :=
    CatCommSq.iso (HoCat.localizerMorphismResolution C).functor L Lcofπ G
  have : Localization.Lifting L (weakEquivalences C)
      (HoCat.resolution ⋙ HoCat.toLocalization L) (G ⋙ F) :=
    ⟨(associator _ _ _).symm ≪≫ isoWhiskerRight eG.symm _ ≪≫
      associator _ _ _ ≪≫ isoWhiskerLeft _ eF'.symm⟩
  have : Localization.Lifting Lcof (weakEquivalences (CofibrantObject C))
        (ι ⋙ HoCat.resolution ⋙ Lcofπ) (F ⋙ G) :=
    ⟨(associator _ _ _).symm ≪≫ isoWhiskerRight eF.symm G ≪≫
      associator _ _ _ ≪≫ isoWhiskerLeft _ eG.symm⟩
  let E : Hcof ≌ H := CategoryTheory.Equivalence.mk F G
    (Localization.liftNatIso Lcof (weakEquivalences _) Lcof (ι ⋙ HoCat.resolution ⋙ Lcofπ) _ _
      ((asIso (whiskerRight HoCat.ιCompResolutionNatTrans Lcofπ)).symm ≪≫
          associator _ _ _))
    (Localization.liftNatIso L (weakEquivalences _)
      (HoCat.resolution ⋙ HoCat.toLocalization L) L _ _
      (asIso (HoCat.resolutionCompToLocalizationNatTrans L)))
  have : F.IsEquivalence := E.isEquivalence_functor
  exact LocalizerMorphism.IsLocalizedEquivalence.mk' (localizerMorphism C) Lcof L F

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
S : C
inst✝¹ : CategoryWithFibrations C
X Y : Over S
f : X ⟶ Y
inst✝ : Fibration f
⊢ Fibration (Over.Hom.left f)

Tactic:
by
  rwa [← fibrations_over_iff]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
⊢ stdSimplex.objEquiv.symm f ∈ Λ[n, i].obj (op ⦋m⦌) ↔ stdSimplex.objEquiv.symm f ∈ Set.univ

Tactic:
obtain ⟨j, hij, hj⟩ : ∃ (j : Fin (n + 1)), j ≠ i ∧ j ∉ Set.range f.toOrderHom := by
    by_contra!
    have : Finset.image f.toOrderHom ⊤ ∪ {i} = ⊤ := by ext k; by_cases k = i <;> aesop
    have := (congr_arg Finset.card this).symm.le.trans (Finset.card_union_le _ _)
    simp only [SimplexCategory.len_mk, Finset.top_eq_univ, Finset.card_univ, Fintype.card_fin,
      Finset.card_singleton, add_le_add_iff_right] at this
    have : n ≤ m + 1 := by simpa using this.trans Finset.card_image_le
    lia

Goal state after:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
f : unop (op ⦋m⦌) ⟶ ⦋n⦌
j : Fin (n + 1)
hij : j ≠ i
hj : j ∉ Set.range ⇑(SimplexCategory.Hom.toOrderHom f)
⊢ stdSimplex.objEquiv.symm f ∈ Λ[n, i].obj (op ⦋m⦌) ↔ stdSimplex.objEquiv.symm f ∈ Set.univ
Module: Mathlib.AlgebraicTopology.SimplicialSet.SubcomplexColimits

Goal state before:
pp: X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
n : SimplexCategoryᵒᵖ
⊢ IsColimit
    (((evaluation SimplexCategoryᵒᵖ (Type u)).obj n).mapCocone
      ((CompleteLattice.MulticoequalizerDiagram.multicofork h).map toSSetFunctor))

Tactic:
have h' : CompleteLattice.MulticoequalizerDiagram (A.obj n) (fun i ↦ (U i).obj n)
        (fun i j ↦ (V i j).obj n) :=
      { eq_inf := by simp [h.eq_inf]
        iSup_eq := by simp [← h.iSup_eq] }

Goal state after:
X : SSet
A : X.Subcomplex
ι : Type u_1
U : ι → X.Subcomplex
V : ι → ι → X.Subcomplex
h : A.MulticoequalizerDiagram U V
n : SimplexCategoryᵒᵖ
h' : CompleteLattice.MulticoequalizerDiagram (A.obj n) (fun i ↦ (U i).obj n) fun i j ↦ (V i j).obj n
⊢ IsColimit
    (((evaluation SimplexCategoryᵒᵖ (Type u)).obj n).mapCocone
      ((CompleteLattice.MulticoequalizerDiagram.multicofork h).map toSSetFunctor))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
⊢ stdSimplex.face {i}ᶜ ≤ Λ[n + 1, j] ↔ ¬i = j

Tactic:
face_le_horn_iff

Goal state after:
n : ℕ
i j : Fin (n + 2)
⊢ {i}ᶜ ≠ Finset.univ ∧ {i}ᶜ ≠ {j}ᶜ ↔ ¬i = j
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

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:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Subcomplex.ofSimplex (yonedaEquiv (stdSimplex.map (SimplexCategory.δ i))) ≤
    Subcomplex.ofSimplex (stdSimplex.objEquiv.symm (SimplexCategory.δ i))

Tactic:
yonedaEquiv_map

Goal state after:
n : ℕ
i : Fin (n + 2)
⊢ Subcomplex.ofSimplex (stdSimplex.objEquiv.symm (SimplexCategory.δ i)) ≤
    Subcomplex.ofSimplex (stdSimplex.objEquiv.symm (SimplexCategory.δ i))
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
X Y : SSet
f : X ⟶ Y
inst✝ : IsIso f
⊢ Fibration f

Tactic:
rw [fibration_iff]

Goal state after:
X✝ Y✝ : SSet
f✝ : X✝ ⟶ Y✝
X Y : SSet
f : X ⟶ Y
inst✝ : IsIso f
⊢ J.rlp f
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
⊢ Mono (inr f g)

Tactic:
mono_iff_injective

Goal state after:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
⊢ Function.Injective ⇑(ConcreteCategory.hom (inr f g))
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
h0 : 0 < i
hn : i < Fin.last n
⊢ innerHornInclusions Λ[n, i].ι

Tactic:
obtain _ | _ | k := n

Goal state after:
case zero
i : Fin (0 + 1)
h0 : 0 < i
hn : i < Fin.last 0
⊢ innerHornInclusions Λ[0, i].ι

case succ.zero
i : Fin (0 + 1 + 1)
h0 : 0 < i
hn : i < Fin.last (0 + 1)
⊢ innerHornInclusions Λ[0 + 1, i].ι

case succ.succ
k : ℕ
i : Fin (k + 1 + 1 + 1)
h0 : 0 < i
hn : i < Fin.last (k + 1 + 1)
⊢ innerHornInclusions Λ[k + 1 + 1, i].ι
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Mono (r ≫ k)
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
⊢ Mono k

Tactic:
mono_iff_injective

Goal state after:
X₁ X₂ X₃ X₄ X₅ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
k : X₄ ⟶ X₅
h₁ : IsPushout t l r b
hr' : Function.Injective ⇑(ConcreteCategory.hom (r ≫ k))
H :
  ∀ (x₃ y₃ : X₃),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom l) →
        (ConcreteCategory.hom (b ≫ k)) x₃ = (ConcreteCategory.hom (b ≫ k)) y₃ → x₃ = y₃
h₂ : IsPullback t l (r ≫ k) (b ≫ k)
this : Function.Injective ⇑(ConcreteCategory.hom l)
⊢ Function.Injective ⇑(ConcreteCategory.hom k)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n✝ n : ℕ
hn : ∀ (s : X _⦋n⦌), spineToSimplex h (X.spine n s) = s
s : X _⦋n + 1⦌
⊢ spineToSimplex h ((X.spine (n + 1) s).interval 1 n ⋯) =
    spineToSimplex h (X.spine n ((ConcreteCategory.hom (SimplicialObject.δ X 0)) s))

Tactic:
spine_δ₀

Goal state after:
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n✝ n : ℕ
hn : ∀ (s : X _⦋n⦌), spineToSimplex h (X.spine n s) = s
s : X _⦋n + 1⦌
⊢ spineToSimplex h ((X.spine (n + 1) s).interval 1 n ⋯) = spineToSimplex h ((X.spine (n + 1) s).interval 1 n ⋯)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case succ.comp_of.inr.inl
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
h'' : δ k ≫ σ i = 𝟙 (mk (n + 1))
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

pp: case succ.comp_of.inr.inr
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
j : Fin (n + 1)
j' : Fin (n + 2)
h'' : δ k ≫ σ i = σ j ≫ δ j'
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m

Tactic:
· exact ⟨_, _, _, P_σ.id_mem _, hf, by simp [h'']⟩

Goal state after:
case succ.comp_of.inr.inr
n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
j : Fin (n + 1)
j' : Fin (n + 2)
h'' : δ k ≫ σ i = σ j ≫ δ j'
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), (f ≫ δ k) ≫ σ i = e ≫ m
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y₀ y₁ : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge y₀ y₁
⊢ ((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x)).map (homMk e) ≫
      (Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x)).obj (mk y₁))).hom =
    (Iso.refl (((Functor.curry.obj (inverse X Y ⋙ mapHomotopyCategory (fst X Y))).obj (mk x)).obj (mk y₀))).hom ≫
      ((Functor.curry.obj (CategoryTheory.Prod.fst X.HomotopyCategory Y.HomotopyCategory)).obj (mk x)).map (homMk e)

Tactic:
dsimp
      rw [Category.comp_id]
      exact homMk_id x

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
hx : map' g x.castSucc = Fin.last (m + 1)
⊢ map' f (map' g x.castSucc) = map' (g.comp f) x.castSucc

Tactic:
rw [Eq.comm, hx, map'_last]
      rw [map'_eq_last_iff] at hx ⊢
      intro i
      apply hx

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
x✝ : { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
g : ℕ → ↑P.II
hg : ∀ (n : ℕ), P.AncestralRel (g (n + 1)) (g n)
n₀ : ℕ
hn₀ : ∀ (m : ℕ), n₀ ≤ m → (↑(g n₀)).dim = (↑(g m)).dim
n : ℕ
⊢ (↑(g (n₀ + n + 1))).dim = (↑(g (n₀ + n))).dim

Tactic:
← hn₀ (n₀ + n + 1) (by lia),

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
x✝ : { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
g : ℕ → ↑P.II
hg : ∀ (n : ℕ), P.AncestralRel (g (n + 1)) (g n)
n₀ : ℕ
hn₀ : ∀ (m : ℕ), n₀ ≤ m → (↑(g n₀)).dim = (↑(g m)).dim
n : ℕ
⊢ (↑(g n₀)).dim = (↑(g (n₀ + n))).dim
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
H : ∀ (k : K), ∃ j y_1, (ConcreteCategory.hom (((F.obj k).mapCocone cX).ι.app j)) y_1 = ↑y k
j : K → J := fun k ↦ ⋯.choose
⊢ ∃ j₀ z, ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)

Tactic:
let z (k : K) : (F.obj k).obj (X.obj (j k)) := (H k).choose_spec.choose

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
K : Type u'
inst✝³ : Category.{v', u'} K
F : K ⥤ C ⥤ Type w'
c : Cone F
hc : (Y : C) → IsLimit (((evaluation C (Type w')).obj Y).mapCone c)
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
hK : HasCardinalLT (Arrow K) κ
J : Type w
inst✝¹ : SmallCategory J
inst✝ : IsCardinalFiltered J κ
X : J ⥤ C
cX : Cocone X
hF : (k : K) → IsColimit ((F.obj k).mapCocone cX)
x : c.pt.obj cX.pt
this : IsFiltered J
y : ↑(F ⋙ (evaluation C (Type w')).obj cX.pt).sections
hy : (Types.isLimitEquivSections (hc cX.pt)).symm y = x
H : ∀ (k : K), ∃ j y_1, (ConcreteCategory.hom (((F.obj k).mapCocone cX).ι.app j)) y_1 = ↑y k
j : K → J := fun k ↦ ⋯.choose
z : (k : K) → (F.obj k).obj (X.obj (j k)) := fun k ↦ ⋯.choose
⊢ ∃ j₀ z, ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
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
d : ℕ
⊢ Mono (c.ιSigmaStdSimplex.app (op ⦋d⦌))

Tactic:
mono_iff_injective

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
d : ℕ
⊢ Function.Injective ⇑(ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋d⦌)))
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case a.notMem.refine_2.refine_2
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : A.N
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
hs : (↑t).subcomplex ≤ c.horn.image c.map
⊢ (↑t).subcomplex < (↑(P.p c.s)).subcomplex

Tactic:
exact lt_of_le_of_lt hs (c.image_horn_lt_subcomplex)

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

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
A : Type u'
inst✝⁴ : Category.{v', u'} A
inst✝³ : HasColimitsOfSize.{w, w, v', u'} A
inst✝² : HasCoproducts A
κ : Cardinal.{w}
inst✝¹ : Fact κ.IsRegular
X : C
M : A
inst✝ : IsCardinalPresentable M κ
⊢ IsCardinalPresentable (freeYoneda X M) κ

Tactic:
by
  let e : coyoneda.obj (op (freeYoneda X M)) ≅
      (evaluation Cᵒᵖ A).obj (op X) ⋙ coyoneda.obj (op M) ⋙ uliftFunctor.{u} :=
    NatIso.ofComponents (fun P ↦ Equiv.toIso (freeYonedaHomEquiv.trans Equiv.ulift.symm))
  constructor
  intro J _ _
  have := preservesColimitsOfShape_of_isCardinalPresentable M κ J
  exact preservesColimitsOfShape_of_natIso e.symm

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

Goal state before:
pp: case refine_1.hK
X : SSet
inst✝ : X.Finite
⊢ HasCardinalLT (Arrow (Discrete X.N)) Cardinal.aleph0

Tactic:
exact hasCardinalLT_of_finite _ _ (by rfl)

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

Goal state before:
pp: case hK
X : SSet
inst✝ : X.Finite
Y : SSet
w✝³ : Y.Finite
w✝² : IsFinitelyPresentable Y
p : Y ⟶ X
h✝¹ : Epi p
Z : SSet
w✝¹ : Z.Finite
w✝ : IsFinitelyPresentable Z
q : Z ⟶ pullback p p
h✝ : Epi q
this✝ : Fact Cardinal.aleph0.IsRegular
this : IsRegularEpi p
⊢ HasCardinalLT (Arrow WalkingParallelPair) Cardinal.aleph0

Tactic:
exact hasCardinalLT_of_finite _ _ (by rfl)

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

Goal state before:
pp: case refine_1.inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
d : ℕ
hd : x.dim = d
i : Fin (d + 1)
h✝ : k.succ ≤ (x.cast hd).simplex.1 i
h : k.succ < (x.cast hd).simplex.1 i
⊢ min x hd ≤ i

Tactic:
by_contra! h'
      have := stdSimplex.monotone_apply (x.cast hd).simplex.1 h'.le
      dsimp at this
      rw [simplex_fst_min, ← not_lt] at this
      tauto

Goal state after:
Module: Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction

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₂
adj₂ : F ⊣₂ G
X₁ Y₁ : C₁
f₁ : X₁ ⟶ Y₁
X₂ Y₂ : C₂
f₂ : X₂ ⟶ Y₂
X₃ Y₃ : C₃
f₃ : X₃ ⟶ Y₃
sq₁₂ : F.PushoutObjObj f₁ f₂
sq₁₃ : G.PullbackObjObj f₁ f₃
α : Arrow.mk sq₁₂.ι ⟶ Arrow.mk f₃
l : Arrow.LiftStruct α
this : sq₁₂.ι ≫ l.l = Arrow.Hom.left α
⊢ f₂ ≫ adj₂.homEquiv l.l = adj₂.homEquiv (sq₁₂.inl ≫ Arrow.Hom.left α)

Tactic:
simp only [← adj₂.homEquiv_naturality_two, ← this,
          sq₁₂.inl_ι_assoc]

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

Goal state before:
pp: X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : Fibration p
sq₁₃ : internalHom.PullbackObjObj i p
⊢ Fibration sq₁₃.π

Tactic:
rw [fibration_iff]

Goal state after:
X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : Fibration p
sq₁₃ : internalHom.PullbackObjObj i p
⊢ J.rlp sq₁₃.π
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
l : Fin u.dim
hl : IsIndex x hd l.succ.succ
hi : i < l.succ.castSucc
⊢ i = l.succ.castSucc ∨ i = l.succ.succ

Tactic:
refine (hu _ rfl l.succ ?_).elim

Goal state after:
case inl
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
l : Fin u.dim
hl : IsIndex x hd l.succ.succ
hi : i < l.succ.castSucc
⊢ IsIndex u ⋯ l.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case inr.inr.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
l : Fin u.dim
hl : IsIndex x hd l.castSucc.succ
hi✝ : l.castSucc.castSucc < i
hi : l.castSucc.succ < i
⊢ i = l.castSucc.castSucc ∨ i = l.castSucc.succ

Tactic:
refine (hu _ rfl l.succ ?_).elim

Goal state after:
case inr.inr.inr
m : ℕ
k : Fin (m + 1)
n : ℕ
x u : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
hu : IsType₂ u
hd : x.dim = u.dim + 1
i : Fin (u.dim + 2)
hu' : u.simplex = (ConcreteCategory.hom (SimplicialObject.δ (Δ[m + 1] ⊗ Δ[n]) i)) (x.cast hd).simplex
l : Fin u.dim
hl : IsIndex x hd l.castSucc.succ
hi✝ : l.castSucc.castSucc < i
hi : l.castSucc.succ < i
⊢ IsIndex u ⋯ l.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonempty

Goal state before:
pp: X : SSet
hX : IsEmpty (X _⦋0⦌)
⊢ IsInitial X

Tactic:
have (n : SimplexCategoryᵒᵖ) : IsEmpty (X.obj n) :=
    Function.isEmpty (X.map (⦋0⦌.const n.unop 0).op)

Goal state after:
X : SSet
hX : IsEmpty (X _⦋0⦌)
this : ∀ (n : SimplexCategoryᵒᵖ), IsEmpty (X.obj n)
⊢ IsInitial X
Module: Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f : RelativeMorphism A B φ
n : SimplexCategoryᵒᵖ
a : X.obj n
ha : a ∈ A.obj n
⊢ (ConcreteCategory.hom (f.map.app n)) a ∈ B.obj n

Tactic:
have := f.map_coe ⟨a, ha⟩

Goal state after:
X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
φ : A.toSSet ⟶ B.toSSet
f : RelativeMorphism A B φ
n : SimplexCategoryᵒᵖ
a : X.obj n
ha : a ∈ A.obj n
this : (ConcreteCategory.hom (f.map.app n)) ↑⟨a, ha⟩ = ↑((ConcreteCategory.hom (φ.app n)) ⟨a, ha⟩)
⊢ (ConcreteCategory.hom (f.map.app n)) a ∈ B.obj n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.Nondegenerate

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
x : X _⦋n⦌
⊢ (X.ιChainComplex x ≫ (X.toNormalizedChainComplex R).f n) ≫ (X.fromNormalizedChainComplex R).f n =
    X.ιChainComplex x ≫ PInfty.f n

Tactic:
rw [Category.assoc, toNormalizedChainComplex_f_fromNormalizedChainComplex_f]

Goal state after:
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 : ℕ
s : Type₁ k.succ n
h : (pairingCore k.succ n).index s = 0
⊢ False

Tactic:
by
    have : s.index = 0 := by rwa [← Fin.castSucc_eq_zero_iff]
    have hs : IsIndex s.x s.hd (Fin.succ 0) := by simpa [this] using s.isIndex
    obtain ⟨i, hi⟩ := mem_range_left s.x s.hd 0 (fun h ↦ by simp [Fin.ext_iff] at h)
    have := stdSimplex.monotone_apply (s.x.cast s.hd).simplex.1 i.zero_le
    have h₁ := hs.simplex_fst_castSucc
    dsimp only [Fin.castSucc_zero] at h₁
    simp [h₁, hi] at this

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

Goal state before:
pp: ⊢ (sSetTopAdj.homEquiv Δ[0] TopCat.I)
      (toTop.map (stdSimplex.δ 1) ≫
        (TopCat.isoOfHomeo (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom) =
    SSet.const (TopCat.toSSetObj₀Equiv.symm 0)

Tactic:
sSetTopAdj_homEquiv_stdSimplex_zero

Goal state after:
⊢ SSet.const
      (TopCat.toSSetObj₀Equiv.symm
        ((ConcreteCategory.hom
            (toTop.map (stdSimplex.δ 1) ≫
              (TopCat.isoOfHomeo
                  (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom))
          default)) =
    SSet.const (TopCat.toSSetObj₀Equiv.symm 0)
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ (sSetTopAdj.homEquiv Δ[0] TopCat.I)
      (toTop.map (stdSimplex.δ 0) ≫
        (TopCat.isoOfHomeo (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom) =
    SSet.const (TopCat.toSSetObj₀Equiv.symm 1)

Tactic:
sSetTopAdj_homEquiv_stdSimplex_zero

Goal state after:
⊢ SSet.const
      (TopCat.toSSetObj₀Equiv.symm
        ((ConcreteCategory.hom
            (toTop.map (stdSimplex.δ 0) ≫
              (TopCat.isoOfHomeo
                  (⦋1⦌.toTopHomeo.trans (stdSimplexHomeomorphUnitInterval.trans Homeomorph.ulift.symm))).hom))
          default)) =
    SSet.const (TopCat.toSSetObj₀Equiv.symm 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.TopAdj

Goal state before:
pp: ⊢ yonedaEquiv.symm ((ConcreteCategory.hom (toSSetObjI.app (op ⦋0⦌))) (const 1 1 (op ⦋0⦌))) =
    yonedaEquiv.symm (TopCat.toSSetObj₀Equiv.symm 1)

Tactic:
trans stdSimplex.δ 0 ≫ toSSetObjI

Goal state after:
⊢ yonedaEquiv.symm ((ConcreteCategory.hom (toSSetObjI.app (op ⦋0⦌))) (const 1 1 (op ⦋0⦌))) = stdSimplex.δ 0 ≫ toSSetObjI

⊢ stdSimplex.δ 0 ≫ toSSetObjI = yonedaEquiv.symm (TopCat.toSSetObj₀Equiv.symm 1)
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: 𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
n : ℕ
h : ¬∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = 0
m : ℕ := ⋯.choose
g : 𝕜 → E
hg : AnalyticAt 𝕜 g z₀
hg_ne : g z₀ ≠ 0
hm : ∀ᶠ (z : 𝕜) in 𝓝 z₀, f z = (z - z₀) ^ ⋯.choose • g z
hmn : n ≤ ⋯.choose
z : 𝕜
hz : f z = (z - z₀) ^ ⋯.choose • g z
⊢ f z = (z - z₀) ^ n • (z - z₀) ^ (m - n) • g z

Tactic:
rwa [← mul_smul, ← pow_add, Nat.add_sub_of_le hmn]

Goal state after: