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

Goal state before:
pp: i : ℕ
hi' :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m),
    ↑j = ↑j' + i → σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : ↑j = ↑j' + (i + 1)
⊢ n + 1 + i = m

Tactic:
by

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

Goal state before:
pp: i : ℕ
hi' :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m),
    ↑j = ↑j' + i → σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : ↑j = ↑j' + (i + 1)
⊢ ↑j = ↑j'.succ + i

Tactic:
by

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

Goal state before:
pp: X Y : SSet
y : Y _⦋0⦌
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (X.map x✝ ≫ ↾fun x ↦ (ConcreteCategory.hom (Y.map ((Opposite.unop x✝¹).const ⦋0⦌ 0).op)) y) =
    (↾fun x ↦ (ConcreteCategory.hom (Y.map ((Opposite.unop x✝²).const ⦋0⦌ 0).op)) y) ≫ Y.map x✝

Tactic:
by

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

Goal state before:
pp: X Y Z : SSet
y : Y _⦋0⦌
g : Y ⟶ Z
⊢ const y ≫ g = const ((ConcreteCategory.hom (g.app (Opposite.op ⦋0⦌))) y)

Tactic:
by

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

Goal state before:
pp: S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 2)
x : S _⦋n + 1⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) ((ConcreteCategory.hom (SimplicialObject.δ S i)) x) =
    (ConcreteCategory.hom (SimplicialObject.δ T i)) ((ConcreteCategory.hom (f.app (op ⦋n + 1⦌))) x)

Tactic:
by

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

Goal state before:
pp: i : ℕ
hi' :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi : n + i = m),
    ↑j = ↑j' + i → σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + (i + 1) = m
hj : ↑j = ↑j' + (i + 1)
⊢ 0 ≤ j'

Tactic:
by

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

Goal state before:
pp: S T : SSet
f : S ⟶ T
n : ℕ
i : Fin (n + 1)
x : S _⦋n⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n + 1⦌))) ((ConcreteCategory.hom (SimplicialObject.σ S i)) x) =
    (ConcreteCategory.hom (SimplicialObject.σ T i)) ((ConcreteCategory.hom (f.app (op ⦋n⦌))) x)

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 2)
x : X.op _⦋n + 1⦌
⊢ (ConcreteCategory.hom (SimplicialObject.δ X.op i)) x =
    opObjEquiv.symm ((ConcreteCategory.hom (SimplicialObject.δ X i.rev)) (opObjEquiv x))

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 1)
x : X.op _⦋n⦌
⊢ (ConcreteCategory.hom (SimplicialObject.σ X.op i)) x =
    opObjEquiv.symm ((ConcreteCategory.hom (SimplicialObject.σ X i.rev)) (opObjEquiv x))

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 2)
x : X.op _⦋n + 1⦌
⊢ (ConcreteCategory.hom (SimplicialObject.δ X i)) (opObjEquiv x) =
    opObjEquiv ((ConcreteCategory.hom (SimplicialObject.δ X.op i.rev)) x)

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 1)
x : X.op _⦋n⦌
⊢ (ConcreteCategory.hom (SimplicialObject.σ X i)) (opObjEquiv x) =
    opObjEquiv ((ConcreteCategory.hom (SimplicialObject.σ X.op i.rev)) x)

Tactic:
by

Goal state after:
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
U V : Cᵒᵖ
g : U ⟶ V
f : X ⟶ U
⊢ (ConcreteCategory.hom (F.map (f ≫ g))) x = (ConcreteCategory.hom (F.map g)) ((ConcreteCategory.hom (F.map f)) x)

Tactic:
by

Goal state after:
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
U V : Cᵒᵖ
g : U ⟶ V
⊢ {u | ∃ f, (ConcreteCategory.hom (F.map f)) x = u} ⊆
    ⇑(ConcreteCategory.hom (F.map g)) ⁻¹' {u | ∃ f, (ConcreteCategory.hom (F.map f)) x = u}

Tactic:
by

Goal state after:
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
⊢ (ConcreteCategory.hom (F.map (𝟙 X))) x = x

Tactic:
by

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

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi : n + i = m
hj : ↑j = ↑j' + i
⊢ σ j ≫ σ₀Iter i hi = σ₀Iter i ⋯ ≫ σ j'

Tactic:
by

Goal state after:
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
G : Subfunctor F
⊢ ofSection x ≤ G ↔ x ∈ G.obj X

Tactic:
by

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

Goal state before:
pp: n m : ℕ
hi : n + 0 = m
⊢ n = m

Tactic:
by

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

Goal state before:
pp: i : ℕ
hi' : ∀ {n m : ℕ} (hi : n + i = m), δ₀Iter i hi ≫ σ₀Iter i hi = 𝟙 ⦋n⦌
n m : ℕ
hi : n + (i + 1) = m
⊢ m = n + i + 1

Tactic:
by

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

Goal state before:
pp: i n m : ℕ
hi : n + i = m
⊢ δ₀Iter i hi ≫ σ₀Iter i hi = 𝟙 ⦋n⦌

Tactic:
by

Goal state after:
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'
⊢ (ConcreteCategory.hom (F'.map (𝟙 X))) ((ConcreteCategory.hom (f.app X)) x) = (ConcreteCategory.hom (f.app X)) x

Tactic:
by

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

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
⊢ ofSection x = range (yonedaEquiv.symm x)

Tactic:
by

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
f : yoneda.obj X ⟶ F
⊢ range f = ofSection (yonedaEquiv f)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : Cᵒᵖ
x : F.obj X
⊢ ofSection x = range (uliftYonedaEquiv.symm x)

Tactic:
by

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
F : Cᵒᵖ ⥤ Type (max v w)
X : C
f : yoneda.obj X ⋙ uliftFunctor.{w, v} ⟶ F
⊢ range f = ofSection (uliftYonedaEquiv f)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X✝ Y✝ : SimplexCategoryᵒᵖ
g : X✝ ⟶ Y✝
⊢ ∀ (j : Fin ((Opposite.unop Y✝).len + 1)),
    WidePullback.π (fun x ↦ f.hom) ((SimplexCategory.Hom.toOrderHom g.unop) j) ≫ f.hom = WidePullback.base fun x ↦ f.hom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
f✝ : Arrow C
inst✝² : ∀ (n : ℕ), HasWidePullback f✝.right (fun x ↦ f✝.left) fun x ↦ f✝.hom
f g : Arrow C
inst✝¹ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
inst✝ : ∀ (n : ℕ), HasWidePullback g.right (fun x ↦ g.left) fun x ↦ g.hom
F : f ⟶ g
n : SimplexCategoryᵒᵖ
j : Fin ((Opposite.unop n).len + 1)
⊢ (WidePullback.π (fun x ↦ f.hom) j ≫ Hom.left F) ≫ g.hom = (WidePullback.base fun x ↦ f.hom) ≫ Hom.right F

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
G : X ⟶ F.augmentedCechNerve
⊢ (𝟭 C).map (G.left.app (Opposite.op ⦋0⦌) ≫ WidePullback.π (fun x ↦ F.hom) 0) ≫ F.hom =
    (Augmented.toArrow.obj X).hom ≫ (𝟭 C).map G.right

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
x : SimplexCategoryᵒᵖ
i : Fin ((Opposite.unop x).len + 1)
⊢ (X.left.map (⦋0⦌.const (Opposite.unop x) i).op ≫ Arrow.Hom.left G) ≫ F.hom = X.hom.app x ≫ Arrow.Hom.right G

Tactic:
by

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

Goal state before:
pp: X : SSet
d : ℕ
inst✝ : X.HasDimensionLT d
n : ℕ
hn : d ≤ n
⊢ X.nonDegenerate n = ∅

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x : ↑(X.nonDegenerate n)
d : ℕ
inst✝ : X.HasDimensionLT d
⊢ n < d

Tactic:
by

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

Goal state before:
pp: X : SSet
d : ℕ
inst✝ : X.HasDimensionLT d
A : X.Subcomplex
n : ℕ
hd : d ≤ n
⊢ A.toSSet.degenerate n = ⊤

Tactic:
by

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

Goal state before:
pp: X : SSet
A B : X.Subcomplex
d : ℕ
inst✝ : X.HasDimensionLT d
⊢ A ≤ B ↔ ∀ i < d, A.obj (op ⦋i⦌) ∩ X.nonDegenerate i ⊆ B.obj (op ⦋i⦌)

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
d : ℕ
inst✝ : X.HasDimensionLT d
⊢ A = ⊤ ↔ ∀ i < d, X.nonDegenerate i ⊆ A.obj (op ⦋i⦌)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
G : Augmented.toArrow.obj X ⟶ F
⊢ ∀ ⦃X_1 Y : SimplexCategoryᵒᵖ⦄ (f : X_1 ⟶ Y),
    X.left.map f ≫
        WidePullback.lift (X.hom.app Y ≫ Arrow.Hom.right G)
          (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop Y) i).op ≫ Arrow.Hom.left G) ⋯ =
      WidePullback.lift (X.hom.app X_1 ≫ Arrow.Hom.right G)
          (fun i ↦ X.left.map (⦋0⦌.const (Opposite.unop X_1) i).op ≫ Arrow.Hom.left G) ⋯ ≫
        F.augmentedCechNerve.left.map f

Tactic:
by

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝¹ : Mono f
d : ℕ
inst✝ : Y.HasDimensionLT d
n : ℕ
hn : d ≤ n
⊢ X.degenerate n = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
A : Augmented.toArrow.obj X ⟶ F
⊢ equivalenceRightToLeft X F (equivalenceLeftToRight X F A) = A

Tactic:
by

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
⊢ Y.degenerate n = ⊤

Tactic:
by

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

Goal state before:
pp: X : SSet
ι : Type u_1
A : ι → X.Subcomplex
d : ℕ
⊢ (⨆ i, A i).toSSet.HasDimensionLT d ↔ ∀ (i : ι), (A i).toSSet.HasDimensionLT d

Tactic:
by

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

Goal state before:
pp: X : SSet
n k : ℕ
hk : n ≤ k
⊢ ⊥.toSSet.degenerate k = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
X : Augmented C
F : Arrow C
⊢ Function.RightInverse (equivalenceRightToLeft X F) (equivalenceLeftToRight X F)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
⊢ ∀ {X' X : Augmented C} {Y : Arrow C} (f : X' ⟶ X) (g : X ⟶ augmentedCechNerve.obj Y),
    (cechNerveEquiv X' Y).symm (f ≫ g) = Augmented.toArrow.map f ≫ (cechNerveEquiv X Y).symm g

Tactic:
by

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

Goal state before:
pp: X : SSet
⊢ X.degenerate 0 = ∅

Tactic:
by

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

Goal state before:
pp: X : SSet
⊢ X.nonDegenerate 0 = Set.univ

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ x ∈ X.degenerate n ↔ x ∉ X.nonDegenerate n

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
i : Fin (n + 1)
x : X _⦋n⦌
⊢ n < n + 1

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
⊢ ∀ {X : Augmented C} {Y Y' : Arrow C} (f : Augmented.toArrow.obj X ⟶ Y) (g : Y ⟶ Y'),
    (cechNerveEquiv X Y') (f ≫ g) = (cechNerveEquiv X Y) f ≫ augmentedCechNerve.map g

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝¹ : Category.{v, u} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
x y : SimplexCategory
g : x ⟶ y
⊢ (widePushout f.left (fun x ↦ f.right) fun x ↦ f.hom) ⟶ widePushout f.left (fun x ↦ f.right) fun x ↦ f.hom

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
f✝ : Arrow C
inst✝² : ∀ (n : ℕ), HasWidePushout f✝.left (fun x ↦ f✝.right) fun x ↦ f✝.hom
f g : Arrow C
inst✝¹ : ∀ (n : ℕ), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
inst✝ : ∀ (n : ℕ), HasWidePushout g.left (fun x ↦ g.right) fun x ↦ g.hom
F : f ⟶ g
n : SimplexCategory
i : Fin (n.len + 1)
⊢ g.right ⟶ g.cechConerve.obj n

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
f✝ : Arrow C
inst✝² : ∀ (n : ℕ), HasWidePushout f✝.left (fun x ↦ f✝.right) fun x ↦ f✝.hom
f g : Arrow C
inst✝¹ : ∀ (n : ℕ), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
inst✝ : ∀ (n : ℕ), HasWidePushout g.left (fun x ↦ g.right) fun x ↦ g.hom
F : f ⟶ g
n : SimplexCategory
i : Fin (n.len + 1)
⊢ f.hom ≫ Hom.right F ≫ WidePushout.ι (fun x ↦ g.hom) i = Hom.left F ≫ WidePushout.head fun x ↦ g.hom

Tactic:
by

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
⊢ (image f).len < n

Tactic:
by

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

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: 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.augmentedCechConerve ⟶ X
⊢ G.left ≫ (Augmented.toArrow.obj X).hom = F.hom ≫ WidePushout.ι (fun x ↦ F.hom) 0 ≫ G.right.app ⦋0⦌

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
⊢ x ∈ X.degenerate n ↔ ∃ m, ∃ (_ : m < n), ∃ f, ∃ (_ : Epi f), x ∈ Set.range ⇑(ConcreteCategory.hom (X.map f.op))

Tactic:
by

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

Goal state before:
pp: X : SSet
n m : ℕ
x✝ : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : X _⦋m⦌
⊢ (ConcreteCategory.hom (X.op.map (SimplexCategory.rev.map f).op)) (opObjEquiv.symm y) =
    opObjEquiv.symm ((ConcreteCategory.hom (X.map f.op)) y)

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: 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 : SimplexCategory
⊢ ∀ (j : Fin (x.len + 1)), F.hom ≫ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x j) = Arrow.Hom.left G ≫ X.hom.app x

Tactic:
by

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

Goal state before:
pp: X : SSet
n m : ℕ
x✝ : m < n
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : X.op _⦋m⦌
⊢ (ConcreteCategory.hom (X.map (SimplexCategory.rev.map f).op)) (opObjEquiv y) =
    opObjEquiv ((ConcreteCategory.hom (X.op.map f.op)) y)

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x : X.op _⦋n⦌
⊢ opObjEquiv x ∈ X.degenerate n ↔ x ∈ X.op.degenerate n

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x : X.op _⦋n⦌
⊢ opObjEquiv x ∈ X.nonDegenerate n ↔ x ∈ X.op.nonDegenerate n

Tactic:
by

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

Goal state before:
pp: X : SSet
s : X.S
d : ℕ
hd : s.dim = d
⊢ X _⦋s.dim⦌ = X _⦋d⦌

Tactic:
by

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

Goal state before:
pp: X : SSet
s : X.S
d : ℕ
hd : s.dim = d
⊢ s.cast hd = s

Tactic:
by

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

Goal state before:
pp: X : SSet
s t : X.S
⊢ s = t → ∃ (h : s.dim = t.dim), (s.cast h).simplex = t.simplex

Tactic:
by

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

Goal state before:
pp: X : SSet
s t : X.S
x✝ : ∃ (h : s.dim = t.dim), (s.cast h).simplex = t.simplex
h₁ : s.dim = t.dim
h₂ : (s.cast h₁).simplex = t.simplex
⊢ s = t

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x y : X _⦋n⦌
⊢ { dim := n, simplex := x } = { dim := n, simplex := y } ↔ x = y

Tactic:
by

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

Goal state before:
pp: X : SSet
s : X.S
d : ℕ
hd : s.dim = d
⊢ (s.cast hd).subcomplex = s.subcomplex

Tactic:
by

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

Goal state before:
pp: X : SSet
s t : X.S
⊢ s ≤ t ↔ ∃ f, (ConcreteCategory.hom (X.map f.op)) t.simplex = s.simplex

Tactic:
by

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

Goal state before:
pp: X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
⊢ { dim := m, simplex := (ConcreteCategory.hom (X.map f.op)) x } ≤ { dim := n, simplex := x }

Tactic:
by

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

Goal state before:
pp: X : SSet
n m : ℕ
hm : m < n + 1
f : ⦋n + 1⦌ ⟶ ⦋m⦌
hf✝ : Epi f
y : X _⦋m⦌
hf : Function.Injective ⇑(SimplexCategory.Hom.toOrderHom f)
⊢ False

Tactic:
by

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

Goal state before:
pp: X : SSet
n m : ℕ
x : X _⦋n⦌
f : ⦋m⦌ ⟶ ⦋n⦌
inst✝ : Mono f
⊢ { dim := m, simplex := (ConcreteCategory.hom (X.map f.op)) x } = { dim := n, simplex := x } ↔ IsIso f

Tactic:
by

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

Goal state before:
pp: X : SSet
⊢ Functor.Elements X → X.S

Tactic:
by

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

Goal state before:
pp: X : SSet
x y : X.S
⊢ x ≤ y ↔ Nonempty (equivElements y ⟶ equivElements x)

Tactic:
by

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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x✝ : X.S
⊢ (fun s ↦ { dim := s.dim, simplex := (ConcreteCategory.hom (e.inv.app (Opposite.op ⦋s.dim⦌))) s.simplex })
      ((fun s ↦ { dim := s.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋s.dim⦌))) s.simplex }) x✝) =
    x✝

Tactic:
by

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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x✝ : Y.S
⊢ (fun s ↦ { dim := s.dim, simplex := (ConcreteCategory.hom (e.hom.app (Opposite.op ⦋s.dim⦌))) s.simplex })
      ((fun s ↦ { dim := s.dim, simplex := (ConcreteCategory.hom (e.inv.app (Opposite.op ⦋s.dim⦌))) s.simplex }) x✝) =
    x✝

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
⊢ X.degenerate (n + 1) = ⋃ i, Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ X i))

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
⊢ x ∈ X.nonDegenerate 0

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋0⦌
⊢ x = (ConcreteCategory.hom (X.map (𝟙 ⦋0⦌).op)) ↑⟨x, ⋯⟩

Tactic:
by

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

Goal state before:
pp: X : SSet
n✝ n : ℕ
hn : ∀ (x : X _⦋n⦌), ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
x : X _⦋n + 1⦌
hx : x ∈ X.nonDegenerate (n + 1)
⊢ x = (ConcreteCategory.hom (X.map (𝟙 ⦋n + 1⦌).op)) ↑⟨x, hx⟩

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: 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_1 Y : SimplexCategory⦄ (f : X_1 ⟶ Y),
    F.augmentedCechConerve.right.map f ≫
        WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app Y) (fun i ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const Y i)) ⋯ =
      WidePushout.desc (Arrow.Hom.left G ≫ X.hom.app X_1) (fun i ↦ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const X_1 i))
          ⋯ ≫
        X.right.map f

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ : SSet
f : X✝ ⟶ Y✝
x✝¹ : Mono f
x✝ : Epi f
⊢ IsIso f

Tactic:
by

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

Goal state before:
pp: X Y : SSet
S₁ S₂ : X.Subcomplex
h : S₁ ≤ S₂
⊢ S₁ ≤ S₁

Tactic:
by

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

Goal state before:
pp: X : SSet
n✝ n : ℕ
hn : ∀ (x : X _⦋n⦌), ∃ m f, ∃ (_ : Epi f), ∃ y, x = (ConcreteCategory.hom (X.map f.op)) ↑y
i : Fin (n + 1)
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
z : ↑(X.nonDegenerate m)
⊢ (ConcreteCategory.hom (SimplicialObject.σ X i)) ((ConcreteCategory.hom (X.map f.op)) ↑z) =
    (ConcreteCategory.hom (X.map (SimplexCategory.σ i ≫ f).op)) ↑z

Tactic:
by

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

Goal state before:
pp: X Y : SSet
x✝¹ x✝ : ⊥.toSSet ⟶ Y
⊢ x✝¹ = x✝

Tactic:
by

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

Goal state before:
pp: X Y : SSet
x✝¹ : SimplexCategoryᵒᵖ
x✝ : ⊥.toSSet.obj x✝¹
val✝ : X.obj x✝¹
h : val✝ ∈ ⊥.obj x✝¹
⊢ Y.obj x✝¹

Tactic:
by

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

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

Goal state after: