mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : Preadditive C
⊢ IsIdempotentComplete C ↔ ∀ (X : C) (p : X ⟶ X), p ≫ p = p → HasKernel p

Tactic:
by
  rw [isIdempotentComplete_iff_hasEqualizer_of_id_and_idempotent]
  constructor
  · intro h X p hp
    have : HasEqualizer (𝟙 X) (𝟙 X - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)
    convert! hasKernel_of_hasEqualizer (𝟙 X) (𝟙 X - p)
    rw [sub_sub_cancel]
  · intro h X p hp
    have : HasKernel (𝟙 _ - p) := h X (𝟙 _ - p) (idem_of_id_sub_idem p hp)
    apply Preadditive.hasEqualizer_of_hasKernel

Goal state after:
Module: Mathlib.CategoryTheory.Idempotents.Basic

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
⊢ ∀ (X : D) (p : X ⟶ X), p ≫ p = p → ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p

Tactic:
intro X' p hp

Goal state after:
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
D : Type u_2
inst✝ : Category.{v_2, u_2} D
ε : C ≌ D
h : IsIdempotentComplete C
X' : D
p : X' ⟶ X'
hp : p ≫ p = p
⊢ ∃ Y i e, i ≫ e = 𝟙 Y ∧ e ≫ i = p
Module: Mathlib.CategoryTheory.Idempotents.FunctorCategories

Goal state before:
pp: case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
⊢ autoParam
    (∀ (X Y : J ⥤ C) (f : X ⟶ Y),
      (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).map f =
        eqToHom ⋯ ≫ ((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
intro X Y f

Goal state after:
case h_map
J : Type u_1
C : Type u_2
inst✝¹ : Category.{v_1, u_1} J
inst✝ : Category.{v_2, u_2} C
X Y : J ⥤ C
f : X ⟶ Y
⊢ (toKaroubi (J ⥤ C) ⋙ karoubiFunctorCategoryEmbedding J C).map f =
    eqToHom ⋯ ≫ ((Functor.whiskeringRight J C (Karoubi C)).obj (toKaroubi C)).map f ≫ eqToHom ⋯
Module: Mathlib.AlgebraicTopology.AlternatingFaceMapComplex

Goal state before:
pp: case h_map
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
⊢ autoParam
    (∀ (X Y : SimplicialObject C) (f : X ⟶ Y),
      (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).map f =
        eqToHom ⋯ ≫ ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).map f ≫ eqToHom ⋯)
    Functor.ext._auto_1

Tactic:
intro X Y f

Goal state after:
case h_map
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
D : Type u_2
inst✝² : Category.{v_2, u_2} D
inst✝¹ : Preadditive D
F : C ⥤ D
inst✝ : F.Additive
X Y : SimplicialObject C
f : X ⟶ Y
⊢ (alternatingFaceMapComplex C ⋙ F.mapHomologicalComplex (ComplexShape.down ℕ)).map f =
    eqToHom ⋯ ≫ ((SimplicialObject.whiskering C D).obj F ⋙ alternatingFaceMapComplex D).map f ≫ eqToHom ⋯
Module: Mathlib.AlgebraicTopology.SimplicialObject.Basic

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X : SimplicialObject C
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
⊢ X.σ j.succ ≫ X.δ i.castSucc = X.δ i ≫ X.σ j

Tactic:
by
  dsimp [δ, σ]
  simp only [← X.map_comp, ← op_comp, SimplexCategory.δ_comp_σ_of_le H]

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

Goal state before:
pp: n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
⊢ ↑((Hom.toOrderHom (mkOfSucc i ≫ δ j)) x) = ↑((Hom.toOrderHom (mkOfSucc i.succ)) x)

Tactic:
simp only [δ, len_mk, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, OrderHom.comp_coe,
    OrderEmbedding.toOrderHom_coe, Function.comp_apply, Fin.succAboveOrderEmb_apply]

Goal state after:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
⊢ ↑(j.succAbove ((Hom.toOrderHom (mkOfSucc i)) x)) = ↑((Hom.toOrderHom (mkOfSucc i.succ)) x)
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (δ₀Iter (i + 1) h)) k) = ↑((ConcreteCategory.hom (δ₀Iter i ⋯)) (Fin.succAbove 0 k))

Tactic:
δ₀Iter_apply ..,

Goal state after:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋n⦌.len + 1)
⊢ ↑⟨↑k + (i + 1), ⋯⟩ = ↑((ConcreteCategory.hom (δ₀Iter i ⋯)) (Fin.succAbove 0 k))
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑(j.succAbove ((ConcreteCategory.hom (δ₀Iter i hi)) k)) = ↑((ConcreteCategory.hom (δ₀Iter (i + 1) ⋯)) k)

Tactic:
δ₀Iter_apply ..,

Goal state after:
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑(j.succAbove ⟨↑k + i, ⋯⟩) = ↑((ConcreteCategory.hom (δ₀Iter (i + 1) ⋯)) k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑(j.succAbove ⟨↑k + i, ⋯⟩) = ↑((ConcreteCategory.hom (δ₀Iter (i + 1) ⋯)) k)

Tactic:
δ₀Iter_apply ..,

Goal state after:
i n m : ℕ
j : Fin (m + 2)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑(j.succAbove ⟨↑k + i, ⋯⟩) = ↑⟨↑k + (i + 1), ⋯⟩
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:
by aesop

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

Goal state before:
pp: n : SimplexCategory
f : n ⟶ n
hf : Function.Injective ⇑(Hom.toOrderHom f)
h : n.len = n.len
⊢ Function.Surjective (Hom.toOrderHom f).toFun

Tactic:
by rwa [← Finite.injective_iff_surjective]

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:
by aesop

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

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (σ j)) ((ConcreteCategory.hom (δ₀Iter (i + 1) ⋯)) k)) =
    ↑((ConcreteCategory.hom (δ₀Iter i ⋯)) k)

Tactic:
δ₀Iter_apply ..,

Goal state after:
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (σ j)) ⟨↑k + (i + 1), ⋯⟩) = ↑((ConcreteCategory.hom (δ₀Iter i ⋯)) k)
Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (σ j)) ⟨↑k + (i + 1), ⋯⟩) = ↑((ConcreteCategory.hom (δ₀Iter i ⋯)) k)

Tactic:
δ₀Iter_apply ..,

Goal state after:
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : ↑j ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ ↑((ConcreteCategory.hom (σ j)) ⟨↑k + (i + 1), ⋯⟩) = ↑⟨↑k + i, ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialObject.Homotopy

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X Y : SimplicialObject C
f g : X ⟶ Y
H : Homotopy f g
X' : SimplicialObject C
p : X' ⟶ X
n : ℕ
⊢ (p.app (op ⦋n⦌) ≫ H.h 0) ≫ Y.δ 0 = (p ≫ g).app (op ⦋n⦌)

Tactic:
simpa [-h_zero_comp_δ_zero] using p.app _ ≫= H.h_zero_comp_δ_zero n

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝¹ : Epi f
d : ℕ
inst✝ : X.HasDimensionLT d
n : ℕ
hn : d ≤ n
x : X _⦋n⦌
⊢ x ∈ X.degenerate n

Tactic:
simp [X.degenerate_eq_univ_of_hasDimensionLT d n hn]

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:
by aesop

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
j✝ : Fin (x.len + 1)
⊢ WidePushout.ι (fun x ↦ F.hom) j✝ ≫
      WidePushout.desc (WidePushout.head fun x ↦ F.hom)
          (fun i ↦ WidePushout.ι (fun x ↦ F.hom) ((SimplexCategory.Hom.toOrderHom f) i)) ⋯ ≫
        WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app y) (fun i ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y i)) ⋯ =
    WidePushout.ι (fun x ↦ F.hom) j✝ ≫
      WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app x) (fun i ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x i)) ⋯ ≫
        X.right.map f

Tactic:
simp only [WidePushout.ι_desc_assoc, WidePushout.ι_desc]

Goal state after:
case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
j✝ : Fin (x.len + 1)
⊢ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y ((SimplexCategory.Hom.toOrderHom f) j✝)) =
    (Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x j✝)) ≫ X.right.map f
Module: Mathlib.AlgebraicTopology.SimplicialSet.Subcomplex

Goal state before:
pp: X Y : SSet
A : X.Subcomplex
p : Y ⟶ X
U✝ V✝ : SimplexCategoryᵒᵖ
f : U✝ ⟶ V✝
⊢ ⇑(ConcreteCategory.hom (p.app U✝)) ⁻¹' ⇑(ConcreteCategory.hom (X.map f)) ⁻¹' A.obj V✝ ⊆
    ⇑(ConcreteCategory.hom (Y.map f)) ⁻¹' ⇑(ConcreteCategory.hom (p.app V✝)) ⁻¹' A.obj V✝

Tactic:
by simp [Set.preimage_preimage]

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:
by 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:
by aesop

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

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

Tactic:
by aesop

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

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

Tactic:
by aesop

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

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

Tactic:
by 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:
by 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:
by 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:
by 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
j : ι
⊢ (limitIsoPi ι X).hom ≫ Pi.π (fun x ↦ X) j = WidePullback.π (fun x ↦ terminal.from X) j

Tactic:
rw [← wideCospan.limitIsoPi_inv_comp_pi, Iso.hom_inv_id_assoc]

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

Goal state before:
pp: X : SSet
x✝¹ x✝ : X.N
h : (fun x ↦ x.subcomplex) x✝¹ = (fun x ↦ x.subcomplex) x✝
⊢ x✝¹ = x✝

Tactic:
dsimp at h
    apply le_antisymm <;> rw [N.le_iff, h]

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:
by 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:
by 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:
by 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:
by 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:
by aesop

Goal state after:
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:
by aesop

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

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

Tactic:
by
        match i with
        | 0 | 1 | n + 2 =>
          rcases j with - | j <;> dsimp [augment, truncate] <;> simp

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:
by 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:
by 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
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:
by 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
j : SimplexCategory
x✝ : (face S).toSSet.obj (op j)
x : Δ[n].obj (op j)
hx : x ∈ (face S).obj (op j)
i₁ i₂ : Fin (j.len + 1)
h : i₁ ≤ i₂
⊢ ⟨(Hom.toOrderHom (objEquiv x)) i₁, ⋯⟩ ≤ ⟨(Hom.toOrderHom (objEquiv x)) i₂, ⋯⟩

Tactic:
by
            simp only [Subtype.mk_le_mk]
            exact OrderHom.monotone _ h

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:
by 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:
by 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:
by aesop

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

Goal state before:
pp: case left
n m : ℕ
x₂ : Δ[n] _⦋m⦌
h₂ : x₂ ∈ Δ[n].nonDegenerate m
f₁ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁ : objEquiv.symm f₁ ∈ Δ[n].nonDegenerate m
h₃ :
  (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
      ⟨objEquiv.symm f₁, h₁⟩ =
    (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
      ⟨x₂, h₂⟩
⊢ ⟨objEquiv.symm f₁, h₁⟩ = ⟨x₂, h₂⟩

Tactic:
obtain ⟨f₂, rfl⟩ := objEquiv.symm.surjective x₂

Goal state after:
case left
n m : ℕ
f₁ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₁ : objEquiv.symm f₁ ∈ Δ[n].nonDegenerate m
f₂ : unop (op ⦋m⦌) ⟶ ⦋n⦌
h₂ : objEquiv.symm f₂ ∈ Δ[n].nonDegenerate m
h₃ :
  (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
      ⟨objEquiv.symm f₁, h₁⟩ =
    (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
      ⟨objEquiv.symm f₂, h₂⟩
⊢ ⟨objEquiv.symm f₁, h₁⟩ = ⟨objEquiv.symm f₂, h₂⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case mp
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a b : Fin (d + 1)
⊢ ¬↑x b < ↑x a → a ≤ b

Tactic:
← not_lt

Goal state after:
case mp
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a b : Fin (d + 1)
⊢ ¬↑x b < ↑x a → ¬b < a
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case zero
n d : ℕ
hd : #∅ ≤ d
hm : #∅ = 0
⊢ (face ∅).toSSet.HasDimensionLT d

Tactic:
rw [face_empty]

Goal state after:
case zero
n d : ℕ
hd : #∅ ≤ d
hm : #∅ = 0
⊢ ⊥.toSSet.HasDimensionLT d
Module: Mathlib.Algebra.Homology.ComplexShapeSigns

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝ : TotalComplexShape c₁ c₂ c₁₂
this : TotalComplexShape c₂ c₁ c₁₂ := symm c₁ c₂ c₁₂
i₁✝ i₁'✝ : I₁
x✝¹ : c₁.Rel i₁✝ i₁'✝
x✝ : I₂
⊢ 1 * c₁.ε₁ c₂ c₁₂ (i₁✝, x✝) = c₂.ε₂ c₁ c₁₂ (x✝, i₁✝) * 1

Tactic:
by aesop

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

Goal state before:
pp: I₁ : Type u_1
I₂ : Type u_2
I₃ : Type u_3
I₁₂ : Type u_4
I₂₃ : Type u_5
J : Type u_6
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
c₃ : ComplexShape I₃
c₁₂ : ComplexShape I₁₂
c₂₃ : ComplexShape I₂₃
c : ComplexShape J
inst✝ : TotalComplexShape c₁ c₂ c₁₂
this : TotalComplexShape c₂ c₁ c₁₂ := symm c₁ c₂ c₁₂
x✝¹ : I₁
x✝ : I₂
⊢ ∀ {i₂' : I₂}, c₂.Rel x✝ i₂' → 1 * c₁.ε₂ c₂ c₁₂ (x✝¹, x✝) = c₂.ε₁ c₁ c₁₂ (x✝, x✝¹) * 1

Tactic:
by aesop

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 1)
⊢ ExtraDegeneracy.s f S n ≫ f.augmentedCechNerve.left.σ i.succ =
    f.augmentedCechNerve.left.σ i ≫ ExtraDegeneracy.s f S (n + 1)

Tactic:
dsimp [SimplicialObject.σ, SimplexCategory.σ]
    ext j
    · induction j using Fin.cases <;> simp
    · simp

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

Goal state before:
pp: case neg
C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁₂ i₁₂' : I₁₂
h₁₂ : ¬c₁₂.Rel i₁₂ i₁₂'
i₁ : I₁
i₂ : I₂
h : c₁.π c₂ c₁₂ (i₁, i₂) = i₁₂
h₁ : ¬c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂' = 0

Tactic:
exact d₁_eq_zero _ _ _ _ _ h₁

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

Goal state before:
pp: case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₃ : c₂.π c₁ c (c₂.next i₂, i₁) = j'
h₄ : c₁.π c₂ c (i₁, c₂.next i₂) = j'
⊢ c₁.σ c₂ c i₁ i₂ • c₁.ε₂ c₂ c (i₁, i₂) • (K.X i₁).d i₂ (c₂.next i₂) ≫ K.ιTotal c i₁ (c₂.next i₂) j' h₄ =
    K.flip.d₁ c i₂ i₁ j' ≫ K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯

Tactic:
K.flip.d₁_eq _ h₂ _ _ h₃,

Goal state after:
case pos
C : Type u_1
I₁ : Type u_2
I₂ : Type u_3
J : Type u_4
inst✝⁶ : Category.{v_1, u_1} C
inst✝⁵ : Preadditive C
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c : ComplexShape J
inst✝⁴ : TotalComplexShape c₁ c₂ c
inst✝³ : TotalComplexShape c₂ c₁ c
inst✝² : TotalComplexShapeSymmetry c₁ c₂ c
inst✝¹ : K.HasTotal c
inst✝ : DecidableEq J
j j' : J
h₀ : c.Rel j j'
i₂ : I₂
i₁ : I₁
h₁ : c₂.π c₁ c (i₂, i₁) = j
h₂ : c₂.Rel i₂ (c₂.next i₂)
h₃ : c₂.π c₁ c (c₂.next i₂, i₁) = j'
h₄ : c₁.π c₂ c (i₁, c₂.next i₂) = j'
⊢ c₁.σ c₂ c i₁ i₂ • c₁.ε₂ c₂ c (i₁, i₂) • (K.X i₁).d i₂ (c₂.next i₂) ≫ K.ιTotal c i₁ (c₂.next i₂) j' h₄ =
    (c₂.ε₁ c₁ c (i₂, i₁) • (K.flip.d i₂ (c₂.next i₂)).f i₁ ≫ K.flip.ιTotal c (c₂.next i₂) i₁ j' h₃) ≫
      K.flip.totalDesc fun i₂ i₁ h ↦ c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j' ⋯
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m✝ p : ℤ
α₁ α₂ : Cocycle K L n
m : ℤ
hm : m + 1 = n
β₁ : Cochain K L m
hβ₁ : δ m n β₁ = ↑α₁
hm' : m + 1 = n
β₂ : Cochain K L m
hβ₂ : δ m n β₂ = ↑α₂
⊢ δ m n (β₁ + β₂) = ↑(α₁ + α₂)

Tactic:
by aesop

Goal state after:
Module: Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : Preadditive C
R : Type u_1
inst✝¹ : Ring R
inst✝ : Linear R C
K L : CochainComplex C ℤ
n m✝ p : ℤ
α : Cocycle K L n
m : ℤ
hm : m + 1 = n
β : Cochain K L m
hβ : δ m n β = ↑α
⊢ δ m n (-β) = ↑(-α)

Tactic:
by aesop

Goal state after: