mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : k ≤ j
⊢ i ≤ k.castSucc.castPred ⋯

Tactic:
Fin.castPred_castSucc

Goal state after:
case inl
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : k ≤ j
⊢ i ≤ k
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: case cast.succ.inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
⊢ j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)

Tactic:
simp_rw [Fin.predAbove_of_le_castSucc i.castSucc _ (Fin.castSucc_le_castSucc_iff.mpr
        (Fin.succ_le_castSucc_iff.mpr h)), Fin.castPred_castSucc, ← Fin.succ_castSucc,
        Fin.succ_predAbove_succ]

Goal state after:
case cast.succ.inr
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
⊢ j.predAbove k.succ = i.predAbove (j.predAbove k.castSucc).succ
Module: Mathlib.AlgebraicTopology.SimplexCategory.Basic

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 0
e1 : (Hom.toOrderHom f) 1 = 0
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 1 = (Hom.toOrderHom (⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0))) 1

Tactic:
exact e1.trans e0.symm

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 1
e1 : (Hom.toOrderHom f) 1 = 1
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 1 = (Hom.toOrderHom (⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0))) 1

Tactic:
exact e1.trans e0.symm

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

Goal state before:
pp: f : ⦋1⦌ ⟶ ⦋2⦌
this : (Hom.toOrderHom f) 0 ≤ (Hom.toOrderHom f) 1
e0 : (Hom.toOrderHom f) 0 = 2
e1 : (Hom.toOrderHom f) 1 = 2
i : Fin (⦋1⦌.len + 1)
⊢ (Hom.toOrderHom f) 1 = (Hom.toOrderHom (⦋1⦌.const ⦋2⦌ ((Hom.toOrderHom f) 0))) 1

Tactic:
exact e1.trans e0.symm

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

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
hf : Mono f
h : n.len = m.len
⊢ n = m

Tactic:
aesop

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

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
hf : Epi f
h : n.len = m.len
⊢ n = m

Tactic:
aesop

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

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : SimplicialObject C
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
⊢ X.σ₀Iter i hi ≫ X.σ j = X.σ₀Iter (i + 1) ⋯

Tactic:
dsimp [σ, σ₀Iter]
  rw [← Functor.map_comp, ← op_comp, SimplexCategory.σ_σ₀Iter ..]

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

Goal state before:
pp: case pos
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h' : x ≤ i.castSucc
⊢ (Hom.toOrderHom θ) x = (Hom.toOrderHom θ) ((Hom.toOrderHom (δ i.succ)) (i.predAbove x))

Tactic:
rw [Fin.predAbove_of_le_castSucc i x h']
    dsimp [δ]
    rw [Fin.succAbove_of_castSucc_lt]
    · rw [Fin.castSucc_castPred]
    · exact (Fin.castSucc_lt_succ_iff.mpr h')

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

Goal state before:
pp: case pos.e_6
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h'✝ : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
⊢ i.castSucc = i.succ.succAbove i

Tactic:
rw [Fin.succAbove_of_castSucc_lt i.succ]

Goal state after:
case pos.e_6.h
n : ℕ
Δ' : SimplexCategory
θ : ⦋n + 1⦌ ⟶ Δ'
i : Fin (n + 1)
hi : (Hom.toOrderHom θ) i.castSucc = (Hom.toOrderHom θ) i.succ
x : Fin (⦋n + 1⦌.len + 1)
h'✝ : i.castSucc < x
y : Fin ⦋n + 1⦌.len := x.pred ⋯
h' : i.castSucc < y.succ
hy : x = y.succ
h'' : y = i
⊢ i.castSucc < i.succ
Module: Mathlib.AlgebraicTopology.SimplexCategory.Rev

Goal state before:
pp: n m : SimplexCategory
f : n ⟶ m
⊢ rev.map (rev.map f) = f

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
⊢ ¬Function.Surjective ⇑(Hom.toOrderHom θ)

Tactic:
rw [← epi_iff_surjective]

Goal state after:
n : ℕ
θ : ⦋n⦌ ⟶ ⦋n + 1⦌
inst✝ : Mono θ
⊢ ¬Epi θ
Module: Mathlib.CategoryTheory.Subfunctor.OfSection

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type w
X : Cᵒᵖ
x : F.obj X
F' : Cᵒᵖ ⥤ Type w
f : F ⟶ F'
⊢ (ofSection x).image f = ofSection ((ConcreteCategory.hom (f.app X)) x)

Tactic:
by
  apply le_antisymm
  · rw [image_le_iff, ofSection_le_iff, preimage_obj, Set.mem_preimage]
    exact ⟨𝟙 X, by simp⟩
  · simp only [ofSection_le_iff, image_obj, Set.mem_image]
    exact ⟨x, mem_ofSection_obj x, rfl⟩

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ y ∈ (ofSection x).obj U ↔ y ∈ (range (yonedaEquiv.symm x)).obj U

Tactic:
simp only [ofSection_obj, Set.mem_ofPred_eq, Opposite.op_unop, range_obj,
    Set.mem_range]

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type v
X : Cᵒᵖ
x : F.obj X
U : Cᵒᵖ
y : F.obj U
⊢ (∃ f, (ConcreteCategory.hom (F.map f)) x = y) ↔ ∃ y_1, (ConcreteCategory.hom ((yonedaEquiv.symm x).app U)) y_1 = y
Module: Mathlib.AlgebraicTopology.SimplicialSet.Dimension

Goal state before:
pp: X : SSet
ι : Type u_1
A : ι → X.Subcomplex
d : ℕ
⊢ (∀ (n : ℕ), d ≤ n → X.degenerate n ⊓ (⨆ i, A i).obj (op ⦋n⦌) = (⨆ i, A i).obj (op ⦋n⦌)) ↔
    ∀ (i : ι) (n : ℕ), d ≤ n → X.degenerate n ⊓ (A i).obj (op ⦋n⦌) = (A i).obj (op ⦋n⦌)

Tactic:
aesop

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
hm : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
hy : (ConcreteCategory.hom (X.map ((image.ι f).op ≫ (factorThruImage f).op))) y = x
this : (image f).len ≤ m
⊢ x ∈ Set.range ⇑(ConcreteCategory.hom (X.map (factorThruImage f).op))

Tactic:
aesop

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

Goal state before:
pp: X : SSet
w✝³ : ℕ
w✝² : X _⦋w✝³⦌
w✝¹ : ℕ
w✝ : X _⦋w✝¹⦌
x✝ :
  ∃ (h : { dim := w✝³, simplex := w✝² }.dim = { dim := w✝¹, simplex := w✝ }.dim),
    ({ dim := w✝³, simplex := w✝² }.cast h).simplex = { dim := w✝¹, simplex := w✝ }.simplex
h₁ : { dim := w✝³, simplex := w✝² }.dim = { dim := w✝¹, simplex := w✝ }.dim
h₂ : ({ dim := w✝³, simplex := w✝² }.cast h₁).simplex = { dim := w✝¹, simplex := w✝ }.simplex
⊢ { dim := w✝³, simplex := w✝² } = { dim := w✝¹, simplex := w✝ }

Tactic:
aesop

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

Goal state before:
pp: case mp
X : SSet
n m : ℕ
hm : m < n + 1
y : X _⦋m⦌
i : Fin (n + 1)
θ : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi (SimplexCategory.σ i ≫ θ)
⊢ (ConcreteCategory.hom (X.map (SimplexCategory.σ i ≫ θ).op)) y ∈
    ⋃ i, Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ X i))

Tactic:
aesop

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

Goal state before:
pp: case mpr
X : SSet
x y : X.S
⊢ Nonempty (equivElements y ⟶ equivElements x) → ∃ f, (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex

Tactic:
rintro ⟨f, hf⟩
    exact ⟨f.unop, hf⟩

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

Goal state before:
pp: case right
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Function.Surjective ⇑(ConcreteCategory.hom (f.app X✝))

Tactic:
rw [← epi_iff_surjective]

Goal state after:
case right
X✝¹ Y✝ : SSet
f : X✝¹ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
X✝ : SimplexCategoryᵒᵖ
⊢ Epi (f.app X✝)
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (⊥.toSSet.map x✝ ≫
      ↾fun x ↦
        match x with
        | ⟨val, h⟩ => ⋯.elim) =
    (↾fun x ↦
        match x with
        | ⟨val, h⟩ => ⋯.elim) ≫
      Y.map x✝

Tactic:
ext ⟨_, h⟩; tauto

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

Goal state before:
pp: X Y : SSet
⊢ ∀ (a : ⊥.toSSet ⟶ Y),
    a =
      {
        app := fun x ↦
          ↾fun x_1 ↦
            match x_1 with
            | ⟨val, h⟩ => ⋯.elim,
        naturality := ⋯ }

Tactic:
by subsingleton

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m : SimplexCategoryᵒᵖ
y : X.obj m
⊢ (∃ f, (ConcreteCategory.hom (X.map f)) x = y) ↔ ∃ f, (ConcreteCategory.hom (X.map f.op)) x = y

Tactic:
aesop

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

Goal state before:
pp: X Y : SSet
ι : Type u_1
A : ι → X.Subcomplex
p : Y ⟶ X
⊢ (⨆ i, A i).preimage p = ⨆ i, (A i).preimage p

Tactic:
aesop

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

Goal state before:
pp: X Y : SSet
ι : Type u_1
A : ι → X.Subcomplex
p : Y ⟶ X
⊢ (⨅ i, A i).preimage p = ⨅ i, (A i).preimage p

Tactic:
aesop

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
⊢ A.preimage A.ι = ⊤

Tactic:
aesop

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
⊢ ⊤.image f = range f

Tactic:
aesop

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
⊢ A.image (𝟙 X) = A

Tactic:
aesop

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
Z : SSet
g : Y ⟶ Z
⊢ A.image (f ≫ g) = (A.image f).image g

Tactic:
aesop

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
Z : SSet
g : Y ⟶ Z
⊢ range (f ≫ g) = (range f).image g

Tactic:
aesop

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

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
f : X ⟶ Y
⊢ A.image f = range (A.ι ≫ f)

Tactic:
aesop

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

Goal state before:
pp: X Y : SSet
ι : Type u_1
S : ι → X.Subcomplex
f : X ⟶ Y
⊢ (⨆ i, S i).image f = ⨆ i, (S i).image f

Tactic:
aesop

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

Goal state before:
pp: X : SSet
n₁ : ℕ
x₁ : X _⦋n₁⦌
hx₁ : x₁ ∈ X.nonDegenerate n₁
x₂ : X _⦋n₁⦌
hx₂ : x₂ ∈ X.nonDegenerate n₁
h' : mk ↑⟨x₂, hx₂⟩ ⋯ ≤ mk ↑⟨x₁, hx₁⟩ ⋯
hf : Mono (𝟙 ⦋(mk ↑⟨x₁, hx₁⟩ ⋯).dim⦌)
h : (ConcreteCategory.hom (X.map (𝟙 ⦋(mk ↑⟨x₁, hx₁⟩ ⋯).dim⦌).op)) (mk ↑⟨x₂, hx₂⟩ ⋯).simplex = (mk ↑⟨x₁, hx₁⟩ ⋯).simplex
⊢ mk ↑⟨x₁, hx₁⟩ ⋯ = mk ↑⟨x₂, hx₂⟩ ⋯

Tactic:
aesop

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
s : Cone (wideCospan ι X)
j : WidePullbackShape ι
⊢ (Pi.lift fun j ↦ s.π.app (some j)) ≫
      { pt := ∏ᶜ fun x ↦ X,
              π :=
                {
                  app := fun X_1 ↦
                    Option.casesOn X_1
                      (terminal.from (((Functor.const (WidePullbackShape ι)).obj (∏ᶜ fun x ↦ X)).obj none)) fun i ↦
                      limit.π (Discrete.functor fun x ↦ X) { as := i },
                  naturality := ⋯ } }.π.app
        none =
    s.π.app none

Tactic:
by subsingleton

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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
n : ℕ
x y : ↑(X.nonDegenerate n)
h :
  ∃ (h : ((fun x ↦ N.mk ↑x ⋯) x).dim = ((fun x ↦ N.mk ↑x ⋯) y).dim),
    (((fun x ↦ N.mk ↑x ⋯) x).cast h).simplex = ((fun x ↦ N.mk ↑x ⋯) y).simplex
⊢ x = y

Tactic:
aesop

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

Goal state before:
pp: case mp
X : SSet
A B : X.Subcomplex
⊢ A ≤ B → ∀ (n : ℕ) (x : ↑(X.nonDegenerate n)), ↑x ∈ A.obj (op ⦋n⦌) → ↑x ∈ B.obj (op ⦋n⦌)

Tactic:
aesop

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

Goal state before:
pp: X : SSet
n✝ : ℕ
Y : SSet
e : X ≅ Y
n : ℕ
x✝ : ↑(X.nonDegenerate n)
x : X _⦋n⦌
hx : x ∈ X.nonDegenerate n
⊢ (ConcreteCategory.hom (e.hom.app (op ⦋n⦌))) x ∈ Y.nonDegenerate n

Tactic:
aesop

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

Goal state before:
pp: X : SSet
n✝ : ℕ
Y : SSet
e : X ≅ Y
n : ℕ
x✝ : ↑(Y.nonDegenerate n)
y : Y _⦋n⦌
hy : y ∈ Y.nonDegenerate n
⊢ (ConcreteCategory.hom (e.inv.app (op ⦋n⦌))) y ∈ X.nonDegenerate n

Tactic:
aesop

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

Goal state before:
pp: X : SSet
n✝ : ℕ
Y : SSet
e : X ≅ Y
n : ℕ
x✝ : ↑(X.nonDegenerate n)
⊢ (fun x ↦
        match x with
        | ⟨y, hy⟩ => ⟨(ConcreteCategory.hom (e.inv.app (op ⦋n⦌))) y, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨x, hx⟩ => ⟨(ConcreteCategory.hom (e.hom.app (op ⦋n⦌))) x, ⋯⟩)
        x✝) =
    x✝

Tactic:
aesop

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

Goal state before:
pp: X : SSet
n✝ : ℕ
Y : SSet
e : X ≅ Y
n : ℕ
x✝ : ↑(Y.nonDegenerate n)
⊢ (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨(ConcreteCategory.hom (e.hom.app (op ⦋n⦌))) x, ⋯⟩)
      ((fun x ↦
          match x with
          | ⟨y, hy⟩ => ⟨(ConcreteCategory.hom (e.inv.app (op ⦋n⦌))) y, ⋯⟩)
        x✝) =
    x✝

Tactic:
aesop

Goal state after:
Module: Mathlib.Order.Fin.SuccAboveOrderIso

Goal state before:
pp: n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
hj✝ : j ∈ {i.succ}ᶜ
hj : ¬j = i.succ
⊢ (fun a ↦ ⟨i.succ.succAboveOrderEmb a, ⋯⟩) (i.predAbove j) = ⟨j, hj✝⟩

Tactic:
aesop

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

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Quiver.IsThin C
n : SimplexCategoryᵒᵖ
x y : (nerve C).obj n
h : x.obj = y.obj
⊢ ∀ (i : ℕ) (hi : i < (unop n).len),
    ComposableArrows.map' x i (i + 1) ⋯ hi = eqToHom ⋯ ≫ ComposableArrows.map' y i (i + 1) ⋯ hi ≫ eqToHom ⋯

Tactic:
by subsingleton

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) :=
  Edge.CompStruct.mk (ComposableArrows.mk₂ f₀₁ f₁₂) ⋯ ⋯ ⋯
x✝ : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
⊢ Arrow.mk (f₀₁ ≫ f₁₂) = Arrow.mk f₀₂

Tactic:
apply ComposableArrows.arrowEquiv.symm.injective

Goal state after:
C : Type u
inst✝ : Category.{v, u} C
x₀ x₁ x₂ : C
f₀₁ : x₀ ⟶ x₁
f₁₂ : x₁ ⟶ x₂
f₀₂ : x₀ ⟶ x₂
h' : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk (f₀₁ ≫ f₁₂)) := ⋯
x✝ : Nonempty ((edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂))
h : (edgeMk f₀₁).CompStruct (edgeMk f₁₂) (edgeMk f₀₂)
⊢ ComposableArrows.arrowEquiv.symm (Arrow.mk (f₀₁ ≫ f₁₂)) = ComposableArrows.arrowEquiv.symm (Arrow.mk f₀₂)
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
A : C
φ ψ : A ⟶ A
hOdd : φ ≫ ψ = 0
hEven : ψ ≫ φ = 0
c : ComplexShape ℕ
inst✝ : DecidableRel c.Rel
hc : ∀ (i j : ℕ), c.Rel i j → Odd (i + j)
i j : ℕ
⊢ ¬c.Rel i j → (if hij : c.Rel i j then if hi : Even i then φ else ψ else 0) = 0

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
U V : SimplexCategoryᵒᵖ
i : U ⟶ V
⊢ {f | Finset.image ⇑(Hom.toOrderHom (objEquiv f)) ⊤ ⊆ S} ⊆
    ⇑(ConcreteCategory.hom (Δ[n].map i)) ⁻¹' {f | Finset.image ⇑(Hom.toOrderHom (objEquiv f)) ⊤ ⊆ S}

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
S₁ S₂ : Finset (Fin (n + 1))
⊢ face S₁ ⊓ face S₂ = face (S₁ ⊓ S₂)

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
i : Fin (n + 1)
⊢ i ∈ S → obj₀Equiv.symm i ∈ (face S).obj (op ⦋0⦌)

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
⊢ f ≫ C.d 0 (0 + 1) = 0

Tactic:
exact w

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
n✝ : ℕ
⊢ f ≫ C.d 0 (n✝ + 1 + 1) = 0

Tactic:
C.shape,

Goal state after:
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
n✝ : ℕ
⊢ f ≫ 0 = 0

case succ.a
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
n✝ : ℕ
⊢ ¬(ComplexShape.up ℕ).Rel 0 (n✝ + 1 + 1)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
j : SimplexCategory
f : j ⟶ ⦋m⦌
x✝ : Fin (⦋n⦌.len + 1)
⊢ x✝ ∈
      Finset.image
        ⇑(Hom.toOrderHom
            (objEquiv
              (objMk
                ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f))))))
        ⊤ →
    x✝ ∈ S

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
X✝ X'✝ : SimplexCategory
f : X✝ ⟶ X'✝
g : X'✝ ⟶ ⦋m⦌
⊢ {
        toFun := fun f ↦
          ⟨objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f))),
            ⋯⟩,
        invFun := fun x ↦
          match x with
          | ⟨x, hx⟩ => Hom.mk { toFun := fun i ↦ e.symm ⟨(Hom.toOrderHom (objEquiv x)) i, ⋯⟩, monotone' := ⋯ },
        left_inv := ⋯, right_inv := ⋯ }
      (f ≫ g) =
    (ConcreteCategory.hom ((face S).toSSet.map f.op))
      ({
          toFun := fun f ↦
            ⟨objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp (e.toOrderEmbedding.toOrderHom.comp (Hom.toOrderHom f))),
              ⋯⟩,
          invFun := fun x ↦
            match x with
            | ⟨x, hx⟩ => Hom.mk { toFun := fun i ↦ e.symm ⟨(Hom.toOrderHom (objEquiv x)) i, ⋯⟩, monotone' := ⋯ },
          left_inv := ⋯, right_inv := ⋯ }
        g)

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
d : SimplexCategoryᵒᵖ
x✝ : unop d ⟶ ⦋n⦌
⊢ (fun f ↦ Hom.mk (ULift.orderIso.{u, 0}.toOrderEmbedding.toOrderHom.comp (Functor.toOrderHom f)))
      ((fun f ↦ ⋯.functor) x✝) =
    x✝

Tactic:
aesop

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

Goal state before:
pp: n d : ℕ
x✝ : ↑(Δ[n].nonDegenerate d)
⊢ (fun s ↦ ⟨objEquiv.symm (Hom.mk s.toOrderHom), ⋯⟩) ((fun s ↦ OrderEmbedding.ofStrictMono ⇑↑s ⋯) x✝) = x✝

Tactic:
aesop

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : i < j
x✝¹ x✝ : Fin n
hk :
  (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) x✝¹ =
    (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) x✝
⊢ (RelEmbedding.trans (i.castPred ⋯).succAboveOrderEmb j.succAboveOrderEmb) x✝¹ =
    (RelEmbedding.trans (i.castPred ⋯).succAboveOrderEmb j.succAboveOrderEmb) x✝

Tactic:
by rwa [Subtype.ext_iff] at hk

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

Goal state before:
pp: case refine_3
n : ℕ
i j : Fin (n + 2)
h : i < j
x✝ : ↥{i, j}ᶜ
m : Fin (n + 1)
hl : j.succAbove m ∈ {i, j}ᶜ
k : Fin n
hk : (i.castPred ⋯).succAbove k = m
⊢ ∃ a, (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) a = ⟨j.succAbove m, hl⟩

Tactic:
exact ⟨k, by simp [hk]⟩

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

Goal state before:
pp: case right
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
j : Fin (n + 1)
hj✝ : j ∈ ↑(nonDegenerateEquiv' x)
hj : ∃ i, ↑x i = j
⊢ ∃ a, (fun i ↦ ⟨↑x i, ⋯⟩) a = ⟨j, hj✝⟩

Tactic:
aesop

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

Goal state before:
pp: n : SimplexCategory
d d' : SimplexCategoryᵒᵖ
f : d ⟶ d'
g : (stdSimplex.obj n).op.obj d
i : Fin (d'.1.len + 1)
⊢ ((opObjEquiv g) ((ConcreteCategory.hom f.unop) i.rev.rev).rev).rev =
    ((ConcreteCategory.hom ((stdSimplex.obj n).map f)) (stdSimplex.opObjEquiv g)) i

Tactic:
aesop

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m : SimplexCategoryᵒᵖ
u : op ⦋n⦌ ⟶ m
⊢ ↑({ toFun := fun x_1 ↦ ⟨(ConcreteCategory.hom (X.map u)) ↑x_1, ⋯⟩ } ⟨yonedaEquiv.toFun (yonedaEquiv.invFun x), ⋯⟩) =
    ↑⟨(ConcreteCategory.hom (X.map u)) (yonedaEquiv.toFun (yonedaEquiv.invFun x)), ⋯⟩

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ (ComplexShape.up ℕ).Rel 0 0 →
    (match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d 0 0 =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d 0 0 ≫
        match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
n✝ : ℕ
⊢ (ComplexShape.up ℕ).Rel (n✝ + 1) 0 →
    (match n✝ + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d (n✝ + 1) 0 =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d (n✝ + 1) 0 ≫
        match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.zero.zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
⊢ (ComplexShape.up ℕ).Rel 0 (0 + 1) →
    (match 0 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d 0 (0 + 1) =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d 0 (0 + 1) ≫
        match 0 + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))

Tactic:
aesop

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ.zero.succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
n✝ : ℕ
⊢ (ComplexShape.up ℕ).Rel (n✝ + 1) (0 + 1) →
    (match n✝ + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))) ≫
        C.d (n✝ + 1) (0 + 1) =
      ((truncate.obj C).augment (C.d 0 1) ⋯).d (n✝ + 1) (0 + 1) ≫
        match 0 + 1 with
        | 0 => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X 0)
        | n.succ => 𝟙 (((truncate.obj C).augment (C.d 0 1) ⋯).X (n + 1))

Tactic:
aesop

Goal state after: