mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplicialSet.Horn

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 2))
j : Fin (n + 2)
⊢ S = Finset.univ ∨ S = {j}ᶜ → {j}ᶜ ⊆ S

Tactic:
aesop

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

Goal state before:
pp: S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
x₂ y₂ : X₂
⊢ Rel' f g (Sum.inr x₂) (Sum.inr y₂) ↔ x₂ = y₂

Tactic:
constructor
  · rintro ⟨_⟩
    rfl
  · rintro rfl
    apply Rel'.refl

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

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

Tactic:
subst hyz

Goal state after:
case inl_inr.inr
S X₁ X₂ : Type u
f : S ⟶ X₁
g : S ⟶ X₂
inst✝ : Mono f
s : S
⊢ Rel' f g (Sum.inl ((ConcreteCategory.hom f) s)) (Sum.inr ((ConcreteCategory.hom g) s))
Module: Mathlib.AlgebraicTopology.SimplicialSet.KanComplex

Goal state before:
pp: Z : SSet
h :
  ∀ ⦃n : ℕ⦄ ⦃i : Fin (n + 2)⦄ (f : (j : Fin (n + 2)) → j ≠ i → (Δ[n] ⟶ Z)),
    horn.IsCompatible f → ∃ φ, ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = f j hj
n : ℕ
X Y : SSet
i : Fin (n + 2)
t : Λ[n + 1, i].toSSet ⟶ Z
x✝¹ : Δ[n + 1] ⟶ ⊤_ SSet
x✝ : CommSq t Λ[n + 1, i].ι (terminal.from Z) x✝¹
φ : Δ[n + 1] ⟶ Z
hφ : ∀ (j : Fin (n + 2)) (hj : j ≠ i), stdSimplex.δ j ≫ φ = horn.ι i j hj ≫ t
⊢ φ ≫ terminal.from Z = x✝¹

Tactic:
by subsingleton

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

Goal state before:
pp: n : ℕ
i : Fin (n + 1)
j k : ↑{i}ᶜ
⊢ {↑j, ↑k}ᶜ = {↑j}ᶜ ⊓ {↑k}ᶜ

Tactic:
aesop

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

Goal state before:
pp: case h.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
⊢ (stdSimplex.spineId (n + 2)).arrow k.castSucc =
    stdSimplex.objEquiv.symm
      ((mkOfSucc k).op.unop ≫ stdSimplex.objEquiv (yonedaEquiv (stdSimplex.map (SimplexCategory.δ j))))

Tactic:
Quiver.Hom.unop_op,

Goal state after:
case h.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hlt : ksucc < j
⊢ (stdSimplex.spineId (n + 2)).arrow k.castSucc =
    stdSimplex.objEquiv.symm (mkOfSucc k ≫ stdSimplex.objEquiv (yonedaEquiv (stdSimplex.map (SimplexCategory.δ j))))
Module: Mathlib.AlgebraicTopology.Quasicategory.StrictSegal

Goal state before:
pp: case h.inr.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hgt : j < ksucc
⊢ (stdSimplex.spineId (n + 2)).arrow k.succ =
    stdSimplex.objEquiv.symm
      ((mkOfSucc k).op.unop ≫ stdSimplex.objEquiv (yonedaEquiv (stdSimplex.map (SimplexCategory.δ j))))

Tactic:
Quiver.Hom.unop_op,

Goal state after:
case h.inr.inl
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 3)
σ₀ : Λ[n + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 2)
j : Fin (n + 3)
hj : j ≠ i
k : Fin (n + 1)
ksucc : Fin (n + 1 + 1 + 1) := k.succ.castSucc
hgt : j < ksucc
⊢ (stdSimplex.spineId (n + 2)).arrow k.succ =
    stdSimplex.objEquiv.symm (mkOfSucc k ≫ stdSimplex.objEquiv (yonedaEquiv (stdSimplex.map (SimplexCategory.δ j))))
Module: Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
p : X.Path 0
⊢ X.spine 0 (p.vertex 0) = p

Tactic:
aesop

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
⊢ ∀ (n : ℕ), X.spine n ∘ StrictSegalCore.spineToSimplex h = id

Tactic:
aesop

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

Goal state before:
pp: X : SSet
h : (n : ℕ) → X.StrictSegalCore n
n : ℕ
⊢ StrictSegalCore.spineToSimplex h ∘ X.spine n = id

Tactic:
aesop

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

Goal state before:
pp: case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
z : Fin (1 + 1)
⊢ (stdSimplex.objEquiv.symm ((diag 2).op.unop ≫ stdSimplex.objEquiv ↑triangle)) z =
    ((ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc k).op)) (yonedaEquiv (stdSimplex.δ j))) z

Tactic:
Quiver.Hom.unop_op,

Goal state after:
case h.inr.inr.succ
X : SSet
sx : X.StrictSegal
n : ℕ
i : Fin (n + 1 + 3)
σ₀ : Λ[n + 1 + 2, i].toSSet ⟶ X
h₀ : 0 < i
hₙ : i < Fin.last (n + 1 + 2)
j : Fin (n + 1 + 3)
hj : j ≠ i
k : Fin (n + 1 + 1)
ksucc : Fin (n + 1 + 1 + 1 + 1) := k.succ.castSucc
heq : j = ksucc
triangle : Λ[n + 3, i].toSSet _⦋2⦌ := horn.primitiveTriangle i h₀ hₙ ↑k ⋯
hi :
  ((horn.spineId i h₀ hₙ).map σ₀).interval (↑k) 2 ⋯ =
    X.spine 2 ((ConcreteCategory.hom (σ₀.app (Opposite.op ⦋2⦌))) triangle)
z : Fin (1 + 1)
⊢ (stdSimplex.objEquiv.symm (diag 2 ≫ stdSimplex.objEquiv ↑triangle)) z =
    ((ConcreteCategory.hom (Δ[n + 1 + 2].map (mkOfSucc k).op)) (yonedaEquiv (stdSimplex.δ j))) z
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
x✝ : F.HomObj G A
⊢ (fun a ↦ { app := fun X y ↦ ↾fun x ↦ (ConcreteCategory.hom (a.app X)) (x, y), naturality := ⋯ })
      ((fun a ↦
          {
            app := fun X ↦
              ↾fun x ↦
                match x with
                | (x, y) => (ConcreteCategory.hom (a.app X y)) x,
            naturality := ⋯ })
        x✝) =
    x✝

Tactic:
aesop

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
x✝ : F ⊗ A ⟶ G
⊢ (fun a ↦
        {
          app := fun X ↦
            ↾fun x ↦
              match x with
              | (x, y) => (ConcreteCategory.hom (a.app X y)) x,
          naturality := ⋯ })
      ((fun a ↦ { app := fun X y ↦ ↾fun x ↦ (ConcreteCategory.hom (a.app X)) (x, y), naturality := ⋯ }) x✝) =
    x✝

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Functor.FunctorHom

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

Tactic:
aesop

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 : 𝟙_ (C ⥤ Type (max v' v u)) ⟶ F.functorHom G
X : C
a : (𝟙_ (C ⥤ Type (max v' v u))).obj X
Y : C
φ : X ⟶ Y
this :
  ((ConcreteCategory.hom (f.app Y)) PUnit.unit).app Y (𝟙 Y) =
    ((ConcreteCategory.hom (f.app X)) PUnit.unit).app Y (φ ≫ 𝟙 Y)
⊢ ((ConcreteCategory.hom
              (((fun f ↦ { app := fun x ↦ ↾fun x_1 ↦ HomObj.ofNatTrans f, naturality := ⋯ })
                    ((fun f ↦
                        {
                          app := fun X ↦
                            ((ConcreteCategory.hom (f.app X)) PUnit.unit).app X (𝟙 (Opposite.unop (Opposite.op X))),
                          naturality := ⋯ })
                      f)).app
                X)).toFun
          a).app
      Y φ =
    ((ConcreteCategory.hom (f.app X)).toFun a).app Y φ

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Monoidal.Closed.FunctorToTypes

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
D : Type u'
inst✝ : Category.{v', u'} D
F X✝ Y✝ : C ⥤ Type (max w v u)
f : X✝ ⟶ Y✝
X : C
a : (F.functorHom X✝).obj X
c✝ d✝ : C
g : c✝ ⟶ d✝
h : (Opposite.unop (coyoneda.rightOp.obj X)).obj c✝
this :
  F.map g ≫ a.app d✝ ((ConcreteCategory.hom ((Opposite.unop (coyoneda.rightOp.obj X)).map g)) h) = a.app c✝ h ≫ X✝.map g
⊢ (F.map g ≫ a.app d✝ (h ≫ g)) ≫ f.app d✝ = (a.app c✝ h ≫ f.app c✝) ≫ Y✝.map g

Tactic:
aesop

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: case mk.mk.nil
V : Type u_1
inst✝ : ReflQuiver V
motive : {x y : FreeRefl V} → (x ⟶ y) → Prop
id : ∀ (x : V), motive (homMk (𝟙rq x))
comp_homMk : ∀ {x y z : V} (f : mk x ⟶ mk y) (g : y ⟶ z), motive f → motive (f ≫ homMk g)
x y : V
⊢ motive ((quotientFunctor V).map Quiver.Path.nil)

Tactic:
simpa using! id x

Goal state after:
Module: Mathlib.CategoryTheory.Category.ReflQuiv

Goal state before:
pp: V✝ : Type u_1
inst✝³ : ReflQuiver V✝
V : Type u_2
inst✝² : ReflQuiver V
inst✝¹ : Unique V
inst✝ : ∀ (x y : V), Subsingleton (x ⟶ y)
x✝ y✝ : FreeRefl V
x y : V
⊢ x = y

Tactic:
by subsingleton

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.δ 1) 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.castSucc).op)))
      x

Tactic:
let φ : strArrowMk₂ (mkOfLe _ _ (Fin.castSucc_le_succ i)) ⟶
        strArrowMk₂ (⦋0⦌.const _ i.castSucc) :=
          StructuredArrow.homMk (Hom.tr (δ 1)).op
          (Quiver.Hom.unop_inj (by ext x; fin_cases x; rfl))

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
φ : strArrowMk₂ (mkOfLe i.castSucc i.succ ⋯) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3 ⟶
  strArrowMk₂ (⦋0⦌.const ⦋n⦌ i.castSucc) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1 :=
  homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
⊢ (ConcreteCategory.hom
        (((Truncated.trunc (0 + 1) 1 ⋯).obj ((truncation 1).obj X)).map
          (Hom.tr (SimplexCategory.δ 1) 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.castSucc).op)))
      x
Module: Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat

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

Tactic:
aesop

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

Goal state before:
pp: V W X : Truncated 2
inst✝¹ : Unique (X.obj (op { obj := ⦋0⦌, property := OneTruncation₂._proof_1 }))
inst✝ : Subsingleton (X.obj (op { obj := ⦋1⦌, property := ι0₂._proof_5 }))
⊢ ∀ {X_1 Y : X.HomotopyCategory} (f : X_1 ⟶ Y), X_1 = Y

Tactic:
by subsingleton

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

Goal state before:
pp: X✝ Y✝ : ((truncation 2).obj Δ[0]).HomotopyCategory
x✝ : X✝ ⟶ Y✝
⊢ X✝ = Y✝

Tactic:
by subsingleton

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 : r.degHom f = r.deg X
Z : C
p : X ⟶ Z
i : Z ⟶ Y
hp : W₁ p
hi : W₂ i
fac : p ≫ i = f
h : r.degHom f = r.deg Z
⊢ r.deg X = r.deg Z

Tactic:
aesop

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 : r.degHom f = r.deg Y
Z : C
p : X ⟶ Z
i : Z ⟶ Y
hp : W₁ p
hi : W₂ i
fac : p ≫ i = f
h : r.degHom f = r.deg Z
⊢ r.deg Z = r.deg Y

Tactic:
aesop

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

Goal state before:
pp: case of_comp.inl
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✝
z✝ X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 2)
g : mk (n✝ + 1) ⟶ z✝
hg : generators.multiplicativeClosure' g
hrec : P g
⊢ P (δ i ≫ g)

pp: case of_comp.inr
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✝
z✝ X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 1)
g : mk n✝ ⟶ z✝
hg : generators.multiplicativeClosure' g
hrec : P g
⊢ P (σ i ≫ g)

Tactic:
· simpa using! (δ_comp g i hrec)

Goal state after:
case of_comp.inr
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✝
z✝ X Y : SimplexCategoryGenRel
n✝ : ℕ
i : Fin (n✝ + 1)
g : mk n✝ ⟶ z✝
hg : generators.multiplicativeClosure' g
hrec : P g
⊢ P (σ i ≫ g)
Module: Mathlib.AlgebraicTopology.SimplexCategory.SemiSimplexCategory

Goal state before:
pp: n m : SemiSimplexCategory
f : toSimplexCategory.obj n ⟶ toSimplexCategory.obj m
inst✝ : Mono f
⊢ toSimplexCategory.map (homOfMono f) = f

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
j i : Fin (n + 2)
h✝ : i.castSucc ≤ j.castSucc
h : i ≤ j
⊢ δ j ≫ toMk₁ i.castSucc = toMk₁ (i.castSucc.castPred ⋯)

Tactic:
Fin.castPred_castSucc

Goal state after:
n : ℕ
j i : Fin (n + 2)
h✝ : i.castSucc ≤ j.castSucc
h : i ≤ j
⊢ δ j ≫ toMk₁ i.castSucc = toMk₁ 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
⊢ A.preimage e.inv = B

Tactic:
aesop

Goal state after:
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
x✝ : A.N
⊢ (fun y ↦ { toN := (SSet.N.orderIsoOfIso e).symm y.toN, notMem := ⋯ })
      ((fun x ↦ { toN := (SSet.N.orderIsoOfIso e) x.toN, notMem := ⋯ }) x✝) =
    x✝

Tactic:
aesop

Goal state after:
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
x✝ : B.N
⊢ (fun x ↦ { toN := (SSet.N.orderIsoOfIso e) x.toN, notMem := ⋯ })
      ((fun y ↦ { toN := (SSet.N.orderIsoOfIso e).symm y.toN, notMem := ⋯ }) x✝) =
    x✝

Tactic:
aesop

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

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

Tactic:
by_cases! hx : x ≤ i

Goal state after:
case pos
n : ℕ
i x : Fin (n + 2)
hx : x ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc

case neg
n : ℕ
i x : Fin (n + 2)
hx : i < x
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc
Module: Mathlib.AlgebraicTopology.SimplicialObject.II

Goal state before:
pp: case pos
n : ℕ
i x : Fin (n + 2)
hx : x ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = x.castSucc.castPred ⋯

Tactic:
Fin.castPred_castSucc

Goal state after:
case pos
n : ℕ
i x : Fin (n + 2)
hx : x ≤ i
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = x
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Pairing

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x : ↑P.II
⊢ (P.ofIso e hA).p ⟨(N.orderIsoOfIso e hA).symm ↑x, ⋯⟩ = ⟨(N.orderIsoOfIso e hA).symm ↑(P.p x), ⋯⟩

Tactic:
by
  let e' := Subcomplex.N.orderIsoOfIso e hA
  ext
  change e'.symm (P.p ⟨e' (e'.symm x), _⟩) = e'.symm (P.p x)
  simp

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
Y : SSet
B : Y.Subcomplex
e : Y ≅ X
hA : A.preimage e.hom = B
x y : ↑P.II
⊢ ⟨(N.orderIsoOfIso e hA).symm ↑x, ⋯⟩ = ⟨(N.orderIsoOfIso e hA).symm ↑y, ⋯⟩ ↔ x = y

Tactic:
aesop

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

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

Tactic:
intro h a b hab

Goal state after:
case refine_2
p q n : ℕ
z : (Δ[p] ⊗ Δ[q]) _⦋n⦌
hn : p + q = n
h : orderHomOfSimplex z hn = OrderHom.id
a b : Fin (n + 1)
hab : (objEquiv z) a = (objEquiv z) b
⊢ a = b
Module: Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
s : A.N
⊢ s ∈ h.I ∩ h.II ↔ s ∈ ∅

Tactic:
simp only [I, II, Set.mem_inter_iff, Set.mem_range, Set.mem_empty_iff_false,
      iff_false, not_and, not_exists, forall_exists_index]

Goal state after:
X : SSet
A : X.Subcomplex
h : A.PairingCore
s : A.N
⊢ ∀ (x : h.ι), h.type₁ x = s → ∀ (x : h.ι), ¬h.type₂ x = s
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
⊢ (∃ y, h.type₁ y = s) ∨ ∃ y, h.type₂ y = s

Tactic:
aesop

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
h : A.PairingCore
inst✝ : h.IsProper
s : h.ι
d : ℕ
hd : h.dim s = d
⊢ ↑(⋯.index hd) = ↑(h.index s)

Tactic:
subst hd
  simp

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
hy : Acc P.AncestralRel y
x : ↑P.II
r : P.AncestralRel x y
⊢ P.rank' ⋯ < P.rank' hy

Tactic:
rw [P.rank'_eq hy, ← Nat.add_one_le_iff]

Goal state after:
X : SSet
A : X.Subcomplex
P : A.Pairing
y : ↑P.II
hy : Acc P.AncestralRel y
x : ↑P.II
r : P.AncestralRel x y
⊢ P.rank' ⋯ + 1 ≤ ⨆ x, P.rank' ⋯ + 1
Module: Mathlib.AlgebraicTopology.SimplicialObject.ChainHomotopy

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
x✝¹ x✝ : Fin (n + 1) × Fin (n + 2)
⊢ γ₁ x✝¹ = γ₁ x✝ → x✝¹ = x✝

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
x✝¹ x✝ : Fin (n + 1) × Fin (n + 2)
⊢ γ₂ x✝¹ = γ₂ x✝ → x✝¹ = x✝

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
n : ℕ
α : Fin (n + 1) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • X.δ x.2 ≫ H.h x.1
β : Fin (n + 3) × Fin (n + 2) → (X _⦋n + 1⦌ ⟶ Y _⦋n + 1⦌) := fun x ↦ (-1) ^ (↑x.1 + ↑x.2) • H.h x.2 ≫ Y.δ x.1
h₂ : ∀ (x : Fin (n + 1) × Fin (n + 2)), x.1.castSucc < x.2 → α x = -β (x.2.succ, x.1.castSucc)
S : Finset (Fin (n + 1) × Fin (n + 2)) := {x | x.1.castSucc < x.2}
γ₁ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.castSucc, x.1.succ)
γ₂ : Fin (n + 1) × Fin (n + 2) → Fin (n + 2 + 1) × Fin (n + 1 + 1) := fun x ↦ (x.2.succ, x.1.castSucc)
γ₃ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.succ)
γ₄ : Fin (n + 1) → Fin (n + 1 + 1 + 1) × Fin (n + 1 + 1) := fun i ↦ (i.castSucc.succ, i.castSucc)
hγ₁ : Function.Injective γ₁
hγ₂ : Function.Injective γ₂
x✝¹ x✝ : Fin (n + 1)
⊢ γ₃ x✝¹ = γ₃ x✝ → x✝¹ = x✝

Tactic:
aesop

Goal state after: