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

Goal state before:
pp: case succ
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
⊢ { s // X.spine (n + 1) s = p }

Tactic:
refine ⟨(h n).concat (p.arrow 0) (hn (p.interval 1 n)).val ?_, ?_⟩

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

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

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

Tactic:
by rw [δ₀_spineToSimplex, ← hn (X.δ 0 s), spine_δ₀]

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 : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ Hom.base (hComp (𝟙 (𝟙 a)) η) = Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)

Tactic:
simp only [hComp, Hom.base_id, base_mk, ← heq_eq_eq, 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 : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ CatEnriched.hComp (𝟙 (homEquiv (𝟙 a))) (Hom.base η) ≍ Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ Hom.base (hComp η (𝟙 (𝟙 b))) = Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)

Tactic:
simp only [hComp, Hom.base_id, base_mk, ← heq_eq_eq, 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 : CatEnrichedOrdinary C
f f' : a ⟶ b
η : f ⟶ f'
⊢ CatEnriched.hComp (Hom.base η) (𝟙 (homEquiv (𝟙 b))) ≍ Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)
Module: Mathlib.CategoryTheory.Functor.FunctorHom

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
X : C
x y : (F.functorHom G).obj X
h : ∀ (Y : C) (f : X ⟶ Y), x.app Y f = y.app Y f
⊢ x.app = y.app

Tactic:
by ext; apply h

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

Goal state before:
pp: X Y : SSet
S : X.Subcomplex
T : Y.Subcomplex
⊢ (S.unionProd T).preimage (β_ X Y).inv = T.unionProd S

Tactic:
by
  apply preimage_β_hom

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (inclusion n).op.HasRightKanExtension F
⊢ X.IsCoskeletal n ↔ IsIso ((coskAdj n).unit.app X)

Tactic:
rw [isCoskeletal_iff]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
inst✝ : ∀ (F : (SimplexCategory.Truncated n)ᵒᵖ ⥤ C), (inclusion n).op.HasRightKanExtension F
⊢ IsRightKanExtension X (𝟙 ((inclusion n).op ⋙ X)) ↔ IsIso ((coskAdj n).unit.app X)
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
W : MorphismProperty (FreeRefl V)
inst✝ : W.IsMultiplicative
hW : ∀ {x y : V} (e : x ⟶ y), W (homMk e)
⊢ morphismPropertyHomMk V ≤ W

Tactic:
rintro _ _ _ ⟨h⟩

Goal state after:
V : Type u_1
inst✝¹ : ReflQuiver V
W : MorphismProperty (FreeRefl V)
inst✝ : W.IsMultiplicative
hW : ∀ {x y : V} (e : x ⟶ y), W (homMk e)
X Y : FreeRefl V
h : (x : V) × (y : V) × (x ⟶ y)
⊢ W (homMk h.snd.snd)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case zero
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hij : i ≤ i
hj : i ≤ n
this : mkOfLe ⟨i, ⋯⟩ ⟨i, ⋯⟩ ⋯ = ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1 ⟶
  strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
⊢ (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩).op))
      (sx.spineToSimplex
        {
          vertex := fun i ↦
            (ConcreteCategory.hom
                (s.π.app
                  (StructuredArrow.mk
                    (((inclusion 2).obj (unop (op { obj := ⦋0⦌, property := lift._proof_2 }))).const ⦋n⦌ i).op)))
              x,
          arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
          arrow_src := ⋯, arrow_tgt := ⋯ }) =
    (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩).op))) x

Tactic:
StrictSegal.spineToSimplex_vertex

Goal state after:
case zero
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hij : i ≤ i
hj : i ≤ n
this : mkOfLe ⟨i, ⋯⟩ ⟨i, ⋯⟩ ⋯ = ⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩
α : strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1 ⟶
  strArrowMk₂ (⦋1⦌.const ⦋0⦌ 0 ≫ ⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_3 :=
  homMk (Hom.tr (⦋1⦌.const ⦋0⦌ 0) ⋯ ⋯).op ⋯
⊢ Path.vertex
      {
        vertex := fun i ↦
          (ConcreteCategory.hom
              (s.π.app
                (StructuredArrow.mk
                  (((inclusion 2).obj (unop (op { obj := ⦋0⦌, property := lift._proof_2 }))).const ⦋n⦌ i).op)))
            x,
        arrow := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x,
        arrow_src := ⋯, arrow_tgt := ⋯ }
      ⟨i, ⋯⟩ =
    (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩).op))) x
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
hf : r.degHom f = r.deg X
⊢ W₂ f

Tactic:
obtain ⟨Z, p, i, hp, hi, fac, h⟩ := r.exists_fac f

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
hf : r.degHom f = r.deg X
Z : C
p : X ⟶ Z
i : Z ⟶ Y
hp : W₁ p
hi : W₂ i
fac : p ≫ i = f
h : r.degHom f = r.deg Z
⊢ W₂ f
Module: Mathlib.AlgebraicTopology.Reedy.Basic

Goal state before:
pp: C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
hf : r.degHom f = r.deg Y
⊢ W₁ f

Tactic:
obtain ⟨Z, p, i, hp, hi, fac, h⟩ := r.exists_fac f

Goal state after:
C : Type u_1
inst✝⁶ : Category.{v_1, u_1} C
W₁ W₂ : MorphismProperty C
inst✝⁵ : W₁.IsMultiplicative
inst✝⁴ : W₂.IsMultiplicative
α : Type u_2
inst✝³ : LinearOrder α
inst✝² : OrderBot α
inst✝¹ : SuccOrder α
inst✝ : WellFoundedLT α
r : ReedyStructure W₁ W₂ α
X Y : C
f : X ⟶ Y
hf : r.degHom f = r.deg Y
Z : C
p : X ⟶ Z
i : Z ⟶ Y
hp : W₁ p
hi : W₂ i
fac : p ≫ i = f
h : r.degHom f = r.deg Z
⊢ W₁ f
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
δ_comp : ∀ {n m : ℕ} (u : mk (m + 1) ⟶ mk n) (i : Fin (m + 2)), P u → P (δ i ≫ u)
σ_comp : ∀ {n m : ℕ} (u : mk m ⟶ mk n) (i : Fin (m + 1)), P u → P (σ i ≫ u)
a b : SimplexCategoryGenRel
f✝ : a ⟶ b
X✝ Y✝ : SimplexCategoryGenRel
f : X✝ ⟶ Y✝
hf : generators.multiplicativeClosure' f
⊢ P f

Tactic:
induction hf with
  | of f h =>
    rcases h with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using! (δ_comp (𝟙 _) i id)
    · simpa using! (σ_comp (𝟙 _) i id)
  | id n => exact id
  | of_comp f g hf hg hrec =>
    rcases hf with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using! (δ_comp g i hrec)
    · simpa using! (σ_comp g i hrec)

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ δ i.succ ≫ σ i = 𝟙 (mk n)

Tactic:
by
  apply CategoryTheory.Quotient.sound
  exact FreeSimplexQuiver.homRel.δ_comp_σ_succ

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

Goal state before:
pp: case singleton
x✝ m : ℕ
⊢ IsAdmissible m [x✝] ↔ List.IsChain (fun x1 x2 ↦ x1 < x2) [x✝] ∧ ∀ (k : ℕ) (h : k < [x✝].length), [x✝][k] ≤ m + k

Tactic:
| singleton _ =>

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

Goal state before:
pp: m : ℕ
L : List ℕ
hL : IsAdmissible m L
j : ℕ
hj : j ∈ L
⊢ j < m + L.length ∧ simplicialEvalσ L j = simplicialEvalσ L (j + 1)

Tactic:
grind [List.mem_iff_getElem]

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

Goal state before:
pp: case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
h : ¬i.castSucc < (S.min' hS).castSucc
⊢ 1 = (ConcreteCategory.hom f) i

Tactic:
simp only [Fin.castSucc_lt_castSucc_iff, Finset.lt_min'_iff, not_forall,
        not_lt] at h

Goal state after:
case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
h : ∃ x, ∃ (_ : x ∈ S), x ≤ i
⊢ 1 = (ConcreteCategory.hom f) i
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ (if i.castSucc < Fin.last (n + 1) then 0 else 1) = (ConcreteCategory.hom f) i

Tactic:
rw [if_pos (by simp)]

Goal state after:
case neg
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ 0 = (ConcreteCategory.hom f) i
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
h' : ∀ b ∈ finset f x, y.castSucc ≤ b
i : Fin (n + 1)
hi : i < y
this : x ≤ (f i).castSucc
⊢ y ≤ i

Tactic:
simpa using h' i.castSucc (by simpa)

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

Tactic:
rw [e₁, e₂]

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 ⋯)) (Fin.cast ⋯ (Fin.castAdd (x₂.len + 1) i)))) =
    Fin.cast ⋯ (Fin.castAdd (y₂.len + 1) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₁)) i))
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 (inr' x₁ x₂)) i = Fin.cast ⋯ (Fin.natAdd x₁.len.succ i)
e₂ :
  (SimplexCategory.Hom.toOrderHom (inr' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i) =
    Fin.cast ⋯ (Fin.natAdd y₁.len.succ ((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 (inr' x₁ x₂)) i))) =
    (SimplexCategory.Hom.toOrderHom (inr' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i)

Tactic:
rw [e₁, e₂]

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 (inr' x₁ x₂)) i = Fin.cast ⋯ (Fin.natAdd x₁.len.succ i)
e₂ :
  (SimplexCategory.Hom.toOrderHom (inr' y₁ y₂)) ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i) =
    Fin.cast ⋯ (Fin.natAdd y₁.len.succ ((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 ⋯)) (Fin.cast ⋯ (Fin.natAdd x₁.len.succ i)))) =
    Fin.cast ⋯ (Fin.natAdd y₁.len.succ ((SimplexCategory.Hom.toOrderHom (WithInitial.down f₂)) i))
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
x : Fin (n + 2)
⊢ map' { toFun := i.predAbove, monotone' := ⋯ } x = i.succ.castSucc.succAbove x

Tactic:
obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last
  · by_cases! hi : i < x
    · rw [Fin.succAbove_of_le_castSucc _ _ (by simpa), Fin.succ_castSucc, map'_eq_castSucc_iff]
      simp only [OrderHom.coe_mk, Fin.castSucc_le_castSucc_iff, Fin.castSucc_lt_castSucc_iff]
      constructor
      · rw [Fin.predAbove_of_castSucc_lt _ _
          (by simpa only [Fin.castSucc_lt_succ_iff] using hi.le), Fin.pred_succ]
      · intro j hj
        by_cases! h : i.castSucc < j
        · rwa [Fin.predAbove_of_castSucc_lt _ _ h, ← Fin.succ_lt_succ_iff,
            Fin.succ_pred]
        · rw [Fin.predAbove_of_le_castSucc _ _ h, ← Fin.castSucc_lt_castSucc_iff,
            Fin.castSucc_castPred]
          exact lt_of_le_of_lt h hi
    · rw [Fin.succAbove_of_castSucc_lt _ _ (by simpa), map'_eq_castSucc_iff]
      simp only [OrderHom.coe_mk, Fin.castSucc_le_castSucc_iff, Fin.castSucc_lt_castSucc_iff]
      constructor
      · simp only [i.predAbove_of_le_castSucc x.castSucc (by simpa),
          Fin.castPred_castSucc, le_refl]
      · 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]
  · simp [map'_last]

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : h.IsProper
f : h.RankFunction α
⊢ h.pairing.IsRegular

Tactic:
exact (h.rankFunctionEquiv α f).isRegular

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := ⋯
U : Type := ⋯
ψ : U → X.S := ⋯
φ : T → U
hφ : ∀ (t : T), ψ (φ t) = (↑↑t).toS
⊢ Function.Injective φ

Tactic:
intro t₁ t₂ h

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
T : Type (max 0 u) := { x // P.AncestralRel x y }
U : Type := (d : Fin (↑(P.p y)).dim) × (⦋↑d⦌ ⟶ ⦋(↑(P.p y)).dim⦌)
ψ : U → X.S :=
  fun x ↦
    match x with
    | ⟨d, f⟩ => { dim := ↑d, simplex := (CategoryTheory.ConcreteCategory.hom (X.map f.op)) (↑(P.p y)).simplex }
φ : T → U
hφ : ∀ (t : T), ψ (φ t) = (↑↑t).toS
t₁ t₂ : T
h : φ t₁ = φ t₂
⊢ t₁ = t₂
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: 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
⊢ IsLimit (((evaluation D C).obj k).mapCone (combine f g c hc))

Tactic:
by
    refine IsLimit.equivOfNatIsoOfIso ?_ _ _ ?_ (hc k)
    · exact cospanIsoMk (Iso.refl _) (Iso.refl _) (Iso.refl _)
    · refine Cone.ext (Iso.refl _) ?_
      rintro (_ | _ | _)
      all_goals cat_disch

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✝ : P.IsProper
j : ι
c : f.Cell j
⊢ (f.filtration j).preimage c.map ≤ c.horn

Tactic:
simpa only [subcomplex_le_horn_iff, ← Subcomplex.image_le_iff,
      Cell.image_face_index_compl] using c.subcomplex_not_le_filtration

Goal state after:
Module: Mathlib.CategoryTheory.ExtremalEpi

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacks C
x✝¹ : ExtremalEpi f
A B : C
i : A ⟶ B
x✝ : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (pullback.snd i b)
⊢ (f ≫ inv (pullback.snd i b) ≫ pullback.fst i b) ≫ i = t ≫ i

Tactic:
sq.w,

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacks C
x✝¹ : ExtremalEpi f
A B : C
i : A ⟶ B
x✝ : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (pullback.snd i b)
⊢ (f ≫ inv (pullback.snd i b) ≫ pullback.fst i b) ≫ i = f ≫ b
Module: Mathlib.CategoryTheory.ExtremalEpi

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacks C
x✝¹ : ExtremalEpi f
A B : C
i : A ⟶ B
x✝ : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (pullback.snd i b)
⊢ f ≫ inv (pullback.snd i b) ≫ pullback.fst i b = t

Tactic:
rw [← cancel_mono i, sq.w, Category.assoc, Category.assoc]

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
X Y : C
f : X ⟶ Y
inst✝ : HasPullbacks C
x✝¹ : ExtremalEpi f
A B : C
i : A ⟶ B
x✝ : Mono i
t : X ⟶ A
b : Y ⟶ B
sq : CommSq t f i b
this : IsIso (pullback.snd i b)
⊢ f ≫ inv (pullback.snd i b) ≫ pullback.fst i b ≫ i = f ≫ b
Module: Mathlib.CategoryTheory.Generator.StrongGenerator

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
inst✝² : HasCoproducts C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : ObjectProperty.Small.{w, v, u} P
⊢ P.IsStrongGenerator ↔ ∀ (X : C), ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, ExtremalEpi p

Tactic:
refine ⟨fun hP X ↦ ?_, fun hP ↦ .mk_of_exists_extremalEpi hP⟩

Goal state after:
C : Type u
inst✝³ : Category.{v, u} C
P : ObjectProperty C
inst✝² : HasCoproducts C
inst✝¹ : LocallySmall.{w, v, u} C
inst✝ : ObjectProperty.Small.{w, v, u} P
hP : P.IsStrongGenerator
X : C
⊢ ∃ ι s, ∃ (_ : ∀ (i : ι), P (s i)), ∃ c x p, ExtremalEpi p
Module: Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
P' : ObjectProperty C
h₁ : P ≤ P'.isoClosure
h₂ : P' ≤ isCardinalPresentable C κ
X : C
⊢ ∃ J x, ∃ (_ : IsCardinalFiltered J κ), P'.colimitsOfShape J X

Tactic:
obtain ⟨J, _, _, hX⟩ := h.exists_colimitsOfShape X
    exact ⟨J, inferInstance, inferInstance, by
      simpa only [colimitsOfShape_isoClosure] using colimitsOfShape_monotone J h₁ _ hX⟩

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
P : ObjectProperty C
κ : Cardinal.{w}
inst✝ : Fact κ.IsRegular
h : P.IsCardinalFilteredGenerator κ
P' : ObjectProperty C
h₁ : P ≤ P'.isoClosure
h₂ : P' ≤ isCardinalPresentable C κ
X : C
⊢ ∃ J x, ∃ (_ : IsCardinalFiltered J κ), P'.colimitsOfShape J X

Tactic:
by
    obtain ⟨J, _, _, hX⟩ := h.exists_colimitsOfShape X
    exact ⟨J, inferInstance, inferInstance, by
      simpa only [colimitsOfShape_isoClosure] using colimitsOfShape_monotone J h₁ _ hX⟩

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)
j : J
x₁ x₂ : c.pt.obj (X.obj j)
h : (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₁ = (ConcreteCategory.hom (c.pt.map (cX.ι.app j))) x₂
this : IsFiltered J
y₁ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₁
y₂ : ↑(F ⋙ (evaluation C (Type w')).obj (X.obj j)).sections := (Types.isLimitEquivSections (hc (X.obj j))) x₂
hy₁ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₁ = x₁
hy₂ : (Types.isLimitEquivSections (hc (X.obj j))).symm y₂ = x₂
k : K
⊢ (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j))) ((ConcreteCategory.hom ((c.π.app k).app (X.obj j))) x₁) =
    (ConcreteCategory.hom ((F.obj k).map (cX.ι.app j))) ((ConcreteCategory.hom ((c.π.app k).app (X.obj j))) x₂)

Tactic:
simp only [← NatTrans.naturality_apply, h]

Goal state after: