mathlib-initiative/mathlib-tactics huggingface dataset:
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₂
i : Fin (x₁.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' x₁ x₂)) i = Fin.cast ⋯ (Fin.castAdd (x₂.len + 1) i)
⊢ (SimplexCategory.Hom.toOrderHom (eqToHom ⋯))
      ({
          toFun := 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,
          monotone' := ⋯ }
        ((SimplexCategory.Hom.toOrderHom (eqToHom ⋯)) ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂)) i))) =
    (SimplexCategory.Hom.toOrderHom (inl' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i)

Tactic:
have e₂ := inl'_eval y₁ y₂ <| (WithInitial.down f₁).toOrderHom i

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₂
i : Fin (x₁.len + 1)
e₁ : (SimplexCategory.Hom.toOrderHom (inl' x₁ x₂)) i = Fin.cast ⋯ (Fin.castAdd (x₂.len + 1) i)
e₂ :
  (SimplexCategory.Hom.toOrderHom (inl' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i) =
    Fin.cast ⋯ (Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i))
⊢ (SimplexCategory.Hom.toOrderHom (eqToHom ⋯))
      ({
          toFun := 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,
          monotone' := ⋯ }
        ((SimplexCategory.Hom.toOrderHom (eqToHom ⋯)) ((SimplexCategory.Hom.toOrderHom (inl' x₁ x₂)) i))) =
    (SimplexCategory.Hom.toOrderHom (inl' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i)
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]

Goal state after:
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' (g.comp f) x.castSucc = Fin.last (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos.inr
n : ℕ
i : Fin (n + 2)
hx : Fin.last (n + 1) ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom (Fin.last (n + 1)).castSucc = Fin.last (n + 1)

Tactic:
obtain rfl : i = Fin.last _ := Fin.last_le_iff.1 hx

Goal state after:
case pos.inr
n : ℕ
hx : Fin.last (n + 1) ≤ Fin.last (n + 1)
⊢ map' (Fin.last (n + 1)).succAboveOrderEmb.toOrderHom (Fin.last (n + 1)).castSucc = Fin.last (n + 1)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

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

Tactic:
by_cases! h : i.castSucc < j

Goal state after:
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

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: case neg.right
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
⊢ i.predAbove j < x

Tactic:
by_cases! h : i.castSucc < j

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

case neg
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
h : j ≤ i.castSucc
⊢ i.predAbove j < x
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
x : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
m : ℕ
hm : p + q = m
i : Fin (n + 1)
⊢ ↑i ≤ ↑((orderHomOfSimplex (↑x) hm) i)

Tactic:
induction i using Fin.induction with

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

Goal state before:
pp: p q n : ℕ
x : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
m : ℕ
hm : p + q = m
i : Fin (n + 1)
⊢ ↑i ≤ ↑((orderHomOfSimplex (↑x) hm) i)

Tactic:
by
  induction i using Fin.induction with
  | zero => simp
  | succ i hi =>
    simpa using! lt_of_le_of_lt hi (strictMono_orderHomOfSimplex x hm Fin.castSucc_lt_succ)

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s)).cast ⋯).simplex ∉ A.obj (Opposite.op ⦋(↑s).dim⦌)

Tactic:
by
    rw [(P.isUniquelyCodimOneFace s).δ_index rfl]
    exact s.val.notMem

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x y : X.N
h : x ≤ y
f₁ f₂ : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
x✝¹ : Mono f₁ ∧ (ConcreteCategory.hom (X.map f₁.op)) y.simplex = x.simplex
x✝ : Mono f₂ ∧ (ConcreteCategory.hom (X.map f₂.op)) y.simplex = x.simplex
left✝¹ : Mono f₁
hf₁ : (ConcreteCategory.hom (X.map f₁.op)) y.simplex = x.simplex
left✝ : Mono f₂
hf₂ : (ConcreteCategory.hom (X.map f₂.op)) y.simplex = x.simplex
⊢ x.simplex = (ConcreteCategory.hom (X.map f₂.op)) y.simplex

Tactic:
hf₂

Goal state after:
X : SSet
inst✝ : X.Nonsingular
x y : X.N
h : x ≤ y
f₁ f₂ : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
x✝¹ : Mono f₁ ∧ (ConcreteCategory.hom (X.map f₁.op)) y.simplex = x.simplex
x✝ : Mono f₂ ∧ (ConcreteCategory.hom (X.map f₂.op)) y.simplex = x.simplex
left✝¹ : Mono f₁
hf₁ : (ConcreteCategory.hom (X.map f₁.op)) y.simplex = x.simplex
left✝ : Mono f₂
hf₂ : (ConcreteCategory.hom (X.map f₂.op)) y.simplex = x.simplex
⊢ x.simplex = x.simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝¹ x✝ : h.ι
hst : h.type₁ x✝¹ = h.type₁ x✝
⊢ { dim := h.dim x✝¹ + 1, simplex := h.simplex x✝¹ } = { dim := h.dim x✝ + 1, simplex := h.simplex x✝ }

Tactic:
rwa [Subcomplex.N.ext_iff, SSet.N.ext_iff] at hst

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
s t : h.ι
hst : h.type₂ s = h.type₂ t
⊢ { dim := h.dim s, simplex := (ConcreteCategory.hom (SimplicialObject.δ X (h.index s))) (h.simplex s) } =
    { dim := h.dim t, simplex := (ConcreteCategory.hom (SimplicialObject.δ X (h.index t))) (h.simplex t) }

Tactic:
rwa [Subcomplex.N.ext_iff, SSet.N.ext_iff] at hst

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝¹ : h.IsInner
inst✝ : h.IsProper
s : h.ι
⊢ ∀ {d : ℕ} (hd : (↑(h.equivII s)).dim = d), ⋯.index hd ≠ 0

Tactic:
rintro _ rfl

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝¹ : h.IsInner
inst✝ : h.IsProper
s : h.ι
⊢ ⋯.index ⋯ ≠ 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝¹ : h.IsInner
inst✝ : h.IsProper
s : h.ι
⊢ ∀ {d : ℕ} (hd : (↑(h.equivII s)).dim = d), ⋯.index hd ≠ Fin.last (d + 1)

Tactic:
rintro _ rfl

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝¹ : h.IsInner
inst✝ : h.IsProper
s : h.ι
⊢ ⋯.index ⋯ ≠ Fin.last ((↑(h.equivII s)).dim + 1)
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: case refine_1
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
F G H : D ⥤ C
f : F ⟶ H
g : G ⟶ H
c : (X : D) → PullbackCone (f.app X) (g.app X)
hc : (X : D) → IsLimit (c X)
k : D
⊢ cospan (f.app k) (g.app k) ≅ cospan f g ⋙ (evaluation D C).obj k

Tactic:
exact cospanIsoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)

Goal state after:
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ P.IsStrongGenerator ↔
    P.IsSeparating ∧ ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i], (∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i

Tactic:
refine ⟨fun ⟨hS₁, hS₂⟩ ↦ ⟨hS₁, fun X Y i _ h ↦ ?_⟩,
    fun ⟨hS₁, hS₂⟩ ↦ ⟨hS₁, fun X A hA ↦ ?_⟩⟩

Goal state after:
case refine_1
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝¹ : P.IsStrongGenerator
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X : C⦄ (A : Subobject X), (∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f) → A = ⊤
X Y : C
i : X ⟶ Y
x✝ : Mono i
h : ∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i
⊢ IsIso i

case refine_2
C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
x✝ : P.IsSeparating ∧ ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i], (∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
hS₁ : P.IsSeparating
hS₂ : ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i], (∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i
X : C
A : Subobject X
hA : ∀ (G : C), P G → ∀ (f : G ⟶ X), A.Factors f
⊢ A = ⊤
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
P : ObjectProperty C
⊢ P.IsStrongGenerator ↔
    P.IsSeparating ∧ ∀ ⦃X Y : C⦄ (i : X ⟶ Y) [Mono i], (∀ (G : C), P G → Function.Surjective fun f ↦ f ≫ i) → IsIso i

Tactic:
refine ⟨fun ⟨hS₁, hS₂⟩ ↦ ⟨hS₁, fun X Y i _ h ↦ ?_⟩,
    fun ⟨hS₁, hS₂⟩ ↦ ⟨hS₁, fun X A hA ↦ ?_⟩⟩
  · rw [Subobject.isIso_iff_mk_eq_top]
    refine hS₂ _ (fun G hG g ↦ ?_)
    rw [Subobject.mk_factors_iff]
    exact h G hG g
  · rw [← Subobject.isIso_arrow_iff_eq_top]
    exact hS₂ A.arrow (fun G hG g ↦ ⟨_, Subobject.factorThru_arrow _ _ (hA G hG g)⟩)

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
Y : K ⥤ C
c : Cocone Y
hc : IsColimit c
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : HasLimitsOfShape Kᵒᵖ (Type v)
hK : HasCardinalLT (Arrow K) κ
inst✝ : ∀ (k : K), IsCardinalPresentable (Y.obj k) κ
this : ∀ (k : Kᵒᵖ), ((Y.op ⋙ coyoneda).obj k).IsCardinalAccessible κ
⊢ IsCardinalPresentable c.pt κ

Tactic:
exact Functor.isCardinalAccessible_of_isLimit
    (coyoneda.mapCone c.op) (isLimitOfPreserves _ hc.op) κ (by simpa)

Goal state after:
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 c' : f.Cell j
h : P.p c.s = P.p c'.s
⊢ c.s = c'.s

Tactic:
exact P.p.injective h

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
G : D ⥤ C'
inst✝ : G.IsEquivalence
⊢ (F ⋙ G).IsDense ↔ F.IsDense

Tactic:
by
  refine ⟨fun _ ↦ ?_, fun _ ↦ inferInstance⟩
  let e : (F ⋙ G) ⋙ G.inv ≅ F := associator .. ≪≫
    isoWhiskerLeft _ G.asEquivalence.unitIso.symm ≪≫ F.rightUnitor
  exact of_iso e

Goal state after:
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✝² : OrderBot ι
inst✝¹ : NoMaxOrder ι
inst✝ : WellFoundedLT ι
m : ι
hm : Order.IsSuccLimit m
⊢ IsLUB (Set.range (⋯.functor ⋙ ⋯.functor).obj) ((Set.principalSegIio m).cocone ⋯.functor).pt

Tactic:
dsimp
    rw [← f.iSup_filtration_iio m hm]
    apply isLUB_iSup

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

Goal state before:
pp: m : ℕ
k : Fin (m + 1)
n : ℕ
t : (Λ[m + 1, k.castSucc].unionProd ∂Δ[n]).N
ht : IsType₂ t
s : Type₁ k n
hst : s.δ = t
d : ℕ
hd : t.dim = d
⊢ ht.type₁ hd = s

Tactic:
by
  subst hst hd
  rw [Type₁.ext_iff, Subcomplex.N.ext_iff, N.ext_iff]
  rw [← s.x.toS.cast_eq_self s.hd, S.ext_iff']
  refine ⟨rfl, objEquiv.injective ?_⟩
  ext i : 2
  change φ s.δ rfl i = _
  by_cases! hi : i = s.index.castSucc
  · subst hi
    conv_lhs => rw [← s.isIndex.min_δ]
    dsimp
    rw [φ_castSucc]
    ext : 1
    · simp [← s.isIndex.simplex_fst_castSucc]
      rfl
    · change (s.x.cast s.hd).simplex.2
        (s.index.castSucc.succAbove (min s.δ rfl)) = _
      rw [s.isIndex.min_δ, Fin.succAbove_castSucc_self]
      exact s.isIndex.simplex_snd_succ -- defeq abuse
  · rw [← s.isIndex.min_δ] at hi
    rw [φ_of_ne _ rfl _ hi]
    change objEquiv (s.x.cast s.hd).simplex
      (s.index.castSucc.succAbove ((min s.δ rfl).predAbove i)) = _
    congr 1
    rw [← s.isIndex.min_δ]
    exact Fin.succAbove_predAbove hi

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₂✝
f₁ f₁' : Arrow C₁
f₂ : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom
sq : f₁ ⟶ f₁'
⊢ (F.map f₁.hom).app f₂.left ≫ (F.map (Arrow.Hom.right sq)).app f₂.left ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.map (Arrow.Hom.left sq)).app f₂.right ≫ sq₁₂'.inr

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 only`. 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₁₂'.isPushout.w]` -/
      simp only [Arrow.mk_left]; grind [sq.w, sq₁₂'.isPushout.w]

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₂✝¹
f₁✝ f₁' : Arrow C₁
f₂✝ : Arrow C₂
sq₁₂✝ : F.PushoutObjObj f₁✝.hom f₂✝.hom
sq₁₂'✝ : F.PushoutObjObj f₁'.hom f₂✝.hom
f₁ : Arrow C₁
f₂ f₂' : Arrow C₂
sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom
sq₁₂' : F.PushoutObjObj f₁.hom f₂'.hom
sq : f₂ ⟶ f₂'
⊢ (F.map f₁.hom).app f₂.left ≫ (F.obj f₁.right).map (Arrow.Hom.left sq) ≫ sq₁₂'.inl =
    (F.obj f₁.left).map f₂.hom ≫ (F.obj f₁.left).map (Arrow.Hom.right sq) ≫ sq₁₂'.inr

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 only`. 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₁₂'.isPushout.w]` -/
      simp only [Arrow.mk_left]; grind [sq.w, sq₁₂'.isPushout.w]

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

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (H.h.app (op ⦋n⦌)))
      ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  ((ConcreteCategory.hom (δ Δ[n] 0)) (stdSimplex.objEquiv.symm (SimplexCategory.σ 0)))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] 0)) (stdSimplex.objMk₁ 1)) =
    (ConcreteCategory.hom (H.h.app (op ⦋n⦌))) ((ConcreteCategory.hom (ι₁.app (op ⦋n⦌))) x)

Tactic:
apply congr_arg

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
⊢ ((ConcreteCategory.hom
          (X.map
            (stdSimplex.objEquiv
                ((ConcreteCategory.hom (δ Δ[n] 0)) (stdSimplex.objEquiv.symm (SimplexCategory.σ 0)))).op))
        x,
      (ConcreteCategory.hom (δ Δ[1] 0)) (stdSimplex.objMk₁ 1)) =
    (ConcreteCategory.hom (ι₁.app (op ⦋n⦌))) x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (H.h.app (op ⦋n⦌)))
      ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  ((ConcreteCategory.hom (δ Δ[n] (Fin.last (n + 1))))
                    (stdSimplex.objEquiv.symm (SimplexCategory.σ (Fin.last n))))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] (Fin.last (n + 1)))) (stdSimplex.objMk₁ (Fin.last n).castSucc.succ)) =
    (ConcreteCategory.hom (H.h.app (op ⦋n⦌))) ((ConcreteCategory.hom (ι₀.app (op ⦋n⦌))) x)

Tactic:
apply congr_arg

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
x : X _⦋n⦌
⊢ ((ConcreteCategory.hom
          (X.map
            (stdSimplex.objEquiv
                ((ConcreteCategory.hom (δ Δ[n] (Fin.last (n + 1))))
                  (stdSimplex.objEquiv.symm (SimplexCategory.σ (Fin.last n))))).op))
        x,
      (ConcreteCategory.hom (δ Δ[1] (Fin.last (n + 1)))) (stdSimplex.objMk₁ (Fin.last n).castSucc.succ)) =
    (ConcreteCategory.hom (ι₀.app (op ⦋n⦌))) x
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
x : X _⦋n + 1⦌
⊢ (ConcreteCategory.hom (H.h.app (op ⦋n + 1⦌)))
      ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc))
                    (stdSimplex.objEquiv.symm (SimplexCategory.σ j.succ)))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] i.castSucc)) (stdSimplex.objMk₁ j.castSucc.succ.succ)) =
    (ConcreteCategory.hom (H.h.app (op ⦋n + 1⦌)))
      ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x)).app (op ⦋n + 1⦌)))
          (stdSimplex.objEquiv.symm (SimplexCategory.σ j)),
        stdSimplex.objMk₁ j.castSucc.succ)

Tactic:
apply congr_arg

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
x : X _⦋n + 1⦌
⊢ ((ConcreteCategory.hom
          (X.map
            (stdSimplex.objEquiv
                ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc))
                  (stdSimplex.objEquiv.symm (SimplexCategory.σ j.succ)))).op))
        x,
      (ConcreteCategory.hom (δ Δ[1] i.castSucc)) (stdSimplex.objMk₁ j.castSucc.succ.succ)) =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x)).app (op ⦋n + 1⦌)))
        (stdSimplex.objEquiv.symm (SimplexCategory.σ j)),
      stdSimplex.objMk₁ j.castSucc.succ)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
⊢ (ConcreteCategory.hom (H.h.app (op ⦋n + 1⦌)))
      ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                    (stdSimplex.objEquiv.symm (SimplexCategory.σ i.succ)))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.succ.succ)) =
    (ConcreteCategory.hom (H.h.app (op ⦋n + 1⦌)))
      ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                    (stdSimplex.objEquiv.symm (SimplexCategory.σ i.castSucc)))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.castSucc.succ))

Tactic:
apply congr_arg

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
x : X _⦋n + 1⦌
⊢ ((ConcreteCategory.hom
          (X.map
            (stdSimplex.objEquiv
                ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                  (stdSimplex.objEquiv.symm (SimplexCategory.σ i.succ)))).op))
        x,
      (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.succ.succ)) =
    ((ConcreteCategory.hom
          (X.map
            (stdSimplex.objEquiv
                ((ConcreteCategory.hom (δ Δ[n + 1] i.castSucc.succ))
                  (stdSimplex.objEquiv.symm (SimplexCategory.σ i.castSucc)))).op))
        x,
      (ConcreteCategory.hom (δ Δ[1] i.castSucc.succ)) (stdSimplex.objMk₁ i.castSucc.castSucc.succ))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Homotopy

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 1)
⊢ (↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ i.succ)) ≫
      δ Y i.castSucc.succ =
    (↾fun x ↦
        (ConcreteCategory.hom ((yonedaEquiv.symm x ▷ Δ[1] ≫ H.h).app (op ⦋n + 1 + 1⦌)))
          ↑(prodStdSimplex.nonDegenerateEquiv₁ i.castSucc)) ≫
      δ Y i.castSucc.succ

Tactic:
ext x
    simp only [TypeCat.Fun.toFun_apply, types_comp_apply, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      ← SSet.δ_naturality_apply]
    dsimp
    apply congr_arg
    ext k : 2
    · rw [stdSimplex.δ_objEquiv_symm_apply, stdSimplex.δ_objEquiv_symm_apply,
        SimplexCategory.δ_comp_σ_succ, ← Fin.castSucc_succ, SimplexCategory.δ_comp_σ_self]
    · rw [stdSimplex.δ_objMk₁_of_lt _ _ (by simp), stdSimplex.δ_objMk₁_of_le _ _ (by simp)]
      rfl

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

Goal state before:
pp: X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
⊢ (ConcreteCategory.hom (H.h.app (op ⦋n + 1⦌)))
      ((ConcreteCategory.hom
            (X.map
              (stdSimplex.objEquiv
                  ((ConcreteCategory.hom (δ Δ[n + 1] i.succ))
                    (stdSimplex.objEquiv.symm (SimplexCategory.σ j.castSucc)))).op))
          x,
        (ConcreteCategory.hom (δ Δ[1] i.succ)) (stdSimplex.objMk₁ j.castSucc.castSucc.succ)) =
    (ConcreteCategory.hom (H.h.app (op ⦋n + 1⦌)))
      ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x)).app (op ⦋n + 1⦌)))
          (stdSimplex.objEquiv.symm (SimplexCategory.σ j)),
        stdSimplex.objMk₁ j.castSucc.succ)

Tactic:
apply congr_arg

Goal state after:
X Y : SSet
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
x : X _⦋n + 1⦌
⊢ ((ConcreteCategory.hom
          (X.map
            (stdSimplex.objEquiv
                ((ConcreteCategory.hom (δ Δ[n + 1] i.succ))
                  (stdSimplex.objEquiv.symm (SimplexCategory.σ j.castSucc)))).op))
        x,
      (ConcreteCategory.hom (δ Δ[1] i.succ)) (stdSimplex.objMk₁ j.castSucc.castSucc.succ)) =
    ((ConcreteCategory.hom ((yonedaEquiv.symm ((ConcreteCategory.hom (δ X i)) x)).app (op ⦋n + 1⦌)))
        (stdSimplex.objEquiv.symm (SimplexCategory.σ j)),
      stdSimplex.objMk₁ j.castSucc.succ)
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:
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: