mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: 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₃
⊢ ι₃ ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ = f₃

Tactic:
← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 3).inv,

Goal state after:
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.faceSingletonComplIso 3).inv ≫ ι₃ ≫ desc f₀ f₂ f₃ h₁₂ h₁₃ h₂₃ =
    (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

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

Tactic:
← cancel_epi (stdSimplex.faceSingletonComplIso.{u} 3).inv,

Goal state after:
X : SSet
f₀ f₁ f₃ : Δ[2] ⟶ X
h₀₂ : stdSimplex.δ 2 ≫ f₁ = stdSimplex.δ 1 ≫ f₃
h₁₂ : stdSimplex.δ 2 ≫ f₀ = stdSimplex.δ 0 ≫ f₃
h₂₃ : stdSimplex.δ 0 ≫ f₀ = stdSimplex.δ 0 ≫ f₁
⊢ (stdSimplex.faceSingletonComplIso 3).inv ≫ ι₃ ≫ desc f₀ f₁ f₃ h₀₂ h₁₂ h₂₃ =
    (stdSimplex.faceSingletonComplIso 3).inv ≫ f₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
f : X.Path n
j l : ℕ
hjl : j + l ≤ n
⊢ (ConcreteCategory.hom (X.map (intervalEdge j l hjl).op)) (sx.spineToSimplex f) =
    (ConcreteCategory.hom (X.map (diag l).op)) (sx.spineToSimplex (f.interval j l hjl))

Tactic:
rw [← spineToSimplex_interval, ← Functor.map_comp_apply, ← op_comp,
    diag_subinterval_eq]

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

Goal state before:
pp: case mp
V : Truncated 2
X✝ Y✝ : V.HomotopyCategory
f : X✝ ⟶ Y✝
⊢ morphismPropertyHomMk V f → (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)).strictMap (quotientFunctor V) f

pp: case mpr
V : Truncated 2
X✝ Y✝ : V.HomotopyCategory
f : X✝ ⟶ Y✝
⊢ (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)).strictMap (quotientFunctor V) f → morphismPropertyHomMk V f

Tactic:
· rintro ⟨_⟩
    exact MorphismProperty.map_mem_strictMap _ _ _ ⟨_⟩

Goal state after:
case mpr
V : Truncated 2
X✝ Y✝ : V.HomotopyCategory
f : X✝ ⟶ Y✝
⊢ (Cat.FreeRefl.morphismPropertyHomMk (OneTruncation₂ V)).strictMap (quotientFunctor V) f → morphismPropertyHomMk V f
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case inr.inr
n : ℕ
i i' : Fin (n + 2)
h : i'.castSucc < i.castSucc
⊢ δ i'.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.castSucc ≫ σ i = σ j ≫ δ j'

Tactic:
rw [Fin.castSucc_lt_castSucc_iff] at h

Goal state after:
case inr.inr
n : ℕ
i i' : Fin (n + 2)
h : i' < i
⊢ δ i'.castSucc ≫ σ i = 𝟙 (mk (n + 1)) ∨ ∃ j j', δ i'.castSucc ≫ σ i = σ j ≫ δ j'
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
⊢ ↑(a₀.predAbove t) = if a < ↑t then ↑t - 1 else ↑t

Tactic:
simp only [Fin.predAbove, a₀]

Goal state after:
L✝ : List ℕ
j a : ℕ
L : List ℕ
h_rec :
  ∀ (m₁ m₂ : ℕ),
    IsAdmissible m₂ L →
      ∀ (hk : m₂ + L.length = m₁) (hj : j < m₁ + 1),
        ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ L hk))) ⟨j, hj⟩) = simplicialEvalσ L j
m₂ : ℕ
hL : IsAdmissible m₂ (a :: L)
hj : j < m₂ + (L.length + 1) + 1
a₀ : Fin (m₂ + 1) := hL.head
t : Fin (m₂ + 2)
⊢ ↑(if h : hL.head.castSucc < t then t.pred ⋯ else t.castPred ⋯) = if a < ↑t then ↑t - 1 else ↑t
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: case neg.zero
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
b : ℕ
hb : b ≤ d
ha : 0 ≤ d
f : { obj := { len := 0 }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : 0 + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : ¬Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f

pp: case neg.succ
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
b : ℕ
hb : b ≤ d
a : ℕ
ha : a + 1 ≤ d
f : { obj := { len := a + 1 }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + 1 + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : ¬Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f

Tactic:
· exact (h₂ (Function.injective_of_subsingleton (α := Fin 1) _)).elim

Goal state after:
case neg.succ
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
b : ℕ
hb : b ≤ d
a : ℕ
ha : a + 1 ≤ d
f : { obj := { len := a + 1 }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + 1 + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : ¬Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsLowerSet s
a : { x // P x }
ma : a ∈ s
b : α
x : b ≤ ↑a
y : P b
⊢ b ∈ Subtype.val '' s

Tactic:
simpa [h (show ⟨b, y⟩ ≤ a by exact x) ma]

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

Goal state before:
pp: ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty ∧ ∀ ⦃b : Finset ι⦄, b ⊆ x → b.Nonempty → b ∈ {s | ∃ v, s = {v}}

Tactic:
by
      constructor
      · rw [hv]; exact Finset.singleton_nonempty _
      · intro t hts ht
        cases Finset.subset_singleton_iff.mp (hv ▸ hts) with
        | inl h => exact (ht.ne_empty h).elim
        | inr h => exact ⟨v, h⟩

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

Goal state before:
pp: X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx✝ : x ∈ (nerve T).nonDegenerate n
hx : Function.Injective x.obj
k : ℕ
i j : Δ[n] _⦋k⦌
hij :
  (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) i =
    (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) j
⊢ i = j

Tactic:
ext l : 1

Goal state after:
X Y : SSet
T : Type u_1
inst✝ : PartialOrder T
n : ℕ
x : nerve T _⦋n⦌
hx✝ : x ∈ (nerve T).nonDegenerate n
hx : Function.Injective x.obj
k : ℕ
i j : Δ[n] _⦋k⦌
hij :
  (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) i =
    (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋k⦌))) j
l : Fin (k + 1)
⊢ i l = j l
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case inr.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
hi✝ : i ≤ j
c : f.Cell i
hx : x ∈ (↑(P.p c.s)).subcomplex.obj d
hi : i < j
⊢ (x ∈ A.obj d ∨ ∃ i < j, ∃ i_1, x ∈ (↑(P.p i_1.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b j).app d)) y) = x

Tactic:
exact Or.inl (Or.inr ⟨i, hi, c, hx⟩)

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

Goal state before:
pp: case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
c : f.Cell i
hx : x ∈ (↑(P.p c.s)).subcomplex.obj d
hi : i ≤ i
⊢ (x ∈ A.obj d ∨ ∃ i_1 < i, ∃ i, x ∈ (↑(P.p i.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b i).app d)) y) = x

Tactic:
← c.range_map,

Goal state after:
case inr.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
d : SimplexCategoryᵒᵖ
x : X.obj d
i : ι
c : f.Cell i
hx : x ∈ (range c.map).obj d
hi : i ≤ i
⊢ (x ∈ A.obj d ∨ ∃ i_1 < i, ∃ i, x ∈ (↑(P.p i.s)).subcomplex.obj d) ∨
    ∃ y, ↑((ConcreteCategory.hom ((f.b i).app d)) y) = x
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : HasLimitsOfShape Jᵒᵖ (Type w)
hJ : HasCardinalLT (Arrow J) κ
X : C
hX : (isCardinalPresentable C κ).ColimitOfShape J X
⊢ isCardinalPresentable C κ X

Tactic:
have := hX.prop_diag_obj

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : LocallySmall.{w, v, u} C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
J : Type u'
inst✝¹ : Category.{v', u'} J
inst✝ : HasLimitsOfShape Jᵒᵖ (Type w)
hJ : HasCardinalLT (Arrow J) κ
X : C
hX : (isCardinalPresentable C κ).ColimitOfShape J X
this : ∀ (j : J), isCardinalPresentable C κ (hX.diag.obj j)
⊢ isCardinalPresentable C κ X
Module: Mathlib.CategoryTheory.Presentable.Presheaf

Goal state before:
pp: A : Type u'
inst✝³ : Category.{v', u'} A
P : ObjectProperty A
inst✝² : HasCoproducts A
inst✝¹ : HasPullbacks A
C : Type w
inst✝ : SmallCategory C
hP₁ : P.IsSeparating
hP₂ : ∀ ⦃X Y : A⦄ (i : X ⟶ Y) [Mono i], (∀ (G : A), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
P₁ P₂ : Cᵒᵖ ⥤ A
i : P₁ ⟶ P₂
x✝ : Mono i
hi : ∀ (G : Cᵒᵖ ⥤ A), ObjectProperty.ofObj (fun T ↦ freeYoneda T.1 ↑T.2) G → Function.Surjective fun f ↦ f ≫ i
X : C
G : A
hG : P G
x : freeYoneda X G ⟶ P₁
⊢ ∃ a, (fun f ↦ f ≫ i.app (op X)) a = freeYonedaHomEquiv ((fun f ↦ f ≫ i) x)

Tactic:
exact ⟨freeYonedaHomEquiv x, by simp [freeYonedaHomEquiv_comp]⟩

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

Goal state before:
pp: case inl
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.castSucc < min x hd
⊢ (objEquiv (x.cast hd).simplex) i.castSucc < φ x hd i.castSucc.succ

Tactic:
rw [Fin.castSucc_lt_iff_succ_le] at hi

Goal state after:
case inl
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
⊢ (objEquiv (x.cast hd).simplex) i.castSucc < φ x hd i.castSucc.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct

Goal state before:
pp: X₁ Y₁ E B : SSet
i : X₁ ⟶ Y₁
p : E ⟶ B
inst✝¹ : Mono i
inst✝ : InnerFibration p
sq₁₃ : internalHom.PullbackObjObj i p
X✝ Y✝ : SSet
g✝ : X✝ ⟶ Y✝
n✝ : ℕ
k : Fin (n✝ + 3)
h0 : 0 < k
hn : k < Fin.last (n✝ + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[n✝ + 2, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[n✝ + 2, k].ι
⊢ innerAnodyneExtensions sq₁₂.ι

Tactic:
intro E B p hp

Goal state after:
X₁ Y₁ E✝ B✝ : SSet
i : X₁ ⟶ Y₁
p✝ : E✝ ⟶ B✝
inst✝¹ : Mono i
inst✝ : InnerFibration p✝
sq₁₃ : internalHom.PullbackObjObj i p✝
X✝ Y✝ : SSet
g✝ : X✝ ⟶ Y✝
n✝ : ℕ
k : Fin (n✝ + 3)
h0 : 0 < k
hn : k < Fin.last (n✝ + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[n✝ + 2, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[n✝ + 2, k].ι
E B : SSet
p : E ⟶ B
hp : innerFibrations p
⊢ HasLiftingProperty sq₁₂.ι p
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.PushoutProduct

Goal state before:
pp: X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : innerAnodyneExtensions j
⊢ innerAnodyneExtensions sq₁₂.ι

Tactic:
intro E B p hp

Goal state after:
X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : innerAnodyneExtensions j
E B : SSet
p : E ⟶ B
hp : innerFibrations p
⊢ HasLiftingProperty sq₁₂.ι p
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
m : ℕ
X Y : SSet
k : Fin (m + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[m + 1, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[m + 1, k].ι
⊢ anodyneExtensions sq₁₂.ι

Tactic:
intro E B p hp

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✝
m : ℕ
X Y : SSet
k : Fin (m + 2)
sq₁₂ : (curriedTensor SSet).PushoutObjObj i Λ[m + 1, k].ι :=
  Functor.PushoutObjObj.ofHasPushout (curriedTensor SSet) i Λ[m + 1, k].ι
E B : SSet
p : E ⟶ B
hp : fibrations SSet p
⊢ HasLiftingProperty sq₁₂.ι p
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PushoutProduct

Goal state before:
pp: X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : anodyneExtensions j
⊢ anodyneExtensions sq₁₂.ι

Tactic:
intro E B p hp

Goal state after:
X₁ X₂ Y₁ Y₂ : SSet
i : X₁ ⟶ Y₁
j : X₂ ⟶ Y₂
sq₁₂ : (curriedTensor SSet).PushoutObjObj i j
inst✝ : Mono i
hj : anodyneExtensions j
E B : SSet
p : E ⟶ B
hp : fibrations SSet p
⊢ HasLiftingProperty sq₁₂.ι p
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd

Goal state before:
pp: case pos
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ φ s.δ ⋯ (min ⋯.δ ⋯).castSucc = (objEquiv (s.x.cast ⋯).simplex) s.index.castSucc

Tactic:
rw [φ_castSucc]

Goal state after:
case pos
m : ℕ
k : Fin (m + 1)
n : ℕ
s : Type₁ k n
ht : IsType₂ s.δ
⊢ (k.castSucc, (s.δ.cast ⋯).simplex.2 (min s.δ ⋯)) = (objEquiv (s.x.cast ⋯).simplex) s.index.castSucc
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : CartesianMonoidalCategory C
inst✝ : MonoidalClosed C
X : Arrow C
I : C
i : IsInitial I
T : C
t : IsTerminal T
⊢ (X.left ◁ᵢ t.uniqueUpToIso SemiCartesianMonoidalCategory.isTerminalTensorUnit ≪≫ ρ_ X.left).hom ≫ X.hom =
    X.hom ▷ T ≫ (X.right ◁ᵢ t.uniqueUpToIso SemiCartesianMonoidalCategory.isTerminalTensorUnit ≪≫ ρ_ X.right).hom

Tactic:
by simp [← whisker_exchange_assoc]

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_1.refine_1.refine_1
C : Type u
inst✝⁴ : Category.{v, u} C
inst✝³ : HasPushouts C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : HasInitial C
X : Arrow C
⊢ ((curriedTensor C).obj X.right).obj (Arrow.mk (initial.to (𝟙_ C))).left ⟶ X.left

Tactic:
exact (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).to _

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
n : ℕ
⊢ (X.chainComplex R).d n 0 ≫ fromChainComplexXZero X R = 0

Tactic:
by_cases! hn : n ≠ 1
  · rw [HomologicalComplex.shape _ _ _ (by simp; lia), zero_comp]
  · subst hn
    ext x
    simp [π₀.sound (Edge.mk' x)]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homology.HomologyZero

Goal state before:
pp: case refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
X : SSet
R : C
x✝ : X _⦋0⦌
⊢ X.ιChainComplex x✝ ≫
      Cofork.π
          ((Cocone.precompose
                (parallelPair.ext
                    (-Iso.refl
                        ((parallelPair
                              ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                                (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                              0).obj
                          WalkingParallelPair.zero))
                    (Iso.refl
                      ((parallelPair
                            ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                              (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                            0).obj
                        WalkingParallelPair.one))
                    ⋯ ⋯).inv).obj
            (Preadditive.cokernelCoforkOfCofork (Cofork.ofπ ((sigmaConst.obj R).map (↾π₀.mk)) ⋯))) ≫
        (Iso.refl
            ((Cocone.precompose
                    (parallelPair.ext
                        (-Iso.refl
                            ((parallelPair
                                  ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                                    (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                                  0).obj
                              WalkingParallelPair.zero))
                        (Iso.refl
                          ((parallelPair
                                ((sigmaConst.obj R).map (SimplicialObject.δ X 1) -
                                  (sigmaConst.obj R).map (SimplicialObject.δ X 0))
                                0).obj
                            WalkingParallelPair.one))
                        ⋯ ⋯).inv).obj
                (Preadditive.cokernelCoforkOfCofork (Cofork.ofπ ((sigmaConst.obj R).map (↾π₀.mk)) ⋯))).pt).hom =
    X.ιChainComplex x✝ ≫ Cofork.π (CokernelCofork.ofπ (π₀.fromChainComplexXZero X R) ⋯)

Tactic:
simp [chainComplex, SSet.chainComplexFunctor, π₀.fromChainComplexXZero]

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✝ : G.PullbackObjObj f₁✝¹ f₃✝¹
f₁✝ f₁' : Arrow C₁
f₃✝ : Arrow C₃
sq₁₃✝ : G.PullbackObjObj f₁✝.hom f₃✝.hom
sq₁₃'✝ : G.PullbackObjObj f₁'.hom f₃✝.hom
f₁ : Arrow C₁
f₃ f₃' : Arrow C₃
sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom
sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom
sq : f₃ ⟶ f₃'
⊢ (sq₁₃.fst ≫ (G.obj (op f₁.left)).map (Arrow.Hom.left sq)) ≫ (G.obj (op f₁.left)).map f₃'.hom =
    (sq₁₃.snd ≫ (G.obj (op f₁.right)).map (Arrow.Hom.right sq)) ≫ (G.map f₁.hom.op).app f₃'.right

Tactic:
by
      #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
      goal without the `simp`. It is not yet clear whether this is due to defeq abuse in
      Mathlib or a problem in the new canonicalizer; a minimization would help. The original
      proof was: `by grind [sq.w, sq₁₃.isPullback.w]` -/
      simp [Arrow.mk_right]; grind [sq.w, sq₁₃.isPullback.w]

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

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

Tactic:
rw [δ_castSucc_map, hf]

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

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
F : TopCat ⥤ C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
⊢ toTopSimplex.inv.app ⦋n⦌ ≫ toTop.map (SSet.yonedaEquiv.symm i) ≫ sSetTopAdj.counit.app X = i.down

Tactic:
← reassoc_of% sSetTopAdj_unit_app_app_down

Goal state after:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasCoproducts C
inst✝ : Preadditive C
n : ℕ
F : TopCat ⥤ C
X : TopCat
i : TopCat.toSSet.obj X _⦋n⦌
⊢ ((ConcreteCategory.hom ((sSetTopAdj.unit.app (TopCat.toSSet.obj X)).app (Opposite.op ⦋n⦌))) i).down ≫
      sSetTopAdj.counit.app X =
    i.down
Module: Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn

Goal state before:
pp: case hbc
𝕜 : Type u_1
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_3
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
f : E → F
inst✝ : CompleteSpace E
s : Set E
c : ℝ≥0
f' : E →L[𝕜] F
hf : ApproximatesLinearOn f f' s c
f'symm : f'.NonlinearRightInverse
ε : ℝ
b : E
ε0 : 0 ≤ ε
hε : closedBall b ε ⊆ s
y : F
hy : y ∈ closedBall (f b) (((↑f'symm.nnnorm)⁻¹ - ↑c) * ε)
hc : ↑c < (↑f'symm.nnnorm)⁻¹
If' : 0 < ↑f'symm.nnnorm
Icf' : ↑c * ↑f'symm.nnnorm < 1
Jcf' : 1 - ↑c * ↑f'symm.nnnorm ≠ 0
g : E → E := ⋯
hg : g = fun x ↦ x + f'symm.toFun (y - f x)
u : ℕ → E := ⋯
hu : u = fun n ↦ g^[n] b
usucc : ∀ (n : ℕ), u (n + 1) = g (u n)
A : ∀ (z : E), dist (g z) z ≤ ↑f'symm.nnnorm * dist (f z) y
B : ∀ z ∈ closedBall b ε, g z ∈ closedBall b ε → dist (f (g z)) y ≤ ↑c * ↑f'symm.nnnorm * dist (f z) y
C :
  ∀ (n : ℕ) (w : E),
    dist w b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y →
      w ∈ closedBall b ε
n : ℕ
IH :
  dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y ∧
    dist (u n) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
Ign :
  dist (g (u n)) b ≤ ↑f'symm.nnnorm * (1 - (↑c * ↑f'symm.nnnorm) ^ n.succ) / (1 - ↑c * ↑f'symm.nnnorm) * dist (f b) y
⊢ dist (f (u n)) y ≤ (↑c * ↑f'symm.nnnorm) ^ n * dist (f b) y

Tactic:
apply IH.1

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

Goal state before:
pp: case coe.e_a
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
⊢ analyticOrderAt (fun x_1 ↦ (x_1 - x) ^ (s + 1) • deriv F x_1 + (s + 1) • (x_1 - x) ^ s • F x_1) x = ↑s

Tactic:
have : analyticOrderAt (fun y ↦ (s + 1) • (y - x) ^ s • F y) x = s := by
      rw [analyticOrderAt_eq_natCast]
      · refine ⟨fun z ↦ (↑(s + 1) : 𝕜) • F z, hFa.fun_const_smul, ?_, .of_forall fun y ↦ ?_⟩
        · simpa using ⟨by norm_cast, hFne⟩
        · simpa only [Nat.cast_smul_eq_nsmul] using smul_comm ..
      · simp_rw [← Nat.cast_smul_eq_nsmul 𝕜]
        fun_prop

Goal state after:
case coe.e_a
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f : 𝕜 → E
x : 𝕜
hf : AnalyticAt 𝕜 f x
inst✝¹ : CompleteSpace E
inst✝ : CharZero 𝕜
s : ℕ
hrne : s + 1 ≠ 0
F : 𝕜 → E
hFa : AnalyticAt 𝕜 F x
hFne : F x ≠ 0
hfF : ∀ᶠ (z : 𝕜) in 𝓝 x, f z = (z - x) ^ (s + 1) • F z + f x
U : Set 𝕜
hUf : ∀ y ∈ U, f y = (y - x) ^ (s + 1) • F y + f x ∧ AnalyticAt 𝕜 F y
hUo : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] U
hUx : x ∈ U
this✝ : ∀ y ∈ U, deriv f y = (y - x) ^ (s + 1) • deriv F y + (s + 1) • (y - x) ^ s • F y
this : analyticOrderAt (fun y ↦ (s + 1) • (y - x) ^ s • F y) x = ↑s
⊢ analyticOrderAt (fun x_1 ↦ (x_1 - x) ^ (s + 1) • deriv F x_1 + (s + 1) • (x_1 - x) ^ s • F x_1) x = ↑s