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
Hcof : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lcofπ : HoCat C ⥤ Hcof := (weakEquivalences (HoCat C)).Q
Lcof : CofibrantObject C ⥤ Hcof := toHoCat ⋙ Lcofπ
H : Type u_1 := (weakEquivalences C).Localization
L : C ⥤ H := (weakEquivalences C).Q
F : Hcof ⥤ H := (localizerMorphism C).localizedFunctor Lcof L
eF : ι ⋙ L ≅ Lcof ⋙ F := CatCommSq.iso (localizerMorphism C).functor Lcof L F
eF' : HoCat.toLocalization L ≅ Lcofπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ toHoCat.associator Lcofπ F)
G : H ⥤ Hcof := (HoCat.localizerMorphismResolution C).localizedFunctor L Lcofπ
eG : HoCat.resolution ⋙ Lcofπ ≅ L ⋙ G := CatCommSq.iso (HoCat.localizerMorphismResolution C).functor L Lcofπ G
⊢ (localizerMorphism C).IsLocalizedEquivalence

Tactic:
have : Localization.Lifting L (weakEquivalences C)
      (HoCat.resolution ⋙ HoCat.toLocalization L) (G ⋙ F) :=
    ⟨(associator _ _ _).symm ≪≫ isoWhiskerRight eG.symm _ ≪≫
      associator _ _ _ ≪≫ isoWhiskerLeft _ eF'.symm⟩

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : ModelCategory C
Hcof : Type u_1 := (weakEquivalences (HoCat C)).Localization
Lcofπ : HoCat C ⥤ Hcof := (weakEquivalences (HoCat C)).Q
Lcof : CofibrantObject C ⥤ Hcof := toHoCat ⋙ Lcofπ
H : Type u_1 := (weakEquivalences C).Localization
L : C ⥤ H := (weakEquivalences C).Q
F : Hcof ⥤ H := (localizerMorphism C).localizedFunctor Lcof L
eF : ι ⋙ L ≅ Lcof ⋙ F := CatCommSq.iso (localizerMorphism C).functor Lcof L F
eF' : HoCat.toLocalization L ≅ Lcofπ ⋙ F :=
  Quotient.natIsoLift (homRel C) (HoCat.toHoCatCompToLocalizationIso L ≪≫ eF ≪≫ toHoCat.associator Lcofπ F)
G : H ⥤ Hcof := (HoCat.localizerMorphismResolution C).localizedFunctor L Lcofπ
eG : HoCat.resolution ⋙ Lcofπ ≅ L ⋙ G := CatCommSq.iso (HoCat.localizerMorphismResolution C).functor L Lcofπ G
this : Localization.Lifting L (weakEquivalences C) (HoCat.resolution ⋙ HoCat.toLocalization L) (G ⋙ F)
⊢ (localizerMorphism C).IsLocalizedEquivalence
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: case inr
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)
⊢ Function.Bijective (rightHomotopyClassToHom L ∘ fun g ↦ g.precomp i)

Tactic:
convert! (Iso.homCongr (asIso (L.map i)) (Iso.refl (L.obj Y))).symm.bijective.comp hX'

Goal state after:
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)
⊢ (rightHomotopyClassToHom L ∘ fun g ↦ g.precomp i) =
    ⇑((asIso (L.map i)).homCongr (Iso.refl (L.obj Y))).symm ∘ rightHomotopyClassToHom L
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
γ₀ : Homotopic.Quotient x₀ x₁
γ₁ : Homotopic.Quotient x₁ x₂
γ₂ : Homotopic.Quotient x₂ x₃
⊢ (γ₀.trans γ₁).trans γ₂ = γ₀.trans (γ₁.trans γ₂)

Tactic:
induction γ₀ using Quotient.ind with

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

Goal state before:
pp: case refine_1
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
hA : A ≤ Λ[n + 1, i]
h : Set.range ⇑(stdSimplex.asOrderHom (stdSimplex.objEquiv.symm (SimplexCategory.δ i))) ∪ {i} ≠ Set.univ
⊢ Set.range ⇑(stdSimplex.asOrderHom (stdSimplex.objEquiv.symm (SimplexCategory.δ i))) ∪ {i} = Set.univ

Tactic:
stdSimplex.coe_asOrderHom_objEquiv_symm,

Goal state after:
case refine_1
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
hA : A ≤ Λ[n + 1, i]
h : Set.range ⇑(stdSimplex.asOrderHom (stdSimplex.objEquiv.symm (SimplexCategory.δ i))) ∪ {i} ≠ Set.univ
⊢ Set.range ⇑(ConcreteCategory.hom (SimplexCategory.δ i)) ∪ {i} = Set.univ
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr
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₄ : X₄
x₃ : X₃
hx₃ : (ConcreteCategory.hom b) x₃ = x₄
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = x₄) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = x₄ ∧ x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)

Tactic:
by_cases h₂ : x₃ ∈ Set.range l

Goal state after:
case pos
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₄ : X₄
x₃ : X₃
hx₃ : (ConcreteCategory.hom b) x₃ = x₄
h₂ : x₃ ∈ Set.range ⇑(ConcreteCategory.hom l)
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = x₄) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = x₄ ∧ x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)

case neg
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₄ : X₄
x₃ : X₃
hx₃ : (ConcreteCategory.hom b) x₃ = x₄
h₂ : x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = x₄) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = x₄ ∧ x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)
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)
x₂ : (fun X ↦ X) X₂
x₃ : (fun X ↦ X) X₃
hx : (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom b) x₃
⊢ ∃ x₁, (ConcreteCategory.hom t) x₁ = x₂ ∧ (ConcreteCategory.hom l) x₁ = x₃

Tactic:
have := (pushoutCocone_inl_eq_inr_iff_of_isColimit h.isColimit ht x₂ x₃).1 hx

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)
x₂ : (fun X ↦ X) X₂
x₃ : (fun X ↦ X) X₃
hx : (ConcreteCategory.hom r) x₂ = (ConcreteCategory.hom b) x₃
this : ∃ s, (ConcreteCategory.hom t) s = x₂ ∧ (ConcreteCategory.hom l) s = x₃
⊢ ∃ x₁, (ConcreteCategory.hom t) x₁ = x₂ ∧ (ConcreteCategory.hom l) x₁ = x₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case «0»
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ (Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨2, ⋯⟩, ⋯⟩), ⋯⟩).1, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃) =
    Subcomplex.homOfLE ⋯ ≫
      match ↑(↑⟨(⟨(fun i ↦ i) ⟨0, ⋯⟩, ⋯⟩, ⟨(fun i ↦ i) ⟨2, ⋯⟩, ⋯⟩), ⋯⟩).2, ⋯ with
      | 0, hi => (stdSimplex.faceSingletonComplIso 0).inv ≫ f₀
      | 1, hi => ⋯.elim
      | 2, hi => (stdSimplex.faceSingletonComplIso 2).inv ≫ f₂
      | 3, hi => (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
simp only [← cancel_epi (stdSimplex.facePairIso.{u} (n := 3) 1 3 (by simp)).hom,
          ← Category.assoc]

Goal state after:
case «0»
X : SSet
f₀ f₂ f₃ : Δ[2] ⟶ X
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₁₃ : stdSimplex.δ 1 ≫ f₀ = stdSimplex.δ 0 ≫ f₂
h₂₃ : stdSimplex.δ 2 ≫ f₂ = stdSimplex.δ 2 ≫ f₃
⊢ (((stdSimplex.facePairIso 1 3 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 0).inv) ≫ f₀ =
    (((stdSimplex.facePairIso 1 3 ⋯).hom ≫ Subcomplex.homOfLE ⋯) ≫ (stdSimplex.faceSingletonComplIso 2).inv) ≫ f₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i ≫ SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f) =
    f.arrow i.succ

Tactic:
mkOfSucc_δ_gt hij,

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j < i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i.succ) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f) = f.arrow i.succ
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₁
⊢ horn.faceι 2 3 ι₃._proof_1 ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ = (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃

Tactic:
exact (horn.isColimit 2).fac _ (.right ⟨3, by simp⟩)

Goal state after:
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'
⊢ Hom.base (hComp (hComp η θ) κ) = Hom.base (eqToHom ⋯ ≫ hComp η (hComp θ κ) ≫ eqToHom ⋯)

Tactic:
simp only [hComp, base_mk, Hom.base_comp, Hom.base_eqToHom,
    ← heq_eq_eq, heq_eqToHom_comp_iff, heq_comp_eqToHom_iff,
    eqToHom_comp_heq_iff, comp_eqToHom_heq_iff]

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'
⊢ CatEnriched.hComp (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base η) (Hom.base θ) ≫ eqToHom ⋯) (Hom.base κ) ≍
    CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Enriched.Basic

Goal state before:
pp: V : Type v
inst✝² : Category.{w, v} V
inst✝¹ : MonoidalCategory V
C✝ : Type u₁
inst✝ : EnrichedCategory V C✝
C : Type u₁
𝒞 : EnrichedCategory (Type v) C
D : Type u₂
𝒟 : EnrichedCategory (Type v) D
F : C ⥤ D
X Y Z : C
⊢ (eComp (Type v) X Y Z ≫ ↾fun f ↦ F.map f) =
    ((↾fun f ↦ F.map f) ⊗ₘ ↾fun f ↦ F.map f) ≫ eComp (Type v) (F.obj X) (F.obj Y) (F.obj Z)

Tactic:
ext ⟨f, g⟩; exact F.map_comp f g

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

Goal state before:
pp: X : Truncated 2
⊢ (ρ_ (hoFunctor₂.obj X)).hom =
    hoFunctor₂.obj X ◁ (HomotopyCategory.isoTerminal (𝟙_ (Truncated 2))).symm.hom ≫
      (iso X (𝟙_ (Truncated 2))).symm.hom ≫ hoFunctor₂.map (ρ_ X).hom

Tactic:
by ext; apply right_unitality

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

Goal state before:
pp: case neg.right
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ ∀ i_1 < x.castSucc, i.predAbove i_1 < x

Tactic:
· intro j hj
        by_cases! h : i.castSucc < j
        · rw [Fin.predAbove_of_castSucc_lt _ _ h, ← Fin.succ_lt_succ_iff, Fin.succ_pred]
          exact hj.trans x.castSucc_lt_succ
        · rwa [Fin.predAbove_of_le_castSucc _ _ h, ← Fin.castSucc_lt_castSucc_iff,
            Fin.castSucc_castPred]

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✝¹ : OrderBot ι
inst✝ : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ f.filtration m ≤ ⨆ i, f.filtration ↑i

Tactic:
conv_lhs => rw [filtration_def]
    simp only [sup_le_iff, iSup_le_iff, ← f.filtration_bot]
    exact ⟨le_trans (by rfl) (le_iSup _ ⟨⊥, hm.bot_lt⟩), fun j hj c ↦
      (f.subcomplex_le_filtration c (Order.lt_succ_of_not_isMax (not_isMax_of_lt hj))).trans
        (le_trans (by rfl) (le_iSup _ ⟨Order.succ j, hm.succ_lt_iff.mpr hj⟩))⟩

Goal state after:
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
z : (k : K) → (F.obj k).obj (X.obj (j k)) := fun k ↦ ⋯.choose
hz : ∀ (k : K), (ConcreteCategory.hom ((F.obj k).map (cX.ι.app (j k)))) (z k) = ↑y k
k : K
⊢ ↑y k =
    (ConcreteCategory.hom ((F.obj k).map (cX.ι.app (IsCardinalFiltered.max j ⋯))))
      ((fun k ↦ (ConcreteCategory.hom ((F.obj k).map (X.map (IsCardinalFiltered.toMax j ⋯ k)))) (z k)) k)

Tactic:
rw [← hz, ← comp_apply, ← Functor.map_comp, cX.w]; rfl

Goal state after:
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
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
j₁ : J
α : j₀ ⟶ j₁
hα :
  ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')
s : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j₁)).sections := ⋯
⊢ (Types.isLimitEquivSections (hc cX.pt)) x =
    (Types.isLimitEquivSections (hc cX.pt))
      ((ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j₁)) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s))

Tactic:
rw [← hy, Equiv.apply_symm_apply]

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
j₀ : J
z : (k : K) → (F.obj k).obj (X.obj j₀)
hz : ∀ (k : K), ↑y k = (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j₀))) (z k)
j₁ : J
α : j₀ ⟶ j₁
hα :
  ∀ ⦃k k' : K⦄ (φ : k ⟶ k'),
    (ConcreteCategory.hom ((F.obj k').map (X.map α))) ((ConcreteCategory.hom ((F.map φ).app (X.obj j₀))) (z k)) =
      (ConcreteCategory.hom ((F.obj k').map (X.map α))) (z k')
s : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j₁)).sections :=
  ⟨fun k ↦ (ConcreteCategory.hom ((F.obj k).map (X.map α))) (z k), ⋯⟩
⊢ y =
    (Types.isLimitEquivSections (hc cX.pt))
      ((ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app j₁)) ((Types.isLimitEquivSections (hc (X.obj j₁))).symm s))
Module: Mathlib.CategoryTheory.Functor.KanExtension.DenseAt

Goal state before:
pp: C : Type u₁
D : Type u₂
inst✝¹ : Category.{v₁, u₁} C
inst✝ : Category.{v₂, u₂} D
F : C ⥤ D
Y : D
hY : F.DenseAt Y
⊢ F.isDenseAt.IsClosedUnderIsomorphisms

Tactic:
by
  rw [isDenseAt_eq_isPointwiseLeftKanExtensionAt]
  infer_instance

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

Goal state before:
pp: case inst
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
⊢ ∀ (k : WalkingParallelPair),
    IsCardinalPresentable ((parallelPair (q ≫ pullback.fst p p) (q ≫ pullback.snd p p)).obj k) Cardinal.aleph0

Tactic:
rintro (_ | _) <;> dsimp

Goal state after:
case inst.zero
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
⊢ IsCardinalPresentable Z Cardinal.aleph0

case inst.one
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
⊢ IsCardinalPresentable Y Cardinal.aleph0
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic

Goal state before:
pp: ⊢ innerAnodyneExtensions ≤ anodyneExtensions

Tactic:
rw [anodyneExtensions_eq_llp_rlp, innerAnodyneExtensions_eq_llp_rlp, le_llp_iff_le_rlp,
    rlp_llp_rlp]

Goal state after:
⊢ modelCategoryQuillen.J.rlp ≤ innerHornInclusions.rlp
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ Q ◁ pushout.inl f g ≫ Q ◁ hP.isoPushout.inv = Q ◁ inl

Tactic:
by
  simp [← MonoidalCategory.whiskerLeft_comp]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ Q ◁ pushout.inr f g ≫ Q ◁ hP.isoPushout.inv = Q ◁ inr

Tactic:
by
  simp [← MonoidalCategory.whiskerLeft_comp]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ Q ◁ inl ≫ Q ◁ hP.isoPushout.hom = Q ◁ pushout.inl f g

Tactic:
by
  simp [← MonoidalCategory.whiskerLeft_comp]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
Z X Y P : C
f : Z ⟶ X
g : Z ⟶ Y
inl : X ⟶ P
inr : Y ⟶ P
hP : IsPushout f g inl inr
inst✝ : HasPushout f g
Q : C
⊢ Q ◁ inr ≫ Q ◁ hP.isoPushout.hom = Q ◁ pushout.inr f g

Tactic:
by
  simp [← MonoidalCategory.whiskerLeft_comp]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
A B X Y Z W : C
f : A ⟶ B
g : X ⟶ Y
h : Z ⊗ W ⟶ X
⊢ f ▷ Z ▷ W ≫ (α_ B Z W).hom ≫ B ◁ h ≫ pushout.inl (f ▷ X) (A ◁ g) =
    (α_ A Z W).hom ≫ A ◁ (h ≫ g) ≫ pushout.inr (f ▷ X) (A ◁ g)

Tactic:
rw [associator_naturality_left_assoc, ← whisker_exchange_assoc, pushout.condition,
    ← MonoidalCategory.whiskerLeft_comp_assoc]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
Q X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ Q ◁ pushout.inl f g ≫ Q ◁ (pushoutSymmetry f g).hom = Q ◁ pushout.inr g f

Tactic:
by
  simp [← MonoidalCategory.whiskerLeft_comp]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : MonoidalCategory C
inst✝ : HasPushouts C
Q X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ Q ◁ pushout.inr f g ≫ Q ◁ (pushoutSymmetry f g).hom = Q ◁ pushout.inl g f

Tactic:
by
  simp [← MonoidalCategory.whiskerLeft_comp]

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

Goal state before:
pp: case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H✝ H : Homotopy f g
n : ℕ
⊢ ((alternatingFaceMapComplex C).map f).f (n + 1) =
    ((alternatingFaceMapComplex C).obj X).d (n + 1) n ≫ ToChainHomotopy.hom H n (n + 1) +
        (prevD (n + 1)) (ToChainHomotopy.hom H) +
      ((alternatingFaceMapComplex C).map g).f (n + 1)

Tactic:
prevD_eq (j' := n + 2) (w := by simp)

Goal state after:
case succ
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H✝ H : Homotopy f g
n : ℕ
⊢ ((alternatingFaceMapComplex C).map f).f (n + 1) =
    ((alternatingFaceMapComplex C).obj X).d (n + 1) n ≫ ToChainHomotopy.hom H n (n + 1) +
        ToChainHomotopy.hom H (n + 1) (n + 2) ≫ ((alternatingFaceMapComplex C).obj Y).d (n + 2) (n + 1) +
      ((alternatingFaceMapComplex C).map g).f (n + 1)
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 : ℕ
hd : x.dim = d
l : Fin d
hl : IsIndex x hd l.succ
i : Fin (d + 1)
hi : i ∈ finset x hd
⊢ l.succ ≤ i

Tactic:
rw [mem_finset_iff] at hi
      simp [← hl.succ_le_simplex_fst_iff, ← hi]

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
hx : IsType₂ x
d : ℕ
hd : x.dim = d
hx' : StrictMono ⇑(objEquiv (x.cast hd).simplex)
i : Fin d
hi✝ : i.succ ≤ min x hd
hi : i.succ = min x hd
⊢ i.castSucc ≤ min x hd

Tactic:
by dsimp; rw [← hi]; exact Fin.castSucc_le_succ i

Goal state after:
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 Y : SSet
f : X ⟶ Y
R : C
n : ℕ
x✝ : ↑(X.nonDegenerate n)
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ (Cofan.mk (∐ fun x ↦ R) (Sigma.ι fun x ↦ R)).inj ⟨x, hx⟩ ≫
      (Iso.refl (Cofan.mk (∐ fun x ↦ R) (Sigma.ι fun x ↦ R)).pt).hom =
    (X.cofanNormalizedChainComplex R n).inj ⟨x, hx⟩

Tactic:
simpa using (X.ιNormalizedChainComplex_eq_ι R n x hx).symm

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin (n + 1)
⊢ stdSimplex.δ i.castSucc ≫ stdSimplex.σ i ≫ f.map = f.map

Tactic:
CosimplicialObject.δ_comp_σ_self_assoc

Goal state after:
X : SSet
n : ℕ
x : X _⦋0⦌
f : X.PtSimplex n x
i : Fin (n + 1)
⊢ f.map = f.map
Module: Mathlib.Topology.Algebra.Module.Cardinality

Goal state before:
pp: E : Type u_1
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
inst✝⁴ : AddGroup E
inst✝³ : MulActionWithZero 𝕜 E
inst✝² : TopologicalSpace E
inst✝¹ : ContinuousAdd E
inst✝ : ContinuousSMul 𝕜 E
s : Set E
x : E
hs : s ∈ 𝓝 x
⊢ #↑s = #E

Tactic:
by
  let g := Homeomorph.addLeft x
  let t := g ⁻¹' s
  have : t ∈ 𝓝 0 := g.continuous.continuousAt.preimage_mem_nhds (by simpa [g] using hs)
  have A : #t = #E := cardinal_eq_of_mem_nhds_zero 𝕜 this
  have B : #t = #s := Cardinal.mk_subtype_of_equiv (· ∈ s) g.toEquiv
  rwa [B] at A

Goal state after:
Module: Mathlib.Analysis.Analytic.Order

Goal state before:
pp: case neg
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f g : 𝕜 → E
z₀ : 𝕜
hf : AnalyticAt 𝕜 f z₀
hg : ¬AnalyticAt 𝕜 g z₀
⊢ min (analyticOrderAt f z₀) (analyticOrderAt g z₀) ≤ analyticOrderAt (f + g) z₀

Tactic:
· simp [*]

Goal state after: