mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.DoldKan.SplitSimplicialObject

Goal state before:
pp: case mp.zero
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
X : SimplicialObject C
s : X.Splitting
inst✝ : Preadditive C
Z : C
f : Z ⟶ X _⦋0⦌
h : f = 0
⊢ f ≫ s.πSummand (IndexSet.id (op ⦋0⦌)) = 0

Tactic:
rw [h, zero_comp]

Goal state after:
Module: Mathlib.Topology.Homotopy.TopCat.Basic

Goal state before:
pp: X Y : TopCat
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
⊢ ι₀ ≫ F.h = f₀

Tactic:
ext x

Goal state after:
X Y : TopCat
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
x : ↑X
⊢ (ConcreteCategory.hom (ι₀ ≫ F.h)) x = (ConcreteCategory.hom f₀) x
Module: Mathlib.Topology.Homotopy.TopCat.Basic

Goal state before:
pp: X Y : TopCat
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
⊢ ι₁ ≫ F.h = f₁

Tactic:
ext x

Goal state after:
X Y : TopCat
f₀ f₁ : X ⟶ Y
F : Homotopy f₀ f₁
x : ↑X
⊢ (ConcreteCategory.hom (ι₁ ≫ F.h)) x = (ConcreteCategory.hom f₁) x
Module: Mathlib.Topology.Category.TopPair

Goal state before:
pp: X✝¹ Y✝¹ X Y Z : TopPair
X✝ Y✝ : TopCat
f : X✝ ⟶ Y✝
⊢ 𝟙 snd ≫ map = map ≫ f

Tactic:
ext x

Goal state after:
X✝¹ Y✝¹ X Y Z : TopPair
X✝ Y✝ : TopCat
f : X✝ ⟶ Y✝
x : ↑snd
⊢ (ConcreteCategory.hom (𝟙 snd ≫ map)) x = (ConcreteCategory.hom (map ≫ f)) x
Module: Mathlib.Topology.Homotopy.Path

Goal state before:
pp: case inr
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x₀ x₁ x₂ x₃ : X
p q : Path x₀ x₁
F : p.Homotopy q
f : C(X, Y)
t x : ↑I
hx : x ∈ {1}
⊢ { toFun := fun x ↦ (⇑f ∘ ⇑F) (t, x), continuous_toFun := ⋯ } x = (p.map ⋯).toContinuousMap x

Tactic:
· rw [Set.mem_singleton_iff] at hx
      simp [hx]

Goal state after:
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
⊢ (IsPathConnected s ∧ ∀ (x : ↑s) (γ : Path x x), γ.Homotopic (Path.refl x)) ↔
    IsPathConnected s ∧
      ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s

Tactic:
refine .and .rfl ⟨fun h x p hp ↦ ?_, fun h x p ↦ ?_⟩

Goal state after:
case refine_1
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : ↑s) (γ : Path x x), γ.Homotopic (Path.refl x)
x : X
p : Path x x
hp : ∀ (t : ↑unitInterval), p t ∈ s
⊢ ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s

case refine_2
X : Type u_1
inst✝ : TopologicalSpace X
s : Set X
h : ∀ (x : X) (p : Path x x), (∀ (t : ↑unitInterval), p t ∈ s) → ∃ F, ∀ (t : ↑unitInterval × ↑unitInterval), F t ∈ s
x : ↑s
p : Path x x
⊢ p.Homotopic (Path.refl x)
Module: Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
⊢ (p.trans q).trans r =
    (p.trans (q.trans r)).reparam (fun t ↦ ⟨transAssocReparamAux t, ⋯⟩) trans_assoc_reparam._proof_1 ⋯ ⋯

Tactic:
ext x

Goal state after:
X : Type u_1
inst✝ : TopologicalSpace X
x₀ x₁ x₂ x₃ : X
p : Path x₀ x₁
q : Path x₁ x₂
r : Path x₂ x₃
x : ↑I
⊢ ((p.trans q).trans r) x =
    ((p.trans (q.trans r)).reparam (fun t ↦ ⟨transAssocReparamAux t, ⋯⟩) trans_assoc_reparam._proof_1 ⋯ ⋯) x
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⟩
⊢ (ConcreteCategory.hom (F₂.map φ)) ((ConcreteCategory.hom (f.app U✝)) ⟨x, hx⟩) =
    (ConcreteCategory.hom (F₂.map φ)) ((ConcreteCategory.hom (g.app U✝)) ⟨x, hx⟩)

Tactic:
by rw [h]

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
⊢ Λ[n, i].obj (op ⦋m⦌) = Set.univ

Tactic:
ext x

Goal state after:
n : ℕ
i : Fin (n + 1)
m : ℕ
h : m + 1 < n
x : Δ[n] _⦋m⦌
⊢ x ∈ Λ[n, i].obj (op ⦋m⦌) ↔ x ∈ Set.univ
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:
rw [← sq.inf_eq]

Goal state after:
X : SSet
A₁ A₂ A₃ A₄ : X.Subcomplex
sq : A₁.BicartSq A₂ A₃ A₄
n : SimplexCategoryᵒᵖ
⊢ A₂.obj n ⊓ A₃.obj n = (A₂ ⊓ A₃).obj n
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: m n : ℕ
h : m < n
⊢ ∂Δ[n].obj (op ⦋m⦌) = Set.univ

Tactic:
ext x

Goal state after:
m n : ℕ
h : m < n
x : Δ[n] _⦋m⦌
⊢ x ∈ ∂Δ[n].obj (op ⦋m⦌) ↔ x ∈ Set.univ
Module: Mathlib.AlgebraicTopology.SimplicialSet.Boundary

Goal state before:
pp: case zero
m : ℕ
h : m < 0
f : unop (op ⦋m⦌) ⟶ ⦋0⦌
⊢ stdSimplex.objEquiv.symm f ∈ ∂Δ[0].obj (op ⦋m⦌)

Tactic:
simp at h

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

Goal state before:
pp: case refine_2
n : ℕ
A : Δ[n].Subcomplex
hA : A ≠ ⊤
⊢ A ≤ ∂Δ[n]

Tactic:
· have := subcomplex_hasDimensionLT_of_neq_top A hA
    rw [Subcomplex.le_iff_contains_nonDegenerate]
    rintro m ⟨x, h₁⟩ h₂
    dsimp at h₂ ⊢
    by_cases! h₃ : m < n
    · simp [boundary_obj_eq_univ m n h₃]
    · simp [← A.mem_nonDegenerate_iff ⟨x, h₂⟩,
        nonDegenerate_eq_empty_of_hasDimensionLT _ _ _ h₃] at h₁

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

Goal state before:
pp: n : ℕ
i a b : Fin (n + 1)
hab : a ≤ b
H : #{i, a, b} ≤ n
⊢ stdSimplex.edge n a b hab ∈ Λ[n, i].obj (op ⦋1⦌)

Tactic:
by
    have hS : ¬ ({i, a, b} = Finset.univ) := fun hS ↦ by
      have := Finset.card_le_card hS.symm.le
      simp only [card_univ, Fintype.card_fin] at this
      lia
    rw [Finset.eq_univ_iff_forall, not_forall] at hS
    obtain ⟨k, hk⟩ := hS
    simp only [mem_insert, mem_singleton, not_or] at hk
    -- this was produced by `simp? [horn_eq_iSup, -Fin.forall_fin_two]`
    simp only [horn_eq_iSup, Subfunctor.iSup_obj, Set.iUnion_coe_set, Set.mem_compl_iff,
      Set.mem_singleton_iff, Set.mem_iUnion, stdSimplex.mem_face_iff, Nat.reduceAdd, mem_compl,
      mem_singleton, exists_prop]
    refine ⟨k, hk.1, fun a ↦ ?_⟩
    fin_cases a
    · exact Ne.symm hk.2.1
    · exact Ne.symm hk.2.2

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
⊢ f ≫ inl f g = g ≫ inr f g

Tactic:
ext x

Goal state after:
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x : S
⊢ (ConcreteCategory.hom (f ≫ inl f g)).toFun x = (ConcreteCategory.hom (g ≫ inr f g)).toFun x
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 c.inr

Tactic:
change Mono ((Pushout.inr f g) ≫
    ((Cocone.forget _).mapIso
      (Cocone.ext (IsColimit.coconePointUniqueUpToIso hc
        (Pushout.isColimitCocone f g)) (by simp))).inv)
  infer_instance

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

Goal state before:
pp: case inr
X₁ X₂ X₃ X₄ : Type u
t : X₁ ⟶ X₂
r : X₂ ⟶ X₄
l : X₁ ⟶ X₃
b : X₃ ⟶ X₄
h : IsPushout t l r b
x₄ : X₄
x₃ : X₃
hx₃ : (ConcreteCategory.hom b) x₃ = x₄
⊢ (∃ x₂, (ConcreteCategory.hom r) x₂ = x₄) ∨
    ∃ x₃, (ConcreteCategory.hom b) x₃ = x₄ ∧ x₃ ∉ Set.range ⇑(ConcreteCategory.hom l)

Tactic:
· by_cases h₂ : x₃ ∈ Set.range l
    · obtain ⟨x₁, rfl⟩ := h₂
      exact Or.inl ⟨t x₁, by simpa only [← hx₃] using! ConcreteCategory.congr_hom h.w x₁⟩
    · exact Or.inr ⟨x₃, hx₃, h₂⟩

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

Goal state before:
pp: case a.right
⊢ stdSimplex.face {1, 2} ≤ Λ[2, 2]

Tactic:
· exact face_le_horn (0 : Fin 3) 2 (by simp)

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

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

Tactic:
Fin.castPred_castSucc,

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

Goal state before:
pp: X : SSet
n : ℕ
f g : X.Path n
h : f = g
i : Fin (n + 1)
⊢ f.vertex i = g.vertex i

Tactic:
by rw [h]

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

Goal state before:
pp: X : SSet
n : ℕ
f g : X.Path n
h : f = g
i : Fin n
⊢ f.arrow i = g.arrow i

Tactic:
by rw [h]

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

Goal state before:
pp: case succ.refine_2
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
i : Fin (n + 1)
⊢ (X.spine (n + 1) ((h n).concat (p.arrow 0) ↑(hn (p.interval 1 n ⋯)) ⋯)).arrow i = p.arrow i

Tactic:
obtain rfl | ⟨i, rfl⟩ := i.eq_zero_or_eq_succ

Goal state after:
case succ.refine_2.inl
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
⊢ (X.spine (n + 1) ((h n).concat (p.arrow 0) ↑(hn (p.interval 1 n ⋯)) ⋯)).arrow 0 = p.arrow 0

case succ.refine_2.inr
X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
hn : (p : X.Path n) → { s // X.spine n s = p }
p : X.Path (n + 1)
i : Fin n
⊢ (X.spine (n + 1) ((h n).concat (p.arrow 0) ↑(hn (p.interval 1 n ⋯)) ⋯)).arrow i.succ = p.arrow i.succ
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'
⊢ CatEnriched.hComp (𝟙 (𝟙 a.toBase)) (Hom.base η) ≍ Hom.base (eqToHom ⋯ ≫ η ≫ eqToHom ⋯)

Tactic:
simp [CatEnriched.id_hComp_heq]

Goal state after:
Module: Mathlib.CategoryTheory.Enriched.Ordinary.Basic

Goal state before:
pp: V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X X' : C
f : X ⟶ X'
Y Z : C
⊢ eComp V X' Y Z ≫ eHomWhiskerRight V f Z = (eHomWhiskerRight V f Y ▷ Y ⟶[V] Z) ≫ eComp V X Y Z

Tactic:
by
  dsimp [eHomWhiskerRight]
  rw [leftUnitor_inv_naturality_assoc, whisker_exchange_assoc]
  simp [e_assoc']

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
F G A : C ⥤ Type w
a : F ⊗ A ⟶ G
c✝ d✝ : C
φ : c✝ ⟶ d✝
y : A.obj c✝
⊢ (F.map φ ≫ ↾fun x ↦ (ConcreteCategory.hom (a.app d✝)) (x, (ConcreteCategory.hom (A.map φ)) y)) =
    (↾fun x ↦ (ConcreteCategory.hom (a.app c✝)) (x, y)) ≫ G.map φ

Tactic:
ext x

Goal state after:
C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F✝ G✝ : C ⥤ D
F G A : C ⥤ Type w
a : F ⊗ A ⟶ G
c✝ d✝ : C
φ : c✝ ⟶ d✝
y : A.obj c✝
x : F.obj c✝
⊢ (ConcreteCategory.hom
          (F.map φ ≫ ↾fun x ↦ (ConcreteCategory.hom (a.app d✝)) (x, (ConcreteCategory.hom (A.map φ)) y))).toFun
      x =
    (ConcreteCategory.hom ((↾fun x ↦ (ConcreteCategory.hom (a.app c✝)) (x, y)) ≫ G.map φ)).toFun x
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
⊢ ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
        (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op).unop =
    (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop

Tactic:
ext x

Goal state after:
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
x :
  Fin
    ((unop
          ((inclusion 2).op.obj
            (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc)
                SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len +
      1)
⊢ ↑((Hom.toOrderHom
          ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯)
                  SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
              (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op).unop)
        x) =
    ↑((Hom.toOrderHom
          (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc)
                SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop)
        x)
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
⊢ ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
        (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 0) ⋯ ⋯).op).unop =
    (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop

Tactic:
ext x

Goal state after:
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
x :
  Fin
    ((unop
          ((inclusion 2).op.obj
            (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ)
                SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).right)).len +
      1)
⊢ ↑((Hom.toOrderHom
          ((strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯)
                  SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom ≫
              (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 0) ⋯ ⋯).op).unop)
        x) =
    ↑((Hom.toOrderHom
          (strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.succ) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom.unop)
        x)
Module: Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated

Goal state before:
pp: A : Truncated 2
inst✝ : A.Quasicategory₂
x y z : A.obj (Opposite.op { obj := { len := 0 }, property := Quasicategory₂._proof_1 })
⊢ ∀ {X Y : A.HomotopyCategory₂} (f : X ⟶ Y), 𝟙 X ≫ f = f

Tactic:
by
    rintro _ _ ⟨f⟩
    exact ((compStruct _ f).comp_unique (idComp _) .refl .refl).congr_homotopyCategory₂HomMk

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
hf : W₁ f
h : r.deg X = r.deg Y
this : ¬MorphismProperty.identities C f
⊢ False

Tactic:
exact h.not_gt (r.lt₁ _ hf this)

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
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = 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
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
⊢ (α.hom ≫ (inclusion 2).op.map (Hom.tr (mkOfSucc 1) ⋯ ⋯).op).unop = α₀.hom.unop

Tactic:
ext 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
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = 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✝
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
x : Fin ((unop ((inclusion 2).op.obj α₀.right)).len + 1)
⊢ ↑((Hom.toOrderHom (α.hom ≫ (inclusion 2).op.map (Hom.tr (mkOfSucc 1) ⋯ ⋯).op).unop) x) =
    ↑((Hom.toOrderHom α₀.hom.unop) x)
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
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = 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
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
⊢ (α.hom ≫ (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op).unop = α₁.hom.unop

Tactic:
ext 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
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = 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✝
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
β₀ : α ⟶ α₀ := ⋯
x : Fin ((unop ((inclusion 2).op.obj α₁.right)).len + 1)
⊢ ↑((Hom.toOrderHom (α.hom ≫ (inclusion 2).op.map (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op).unop) x) =
    ↑((Hom.toOrderHom α₁.hom.unop) x)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: case h
x y : SimplexCategoryGenRel
x✝ y✝ : Paths FreeSimplexQuiver
f : x✝ ⟶ y✝
⊢ generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map f)

Tactic:
| _ f
   => 

Goal state after:
case h
x y : SimplexCategoryGenRel
x✝ y✝ : Paths FreeSimplexQuiver
f : x✝ ⟶ y✝
⊢ generators.multiplicativeClosure ((Quotient.functor FreeSimplexQuiver.homRel).map 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
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = 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
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
⊢ (α.hom ≫ (inclusion 2).op.map (Hom.tr (mkOfSucc 0) ⋯ ⋯).op).unop = α₂.hom.unop

Tactic:
ext 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
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = 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✝
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
β₀ : α ⟶ α₀ := ⋯
β₁ : α ⟶ α₁ := ⋯
x : Fin ((unop ((inclusion 2).op.obj α₂.right)).len + 1)
⊢ ↑((Hom.toOrderHom (α.hom ≫ (inclusion 2).op.map (Hom.tr (mkOfSucc 0) ⋯ ⋯).op).unop) x) =
    ↑((Hom.toOrderHom α₂.hom.unop) x)
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic

Goal state before:
pp: n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ σ i.castSucc ≫ σ j = σ j.succ ≫ σ i

Tactic:
apply CategoryTheory.Quotient.sound
  exact FreeSimplexQuiver.homRel.σ_comp_σ H

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

Goal state before:
pp: case succ
n : ℕ
i : Fin (n + 1 + 1)
i' : Fin (n + 1 + 2)
⊢ ∃ z e m, ∃ (_ : P_σ e) (_ : P_δ m), δ i' ≫ σ i = e ≫ m

Tactic:
obtain h | ⟨j, j', h⟩ := switch_δ_σ i i'
    · exact ⟨_, _, _, P_σ.id_mem _, P_δ.id_mem _, by simp [h]⟩
    · exact ⟨_, _, _, P_σ.σ _, P_δ.δ _, 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
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = 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
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₂)) x
t : Fin (1 + 1)
⊢ (α.hom ≫ (mkOfSucc 0).op).unop = α₂.hom.unop

Tactic:
ext 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
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = 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✝
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
β₀ : α ⟶ α₀ := ⋯
β₁ : α ⟶ α₁ := ⋯
β₂ : α ⟶ α₂ := ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x✝) = (ConcreteCategory.hom (s.π.app α₀)) x✝
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x✝) = (ConcreteCategory.hom (s.π.app α₂)) x✝
t : Fin (1 + 1)
x : Fin ((unop (op ⦋1⦌)).len + 1)
⊢ ↑((Hom.toOrderHom (α.hom ≫ (mkOfSucc 0).op).unop) x) = ↑((Hom.toOrderHom α₂.hom.unop) x)