mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
U✝ V✝ : C
φ : U✝ ⟶ V✝
x : F₁.obj U✝
hx : x ∈ A.obj U✝
h : (ConcreteCategory.hom (f.app U✝)) ⟨x, hx⟩ = (ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩
⊢ x ∈
    ⇑(ConcreteCategory.hom (F₁.map φ)) ⁻¹'
      {x | ∃ (hx : x ∈ A.obj V✝), (ConcreteCategory.hom (f.app V✝)) ⟨x, hx⟩ = (ConcreteCategory.hom (g.app V✝)) ⟨x, hx⟩}

Tactic:
exact ⟨A.map _ hx,
      (NatTrans.naturality_apply f φ ⟨x, hx⟩).trans (Eq.trans (by rw [h])
        (NatTrans.naturality_apply g φ ⟨x, hx⟩).symm)⟩

Goal state after:
Module: Mathlib.CategoryTheory.Subfunctor.Equalizer

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F₁ F₂ : C ⥤ Type w
A : Subfunctor F₁
f g : A.toFunctor ⟶ F₂
⊢ Mono (homOfLe ⋯)

Tactic:
infer_instance

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

Goal state before:
pp: X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
⊢ A₂.obj n ⊔ A₃.obj n = A₄.obj n

Tactic:
by
              rw [← sq.sup_eq]
              rfl

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ Mono (Subcomplex.homOfLE ⋯)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁸ : Category.{v, u} C
W : MorphismProperty C
J : Type u''
inst✝⁷ : Category.{v'', u''} J
K : Type u'
inst✝⁶ : LinearOrder K
inst✝⁵ : SuccOrder K
inst✝⁴ : OrderBot K
inst✝³ : WellFoundedLT K
inst✝² : (monomorphisms C).IsStableUnderTransfiniteCompositionOfShape K
inst✝¹ : HasPullbacks C
inst✝ : HasIterationOfShape K C
⊢ ((monomorphisms C).functorCategory J).IsStableUnderTransfiniteCompositionOfShape K

Tactic:
infer_instance

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Mono (faceι i)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.MorphismProperty.FunctorCategory

Goal state before:
pp: C : Type u
inst✝⁴ : Category.{v, u} C
W : MorphismProperty C
J : Type u''
inst✝³ : Category.{v'', u''} J
K' : Type u'
inst✝² : (monomorphisms C).IsStableUnderCoproductsOfShape K'
inst✝¹ : HasCoproductsOfShape K' C
inst✝ : HasPullbacks C
⊢ ((monomorphisms C).functorCategory J).IsStableUnderCoproductsOfShape K'

Tactic:
infer_instance

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
⊢ Mono (ι i ≫ ∂Δ[n + 1].ι)

Tactic:
infer_instance

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ J.rlp.IsMultiplicative

Tactic:
infer_instance

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ J.rlp.IsStableUnderRetracts

Tactic:
infer_instance

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ (monomorphisms SSet).IsMultiplicative

Tactic:
infer_instance

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ (monomorphisms SSet).IsStableUnderRetracts

Tactic:
infer_instance

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
c : PushoutCocone f g
hc : IsColimit c
inst✝ : Mono f
⊢ Mono
    (Pushout.inr f g ≫
      ((Cocone.forget (span f g)).mapIso
          (Cocone.ext (hc.coconePointUniqueUpToIso (Pushout.isColimitCocone f g)) ⋯)).inv)

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: case h_obj
C : Type u
inst✝ : Category.{v, u} C
x✝ : ↑chosenTerminal ⥤ C
⊢ ∀ (X : ↑chosenTerminal),
    ((Functor.const ↑chosenTerminal).obj ((fun F ↦ F.obj { down := { as := () } }) x✝)).obj X = x✝.obj X

Tactic:
intro

Goal state after:
case h_obj
C : Type u
inst✝ : Category.{v, u} C
x✝ : ↑chosenTerminal ⥤ C
X✝ : ↑chosenTerminal
⊢ ((Functor.const ↑chosenTerminal).obj ((fun F ↦ F.obj { down := { as := () } }) x✝)).obj X✝ = x✝.obj X✝
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: ⊢ MonoidalCategory Cat

Tactic:
infer_instance

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Cartesian.Cat

Goal state before:
pp: ⊢ SymmetricCategory Cat

Tactic:
infer_instance

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
p✝ : X.Path n
p : X.Path (n + 1)
⊢ p.vertex (Fin.succ 0) = (ConcreteCategory.hom (X.map (⦋0⦌.const ⦋n⦌ 0).op)) (spineToSimplex h (p.interval 1 n ⋯))

Tactic:
exact Path.congr_vertex (spine_spineToSimplex h (p.interval 1 n)).symm 0

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'
⊢ hComp η (𝟙 (𝟙 b)) = eqToHom ⋯ ≫ η ≫ eqToHom ⋯

Tactic:
by
  ext
  simp only [hComp, Hom.base_id, base_mk, ← heq_eq_eq, eqToHom_comp_heq_iff, comp_eqToHom_heq_iff]
  rw [homEquiv_id]
  simp [CatEnriched.hComp_id_heq]

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

Goal state before:
pp: C : Type u₁
inst✝² : Category.{v₁, u₁} C
inst✝¹ : MonoidalCategory C
X Y : Center C
f : X ⟶ Y
inst✝ : IsIso f.f
⊢ IsIso (isoMk f).hom

Tactic:
infer_instance

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
X₁✝ Y₁✝ X₂✝ Y₂✝ : Center C
f✝ : X₁✝ ⟶ Y₁✝
g✝ : X₂✝ ⟶ Y₂✝
⊢ (tensorHom f✝ g✝).f = (whiskerRight f✝ X₂✝ ≫ Y₁✝.whiskerLeft g✝).f

Tactic:
simp [tensorHom_def]

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

Goal state before:
pp: C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : MonoidalCategory C
A✝ B✝ : Center C
f : A✝ ⟶ B✝
i : IsIso f.f
⊢ IsIso (isoMk f).hom

Tactic:
infer_instance

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
inst✝ : X.IsCoskeletal n
⊢ X.IsCoskeletal n

Tactic:
infer_instance

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
this : Unique (W₁.MapFactorizationData W₂ f)
⊢ Subsingleton (W₁.MapFactorizationData W₂ f)

Tactic:
infer_instance

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 Z : C
f : X ⟶ Y
g : Y ⟶ Z
w✝ : C
g₁ : Y ⟶ w✝
g₂ : w✝ ⟶ Z
left✝¹ : W₁ g₁
left✝ : W₂ g₂
h_fac : g₁ ≫ g₂ = g
h_deg : r.degHom g = r.deg w✝
⊢ r.degHom ((f ≫ g₁) ≫ g₂) ≤ r.deg w✝

Tactic:
exact r.degHom_le (f ≫ g₁) g₂

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

Goal state before:
pp: P : MorphismProperty SimplexCategoryGenRel
id : ∀ {n : ℕ}, P (𝟙 (mk n))
comp_δ : ∀ {n m : ℕ} (u : mk n ⟶ mk m) (i : Fin (m + 2)), P u → P (u ≫ δ i)
comp_σ : ∀ {n m : ℕ} (u : mk n ⟶ mk (m + 1)) (i : Fin (m + 1)), P u → P (u ≫ σ i)
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
  | comp_of f g hf hg hrec =>
    rcases hg with ⟨⟨i⟩⟩ | ⟨⟨i⟩⟩
    · simpa using! (comp_δ f i hrec)
    · simpa using! (comp_σ f i hrec)

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

Goal state before:
pp: case of.σ
x y : SimplexCategoryGenRel
e : x ⟶ y
n✝ : ℕ
i✝ : Fin (n✝ + 1)
⊢ IsSplitEpi (σ i✝)

Tactic:
infer_instance

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

Goal state before:
pp: case id
x y : SimplexCategoryGenRel
e : x ⟶ y
x✝ : SimplexCategoryGenRel
⊢ IsSplitEpi (𝟙 x✝)

Tactic:
infer_instance

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

Goal state before:
pp: case comp_of.σ
x y : SimplexCategoryGenRel
e : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 1)
f✝ : x✝ ⟶ mk (n✝ + 1)
hf✝ : degeneracies.multiplicativeClosure f✝
hf_ih✝ : IsSplitEpi f✝
⊢ IsSplitEpi (f✝ ≫ σ i✝)

Tactic:
infer_instance

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

Goal state before:
pp: case of.δ
x y : SimplexCategoryGenRel
m : x ⟶ y
n✝ : ℕ
i✝ : Fin (n✝ + 2)
⊢ IsSplitMono (δ i✝)

Tactic:
infer_instance

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

Goal state before:
pp: case id
x y : SimplexCategoryGenRel
m : x ⟶ y
x✝ : SimplexCategoryGenRel
⊢ IsSplitMono (𝟙 x✝)

Tactic:
infer_instance

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

Goal state before:
pp: case comp_of.δ
x y : SimplexCategoryGenRel
m : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
f✝ : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure f✝
hf_ih✝ : IsSplitMono f✝
⊢ IsSplitMono (f✝ ≫ δ i✝)

Tactic:
infer_instance

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

Goal state before:
pp: case comp_of.inl
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
e : x✝ = y✝
h✝ : i = eqToHom e
⊢ x✝.len < z✝.len

Tactic:
cases hg

Goal state after:
case comp_of.inl.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
i : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure i
e : x✝ = mk n✝
h✝ : i = eqToHom e
⊢ x✝.len < (mk (n✝ + 1)).len
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_of.inr
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ y✝ z✝ : SimplexCategoryGenRel
i : x✝ ⟶ y✝
u : y✝ ⟶ z✝
hf✝ : faces.multiplicativeClosure i
hg : faces u
h' : x✝.len < y✝.len
⊢ x✝.len < z✝.len

Tactic:
cases hg

Goal state after:
case comp_of.inr.δ
x y : SimplexCategoryGenRel
f : x ⟶ y
x✝ : SimplexCategoryGenRel
n✝ : ℕ
i✝ : Fin (n✝ + 2)
i : x✝ ⟶ mk n✝
hf✝ : faces.multiplicativeClosure i
h' : x✝.len < (mk n✝).len
⊢ x✝.len < (mk (n✝ + 1)).len
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono

Goal state before:
pp: case comp_σ.comp_of.zero
x y : SimplexCategoryGenRel
n : ℕ
z : SimplexCategoryGenRel
e : mk n ⟶ z
he : P_σ e
y✝ : SimplexCategoryGenRel
f : z ⟶ y✝
hf : faces.multiplicativeClosure f
j : Fin (0 + 1)
g : y✝ ⟶ mk (0 + 1)
hg : faces g
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ g) ≫ σ j = e_1 ≫ m

Tactic:
cases hg

Goal state after:
case comp_σ.comp_of.zero.δ
x y : SimplexCategoryGenRel
n : ℕ
z : SimplexCategoryGenRel
e : mk n ⟶ z
he : P_σ e
j : Fin (0 + 1)
i✝ : Fin (0 + 2)
f : z ⟶ mk 0
hf : faces.multiplicativeClosure f
⊢ ∃ z_1 e_1 m, ∃ (_ : P_σ e_1) (_ : P_δ m), (e ≫ f ≫ δ i✝) ≫ σ j = e_1 ≫ m
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
hk' : j.castSucc < k
⊢ (j.predAbove k).castSucc < i

Tactic:
rwa [Fin.predAbove_of_castSucc_lt _ _ hk', Fin.castSucc_pred_lt_iff]

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

Goal state before:
pp: case pos
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
⊢ ∃ a, toMk₁ a = f

Tactic:
refine ⟨(S.min' hS).castSucc, ConcreteCategory.hom_ext _ _ (fun i ↦ ?_)⟩

Goal state after:
case pos
n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ (ConcreteCategory.hom (toMk₁ (S.min' hS).castSucc)) i = (ConcreteCategory.hom f) i
Module: Mathlib.AlgebraicTopology.SimplicialSet.Coskeletal

Goal state before:
pp: X : Cat
⊢ ((truncation 2).obj (nerve ↑X)).IsStrictSegal

Tactic:
infer_instance

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

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

Tactic:
Fin.le_def

Goal state after:
case left.left
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₁.len + 1)
h : ↑(Fin.castAdd (x₂.len + 1) i✝¹) ≤ ↑(Fin.castAdd (x₂.len + 1) 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)
        (Fin.castAdd (x₂.len + 1) 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)
        (Fin.castAdd (x₂.len + 1) i✝))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: 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 : Fin.castAdd (x₂.len + 1) i✝¹ ≤ Fin.natAdd (x₁.len + 1) 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)
      (Fin.castAdd (x₂.len + 1) 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)
      (Fin.natAdd (x₁.len + 1) i✝)

Tactic:
Fin.le_def

Goal state after:
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 : ↑(Fin.castAdd (x₂.len + 1) i✝¹) ≤ ↑(Fin.natAdd (x₁.len + 1) 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)
        (Fin.castAdd (x₂.len + 1) 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)
        (Fin.natAdd (x₁.len + 1) i✝))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: 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 : Fin.natAdd (x₁.len + 1) i✝¹ ≤ Fin.castAdd (x₂.len + 1) 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)
      (Fin.natAdd (x₁.len + 1) 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)
      (Fin.castAdd (x₂.len + 1) i✝)

Tactic:
Fin.le_def

Goal state after:
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 : ↑(Fin.natAdd (x₁.len + 1) i✝¹) ≤ ↑(Fin.castAdd (x₂.len + 1) 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)
        (Fin.natAdd (x₁.len + 1) 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)
        (Fin.castAdd (x₂.len + 1) i✝))
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

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

Tactic:
Fin.le_def

Goal state after:
case right.right
x₁ y₁ x₂ y₂ : SimplexCategory
f₁ : x₁ ⟶ y₁
f₂ : x₂ ⟶ y₂
i✝¹ i✝ : Fin (x₂.len + 1)
h : ↑(Fin.natAdd (x₁.len + 1) i✝¹) ≤ ↑(Fin.natAdd (x₁.len + 1) 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)
        (Fin.natAdd (x₁.len + 1) 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)
        (Fin.natAdd (x₁.len + 1) i✝))
Module: Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex

Goal state before:
pp: X : SSet
A : X.Subcomplex
Y : SSet
B : Y.Subcomplex
e : X ≅ Y
hA : B.preimage e.hom = A
y : B.N
⊢ ((SSet.N.orderIsoOfIso e).symm y.toN).simplex ∉ A.obj (Opposite.op ⦋((SSet.N.orderIsoOfIso e).symm y.toN).dim⦌)

Tactic:
by
    obtain rfl : A.preimage e.inv = B := by aesop
    exact y.notMem

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

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst✝ : Mono f
hf : (ConcreteCategory.hom (X.map f.op)) (y.cast ⋯).simplex = (x.cast hd).simplex
⊢ Mono f

Tactic:
infer_instance

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

Goal state before:
pp: X : SSet
x y : X.S
hxy : x.IsUniquelyCodimOneFace y
d : ℕ
hd : x.dim = d
f : ⦋d⦌ ⟶ ⦋d + 1⦌
inst✝ : Mono f
hf : (ConcreteCategory.hom (X.map f.op)) (y.cast ⋯).simplex = (x.cast hd).simplex
⊢ Mono (SimplexCategory.δ (hxy.index hd))

Tactic:
infer_instance

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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
d dx : ℕ
x : X _⦋dx⦌
hd : { dim := dx, simplex := x }.dim = d
dy : ℕ
y : X _⦋dy⦌
hxy : { dim := dx, simplex := x }.IsUniquelyCodimOneFace { dim := dy, simplex := y }
⊢ ⋯.index hd = hxy.index hd

Tactic:
obtain rfl : dy = dx + 1 := hxy.dim_eq

Goal state after:
X Y : SSet
e : X ≅ Y
d dx : ℕ
x : X _⦋dx⦌
hd : { dim := dx, simplex := x }.dim = d
y : X _⦋dx + 1⦌
hxy : { dim := dx, simplex := x }.IsUniquelyCodimOneFace { dim := dx + 1, simplex := y }
⊢ ⋯.index hd = hxy.index hd
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
x : A.N
hx : x ∈ P.I
⊢ ↑⟨x, hx⟩ ≠ ↑y

Tactic:
obtain ⟨y, hy⟩ := y

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
x : A.N
hx : x ∈ P.I
y : A.N
hy : y ∈ P.II
⊢ ↑⟨x, hx⟩ ≠ ↑⟨y, hy⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex

Goal state before:
pp: p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
i j : Fin (n + 1)
h : i ≤ j
⊢ ↑(x.1 i) + ↑(x.2 i) ≤ ↑(x.1 j) + ↑(x.2 j)

Tactic:
have := (objEquiv x).monotone h

Goal state after:
p q n : ℕ
x : (Δ[p] ⊗ Δ[q]) _⦋n⦌
m : ℕ
hm : p + q = m
i j : Fin (n + 1)
h : i ≤ j
this : (objEquiv x) i ≤ (objEquiv x) j
⊢ ↑(x.1 i) + ↑(x.2 i) ≤ ↑(x.1 j) + ↑(x.2 j)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
n : ℕ
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
i : Fin (n + 2)
this✝ : Mono (yonedaEquiv.symm x)
this :
  (ConcreteCategory.hom (SimplicialObject.δ X i)) x =
    (ConcreteCategory.hom ((yonedaEquiv.symm x).app (op ⦋n⦌))) (stdSimplex.objEquiv.symm (SimplexCategory.δ i))
⊢ Mono (SimplexCategory.δ i)

Tactic:
infer_instance

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

Goal state before:
pp: X : SSet
inst✝ : X.Nonsingular
x y : X.N
h : x ≤ y
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
w✝ : Mono f
hf : (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
⊢ ∃ x_1, Mono x_1 ∧ (ConcreteCategory.hom (X.map x_1.op)) y.simplex = x.simplex

Tactic:
exact ⟨f, inferInstance, hf⟩

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
s : A.N
this : ∃ s_1, s = h.type₁ s_1 ∨ s = h.type₂ s_1
⊢ s ∈ h.I ∪ h.II ↔ s ∈ Set.univ

Tactic:
simp only [I, II, Set.mem_union, Set.mem_range, Set.mem_univ, iff_true]

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
s : A.N
this : ∃ s_1, s = h.type₁ s_1 ∨ s = h.type₂ s_1
⊢ (∃ y, h.type₁ y = s) ∨ ∃ y, h.type₂ y = s
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
x✝ : h.pairing.IsRegular
⊢ h.pairing.IsProper

Tactic:
infer_instance

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.PairingCore
inst✝ : P.IsProper
⊢ Nonempty (P.pairing.RankFunction ℕ) ↔ Nonempty (P.RankFunction ℕ)

Tactic:
exact (P.rankFunctionEquiv ℕ).symm.nonempty_congr

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

Goal state before:
pp: J : Type u_1
inst✝¹ : Category.{u_2, u_1} J
inst✝ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
n : ℕ
h : ∀ (j : J), (F.obj j).HasDimensionLT n
⊢ ∀ (i : J), (Subcomplex.range (c.ι.app i)).toSSet.HasDimensionLT n

Tactic:
infer_instance

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

Goal state before:
pp: J : Type u_1
inst✝² : Category.{u_2, u_1} J
inst✝¹ : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
inst✝ : Finite J
h : ∀ (j : J), (F.obj j).Finite
⊢ ∀ (i : J), (Subcomplex.range (c.ι.app i)).toSSet.Finite

Tactic:
infer_instance

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

Goal state before:
pp: case left
J : Type u_1
inst✝³ : Category.{?u.4, u_1} J
inst✝² : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst✝¹ : X.Finite
inst✝ : Y.Finite
⊢ X.Finite

Tactic:
infer_instance

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

Goal state before:
pp: case right
J : Type u_1
inst✝³ : Category.{?u.4, u_1} J
inst✝² : HasColimitsOfShape J (Type u)
F : J ⥤ SSet
c : Cocone F
hc : IsColimit c
X Y : SSet
inst✝¹ : X.Finite
inst✝ : Y.Finite
⊢ Y.Finite

Tactic:
infer_instance

Goal state after: