mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
l : J.L
z : d.multispan.obj (WalkingMultispan.left l)
⊢ d.multispan.ιColimitType (WalkingMultispan.right (J.fst l))
      ((ConcreteCategory.hom (d.multispan.map (WalkingMultispan.Hom.fst l))) z) =
    d.multispan.ιColimitType (WalkingMultispan.left l) z

Tactic:
rw [ιColimitType_map]

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

Goal state before:
pp: case mp.refine_2
J : MultispanShape
d : MultispanIndex J (Type u)
c : d.multispan.CoconeTypes
this : ∀ (x : d.multispan.ColimitType), ∃ i a, d.multispan.ιColimitType (WalkingMultispan.right i) a = x
hc : c.IsColimit
i : J.R
z : d.right i
⊢ ∃ i_1 a,
    c.ι (WalkingMultispan.right i_1) a =
      d.multispan.descColimitType c (d.multispan.ιColimitType (WalkingMultispan.right i) z)

Tactic:
exact ⟨i, z, by simp⟩

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

Goal state before:
pp: case pos
n : ℕ
A : Δ[n + 1].Subcomplex
i : Fin (n + 2)
h : ¬stdSimplex.face {i}ᶜ ≤ A
d : ℕ
x : ↑(Δ[n + 1].nonDegenerate d)
hx : ↑x ∈ A.obj (op ⦋d⦌)
hd : d < n
⊢ ↑x ∈ Λ[n + 1, i].obj (op ⦋d⦌)

Tactic:
simp [horn_obj_eq_univ i d]

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

Goal state before:
pp: n : ℕ
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (mkOfSucc i ≫ SimplexCategory.δ j) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i) 2 ⋯)

Tactic:
mkOfSucc_δ_eq hij,

Goal state after:
n : ℕ
X : Truncated (n + 2)
sx : X.StrictSegal
m : ℕ
h : m ≤ n + 1
f : X.Path (m + 1)
i : Fin m
j : Fin (m + 2)
hij : j = i.succ.castSucc
⊢ (ConcreteCategory.hom (X.map (tr (intervalEdge (↑i) 2 ⋯) ⋯ ⋯).op)) (sx.spineToSimplex (m + 1) ⋯ f) =
    sx.spineToDiagonal 2 ⋯ (f.interval (↑i) 2 ⋯)
Module: Mathlib.CategoryTheory.Bicategory.CatEnriched

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
| CatEnriched.hComp (Hom.base η) (eqToHom ⋯ ≫ CatEnriched.hComp (Hom.base θ) (Hom.base κ) ≫ eqToHom ⋯)

Tactic:
1

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory Cat C
a b c d : CatEnrichedOrdinary C
f f' : a ⟶ b
g g' : b ⟶ c
h h' : c ⟶ d
η : f ⟶ f'
θ : g ⟶ g'
κ : h ⟶ h'
| Hom.base η
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
f : 𝟙_ (C ⥤ Type (max v' v u)) ⟶ F.functorHom G
X Y : C
φ : X ⟶ Y
⊢ F.map φ ≫ ((ConcreteCategory.hom (f.app Y)) PUnit.unit).app Y (𝟙 (Opposite.unop (Opposite.op Y))) =
    ((ConcreteCategory.hom (f.app X)) PUnit.unit).app X (𝟙 (Opposite.unop (Opposite.op X))) ≫ G.map φ

Tactic:
← (f.app X (PUnit.unit)).naturality φ

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F G : C ⥤ D
f : 𝟙_ (C ⥤ Type (max v' v u)) ⟶ F.functorHom G
X Y : C
φ : X ⟶ Y
⊢ F.map φ ≫ ((ConcreteCategory.hom (f.app Y)) PUnit.unit).app Y (𝟙 (Opposite.unop (Opposite.op Y))) =
    F.map φ ≫
      ((ConcreteCategory.hom (f.app X)) PUnit.unit).app Y
        ((ConcreteCategory.hom ((Opposite.unop (coyoneda.rightOp.obj X)).map φ)) (𝟙 (Opposite.unop (Opposite.op X))))
Module: Mathlib.AlgebraicTopology.SimplicialSet.Monoidal

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
B : Y.Subcomplex
⊢ range (A.ι ⊗ₘ B.ι) ≤ A.prod B

Tactic:
by
    rintro m _ ⟨⟨y₁, y₂⟩, ⟨⟩⟩
    exact ⟨Subtype.coe_prop _, Subtype.coe_prop _⟩

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

Goal state before:
pp: V : Truncated 2
φ : V.obj (op { obj := ⦋2⦌, property := ι0₂._proof_3 })
⊢ 0 ≤ 1

Tactic:
by decide

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

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

Tactic:
rintro ⟨⟨_, _, e⟩⟩
    exact morphismPropertyHomMk_of_edge e

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

Goal state before:
pp: case e'_2.e'_6
V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
obj : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) → D
map : {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)
map_id : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀ {x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂}
    {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀✝ x₁✝ x₂✝ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁✝ : Edge x₀✝ x₁✝
e₁₂✝ : Edge x₁✝ x₂✝
e₀₂✝ : Edge x₀✝ x₂✝
h : e₀₁✝.CompStruct e₁₂✝ e₀₂✝
e_1✝ :
  ((Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₀✝) ⟶
      (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₂✝)) =
    (obj x₀✝ ⟶ obj x₂✝)
e_3✝ :
  (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₀✝) =
    obj x₀✝
e_4✝ :
  (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₁✝) =
    obj x₁✝
⊢ (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₀₁✝)) =
    map e₀₁✝

Tactic:
apply Cat.FreeRefl.lift'_map

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

Goal state before:
pp: case e'_2.e'_7
V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
obj : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) → D
map : {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)
map_id : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀ {x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂}
    {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀✝ x₁✝ x₂✝ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁✝ : Edge x₀✝ x₁✝
e₁₂✝ : Edge x₁✝ x₂✝
e₀₂✝ : Edge x₀✝ x₂✝
h : e₀₁✝.CompStruct e₁₂✝ e₀₂✝
e_1✝ :
  ((Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₀✝) ⟶
      (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₂✝)) =
    (obj x₀✝ ⟶ obj x₂✝)
e_4✝ :
  (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₁✝) =
    obj x₁✝
e_5✝ :
  (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₂✝) =
    obj x₂✝
⊢ (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₁₂✝)) =
    map e₁₂✝

Tactic:
apply Cat.FreeRefl.lift'_map

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

Goal state before:
pp: case e'_3
V W : Truncated 2
D : Type u_1
inst✝ : Category.{v_1, u_1} D
obj : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }) → D
map : {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} → Edge x y → (obj x ⟶ obj y)
map_id : ∀ (x : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })), map (Edge.id x) = 𝟙 (obj x)
map_comp :
  ∀ {x₀ x₁ x₂ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} {e₀₁ : Edge x₀ x₁} {e₁₂ : Edge x₁ x₂}
    {e₀₂ : Edge x₀ x₂} (x : e₀₁.CompStruct e₁₂ e₀₂), map e₀₁ ≫ map e₁₂ = map e₀₂
X Y : Cat.FreeRefl (OneTruncation₂ V)
x₀✝ x₁✝ x₂✝ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e₀₁✝ : Edge x₀✝ x₁✝
e₁₂✝ : Edge x₁✝ x₂✝
e₀₂✝ : Edge x₀✝ x₂✝
h : e₀₁✝.CompStruct e₁₂✝ e₀₂✝
e_1✝ :
  ((Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₀✝) ⟶
      (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).obj
        ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).obj x₂✝)) =
    (obj x₀✝ ⟶ obj x₂✝)
⊢ (Cat.FreeRefl.lift' obj (fun {v w} f ↦ map f) map_id).map
      ((Cat.FreeRefl.quotientFunctor (OneTruncation₂ V)).map (Quiver.Hom.toPath e₀₂✝)) =
    map e₀₂✝

Tactic:
apply Cat.FreeRefl.lift'_map

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
h : W₁.MapFactorizationData W₂ f
this : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Subsingleton (W₁.MapFactorizationData W₂ f)
⊢ r.degHom f = r.deg h.Z

Tactic:
← Subsingleton.elim (r.mapFactorizationData f) h

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
h : W₁.MapFactorizationData W₂ f
this : ∀ ⦃X Y : C⦄ (f : X ⟶ Y), Subsingleton (W₁.MapFactorizationData W₂ f)
⊢ r.degHom f = r.deg (r.mapFactorizationData f).Z
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: x y : OneTruncation₂ ((truncation 2).obj Δ[0])
⊢ x ⟶ y

Tactic:
obtain rfl : x = default := Unique.uniq _ _

Goal state after:
y : OneTruncation₂ ((truncation 2).obj Δ[0])
⊢ default ⟶ y
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: x y : SimplexCategoryGenRel
h : x.len = y.len
⊢ x = y

Tactic:
cases x

Goal state after:
case H
y : SimplexCategoryGenRel
n✝ : ℕ
h : (mk n✝).len = y.len
⊢ mk n✝ = y
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

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

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

Tactic:
· exact (h₁ (fun _ ↦ ⟨0, Subsingleton.elim (α := Fin 1) _ _⟩)).elim

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
φ : ⦋1⦌ ⟶ ⦋n⦌
⊢ 0 ≤ 1

Tactic:
by decide

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
φ : ⦋1⦌ ⟶ ⦋n⦌
⊢ (ConcreteCategory.hom (X.map φ.op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ φ fac_aux₁._proof_1))) x

Tactic:
obtain ⟨i, j, hij, rfl⟩ : ∃ i j hij, φ = mkOfLe i j hij :=
    ⟨φ.toOrderHom 0, φ.toOrderHom 1, φ.toOrderHom.monotone (by decide),
      Hom.ext_one_left _ _ rfl rfl⟩

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i j : Fin (n + 1)
hij : i ≤ j
⊢ (ConcreteCategory.hom (X.map (mkOfLe i j hij).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe i j hij) fac_aux₁._proof_1))) x
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)
α : strArrowMk₂ f hi ⟶
  strArrowMk₂ (⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom f) k)) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1 :=
  homMk (Hom.tr (⦋0⦌.const ⦋i⦌ k) ⋯ hi).op ⋯
⊢ Path.vertex
      { 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 := ⋯ }
      ((Hom.toOrderHom f) k) =
    (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋i⦌ k).op)) ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk f.op))) x)

Tactic:
exact ConcreteCategory.congr_hom (s.w α).symm x

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

Goal state before:
pp: case mp
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ (∀ b ∈ finset f x, b = Fin.last (n + 1)) → ∀ (i : Fin (n + 1)), (f i).castSucc < x

Tactic:
intro h

Goal state after:
case mp
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ b ∈ finset f x, b = Fin.last (n + 1)
⊢ ∀ (i : Fin (n + 1)), (f i).castSucc < x
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)
⊢ (∀ (i : Fin (n + 1)), (f i).castSucc < x) → ∀ b ∈ finset f x, b = Fin.last (n + 1)

Tactic:
intro h

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
⊢ ∀ b ∈ finset f x, b = Fin.last (n + 1)
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)
⊢ x ≤ (f y).castSucc → ((∀ b ∈ finset f x, y.castSucc ≤ b) ↔ ∀ i < y, (f i).castSucc < x)

Tactic:
intro h

Goal state after:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
y : Fin (n + 1)
h : x ≤ (f y).castSucc
⊢ (∀ b ∈ finset f x, y.castSucc ≤ b) ↔ ∀ i < y, (f i).castSucc < x
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x : AugmentedSimplexCategory
⊢ x ◁ 𝟙 WithInitial.star = 𝟙 (x ⊗ WithInitial.star)

Tactic:
cases x

Goal state after:
case of
a✝ : SimplexCategory
⊢ WithInitial.of a✝ ◁ 𝟙 WithInitial.star = 𝟙 (WithInitial.of a✝ ⊗ WithInitial.star)

case star
⊢ WithInitial.star ◁ 𝟙 WithInitial.star = 𝟙 (WithInitial.star ⊗ WithInitial.star)
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x : AugmentedSimplexCategory
⊢ 𝟙 WithInitial.star ▷ x = 𝟙 (WithInitial.star ⊗ x)

Tactic:
cases x

Goal state after:
case of
a✝ : SimplexCategory
⊢ 𝟙 WithInitial.star ▷ WithInitial.of a✝ = 𝟙 (WithInitial.star ⊗ WithInitial.of a✝)

case star
⊢ 𝟙 WithInitial.star ▷ WithInitial.star = 𝟙 (WithInitial.star ⊗ WithInitial.star)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: 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

Tactic:
· rw [Fin.predAbove_of_le_castSucc _ _ h, ← Fin.castSucc_lt_castSucc_iff,
            Fin.castSucc_castPred]
          exact lt_of_le_of_lt h hi

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

Goal state before:
pp: case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
⊢ orderHomOfSimplex z hn = OrderHom.id → Function.Injective ⇑(objEquiv z)

Tactic:
intro h

Goal state after:
case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
h : orderHomOfSimplex z hn = OrderHom.id
⊢ Function.Injective ⇑(objEquiv z)
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: case snd
p q n : ℕ
z₁ z₂ : ↑((Δ[p] ⊗ Δ[q]).nonDegenerate n)
h : (↑z₁).1 = (↑z₂).1
hn : p + q = n
i : Fin (n + 1)
⊢ ((objEquiv ↑z₁) i).2 = ((objEquiv ↑z₂) i).2

Tactic:
have h₁ := z₁.2
    have h₂ := z₂.2
    rw [nonDegenerate_max_dim_iff] at h₁ h₂
    simpa only [orderHomOfSimplex_coe, h, Fin.ext_iff, add_right_inj]
      using! DFunLike.congr_fun (h₁.trans h₂.symm) i

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 t : ↑P.II
x✝ :
  { dim := (↑s).dim + 1, simplex := ((↑(P.p s)).cast ⋯).simplex } =
    { dim := (↑t).dim + 1, simplex := ((↑(P.p t)).cast ⋯).simplex }
⊢ s = t

Tactic:
by
    apply P.p.injective
    rwa [Subtype.ext_iff, N.ext_iff, SSet.N.ext_iff,
      ← (P.p s).val.cast_eq_self (P.isUniquelyCodimOneFace s).dim_eq,
      ← (P.p t).val.cast_eq_self (P.isUniquelyCodimOneFace t).dim_eq]

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
α : Type v
inst✝² : PartialOrder α
inst✝¹ : WellFoundedLT α
inst✝ : P.IsProper
f : P.WeakRankFunction α
⊢ WellFounded P.AncestralRel

Tactic:
rw [wellFounded_iff_isEmpty_descending_chain]
  refine ⟨fun ⟨g, hg⟩ ↦ ?_⟩
  obtain ⟨n₀, hn₀⟩ :=
    (wellFoundedGT_iff_monotone_chain_condition (α := ℕᵒᵈ)).1
      inferInstance ⟨fun n ↦ (g n).1.dim,
        monotone_nat_of_le_succ (fun n ↦ (hg n).dim_le)⟩
  dsimp at hn₀
  refine not_strictAnti_of_wellFoundedLT (fun n ↦ f.rank (g (n₀ + n)))
    (strictAnti_nat_of_succ_lt (fun n ↦ ?_))
  rw [← add_assoc]
  exact f.lt (hg _) (by rw [← hn₀ (n₀ + n + 1) (by lia), ← hn₀ (n₀ + n) (by lia)])

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

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.RankFunction α
x y : ↑h.pairing.II
hxy : h.pairing.AncestralRel x y
⊢ f.rank (h.equivII.symm x) < f.rank (h.equivII.symm y)

Tactic:
by
        obtain ⟨x, rfl⟩ := h.equivII.surjective x
        obtain ⟨y, rfl⟩ := h.equivII.surjective y
        rw [← ancestralRel_iff] at hxy
        simpa using f.lt hxy

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

Goal state before:
pp: X✝ : SSet
A✝ : X✝.Subcomplex
X : SSet
A : X.Subcomplex
h : A.PairingCore
α : Type v
inst✝ : PartialOrder α
f : h.WeakRankFunction α
x y : ↑h.pairing.II
hxy : h.pairing.AncestralRel x y
⊢ (↑x).dim = (↑y).dim → f.rank (h.equivII.symm x) < f.rank (h.equivII.symm y)

Tactic:
by
        obtain ⟨x, rfl⟩ := h.equivII.surjective x
        obtain ⟨y, rfl⟩ := h.equivII.surjective y
        rw [← ancestralRel_iff] at hxy
        simpa using f.lt hxy

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 ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
⊢ ¬(↑c.s).subcomplex ≤ c.horn.image c.map

Tactic:
intro h

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝¹ : LinearOrder ι
f : P.RankFunction ι
i : ι
c : f.Cell i
inst✝ : P.IsProper
h : (↑c.s).subcomplex ≤ c.horn.image c.map
⊢ False
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 : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
⊢ ((f.t j).app (op ⦋d⦌) ≫ ↾fun x ↦ ⟨↑x, ⋯⟩) = (f.m j).app (op ⦋d⦌) ≫ (f.b j).app (op ⦋d⦌) ∧
    (∀ (x₁ y₁ : f.sigmaHorn j _⦋d⦌),
        (ConcreteCategory.hom ((f.t j).app (op ⦋d⦌))) x₁ = (ConcreteCategory.hom ((f.t j).app (op ⦋d⦌))) y₁ ∧
            (ConcreteCategory.hom ((f.m j).app (op ⦋d⦌))) x₁ = (ConcreteCategory.hom ((f.m j).app (op ⦋d⦌))) y₁ →
          x₁ = y₁) ∧
      ∀ (x₂ : ↑((f.filtration j).obj (op ⦋d⦌))) (x₃ : f.sigmaStdSimplex j _⦋d⦌),
        ⟨↑x₂, ⋯⟩ = (ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) x₃ →
          ∃ x₁,
            (ConcreteCategory.hom ((f.t j).app (op ⦋d⦌))) x₁ = x₂ ∧
              (ConcreteCategory.hom ((f.m j).app (op ⦋d⦌))) x₁ = x₃

Tactic:
refine ⟨congr_app (f.w j) (op ⦋d⦌),
      fun a₁ a₂ h ↦ (mono_iff_injective _).mp
        ((NatTrans.mono_iff_mono_app (f.m j)).mp inferInstance _) h.2, fun y b h ↦ ?_⟩

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 : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
y : ↑((f.filtration j).obj (op ⦋d⦌))
b : f.sigmaStdSimplex j _⦋d⦌
h : ⟨↑y, ⋯⟩ = (ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) b
⊢ ∃ x₁, (ConcreteCategory.hom ((f.t j).app (op ⦋d⦌))) x₁ = y ∧ (ConcreteCategory.hom ((f.m j).app (op ⦋d⦌))) x₁ = b
Module: Mathlib.CategoryTheory.Presentable.Limits

Goal state before:
pp: case hsurj
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)
this : IsFiltered J
⊢ ∀ (x : (c.pt.mapCocone cX).pt), ∃ i xi, x = (ConcreteCategory.hom ((c.pt.mapCocone cX).ι.app i)) xi

Tactic:
exact isColimitMapCocone.surjective c hc κ hK cX hF

Goal state after: