mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.Quasicategory.Basic

Goal state before:
pp: S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
      (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
⊢ ∀ (j : Fin (n + 1 + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h) =
      (ConcreteCategory.hom ((Λ[n + 2, i].ι ≫ yonedaEquiv.symm σ).app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)

Tactic:
intro j hj

Goal state after:
S : SSet
filler :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 3)⦄ (σ₀ : Λ[n + 2, i].toSSet ⟶ S),
    0 < i →
      i < Fin.last (n + 2) →
        ∃ σ,
          ∀ (j : Fin (n + 3)) (h : j ≠ i),
            (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
              (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ S
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
σ : S _⦋n + 2⦌
h :
  ∀ (j : Fin (n + 3)) (h : j ≠ i),
    (ConcreteCategory.hom (SimplicialObject.δ S j)) σ =
      (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)
j : Fin (n + 1 + 2)
hj : j ≠ i
⊢ (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j hj) =
    (ConcreteCategory.hom ((Λ[n + 2, i].ι ≫ yonedaEquiv.symm σ).app (Opposite.op ⦋n + 1⦌))) (horn.face i j hj)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HornColimits

Goal state before:
pp: case succ.e_a
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
⊢ stdSimplex.δ (k.succ.pred ⋯) ≫ stdSimplex.δ j.castSucc = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ stdSimplex.δ k.succ

Tactic:
Fin.pred_succ,

Goal state after:
case succ.e_a
X : SSet
n : ℕ
i : Fin (n + 1 + 2)
g : Λ[n + 1 + 1, i].toSSet ⟶ X
j : Fin (n + 2)
hj : j.castSucc ≠ i
k : Fin (n + 2)
hk : k.succ ≠ i
hjk : j.castSucc < k.succ
⊢ stdSimplex.δ k ≫ stdSimplex.δ j.castSucc = stdSimplex.δ (j.castSucc.castPred ⋯) ≫ stdSimplex.δ k.succ
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
⊢ ∀ (j : Fin (n + 3)) (h : j ≠ i),
    (ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) =
      (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j h)

Tactic:
intro j hj

Goal state after:
case h
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
⊢ (ConcreteCategory.hom (SimplicialObject.δ X j)) (sx.spineToSimplex ((horn.spineId i h₀ hₙ).map σ₀)) =
    (ConcreteCategory.hom (σ₀.app (Opposite.op ⦋n + 1⦌))) (horn.face i j hj)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u_1
inst✝ : EnrichedCategory Cat C
a b : CatEnriched C
f f' : a ⟶ b
η : f ⟶ f'
⊢ hComp (𝟙 (𝟙 a)) η = eqToHom ⋯ ≫ η ≫ eqToHom ⋯

Tactic:
simp [← heq_eq_eq, id_hComp_heq]

Goal state after:
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c : CatEnrichedOrdinary C
f₁ f₂ f₃ : a ⟶ b
g₁ g₂ g₃ : b ⟶ c
η : f₁ ⟶ f₂
η' : f₂ ⟶ f₃
θ : g₁ ⟶ g₂
θ' : g₂ ⟶ g₃
⊢ hComp η θ ≫ hComp η' θ' = hComp (η ≫ η') (θ ≫ θ')

Tactic:
simp [hComp, ← CatEnriched.hComp_comp, Hom.comp_eq]

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case mk.mk.nil
V : Type u_1
inst✝ : ReflQuiver V
motive : {x y : FreeRefl V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk : ∀ {x y z : V} (f : mk x ⟶ mk y) (g : y ⟶ z), motive f → motive (f ≫ homMk g)
x y : V
⊢ motive ((quotientFunctor V).map Quiver.Path.nil)

Tactic:
| nil =>

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case comp_homMk
V : Type u_1
inst✝ : ReflQuiver V
X✝ Y✝ : FreeRefl V
x✝ y✝ z✝ : V
f✝ : mk x✝ ⟶ mk y✝
g✝ : y✝ ⟶ z✝
h : (morphismPropertyHomMk V).multiplicativeClosure f✝
⊢ (morphismPropertyHomMk V).multiplicativeClosure (f✝ ≫ homMk g✝)

Tactic:
exact comp_mem _ _ _ h (le_multiplicativeClosure _ _ (morphismPropertyHomMk_homMk _))

Goal state after:
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)
⊢ ⊤ ≤ W

Tactic:
rw [← multiplicativeClosure_morphismPropertyHomMk,
      MorphismProperty.multiplicativeClosure_le_iff]
    rintro _ _ _ ⟨h⟩
    apply hW

Goal state after:
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
fac fac' : W₁.MapFactorizationData W₂ f
⊢ fac.Z = fac'.Z

Tactic:
have := r.subsingleton_mapFactorizationData 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
fac fac' : W₁.MapFactorizationData W₂ f
this : Subsingleton (W₁.MapFactorizationData W₂ f)
⊢ fac.Z = fac'.Z
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
fac fac' : W₁.MapFactorizationData W₂ f
⊢ ∃ (h : fac.Z = fac'.Z), fac.i = fac'.i ≫ eqToHom ⋯ ∧ fac.p = eqToHom h ≫ fac'.p

Tactic:
have := r.subsingleton_mapFactorizationData 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
fac fac' : W₁.MapFactorizationData W₂ f
this : Subsingleton (W₁.MapFactorizationData W₂ f)
⊢ ∃ (h : fac.Z = fac'.Z), fac.i = fac'.i ≫ eqToHom ⋯ ∧ fac.p = eqToHom h ≫ fac'.p
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

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

Tactic:
| nil =>

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

Goal state before:
pp: case nil
m : ℕ
hL : IsAdmissible (m + 1) []
j : ℕ
hj : j ≤ m
⊢ IsAdmissible m (simplicialInsert j [])

Tactic:
| nil =>

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

Goal state before:
pp: m : ℕ
L : List ℕ
hL : IsAdmissible (m + 1) L
j : ℕ
hj : j ≤ m
⊢ IsAdmissible m (simplicialInsert j L)

Tactic:
induction L generalizing j m with

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

Goal state before:
pp: case nil
L₁ : List ℕ
m₁ m₂ m₃ : ℕ
h : m₂ + L₁.length = m₁
h' : m₃ + [].length = m₂
⊢ standardσ L₁ h ≫ standardσ [] h' = standardσ ([] ++ L₁) ⋯

Tactic:
| nil =>

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

Goal state before:
pp: case nil
L : List ℕ
j : ℕ
hj : ∀ k ∈ [], j ≤ k
⊢ simplicialEvalσ [] j = j

Tactic:
| nil =>

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

Goal state before:
pp: case nil
L : List ℕ
j m₁ m₂ : ℕ
hL : IsAdmissible m₂ []
hk : m₂ + [].length = m₁
hj : j < m₁ + 1
⊢ ↑((SimplexCategory.Hom.toOrderHom (toSimplexCategory.map (standardσ [] hk))) ⟨j, hj⟩) = simplicialEvalσ [] j

Tactic:
| nil =>

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

Goal state before:
pp: case nil
m₁ m : ℕ
hL : IsAdmissible (m + 1) []
j : ℕ
hj : j < m + 1
hm₁ : m + [].length + 1 = m₁
⊢ standardσ (simplicialInsert j []) ⋯ = standardσ [] ⋯ ≫ σ (Fin.ofNat (m + 1) j)

Tactic:
| nil =>

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

Goal state before:
pp: case nil
j m : ℕ
hL : IsAdmissible m []
hj₁ : j < m + [].length
hj₂ : simplicialEvalσ [] j = simplicialEvalσ [] (j + 1)
⊢ j ∈ []

Tactic:
| nil =>

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

Goal state before:
pp: X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
z₀ z₁ : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge z₀ z₁
⊢ (mapHomotopyCategory (α_ X Y Z).hom).map
        ((inverse (X ⊗ Y) Z).map (Prod.mkHom ((inverse X Y).map (Prod.mkHom (𝟙 (mk x)) (𝟙 (mk y)))) (homMk e))) ≫
      𝟙
        ((((Functor.curry₃.obj
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                  (mk x)).obj
              (mk y)).obj
          (mk z₁)) =
    𝟙
        ((((Functor.curry₃.obj
                      (prod.inverseAssociator X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory ⋙
                        (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙
                          inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom)).obj
                  (mk x)).obj
              (mk y)).obj
          (mk z₀)) ≫
      (inverse X (Y ⊗ Z)).map (Prod.mkHom (𝟙 (mk x)) ((inverse Y Z).map (𝟙 (mk y), homMk e)))

Tactic:
rw [Category.comp_id, Category.id_comp, ← prod_id,
          inverse_map_mkHom_id_homMk, inverse_map_mkHom_id_homMk,
          CategoryTheory.Functor.map_id]

Goal state after:
X X' Y Y' Z : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
y : Y.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
z₀ z₁ : Z.obj (Opposite.op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge z₀ z₁
⊢ (mapHomotopyCategory (α_ X Y Z).hom).map
      ((inverse (X ⊗ Y) Z).map (Prod.mkHom (𝟙 ((inverse X Y).obj (mk x, mk y))) (homMk e))) =
    homMk ((Edge.id x).tensor ((Edge.id y).tensor e))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: case hᵥ
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin (i + 1)
⊢ ((sx.spineEquiv i)
          ((ConcreteCategory.hom (X.map (op f)))
            (sx.spineToSimplex
              { vertex := fun i ↦ (ConcreteCategory.hom (s.π.app (StructuredArrow.mk (⦋0⦌.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 := ⋯ }))).vertex
      k =
    ((sx.spineEquiv i) ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))) x)).vertex k

Tactic:
dsimp only [spineEquiv, Equiv.coe_fn_mk]
      rw [dsimp% show op f = f.op from rfl]
      rw [spine_map_vertex, spine_spineToSimplex_apply, spine_vertex]
      let α : strArrowMk₂ f hi ⟶ strArrowMk₂ (⦋0⦌.const ⦋n⦌ (f.toOrderHom k)) :=
        StructuredArrow.homMk ((Hom.tr (⦋0⦌.const _ (by exact k))).op) (by simp; rfl)
      exact ConcreteCategory.congr_hom (s.w α).symm x

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

Goal state before:
pp: case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ (i : Fin (n + 1)), (f i).castSucc < x
i : Fin (n + 1)
hi : i.castSucc ∈ finset f x
this : i.castSucc ≠ Fin.last (n + 1)
⊢ False

Tactic:
simp only [castSucc_mem_finset_iff] at hi

Goal state after:
case mpr
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ (i : Fin (n + 1)), (f i).castSucc < x
i : Fin (n + 1)
this : i.castSucc ≠ Fin.last (n + 1)
hi : x ≤ (f i).castSucc
⊢ False
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: n : ℕ
x : Fin (n + 2)
⊢ map' OrderHom.id x = x

Tactic:
obtain ⟨x, rfl⟩ | rfl := Fin.eq_castSucc_or_eq_last x
  · rw [map'_eq_castSucc_iff]
    simp
  · simp

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

Goal state before:
pp: case pos.inl.right
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
⊢ ∀ i_1 < x, i.succAbove i_1 < x.castSucc

Tactic:
intro j hj

Goal state after:
case pos.inl.right
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
j : Fin (n + 1)
hj : j < x
⊢ i.succAbove j < x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
⊢ ∀ i_1 < x, i.succAbove i_1 < x.succ

Tactic:
intro j hj

Goal state after:
case neg
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
⊢ i.succAbove j < x.succ
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

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

Tactic:
intro j hj

Goal state after:
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
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

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

Tactic:
intro j hj

Goal state after:
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
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
inst✝ : P.IsRegular
hP : IsEmpty { f // ∀ (n : ℕ), P.AncestralRel (f (n + 1)) (f n) }
f : ℕ → ↑(P.ofIso e hA).II
hf : ∀ (n : ℕ), (P.ofIso e hA).AncestralRel (f (n + 1)) (f n)
n : ℕ
⊢ P.AncestralRel ((fun n ↦ ⟨(N.orderIsoOfIso e hA) ↑(f n), ⋯⟩) (n + 1)) ((fun n ↦ ⟨(N.orderIsoOfIso e hA) ↑(f n), ⋯⟩) n)

Tactic:
simpa [← P.ofIso_ancestralRel_iff e hA] using hf n

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

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

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

Tactic:
· refine ⟨s, Or.inr ?_⟩
      simp [(P.isUniquelyCodimOneFace s).δ_index]

Goal state after:
case inr
X : SSet
A : X.Subcomplex
P : A.Pairing
inst✝ : P.IsProper
s : ↑P.II
⊢ ∃ s_1,
    (↑(P.p s)).toS = { dim := (↑s_1).dim + 1, simplex := ((↑(P.p s_1)).cast ⋯).simplex } ∨
      (↑(P.p s)).toS =
        { dim := (↑s_1).dim,
          simplex := (ConcreteCategory.hom (SimplicialObject.δ X (⋯.index ⋯))) ((↑(P.p s_1)).cast ⋯).simplex }
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
⊢ ∀ i_1 < i, f.filtration i_1 ≤ f.filtration i

Tactic:
intro j hj

Goal state after:
case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
i : ι
hi : Order.IsSuccLimit i
j : ι
hj : j < i
⊢ f.filtration j ≤ f.filtration i
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex

Goal state before:
pp: case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
⊢ ∀ a < m, f.filtration a ≤ f.filtration m

Tactic:
intro j hj

Goal state after:
case a
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝² : LinearOrder ι
f : P.RankFunction ι
inst✝¹ : OrderBot ι
inst✝ : SuccOrder ι
m : ι
hm : Order.IsSuccLimit m
j : ι
hj : j < m
⊢ f.filtration j ≤ f.filtration m
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:
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 notMem
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁴ : LinearOrder ι
f : P.RankFunction ι
inst✝³ : P.IsProper
inst✝² : OrderBot ι
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
s : A.N
a✝ : s.subcomplex ≤ ⊤
⊢ s.subcomplex ≤ ⨆ i, f.filtration i

Tactic:
| notMem s =>

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

Goal state before:
pp: case a.notMem
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
inst✝ : P.IsProper
j : ι
c : f.Cell j
s : A.N
hs : s.subcomplex ≤ c.horn.image c.map
⊢ s.subcomplex ≤ f.filtration j

Tactic:
| notMem s =>

Goal state after:
Module: Mathlib.CategoryTheory.SmallRepresentatives

Goal state before:
pp: κ : Cardinal.{w}
C : Type u
inst✝ : Category.{v, u} C
hC : HasCardinalLT (Arrow C) κ
Ω : Type w := κ.ord.ToType
⊢ Nonempty (Arrow C ↪ Ω)

Tactic:
← Cardinal.lift_mk_le'

Goal state after:
κ : Cardinal.{w}
C : Type u
inst✝ : Category.{v, u} C
hC : HasCardinalLT (Arrow C) κ
Ω : Type w := κ.ord.ToType
⊢ Cardinal.lift.{w, max u v} (Cardinal.mk (Arrow C)) ≤ Cardinal.lift.{max u v, w} (Cardinal.mk Ω)
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
⊢ ∀ (G : C),
    P G →
      ∀
        (g₁ g₂ :
          G ⟶ colimit (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)),
        g₁ ≫
              colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
                (E.coconeAt X) =
            g₂ ≫
              colimit.desc (CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι)
                (E.coconeAt X) →
          g₁ = g₂

Tactic:
intro G hG (g₁ : G ⟶ colimit Φ) (g₂ : G ⟶ colimit Φ)
        (h : g₁ ≫ colimit.desc Φ (E.coconeAt X) = g₂ ≫ colimit.desc Φ (E.coconeAt X))

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
X : C
E : (P.colimitsCardinalClosure κ).ι.LeftExtension (P.colimitsCardinalClosure κ).ι :=
  Functor.LeftExtension.mk (𝟭 C) (P.colimitsCardinalClosure κ).ι.rightUnitor.inv
this : HasColimitsOfShape (CostructuredArrow (P.colimitsCardinalClosure κ).ι X) C
Φ : CostructuredArrow (P.colimitsCardinalClosure κ).ι X ⥤ C :=
  CostructuredArrow.proj (P.colimitsCardinalClosure κ).ι X ⋙ (P.colimitsCardinalClosure κ).ι
G : C
hG : P G
g₁ g₂ : G ⟶ colimit Φ
h : g₁ ≫ colimit.desc Φ (E.coconeAt X) = g₂ ≫ colimit.desc Φ (E.coconeAt X)
⊢ g₁ = g₂
Module: Mathlib.CategoryTheory.Presentable.StrongGenerator

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
⊢ isCardinalPresentable C κ = P.colimitsCardinalClosure κ

Tactic:
refine le_antisymm ?_ (P.colimitsCardinalClosure_le_isCardinalPresentable hS₂)

Goal state after:
C : Type u
inst✝⁴ : Category.{v, u} C
κ : Cardinal.{w}
inst✝³ : Fact κ.IsRegular
inst✝² : HasColimitsOfSize.{w, w, v, u} C
inst✝¹ : LocallySmall.{w, v, u} C
P : ObjectProperty C
inst✝ : ObjectProperty.Small.{w, v, u} P
hS₁ : P.IsStrongGenerator
hS₂ : P ≤ isCardinalPresentable C κ
⊢ isCardinalPresentable C κ ≤ P.colimitsCardinalClosure κ
Module: Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback

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

Tactic:
by
  simp [← comp_whiskerRight]

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

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

Tactic:
by
  simp [← comp_whiskerRight]

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

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

Tactic:
by
  simp [← comp_whiskerRight]

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

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

Tactic:
by
  simp [← comp_whiskerRight]

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

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

Tactic:
by
  simp [← comp_whiskerRight]

Goal state after: