mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Limits.Preserves.Shapes.Multiequalizer

Goal state before:
pp: C : Type u_1
D : Type u_2
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Category.{v_2, u_2} D
J : MulticospanShape
d : MulticospanIndex J C
c : Multifork d
F : C ⥤ D
⊢ ∀ {X Y : WalkingMulticospan J} (f : X ⟶ Y),
    (d.map F).multicospan.map f ≫
        (match Y with
          | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
          | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom =
      (match X with
          | WalkingMulticospan.left a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.left a))
          | WalkingMulticospan.right a => Iso.refl ((d.map F).multicospan.obj (WalkingMulticospan.right a))).hom ≫
        (d.multicospan ⋙ F).map f

Tactic:
by rintro a b (_ | _) <;> simp

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

Goal state before:
pp: case mpr.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
h₁ :
  ∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
    c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
      d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂
h₂ : ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x
x : c.pt
⊢ ∃ a, d.multispan.descColimitType c a = x

Tactic:
obtain ⟨i, y, rfl⟩ := h₂ x

Goal state after:
case mpr.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
h₁ :
  ∀ (i₁ i₂ : J.R) (x₁ : d.right i₁) (x₂ : d.right i₂),
    c.ι (WalkingMultispan.right i₁) x₁ = c.ι (WalkingMultispan.right i₂) x₂ →
      d.multispan.ιColimitType (WalkingMultispan.right i₁) x₁ = d.multispan.ιColimitType (WalkingMultispan.right i₂) x₂
h₂ : ∀ (x : c.pt), ∃ i a, c.ι (WalkingMultispan.right i) a = x
i : J.R
y : d.right i
⊢ ∃ a, d.multispan.descColimitType c a = c.ι (WalkingMultispan.right i) y
Module: Mathlib.CategoryTheory.Limits.Types.Multicoequalizer

Goal state before:
pp: case refine_2
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
x✝ :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).pt
x : X
hx : x ∈ c.multicofork.pt
⊢ ∃ i a,
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
        (WalkingMultispan.right i) a =
      ⟨x, hx⟩

Tactic:
simp only [MulticoequalizerDiagram.multicofork_pt, ← c.iSup_eq,
      Set.iSup_eq_iUnion, Set.mem_iUnion] at hx

Goal state after:
case refine_2
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
x✝ :
  ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).pt
x : X
hx✝ : x ∈ c.multicofork.pt
hx : ∃ i, x ∈ U i
⊢ ∃ i a,
    ((c.multispanIndex.map Set.functorToTypes).multispan.coconeTypesEquiv.symm (c.multicofork.map Set.functorToTypes)).ι
        (WalkingMultispan.right i) a =
      ⟨x, hx✝⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
S : SSet
σ₁ σ₂ : Λ[n + 1, i].toSSet ⟶ S
h :
  ∀ (j : Fin (n + 2)) (h : j ≠ i),
    (ConcreteCategory.hom (σ₁.app (op ⦋n⦌))) (face i j h) = (ConcreteCategory.hom (σ₂.app (op ⦋n⦌))) (face i j h)
⊢ σ₁ = σ₂

Tactic:
by
  rw [← Subfunctor.equalizer_eq_iff]
  apply le_antisymm (Subfunctor.equalizer_le σ₁ σ₂)
  simp only [horn_eq_iSup, iSup_le_iff,
    Subtype.forall, Set.mem_compl_iff, Set.mem_singleton_iff,
    ← stdSimplex.ofSimplex_yonedaEquiv_δ, Subcomplex.ofSimplex_le_iff]
  intro j hj
  exact (Subfunctor.mem_equalizer_iff σ₁ σ₂ (face i j hj)).2 (by apply h)

Goal state after:
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
⊢ Function.Injective ⇑(hom φ)

Tactic:
intro x₁

Goal state after:
J : Type u'
x✝¹ : Category.{v', u'} J
x✝ : IsFiltered J
F₁ F₂ : J ⥤ Type u
c₁ : Cocone F₁
c₂ : Cocone F₂
hc₁ : IsColimit c₁
hc₂ : IsColimit c₂
f : F₁ ⟶ F₂
φ : c₁.pt ⟶ c₂.pt
hf : ∀ (j : J), Function.Injective ⇑(hom (f.app j))
hφ : ∀ (j : J) (x : ToType (F₁.obj j)), (hom φ) ((hom (c₁.ι.app j)) x) = (hom (c₂.ι.app j)) ((hom (f.app j)) x)
x₁ : c₁.pt
⊢ ∀ ⦃a₂ : c₁.pt⦄, (hom φ) x₁ = (hom φ) a₂ → x₁ = a₂
Module: Mathlib.CategoryTheory.Types.Monomorphisms

Goal state before:
pp: T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective ⇑(hom (f j))
⊢ Function.Injective ⇑(hom (Limits.Sigma.map f))

Tactic:
intro x₁

Goal state after:
T : Type u'
X₁ X₂ : T → Type u
inst✝¹ : HasCoproduct X₁
inst✝ : HasCoproduct X₂
f : (j : T) → X₁ j ⟶ X₂ j
h : ∀ (j : T), Function.Injective ⇑(hom (f j))
x₁ : ∐ X₁
⊢ ∀ ⦃a₂ : ∐ X₁⦄, (hom (Limits.Sigma.map f)) x₁ = (hom (Limits.Sigma.map f)) a₂ → x₁ = a₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
⊢ ∀ (x₃ y₃ : sigmaStdSimplex i d _⦋n⦌),
    x₃ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) →
        (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₃ = (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) y₃ → x₃ = y₃

Tactic:
intro x₁

Goal state after:
case refine_3
X Y : SSet
i : X ⟶ Y
d : ℕ
x✝ : SimplexCategoryᵒᵖ
n : ℕ
x₁ : sigmaStdSimplex i d _⦋n⦌
⊢ ∀ (y₃ : sigmaStdSimplex i d _⦋n⦌),
    x₁ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) →
      y₃ ∉ Set.range ⇑(ConcreteCategory.hom ((l i d).app (op ⦋n⦌))) →
        (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) x₁ = (ConcreteCategory.hom ((b i d).app (op ⦋n⦌))) y₃ → x₁ = y₃
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: n : ℕ
X : Truncated (n + 1)
inst✝ : X.IsStrictSegal
d : ℕ
hd : ⦋d + 1⦌.len ≤ n + 1
x y : X.obj (op { obj := ⦋d + 1⦌, property := hd })
h :
  ∀ (i : Fin (d + 1)),
    (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ hd).op)) x =
      (ConcreteCategory.hom (X.map (tr (mkOfSucc i) ⋯ hd).op)) y
⊢ X.spine (d + 1) hd x = X.spine (d + 1) hd y

Tactic:
ext i; apply h

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

Goal state before:
pp: X Y : SSet
sx : X.StrictSegal
sy : Y.StrictSegal
n : ℕ
f : X.Path (n + 1)
σ : X ⟶ Y
k : Fin (n + 1)
⊢ (ConcreteCategory.hom (Y.map (mkOfSucc k).op)) (sy.spineToSimplex (f.map σ)) =
    (ConcreteCategory.hom (Y.map (mkOfSucc k).op))
      ((ConcreteCategory.hom (σ.app (Opposite.op ⦋n + 1⦌))) (sx.spineToSimplex f))

Tactic:
rw [← types_comp_apply (σ.app _) (Y.map _), ← σ.naturality, types_comp_apply,
    spineToSimplex_arrow, spineToSimplex_arrow, Path.map_arrow]

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

Goal state before:
pp: case mp
X₁ X₂ Y₁ Y₂ : SSet
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
m : SimplexCategoryᵒᵖ
y₁ : Y₁.obj m
y₂ : Y₂.obj m
x₁ : X₁.obj m
x₂ : X₂.obj m
h :
  ((ConcreteCategory.hom ((f₁ ⊗ₘ f₂).app m)) (x₁, x₂)).1 = (y₁, y₂).1 ∧
    ((ConcreteCategory.hom ((f₁ ⊗ₘ f₂).app m)) (x₁, x₂)).2 = (y₁, y₂).2
⊢ (y₁, y₂) ∈ ((range f₁).prod (range f₂)).obj m

Tactic:
exact ⟨⟨x₁, h.1⟩, ⟨x₂, h.2⟩⟩

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:
← multiplicativeClosure_morphismPropertyHomMk,

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)
⊢ (morphismPropertyHomMk V).multiplicativeClosure ≤ W
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
x₀ x₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e : Edge x₀ x₁
y₁ : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })
e' : Edge x₀ y₁
h : e.edge = e'.edge
⊢ x₁ = y₁

Tactic:
rw [← e.tgt_eq, ← e'.tgt_eq, h]

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
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 (s.π.app (strArrowMk₂ (⦋1⦌.const ⦋n⦌ ⟨i, ⋯⟩) fac_aux₁._proof_1))) x

Tactic:
dsimp% s.π.naturality_apply α x

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 : ℕ
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 α.right.unop.hom.op))
    ((ConcreteCategory.hom (s.π.app (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ⟨i, ⋯⟩) lift._proof_1))) x)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

Goal state before:
pp: V : Truncated 2
W : MorphismProperty V.HomotopyCategory
inst✝ : W.IsMultiplicative
hW : ∀ {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} (e : Edge x y), W (homMk e)
⊢ ⊤ ≤ W

Tactic:
← multiplicativeClosure_morphismPropertyHomMk,

Goal state after:
V : Truncated 2
W : MorphismProperty V.HomotopyCategory
inst✝ : W.IsMultiplicative
hW : ∀ {x y : V.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 })} (e : Edge x y), W (homMk e)
⊢ (morphismPropertyHomMk V).multiplicativeClosure ≤ W
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: n : ℕ
hn :
  ∀ (i : Fin (n + 1)) {x : SimplexCategoryGenRel} (f : x ⟶ mk (n + 1)),
    P_δ f → ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), f ≫ σ i = e ≫ m
i : Fin (n + 1 + 1)
x X Y : SimplexCategoryGenRel
k : Fin (n + 1 + 2)
f : x ⟶ mk (n + 1)
hf : faces.multiplicativeClosure f
h' : x.len < (mk (n + 1)).len
j : Fin (n + 1)
j' : Fin (n + 2)
h'' : δ k ≫ σ i = σ j ≫ δ j'
z : SimplexCategoryGenRel
e : x ⟶ z
m : z ⟶ mk n
he : P_σ e
hm : P_δ m
fac : f ≫ σ j = e ≫ m
⊢ (f ≫ δ k) ≫ σ i = e ≫ m ≫ δ j'

Tactic:
simp [h'', reassoc_of% fac]

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

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

Tactic:
by
  induction L with | nil => grind | cons _ _ _ => simp only [List.forall_mem_cons] at hj; grind

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)
m : s.pt ⟶ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).pt
hm :
  ∀ (j : StructuredArrow (op ⦋n⦌) (inclusion 2).op),
    m ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j
x : s.pt
⊢ (sx.spineEquiv n) ((ConcreteCategory.hom m).toFun x) =
    (sx.spineEquiv n) ((ConcreteCategory.hom (↾fun x ↦ lift sx s x)).toFun x)

Tactic:
simp only [spineEquiv, RightExtension.coneAt_pt, rightExtensionInclusion_left,
      TypeCat.Fun.toFun_apply, Equiv.coe_fn_mk, lift, Nat.reduceAdd, ObjectProperty.ι_obj,
      const_obj_obj, comp_obj, proj_obj, mk_right, op_obj, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      spine_spineToSimplex_apply]

Goal state after:
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
m : s.pt ⟶ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).pt
hm :
  ∀ (j : StructuredArrow (op ⦋n⦌) (inclusion 2).op),
    m ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j
x : s.pt
⊢ X.spine n ((ConcreteCategory.hom m) x) =
    { 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 := ⋯ }
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i j : Fin (x₁.len + 1 + (x₂.len + 1))
h : i ≤ j
⊢ (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)
      i ≤
    (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)
      j

Tactic:
cases i using Fin.addCases <;>
        cases j using Fin.addCases <;>
        rw [Fin.le_def] at h ⊢ <;>
        simp at h ⊢

Goal state after:
case left.left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₁.len + 1)
h : i✝¹ ≤ i✝
⊢ (SimplexCategory.Hom.toOrderHom f₁) i✝¹ ≤ (SimplexCategory.Hom.toOrderHom f₁) i✝

case left.right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ : Fin (x₁.len + 1)
i✝ : Fin (x₂.len + 1)
h : ↑i✝¹ ≤ x₁.len + 1 + ↑i✝
⊢ ↑((SimplexCategory.Hom.toOrderHom f₁) i✝¹) ≤ y₁.len + 1 + ↑((SimplexCategory.Hom.toOrderHom f₂) i✝)

case right.left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ : Fin (x₂.len + 1)
i✝ : Fin (x₁.len + 1)
h : x₁.len + 1 + ↑i✝¹ ≤ ↑i✝
⊢ y₁.len + 1 + ↑((SimplexCategory.Hom.toOrderHom f₂) i✝¹) ≤ ↑((SimplexCategory.Hom.toOrderHom f₁) i✝)

case right.right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₂.len + 1)
h : i✝¹ ≤ i✝
⊢ (SimplexCategory.Hom.toOrderHom f₂) i✝¹ ≤ (SimplexCategory.Hom.toOrderHom f₂) i✝
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

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

Tactic:
simp only [Fin.succAbove_of_lt_succ _ _ hx,
        OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply,
        le_refl, Fin.castSucc_lt_castSucc_iff, true_and]

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

Goal state before:
pp: case neg
n : ℕ
i x : Fin (n + 2)
hx : i < x
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc

Tactic:
· obtain ⟨x, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt hx)
      rw [Fin.predAbove_of_castSucc_lt _ _ (by simpa [Fin.le_castSucc_iff]),
        Fin.pred_castSucc_succ, map'_eq_castSucc_iff]
      simp only [Fin.succAbove_of_lt_succ _ _ hx,
        OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply,
        le_refl, Fin.castSucc_lt_castSucc_iff, true_and]
      intro j hj
      by_cases! h : j.castSucc < i
      · simpa [Fin.succAbove_of_castSucc_lt _ _ h] using hj.le
      · rwa [Fin.succAbove_of_le_castSucc _ _ h, Fin.succ_lt_succ_iff]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
⊢ inr (WithInitial.of x) (WithInitial.of y) ≫
      (WithInitial.of x ⊗ WithInitial.of y).inl (WithInitial.of z) ≫
        (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)).hom =
    inl (WithInitial.of y) (WithInitial.of z) ≫ inr (WithInitial.of x) (WithInitial.of y ⊗ WithInitial.of z)

Tactic:
change inr' _ _ ≫ inl' _ _ ≫ WithInitial.down _ = inl' _ _ ≫ inr' _ _

Goal state after:
x✝ y✝ z✝ : AugmentedSimplexCategory
x y z : SimplexCategory
⊢ inr' x y ≫
      inl' (tensorObjOf x y) z ≫ WithInitial.down (α_ (WithInitial.of x) (WithInitial.of y) (WithInitial.of z)).hom =
    inl' y z ≫ inr' x (tensorObjOf y z)
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

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

Tactic:
| succ i hi =>

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

Goal state before:
pp: X₁ X₂ : SSet
d₁ d₂ : ℕ
inst✝¹ : X₁.HasDimensionLT d₁
inst✝ : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
⊢ ∀ (i : X₁.N) (i_1 : X₂.N),
    (Subcomplex.range (yonedaEquiv.symm i.simplex ⊗ₘ yonedaEquiv.symm i_1.simplex)).toSSet.HasDimensionLT n

Tactic:
intro x₁

Goal state after:
X₁ X₂ : SSet
d₁ d₂ : ℕ
inst✝¹ : X₁.HasDimensionLT d₁
inst✝ : X₂.HasDimensionLT d₂
n : ℕ
hn : d₁ + d₂ ≤ n + 1
x₁ : X₁.N
⊢ ∀ (i : X₂.N), (Subcomplex.range (yonedaEquiv.symm x₁.simplex ⊗ₘ yonedaEquiv.symm i.simplex)).toSSet.HasDimensionLT n
Module: Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Pullbacks

Goal state before:
pp: case refine_2
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
⊢ (Cone.postcompose
          (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
              (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
              (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
      (c k) ≅
    ((evaluation D C).obj k).mapCone (combine f g c hc)

Tactic:
refine Cone.ext (Iso.refl _) ?_

Goal state after:
case refine_2
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
⊢ ∀ (j : WalkingCospan),
    ((Cone.postcompose
                  (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
                      (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
                      (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
              (c k)).π.app
        j =
      (Iso.refl
            ((Cone.postcompose
                    (cospanIsoMk (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.one))
                        (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.left))
                        (Iso.refl ((cospan (f.app k) (g.app k)).obj WalkingCospan.right)) ⋯ ⋯).hom).obj
                (c k)).pt).hom ≫
        (((evaluation D C).obj k).mapCone (combine f g c hc)).π.app j
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 κ
inst✝ : LocallySmall.{w, v, u} C
X : C
J : Type w
w✝¹ : SmallCategory J
w✝ : IsCardinalFiltered J κ
hX : P.ColimitOfShape J X
κ' : Cardinal.{w}
h₁ : κ'.IsRegular
h₂ : ∀ (i : Unit ⊕ Unit), HasCardinalLT (Sum.elim (fun x ↦ Arrow J) (fun x ↦ κ.ord.ToType) i) κ'
⊢ ∃ κ', ∃ (_ : Fact κ'.IsRegular) (_ : κ ≤ κ'), HasCardinalLT (Arrow J) κ'

Tactic:
exact ⟨κ', ⟨h₁⟩,
      le_of_lt (by simpa [hasCardinalLT_iff_cardinal_mk_lt] using h₂ (Sum.inr ⟨⟩)),
      h₂ (Sum.inl ⟨⟩)⟩

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝³ : LinearOrder ι
f : P.RankFunction ι
inst✝² : P.IsProper
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
j : ι
x✝ : SimplexCategoryᵒᵖ
d : ℕ
y : ↑((f.filtration j).obj (op ⦋d⦌))
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
h : ⟨↑y, ⋯⟩ = (ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b)
hb : b ∈ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ ∃ x₁,
    (ConcreteCategory.hom ((f.t j).app (op ⦋d⦌))) x₁ = y ∧
      (ConcreteCategory.hom ((f.m j).app (op ⦋d⦌))) x₁ = (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b

Tactic:
refine ⟨x.ιSigmaHorn.app _ ⟨b, hb⟩, ?_, ?_⟩

Goal state after:
case refine_1
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⦌))
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
h : ⟨↑y, ⋯⟩ = (ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b)
hb : b ∈ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ (ConcreteCategory.hom ((f.t j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaHorn.app (op ⦋d⦌))) ⟨b, hb⟩) = y

case refine_2
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⦌))
x : f.Cell j
b : Δ[x.dim + 1] _⦋d⦌
h : ⟨↑y, ⋯⟩ = (ConcreteCategory.hom ((f.b j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b)
hb : b ∈ Λ[x.dim + 1, x.index].obj (op ⦋d⦌)
⊢ (ConcreteCategory.hom ((f.m j).app (op ⦋d⦌))) ((ConcreteCategory.hom (x.ιSigmaHorn.app (op ⦋d⦌))) ⟨b, hb⟩) =
    (ConcreteCategory.hom (x.ιSigmaStdSimplex.app (op ⦋d⦌))) b
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
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
⊢ inl ▷ Q ≫ hP.desc h k w ▷ Q = h ▷ Q

Tactic:
← comp_whiskerRight,

Goal state after:
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
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
⊢ (inl ≫ hP.desc h k w) ▷ Q = h ▷ Q
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
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
⊢ inr ▷ Q ≫ hP.desc h k w ▷ Q = k ▷ Q

Tactic:
← comp_whiskerRight,

Goal state after:
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
W : C
h : X ⟶ W
k : Y ⟶ W
w : f ≫ h = g ≫ k
Q : C
⊢ (inr ≫ hP.desc h k w) ▷ Q = k ▷ Q