mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma

Goal state before:
pp: C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X✝ Y✝ Y : C
inst✝¹ : IsFibrant Y
h✝¹ : IsCofibrant Y
X : C
inst✝ : IsCofibrant X
h✝ : IsFibrant X
E : BifibrantObject.HoCat C ≌ H :=
  Localization.uniq BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L) (weakEquivalences (BifibrantObject C))
e : BifibrantObject.toHoCat ⋙ E.functor ≅ BifibrantObject.ι ⋙ L :=
  Localization.compUniqFunctor BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L) (weakEquivalences (BifibrantObject C))
f : RightHomotopyClass X Y
⊢ rightHomotopyClassToHom L f =
    (BifibrantObject.HoCat.homEquivRight.trans
        (E.fullyFaithfulFunctor.homEquiv.trans
          ((e.app (BifibrantObject.mk X)).homCongr (e.app (BifibrantObject.mk Y)))))
      f

Tactic:
obtain ⟨f, rfl⟩ := RightHomotopyClass.mk_surjective f

Goal state after:
C : Type u_1
inst✝⁵ : Category.{v_1, u_1} C
inst✝⁴ : ModelCategory C
H : Type u_2
inst✝³ : Category.{v_2, u_2} H
L : C ⥤ H
inst✝² : L.IsLocalization (weakEquivalences C)
X✝ Y✝ Y : C
inst✝¹ : IsFibrant Y
h✝¹ : IsCofibrant Y
X : C
inst✝ : IsCofibrant X
h✝ : IsFibrant X
E : BifibrantObject.HoCat C ≌ H :=
  Localization.uniq BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L) (weakEquivalences (BifibrantObject C))
e : BifibrantObject.toHoCat ⋙ E.functor ≅ BifibrantObject.ι ⋙ L :=
  Localization.compUniqFunctor BifibrantObject.toHoCat (BifibrantObject.ι ⋙ L) (weakEquivalences (BifibrantObject C))
f : X ⟶ Y
⊢ rightHomotopyClassToHom L (RightHomotopyClass.mk f) =
    (BifibrantObject.HoCat.homEquivRight.trans
        (E.fullyFaithfulFunctor.homEquiv.trans
          ((e.app (BifibrantObject.mk X)).homCongr (e.app (BifibrantObject.mk Y)))))
      (RightHomotopyClass.mk f)
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (weakEquivalences C).HasTwoOutOfThreeProperty
⊢ (weakEquivalences Cᵒᵖ).HasTwoOutOfThreeProperty

Tactic:
rw [weakEquivalences_op]
  infer_instance

Goal state after:
Module: Mathlib.AlgebraicTopology.ModelCategory.Opposite

Goal state before:
pp: C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : ModelCategory C
inst✝ : (weakEquivalences C).IsStableUnderRetracts
⊢ (weakEquivalences Cᵒᵖ).IsStableUnderRetracts

Tactic:
rw [weakEquivalences_op]
  infer_instance

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
⊢ stdSimplex.face {i}ᶜ ≤ ⨆ i, stdSimplex.face {i}ᶜ

Tactic:
exact le_iSup (fun (i : Fin (n +1)) ↦ stdSimplex.face {i}ᶜ) i

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 (J ⥤ C)).IsStableUnderTransfiniteCompositionOfShape K

Tactic:
by
  rw [← functorCategory_monomorphisms]
  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 (J ⥤ C)).IsStableUnderCoproductsOfShape K'

Tactic:
by
  rw [← functorCategory_monomorphisms]
  infer_instance

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

Goal state before:
pp: n : ℕ
X : SSet
f g : ∂Δ[n + 1].toSSet ⟶ X
h : ∀ (i : Fin (n + 2)), ι i ≫ f = ι i ≫ g
⊢ f = g

Tactic:
ext m ⟨x, hx⟩
  simp only [boundary_eq_iSup, stdSimplex.face_singleton_compl, Subfunctor.iSup_obj,
    Set.mem_iUnion, Subcomplex.mem_ofSimplex_obj_iff, op_unop] at hx
  obtain ⟨i, ⟨y, rfl⟩⟩ := hx
  exact ConcreteCategory.congr_hom (congr_app (h i) _) _

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
hij : j ≠ i
⊢ ι i j hij ≫ Λ[n + 1, i].ι = stdSimplex.δ j

Tactic:
rw [ι, face, Equiv.symm_apply_apply, Subfunctor.lift_ι]

Goal state after:
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))
i₁ : T
x₁ : X₁ i₁
i₂ : T
x₂ : X₁ i₂
hx : (hom (Sigma.ι X₂ i₁)) ((hom (f i₁)) x₁) = (hom (Sigma.ι X₂ i₂)) ((hom (f i₂)) x₂)
⊢ (hom (Sigma.ι X₁ i₁)) x₁ = (hom (Sigma.ι X₁ i₂)) x₂

Tactic:
obtain rfl := Cofan.eq_of_inj_apply_eq_of_isColimit (coproductIsCoproduct X₂) _ _ hx

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))
i₁ : T
x₁ x₂ : X₁ i₁
hx : (hom (Sigma.ι X₂ i₁)) ((hom (f i₁)) x₁) = (hom (Sigma.ι X₂ i₁)) ((hom (f i₁)) x₂)
⊢ (hom (Sigma.ι X₁ i₁)) x₁ = (hom (Sigma.ι X₁ i₁)) x₂
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
z₂ : X₂
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) y₀✝)) (Sum.inr z₂)
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inr z₂)

Tactic:
rw [inl_rel'_inr_iff] at hyz

Goal state after:
case inl_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
x₀✝ y₀✝ : S
h : (ConcreteCategory.hom g) x₀✝ = (ConcreteCategory.hom g) y₀✝
z₂ : X₂
hyz : ∃ s, (ConcreteCategory.hom f) y₀✝ = (ConcreteCategory.hom f) s ∧ z₂ = (ConcreteCategory.hom g) s
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) x₀✝)) (Sum.inr z₂)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inl_inr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
z₁ : X₁
hyz : Rel' f g (Sum.inl z₁) (Sum.inr ((ConcreteCategory.hom g) s))
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inl z₁)

Tactic:
rw [inl_rel'_inr_iff] at hyz

Goal state after:
case inl_inr.inl
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
z₁ : X₁
hyz : ∃ s_1, z₁ = (ConcreteCategory.hom f) s_1 ∧ (ConcreteCategory.hom g) s = (ConcreteCategory.hom g) s_1
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inl z₁)
Module: Mathlib.CategoryTheory.Limits.Types.Pushouts

Goal state before:
pp: case inr_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
z₂ : X₂
hyz : Rel' f g (Sum.inl ((ConcreteCategory.hom f) s✝)) (Sum.inr z₂)
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inr z₂)

Tactic:
rw [inl_rel'_inr_iff] at hyz

Goal state after:
case inr_inl.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s✝ : S
z₂ : X₂
hyz : ∃ s, (ConcreteCategory.hom f) s✝ = (ConcreteCategory.hom f) s ∧ z₂ = (ConcreteCategory.hom g) s
⊢ Rel' f g (Sum.inr ((ConcreteCategory.hom g) s✝)) (Sum.inr z₂)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Skeleton

Goal state before:
pp: X : SSet
i n : ℕ
hi : i < n
j : ℕ
f : ⦋i⦌ ⟶ ⦋j⦌
w✝ : Epi f
y : ↑(X.nonDegenerate j)
⊢ Subcomplex.ofSimplex ↑y ≤ ⨆ x, Subcomplex.ofSimplex ↑x

Tactic:
exact le_trans (by rfl) (le_iSup _ y)

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

Goal state before:
pp: n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
k : Fin (m + 1)
⊢ ((sy.spineEquiv (m + 1) ⋯) (sy.spineToSimplex (m + 1) ⋯ (f.map σ))).arrow k =
    ((sy.spineEquiv (m + 1) ⋯)
          ((ConcreteCategory.hom (σ.app (op { obj := ⦋m + 1⦌, property := ⋯ }))) (sx.spineToSimplex (m + 1) ⋯ f))).arrow
      k

Tactic:
dsimp only [spineEquiv, Equiv.coe_fn_mk, spine_arrow]

Goal state after:
n : ℕ
X Y : Truncated (n + 1)
sx : X.StrictSegal
sy : Y.StrictSegal
m : ℕ
h : m ≤ n
f : X.Path (m + 1)
σ : X ⟶ Y
k : Fin (m + 1)
⊢ (ConcreteCategory.hom (Y.map (tr (mkOfSucc k) ⋯ ⋯).op)) (sy.spineToSimplex (m + 1) ⋯ (f.map σ)) =
    (ConcreteCategory.hom (Y.map (tr (mkOfSucc k) ⋯ ⋯).op))
      ((ConcreteCategory.hom (σ.app (op { obj := ⦋m + 1⦌, property := ⋯ }))) (sx.spineToSimplex (m + 1) ⋯ f))
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)
⊢ ((sy.spineEquiv (n + 1)) (sy.spineToSimplex (f.map σ))).arrow k =
    ((sy.spineEquiv (n + 1)) ((ConcreteCategory.hom (σ.app (Opposite.op ⦋n + 1⦌))) (sx.spineToSimplex f))).arrow k

Tactic:
dsimp only [spineEquiv, Equiv.coe_fn_mk, spine_arrow]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 2)
⊢ (stdSimplex.spineId (n + 2)).arrow j ∈ Λ[n + 2, i].obj (op ⦋1⦌)

Tactic:
convert! (horn.primitiveEdge.{u} h₀ hₙ j).2

Goal state after:
n : ℕ
i : Fin (n + 3)
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 2)
⊢ (stdSimplex.spineId (n + 2)).arrow j = ↑(primitiveEdge h₀ hₙ j)
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
A A' : (C ⥤ Type w)ᵒᵖ
f : A ⟶ A'
x : F.HomObj G (Opposite.unop A)
X Y : C
φ : X ⟶ Y
a : (Opposite.unop A').obj X
⊢ F.map φ ≫ x.app Y ((ConcreteCategory.hom (f.unop.app Y)) ((ConcreteCategory.hom ((Opposite.unop A').map φ)) a)) =
    x.app X ((ConcreteCategory.hom (f.unop.app X)) a) ≫ G.map φ

Tactic:
by
        rw [← HomObj.naturality]
        congr 2
        exact ConcreteCategory.congr_hom (f.unop.naturality φ) a

Goal state after:
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
A : C ⥤ Type (max u v v')
φ : A ⟶ F.functorHom G
X Y : C
f : X ⟶ Y
a : A.obj X
⊢ F.map f ≫
      ((ConcreteCategory.hom (φ.app Y)) ((ConcreteCategory.hom (A.map f)) a)).app Y
        (𝟙 (Opposite.unop (Opposite.op Y))) =
    ((ConcreteCategory.hom (φ.app X)) a).app X (𝟙 (Opposite.unop (Opposite.op X))) ≫ G.map f

Tactic:
by
        rw [← (φ.app X a).naturality f (𝟙 _)]
        have := HomObj.congr_app (ConcreteCategory.congr_hom (φ.naturality f) a) Y (𝟙 _)
        simp_all [-NatTrans.naturality, functorHom, homObjFunctor]

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

Goal state before:
pp: K : SSet
x : K _⦋0⦌
Δ Δ' : SimplexCategoryᵒᵖ
f : Δ ⟶ Δ'
⊢ (ConcreteCategory.hom (K.map ((Opposite.unop Δ').const ⦋0⦌ 0).op)) x =
    (ConcreteCategory.hom (K.map f)) ((ConcreteCategory.hom (K.map ((Opposite.unop Δ).const ⦋0⦌ 0).op)) x)

Tactic:
rw [← Functor.map_comp_apply]

Goal state after:
K : SSet
x : K _⦋0⦌
Δ Δ' : SimplexCategoryᵒᵖ
f : Δ ⟶ Δ'
⊢ (ConcreteCategory.hom (K.map ((Opposite.unop Δ').const ⦋0⦌ 0).op)) x =
    (ConcreteCategory.hom (K.map (((Opposite.unop Δ).const ⦋0⦌ 0).op ≫ f))) x
Module: Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal

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

Tactic:
isCoskeletal_iff

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

Goal state before:
pp: V : Type u_1
inst✝¹ : ReflQuiver V
D : Type u_2
inst✝ : Category.{v_1, u_2} D
F G : FreeRefl V ⥤ D
h₁ : ∀ (v : V), F.obj (mk v) = G.obj (mk v)
h₂ : ∀ {v w : V} (f : v ⟶ w), F.map (homMk f) = eqToHom ⋯ ≫ G.map (homMk f) ≫ eqToHom ⋯
x✝ : Paths V
⊢ (quotientFunctor V ⋙ F).obj x✝ = (quotientFunctor V ⋙ G).obj x✝

Tactic:
apply h₁

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

Goal state before:
pp: X✝ : SSet
sx✝ : X✝.StrictSegal
X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : Fin n
⊢ (ConcreteCategory.hom
        (((Truncated.trunc (0 + 1) 1 ⋯).obj ((truncation 1).obj X)).map
          (Hom.tr (SimplexCategory.δ 0) Truncated.Path₁._proof_1 Truncated.Path₁._proof_5).op))
      ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (mkOfLe i.castSucc i.succ ⋯).op))) x) =
    (ConcreteCategory.hom
        (s.π.app
          (StructuredArrow.mk
            (((inclusion 2).obj (unop (op { obj := ⦋0⦌, property := lift._proof_2 }))).const ⦋n⦌ i.succ).op)))
      x

Tactic:
by
      dsimp
      let φ : strArrowMk₂ (mkOfLe _ _ (Fin.castSucc_le_succ i)) ⟶
          strArrowMk₂ (⦋0⦌.const _ i.succ) :=
        StructuredArrow.homMk (Hom.tr (δ 0)).op
          (Quiver.Hom.unop_inj (by ext x; fin_cases x; rfl))
      exact ConcreteCategory.congr_hom (s.w φ) x

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

Goal state before:
pp: case id
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✝
n : SimplexCategoryGenRel
⊢ P (𝟙 n)

Tactic:
exact id

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

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

Tactic:
exact id

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

Goal state before:
pp: case cons
j a : ℕ
L : List ℕ
h_rec : ∀ {m : ℕ}, IsAdmissible m L → j < m + L.length → simplicialEvalσ L j = simplicialEvalσ L (j + 1) → j ∈ L
m : ℕ
hL : IsAdmissible m (a :: L)
hj₁ : j < m + (a :: L).length
hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)
this : ∀ ⦃b : ℕ⦄, a + 1 ≤ b → simplicialEvalσ L (a + 1) ≤ simplicialEvalσ L b
⊢ j ∈ a :: L

Tactic:
rcases lt_trichotomy j a with h | h | h

Goal state after:
case cons.inl
j a : ℕ
L : List ℕ
h_rec : ∀ {m : ℕ}, IsAdmissible m L → j < m + L.length → simplicialEvalσ L j = simplicialEvalσ L (j + 1) → j ∈ L
m : ℕ
hL : IsAdmissible m (a :: L)
hj₁ : j < m + (a :: L).length
hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)
this : ∀ ⦃b : ℕ⦄, a + 1 ≤ b → simplicialEvalσ L (a + 1) ≤ simplicialEvalσ L b
h : j < a
⊢ j ∈ a :: L

case cons.inr.inl
j a : ℕ
L : List ℕ
h_rec : ∀ {m : ℕ}, IsAdmissible m L → j < m + L.length → simplicialEvalσ L j = simplicialEvalσ L (j + 1) → j ∈ L
m : ℕ
hL : IsAdmissible m (a :: L)
hj₁ : j < m + (a :: L).length
hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)
this : ∀ ⦃b : ℕ⦄, a + 1 ≤ b → simplicialEvalσ L (a + 1) ≤ simplicialEvalσ L b
h : j = a
⊢ j ∈ a :: L

case cons.inr.inr
j a : ℕ
L : List ℕ
h_rec : ∀ {m : ℕ}, IsAdmissible m L → j < m + L.length → simplicialEvalσ L j = simplicialEvalσ L (j + 1) → j ∈ L
m : ℕ
hL : IsAdmissible m (a :: L)
hj₁ : j < m + (a :: L).length
hj₂ : simplicialEvalσ (a :: L) j = simplicialEvalσ (a :: L) (j + 1)
this : ∀ ⦃b : ℕ⦄, a + 1 ≤ b → simplicialEvalσ L (a + 1) ≤ simplicialEvalσ L b
h : a < j
⊢ j ∈ a :: L
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

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

Tactic:
grind [Fin.castPred, Fin.predAbove_of_le_castSucc, toMk₁_of_castSucc_lt]

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case right
ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
⊢ sSup x✝ ∈ lowerBounds (upperBounds x✝)

Tactic:
intro L hL _ ht
      cases ht with
      | inl ht =>
        simp only [Set.mem_iUnion] at ht
        obtain ⟨K, hK, htK⟩ := ht
        exact hL hK htK
      | inr ht =>
        obtain ⟨v, hv⟩ := ht
        exact hv ▸ L.singleton_mem v

Goal state after:
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
⊢ ((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 := ⋯ }))).arrow
      k =
    ((sx.spineEquiv i) ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))) x)).arrow k

Tactic:
dsimp only [spineEquiv, Equiv.coe_fn_mk, spine_arrow]

Goal state after:
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
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((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 := ⋯ })) =
    (ConcreteCategory.hom (X.map (mkOfSucc k).op)) ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))) 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
⊢ (ConcreteCategory.hom (X.map (mkOfSucc k).op))
      ((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 := ⋯ })) =
    (ConcreteCategory.hom (X.map (mkOfSucc k).op)) ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))) x)

Tactic:
rw [← Functor.map_comp_apply]

Goal state after:
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
⊢ (ConcreteCategory.hom (X.map (op f ≫ (mkOfSucc k).op)))
      (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 := ⋯ }) =
    (ConcreteCategory.hom (X.map (mkOfSucc k).op)) ((ConcreteCategory.hom (s.π.app (StructuredArrow.mk (op f)))) x)
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case inl.inl.inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : map' f y.castSucc = z.castSucc
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc

Tactic:
hz,

Goal state after:
case inl.inl.inl
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
z : Fin (n + 1)
hz : map' f y.castSucc = z.castSucc
⊢ z.castSucc = map' (g.comp f) x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j k : SimplicialThickening J
⊢ eComp SSet i j k ≫ nerveMap (functorMap f i k) =
    (nerveMap (functorMap f i j) ⊗ₘ nerveMap (functorMap f j k)) ≫
      eComp SSet { as := f i.as } { as := f j.as } { as := f k.as }

Tactic:
ext
    simp only [eComp, EnrichedCategory.comp]
    exact Functor.ext (by cat_disch)

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

Goal state before:
pp: case inl.inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
hz : map' f y.castSucc = Fin.last (n + 1)
⊢ map' f y.castSucc = map' (g.comp f) x.castSucc

Tactic:
hz,

Goal state after:
case inl.inl.inr
n m p : ℕ
f : Fin (n + 1) →o Fin (m + 1)
g : Fin (m + 1) →o Fin (p + 1)
x : Fin (p + 1)
y : Fin (m + 1)
hy : x.castSucc ≤ (g y).castSucc ∧ ∀ i < y, (g i).castSucc < x.castSucc
hz : map' f y.castSucc = Fin.last (n + 1)
⊢ Fin.last (n + 1) = map' (g.comp f) x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝¹ : h.IsInner
inst✝ : h.IsProper
s : h.ι
⊢ ⋯.index ⋯ ≠ 0

Tactic:
simpa using IsInner.ne_zero s

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
⊢ range c.map = (↑(P.p c.s)).subcomplex

Tactic:
by
  rw [range_eq_ofSimplex, Equiv.apply_symm_apply, S.ofSimplex_eq_subcomplex_mk,
    ← S.cast_eq_self _ (P.dim_p c.s)]
  dsimp [S.subcomplex]

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 ≤ ⊤
t : ↑P.II
ht : s = ↑t ∨ s = ↑(P.p t)
⊢ s.subcomplex ≤ (↑(P.p { s := t, rank_s := ⋯ }.s)).subcomplex

Tactic:
obtain rfl | rfl := ht

Goal state after:
case notMem.inl
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁴ : LinearOrder ι
f : P.RankFunction ι
inst✝³ : P.IsProper
inst✝² : OrderBot ι
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
t : ↑P.II
a✝ : (↑t).subcomplex ≤ ⊤
⊢ (↑t).subcomplex ≤ (↑(P.p { s := t, rank_s := ⋯ }.s)).subcomplex

case notMem.inr
X : SSet
A : X.Subcomplex
P : A.Pairing
ι : Type v
inst✝⁴ : LinearOrder ι
f : P.RankFunction ι
inst✝³ : P.IsProper
inst✝² : OrderBot ι
inst✝¹ : SuccOrder ι
inst✝ : NoMaxOrder ι
t : ↑P.II
a✝ : (↑(P.p t)).subcomplex ≤ ⊤
⊢ (↑(P.p t)).subcomplex ≤ (↑(P.p { s := t, rank_s := ⋯ }.s)).subcomplex