mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.DoldKan.NCompGamma

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
P : Karoubi (SimplicialObject C)
⊢ natTrans.app P = (N₂ ⋙ Γ₂).map P.decompId_i ≫ (Γ₂N₂ToKaroubiIso.hom ≫ Γ₂N₁.natTrans).app P.X ≫ P.decompId_p

Tactic:
by
  dsimp only [natTrans]
  simp only [whiskeringLeft_obj_preimage_app, Functor.id_map]

Goal state after:
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
⊢ (S₁.s.cofan (op ⦋j⦌)).inj A ≫
      ((alternatingFaceMapComplex C).map Φ.F).f j ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) =
    (S₁.s.cofan (op ⦋j⦌)).inj A ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j

Tactic:
dsimp [alternatingFaceMapComplex]

Goal state after:
case e_a
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : Preadditive C
inst✝ : HasFiniteCoproducts C
S₁ S₂ : Split C
Φ : S₁ ⟶ S₂
i j : ℕ
x✝ : (ComplexShape.down ℕ).Rel i j
A : Splitting.IndexSet (op ⦋j⦌)
⊢ (S₁.s.cofan (op ⦋j⦌)).inj A ≫ Φ.F.app (op ⦋j⦌) ≫ S₂.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) =
    (S₁.s.cofan (op ⦋j⦌)).inj A ≫ S₁.s.πSummand (Splitting.IndexSet.id (op ⦋j⦌)) ≫ Φ.f j
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
⊢ F.eval 0 = p₀

Tactic:
ext t

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : ↑I
⊢ (F.eval 0) t = p₀ t
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
⊢ F.eval 1 = p₁

Tactic:
ext t

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₀ p₁ : Path x₀ x₁
F : p₀.Homotopy p₁
t : ↑I
⊢ (F.eval 1) t = p₁ t
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Homotopic.Quotient x y
⊢ γ.cast ⋯ ⋯ = γ

Tactic:
induction γ using Quotient.ind with | mk γ =>
  rfl

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x y : X
γ : Homotopic.Quotient x y
x' y' : X
hx : x' = x
hy : y' = y
x'' y'' : X
hx' : x'' = x'
hy' : y'' = y'
⊢ (γ.cast hx hy).cast hx' hy' = γ.cast ⋯ ⋯

Tactic:
induction γ using Quotient.ind with | mk γ =>
  rfl

Goal state after:
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), p₁ t = p₂ t
⊢ p₁ = p₂

Tactic:
ext t

Goal state after:
X : Type u
inst✝ : TopologicalSpace X
x₀ x₁ : X
p₁ p₂ : Path x₀ x₁
hp : ∀ (t : ↑I), p₁ t = p₂ t
t : ↑I
⊢ p₁ t = p₂ t
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'
⊢ Function.Bijective (rightHomotopyClassToHom L)

Tactic:
have hX' := this X' inferInstance

Goal state after:
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)
⊢ Function.Bijective (rightHomotopyClassToHom L)
Module: Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy

Goal state before:
pp: case refine_2.refine_1
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
h : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj ⟶ X.obj
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 X.obj)
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 Y.obj)
⊢ F.map f ≫ F.map (homMk g') = 𝟙 (F.obj X)

Tactic:
rw [← F.map_comp, ← F.map_id]
      apply h
      assumption

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

Goal state before:
pp: case refine_2.refine_2
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
D : Type u_1
inst✝ : Category.{v_1, u_1} D
F : BifibrantObject C ⥤ D
h : ∀ ⦃K L : BifibrantObject C⦄ (f g : K ⟶ L), homRel C f g → F.map f = F.map g
X Y : BifibrantObject C
f : X ⟶ Y
hf : WeakEquivalence f.hom
g' : Y.obj ⟶ X.obj
h₁ : RightHomotopyRel (f.hom ≫ g') (𝟙 X.obj)
h₂ : RightHomotopyRel (g' ≫ f.hom) (𝟙 Y.obj)
⊢ F.map (homMk g') ≫ F.map f = 𝟙 (F.obj Y)

Tactic:
rw [← F.map_comp, ← F.map_id]
      apply h
      assumption

Goal state after:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := (c.multispanIndex.map Set.functorToTypes).multispan
⊢ IsColimit (c.multicofork.map Set.functorToTypes)

Tactic:
apply _root_.Nonempty.some

Goal state after:
X : Type u
ι : Type w
A : Set X
U : ι → Set X
V : ι → ι → Set X
c : MulticoequalizerDiagram A U V
e : WalkingMultispan (MultispanShape.prod ι) ⥤ Type u := ⋯
⊢ Nonempty (IsColimit (c.multicofork.map Set.functorToTypes))
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
z₁ : X₁
hyz :
  (ConcreteCategory.hom f) y₀✝ = z₁ ∨
    ∃ x₀ y₀,
      ∃ (_ : (ConcreteCategory.hom g) x₀ = (ConcreteCategory.hom g) y₀),
        (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) x₀ ∧ z₁ = (ConcreteCategory.hom f) y₀
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inl z₁)

Tactic:
obtain rfl | ⟨_, _, h', h'', rfl⟩ := hyz

Goal state after:
case inl_inl.inl.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inl ((ConcreteCategory.hom f) y₀✝))

case inl_inl.inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
w✝¹ w✝ : S
h' : (ConcreteCategory.hom g) w✝¹ = (ConcreteCategory.hom g) w✝
h'' : (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) w✝¹
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inl ((ConcreteCategory.hom f) w✝))
Module: Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝ : Cofibration f
⊢ Mono f

Tactic:
rwa [← cofibration_iff]

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

Goal state before:
pp: case a.right
⊢ stdSimplex.face {1, 2} ≤ Λ[2, 1]

Tactic:
exact face_le_horn (0 : Fin 3) 1 (by simp)

Goal state after:
Module: Mathlib.AlgebraicTopology.Quasicategory.InnerFibration

Goal state before:
pp: X : SSet
⊢ X.Quasicategory ↔ InnerFibration (terminal.from X)

Tactic:
rw [quasicategory_iff_hasLiftingProperty.{u} _ terminalIsTerminal, innerFibration_iff]

Goal state after:
X : SSet
⊢ (∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → HasLiftingProperty Λ[n, i].ι (terminalIsTerminal.from X)) ↔
    innerFibrations (terminal.from X)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X Y : SSet
i : X ⟶ Y
⊢ ⊤ ≤ ⨆ n, (skeletonOfMono i) n

Tactic:
rw [← Y.iSup_skeleton, iSup_le_iff]

Goal state after:
X Y : SSet
i : X ⟶ Y
⊢ ∀ (i_1 : ℕ), Y.skeleton i_1 ≤ ⨆ n, (skeletonOfMono i) n
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ X.spine l ⋯ ((ConcreteCategory.hom (X.map (tr (subinterval j l hjl) ⋯ h).op)) (sx.spineToSimplex m h f)) =
    f.interval j l hjl

Tactic:
convert! spine_map_subinterval X m h j l hjl <| sx.spineToSimplex m h f

Goal state after:
n : ℕ
X : Truncated (n + 1)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path m
j l : ℕ
hjl : j + l ≤ m
⊢ f = X.spine m h (sx.spineToSimplex m h f)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: case succ.refine_1
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
⊢ (ConcreteCategory.hom (SimplicialObject.δ X 0)) (p.arrow 0) =
    (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋n⦌ 0).op)) ↑(hn (p.interval 1 n ⋯))

pp: case succ.refine_2
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
⊢ X.spine (n + 1) ((h n).concat (p.arrow 0) ↑(hn (p.interval 1 n ⋯)) ?succ.refine_1) = p

Tactic:
· rw [p.arrow_tgt 0]
      exact Path.congr_vertex (hn (p.interval 1 n)).prop.symm 0

Goal state after:
case succ.refine_2
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
⊢ X.spine (n + 1) ((h n).concat (p.arrow 0) ↑(hn (p.interval 1 n ⋯)) ⋯) = p
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: case succ
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) = s

Tactic:
exact (h n).injective (map_mkOfSucc_zero_spineToSimplex _ _)
      (by rw [δ₀_spineToSimplex, ← hn (X.δ 0 s), spine_δ₀])

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V✝ : Type u'
inst✝⁷ : Category.{v', u'} V✝
inst✝⁶ : MonoidalCategory V✝
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
inst✝⁴ : EnrichedOrdinaryCategory V✝ C✝
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
P : ObjectProperty C
X✝ Y✝ Z✝ : P.FullSubcategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (eHomEquiv V) (P.ι.map (f ≫ g)) =
    (λ_ (𝟙_ V)).inv ≫
      ((P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) f ⊗ₘ (P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) g) ≫
        eComp V X✝ Y✝ Z✝

Tactic:
Functor.map_comp,

Goal state after:
V✝ : Type u'
inst✝⁷ : Category.{v', u'} V✝
inst✝⁶ : MonoidalCategory V✝
C✝ : Type u
inst✝⁵ : Category.{v, u} C✝
inst✝⁴ : EnrichedOrdinaryCategory V✝ C✝
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
P : ObjectProperty C
X✝ Y✝ Z✝ : P.FullSubcategory
f : X✝ ⟶ Y✝
g : Y✝ ⟶ Z✝
⊢ (eHomEquiv V) (P.ι.map f ≫ P.ι.map g) =
    (λ_ (𝟙_ V)).inv ≫
      ((P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) f ⊗ₘ (P.fullyFaithfulι.homEquiv.trans (eHomEquiv V)) g) ≫
        eComp V X✝ Y✝ Z✝
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case comp_homMk
V✝ : Type u_1
inst✝³ : ReflQuiver V✝
V : Type u_2
inst✝² : ReflQuiver V
inst✝¹ : Unique V
inst✝ : (x y : V) → Unique (x ⟶ y)
x✝ y✝ : FreeRefl V
x y z : V
f✝ : mk x ⟶ mk y
g : y ⟶ z
h : f✝ = homMk default
⊢ f✝ ≫ homMk g = homMk default

Tactic:
obtain rfl := Subsingleton.elim y z
      obtain rfl := Subsingleton.elim g (𝟙rq _)
      simp [h]

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

Goal state before:
pp: case h.comp.σ
x y : SimplexCategoryGenRel
x✝ y✝ : Paths FreeSimplexQuiver
u✝ : FreeSimplexQuiver
n✝ : ℕ
i✝ : Fin (n✝ + 1)
p✝ : (Paths.of FreeSimplexQuiver).obj u✝ ⟶ (Paths.of FreeSimplexQuiver).obj (FreeSimplexQuiver.mk (n✝ + 1))
h : generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map p✝)
⊢ generators.multiplicativeClosure
    ((Quotient.functor FreeSimplexQuiver.homRel).map
      (p✝ ≫ (Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.Hom.σ i✝)))

Tactic:
· exact generators.multiplicativeClosure.comp_mem _ _ h <| .of _ <| .σ _

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
n : ℕ
hn : n < d
i : Fin (n + 2)
⊢ { len := n }.len ≤ d

Tactic:
dsimp; lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
n : ℕ
hn : n < d
i : Fin (n + 2)
⊢ { len := n + 1 }.len ≤ d

Tactic:
dsimp; lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
n : ℕ
hn : n < d
i : Fin (n + 1)
⊢ { len := n + 1 }.len ≤ d

Tactic:
dsimp; lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
n : ℕ
hn : n < d
i : Fin (n + 1)
⊢ { len := n }.len ≤ d

Tactic:
dsimp; lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : toMk₁ i = toMk₁ j
hij : i < j
⊢ ↑j ≤ ⦋n⦌.len + 1

Tactic:
dsimp; lia

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: n : ℕ
⊢ Function.Surjective toMk₁

Tactic:
by
  intro f
  let S : Finset (Fin (n + 1)) := { i | f i = 1}
  by_cases hS : S.Nonempty
  · refine ⟨(S.min' hS).castSucc, ConcreteCategory.hom_ext _ _ (fun i ↦ ?_)⟩
    dsimp [toMk₁_apply]
    split_ifs with h
    · have hi : i ∉ S := fun hi ↦ by have := S.min'_le _ hi; grind
      #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
      goal. 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: `grind` -/
      simp [S] at hi; grind
    · simp only [Fin.castSucc_lt_castSucc_iff, Finset.lt_min'_iff, not_forall,
        not_lt] at h
      obtain ⟨j, hj, hij⟩ := h
      have := f.toOrderHom.monotone hij
      #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
      goal. 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:
      `grind [show f j ≤ f i from f.toOrderHom.monotone hij]` -/
      simp_all [ConcreteCategory.hom, S]
      grind
  · refine ⟨Fin.last _, ConcreteCategory.hom_ext _ _ (fun i ↦ ?_)⟩
    dsimp [toMk₁_apply]
    rw [if_pos (by simp)]
    obtain ⟨j, hj⟩ : ∃ (j : Fin 2), f i = j := ⟨_, rfl⟩
    fin_cases j
    · #adaptation_note /-- Before https://github.com/leanprover/lean4/pull/13166
      (replacing grind's canonicalizer with a type-directed normalizer), `grind` closed this
      goal. 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: `grind` -/
      simp_all
    · exact (hS ⟨i, by simpa [S]⟩).elim

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

Goal state before:
pp: ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
v : ι
⊢ {v} ∈ (⋂ K ∈ s, K.faces) ∩ {t | t.Nonempty}

Tactic:
by
        grind [Set.mem_iInter, Finset.singleton_nonempty, singleton_mem]

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

Goal state before:
pp: case mpr
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
i : Fin (d + 2)
h₁ : (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x
h₂ : ∀ (y_1 : Fin (d + 2)), (fun i ↦ (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x) y_1 → y_1 = i
f : ⦋{ dim := d, simplex := x }.dim⦌ ⟶ ⦋{ dim := d + 1, simplex := y }.dim⦌
x✝ :
  (fun f ↦
      Mono f ∧
        (ConcreteCategory.hom (X.map f.op)) { dim := d + 1, simplex := y }.simplex = { dim := d, simplex := x }.simplex)
    f
h₃ : Mono f
h₄ : (ConcreteCategory.hom (X.map f.op)) { dim := d + 1, simplex := y }.simplex = { dim := d, simplex := x }.simplex
⊢ f = SimplexCategory.δ i

Tactic:
obtain ⟨j, rfl⟩ := SimplexCategory.eq_δ_of_mono f

Goal state after:
case mpr
X : SSet
d : ℕ
x : X _⦋d⦌
y : X _⦋d + 1⦌
i : Fin (d + 2)
h₁ : (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x
h₂ : ∀ (y_1 : Fin (d + 2)), (fun i ↦ (ConcreteCategory.hom (SimplicialObject.δ X i)) y = x) y_1 → y_1 = i
j : Fin ({ dim := d, simplex := x }.dim + 2)
x✝ :
  Mono (SimplexCategory.δ j) ∧
    (ConcreteCategory.hom (X.map (SimplexCategory.δ j).op)) { dim := d + 1, simplex := y }.simplex =
      { dim := d, simplex := x }.simplex
h₃ : Mono (SimplexCategory.δ j)
h₄ :
  (ConcreteCategory.hom (X.map (SimplexCategory.δ j).op)) { dim := d + 1, simplex := y }.simplex =
    { dim := d, simplex := x }.simplex
⊢ SimplexCategory.δ j = SimplexCategory.δ i
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
x : A.N
⊢ ∃ s,
    x.toS = { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } ∨
      x.toS =
        { dim := (↑s).dim,
          simplex := (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s)).cast ⋯).simplex }

Tactic:
obtain ⟨s, rfl | rfl⟩ := P.exists_or x
    · refine ⟨s, Or.inr ?_⟩
      simp [(P.isUniquelyCodimOneFace s).δ_index]
    · refine ⟨s, Or.inl ?_⟩
      nth_rw 1 [← (P.p s).val.cast_eq_self (P.isUniquelyCodimOneFace s).dim_eq]
      rfl

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

Goal state before:
pp: 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
⊢ IsIso A.arrow

Tactic:
exact hS₂ A.arrow (fun G hG g ↦ ⟨_, Subobject.factorThru_arrow _ _ (hA G hG g)⟩)

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

Goal state before:
pp: case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : IsCardinalPresentable X κ
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
this : EssentiallySmall.{w, w, w} J
⊢ P.retractClosure X

Tactic:
obtain ⟨j, f, hf⟩ := IsCardinalPresentable.exists_hom_of_isColimit κ p.isColimit (𝟙 X)

Goal state after:
case refine_1
C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
X : C
hX : IsCardinalPresentable X κ
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ
p : P.ColimitOfShape J X
this : EssentiallySmall.{w, w, w} J
j : J
f : X ⟶ p.diag.obj j
hf : f ≫ { pt := X, ι := p.ι }.ι.app j = 𝟙 X
⊢ P.retractClosure X
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ { dim := c.dim,
      simplex :=
        ↑((ConcreteCategory.hom ((f.b j).app (op ⦋c.dim⦌)))
            ((ConcreteCategory.hom (c.ιSigmaStdSimplex.app (op ⦋c.dim⦌)))
              (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index)))) } =
    { dim := (↑c.s).dim, simplex := (↑c.s).simplex }

Tactic:
rw [S.ext_iff, c.ι_b_app_apply, Cell.mapToSucc]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
c : f.Cell j
⊢ ↑((ConcreteCategory.hom ((lift c.map ⋯).app (op ⦋c.dim⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ c.index))) =
    (↑c.s).simplex
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: A B X Y : SSet
i : A ⟶ B
hi : modelCategoryQuillen.J i
f : X ⟶ Y
hf : RelativeCellComplex (fun x ↦ modelCategoryQuillen.J.homFamily) f
⊢ Limits.PreservesColimit hf.F (coyoneda.obj (Opposite.op A))

Tactic:
have : IsFinitelyPresentable.{u} A := by
      simp only [modelCategoryQuillen.J, iSup_iff] at hi
      obtain ⟨n, ⟨i⟩⟩ := hi
      infer_instance

Goal state after:
A B X Y : SSet
i : A ⟶ B
hi : modelCategoryQuillen.J i
f : X ⟶ Y
hf : RelativeCellComplex (fun x ↦ modelCategoryQuillen.J.homFamily) f
this : IsFinitelyPresentable A
⊢ Limits.PreservesColimit hf.F (coyoneda.obj (Opposite.op A))
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Basic

Goal state before:
pp: X✝ Y✝ Z✝ : SSet
e : Y✝ ⟶ Z✝
x✝ : isomorphisms SSet e
f : X✝ ⟶ Y✝
left✝ : Mono f
P : (Subcomplex.range f).Pairing
hP : P.IsRegular
⊢ (Subcomplex.range f).preimage (asIso e).symm.hom = Subcomplex.range (f ≫ e)

Tactic:
simp [Subcomplex.preimage_inv, Subcomplex.range_comp]

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

Goal state before:
pp: X✝ Y✝ Z✝ : SSet
e : Y✝ ⟶ Z✝
x✝ : isomorphisms SSet e
f : X✝ ⟶ Y✝
left✝ : Mono f
P : (Subcomplex.range f).Pairing
hP : P.IsRegular
hP' : P.IsInner
⊢ (Subcomplex.range f).preimage (asIso e).symm.hom = Subcomplex.range (f ≫ e)

Tactic:
simp [Subcomplex.preimage_inv, Subcomplex.range_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
Q : C
⊢ f ▷ Q ≫ inl ▷ Q = g ▷ Q ≫ inr ▷ Q

Tactic:
simp [← MonoidalCategory.comp_whiskerRight, hP.w]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight W)
⊢ (tensorRight W).map (pushout.inl (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) ≫
      (⋯.isoPushout ≪≫
            HasColimit.isoOfNatIso
              (spanExt (α_ X₁.left X₂.left W) (α_ X₁.right X₂.left W) (α_ X₁.left X₂.right W) ⋯ ⋯)).hom ≫
        (X₁ □ Arrow.mk (X₂.hom ▷ W)).hom =
    (tensorRight W).map (pushout.inl (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) ≫
      (Arrow.mk ((X₁ □ X₂).hom ▷ W)).hom ≫ (α_ X₁.right X₂.right W).hom

Tactic:
simp [← comp_whiskerRight_assoc]

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

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasPushouts C
inst✝¹ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight W)
⊢ (tensorRight W).map (pushout.inr (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) ≫
      (⋯.isoPushout ≪≫
            HasColimit.isoOfNatIso
              (spanExt (α_ X₁.left X₂.left W) (α_ X₁.right X₂.left W) (α_ X₁.left X₂.right W) ⋯ ⋯)).hom ≫
        (X₁ □ Arrow.mk (X₂.hom ▷ W)).hom =
    (tensorRight W).map (pushout.inr (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) ≫
      (Arrow.mk ((X₁ □ X₂).hom ▷ W)).hom ≫ (α_ X₁.right X₂.right W).hom

Tactic:
simp [← comp_whiskerRight_assoc]

Goal state after: