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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
n : ℕ
φ : (m : Fin (n + 1)) × (_ : ⦋n⦌ ⟶ ⦋↑m⦌) × ↑(X.nonDegenerate ↑m) → X _⦋n⦌ :=
  fun x ↦
    match x with
    | ⟨m, ⟨f, x⟩⟩ => (ConcreteCategory.hom (X.map f.op)) ↑x
x : X _⦋n⦌
⊢ ∃ a, φ a = x

Tactic:
by

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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x : X.N
⊢ (fun y ↦ mk ((ConcreteCategory.hom (e.inv.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯)
      ((fun x ↦ mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯) x) =
    x

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x✝ : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁ : ↑(X.nonDegenerate m)
hy₁ : x✝ = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : ↑(X.nonDegenerate m)
hy₂ : x✝ = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : Fin (m + 1) → Fin (n + 1) :=
  fun y ↦ if y = (SimplexCategory.Hom.toOrderHom f₁) x then x else (SimplexCategory.Hom.toOrderHom hf.section_) y
y : Fin (m + 1)
⊢ (SimplexCategory.Hom.toOrderHom f₁) (α y) = y

Tactic:
by

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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x✝ : Y.N
⊢ (fun x ↦ mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯)
      ((fun y ↦ mk ((ConcreteCategory.hom (e.inv.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯) x✝) =
    x✝

Tactic:
by

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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
n : SimplexCategoryᵒᵖ
⊢ Finite (X.obj n)

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x✝ : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁✝ : ↑(X.nonDegenerate m)
hy₁ : x✝ = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁✝
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂✝ : ↑(X.nonDegenerate m)
hy₂ : x✝ = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂✝
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : Fin (m + 1) → Fin (n + 1) :=
  fun y ↦ if y = (SimplexCategory.Hom.toOrderHom f₁) x then x else (SimplexCategory.Hom.toOrderHom hf.section_) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁) (α y) = y
y₁ y₂ : Fin (m + 1)
h : y₁ ≤ y₂
h' : α y₂ < α y₁
this : y₂ ≤ y₁
⊢ False

Tactic:
by

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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
A : X.Subcomplex
⊢ A.toSSet.Finite

Tactic:
by

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

Goal state before:
pp: X : SSet
inst✝ : X.Finite
A : X.Subcomplex
⊢ A.toSSet.Finite

Tactic:
by
  obtain ⟨d, _⟩ := X.hasDimensionLT_of_finite
  refine finite_of_hasDimensionLT _ d (fun i hi ↦ ?_)
  apply Finite.of_injective (f := fun a ↦ a.1.1)
  rintro ⟨⟨x, _⟩, _⟩ ⟨⟨y, _⟩, _⟩ rfl
  rfl

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

Goal state before:
pp: X : SSet
n : ℕ
x✝ : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁✝ : ↑(X.nonDegenerate m)
hy₁ : x✝ = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁✝
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂✝ : ↑(X.nonDegenerate m)
hy₂ : x✝ = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂✝
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : Fin (m + 1) → Fin (n + 1) :=
  fun y ↦ if y = (SimplexCategory.Hom.toOrderHom f₁) x then x else (SimplexCategory.Hom.toOrderHom hf.section_) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁) (α y) = y
y₁ y₂ : Fin (m + 1)
h : y₁ ≤ y₂
h' : α y₂ < α y₁
⊢ False

Tactic:
suffices y₂ ≤ y₁ by simp [show y₁ = y₂ by lia] at h'

Goal state after:
X : SSet
n : ℕ
x✝ : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁✝ : ↑(X.nonDegenerate m)
hy₁ : x✝ = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁✝
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂✝ : ↑(X.nonDegenerate m)
hy₂ : x✝ = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂✝
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : Fin (m + 1) → Fin (n + 1) :=
  fun y ↦ if y = (SimplexCategory.Hom.toOrderHom f₁) x then x else (SimplexCategory.Hom.toOrderHom hf.section_) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁) (α y) = y
y₁ y₂ : Fin (m + 1)
h : y₁ ≤ y₂
h' : α y₂ < α y₁
⊢ y₂ ≤ y₁
Module: Mathlib.AlgebraicTopology.SimplicialSet.Degenerate

Goal state before:
pp: X : SSet
n : ℕ
x✝ : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁ : ↑(X.nonDegenerate m)
hy₁ : x✝ = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : ↑(X.nonDegenerate m)
hy₂ : x✝ = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : Fin (m + 1) → Fin (n + 1) :=
  fun y ↦ if y = (SimplexCategory.Hom.toOrderHom f₁) x then x else (SimplexCategory.Hom.toOrderHom hf.section_) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁) (α y) = y
⊢ Monotone α

Tactic:
by

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

Goal state before:
pp: X Y : SSet
inst✝ : Y.Finite
f : X ⟶ Y
hf : Mono f
⊢ X.Finite

Tactic:
by

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

Goal state before:
pp: X Y : SSet
e : X ≅ Y
x y : X.N
⊢ { toFun := fun x ↦ mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯,
          invFun := fun y ↦ mk ((ConcreteCategory.hom (e.inv.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯, left_inv := ⋯,
          right_inv := ⋯ }
        x ≤
      { toFun := fun x ↦ mk ((ConcreteCategory.hom (e.hom.app (Opposite.op ⦋x.dim⦌))) x.simplex) ⋯,
          invFun := fun y ↦ mk ((ConcreteCategory.hom (e.inv.app (Opposite.op ⦋y.dim⦌))) y.simplex) ⋯, left_inv := ⋯,
          right_inv := ⋯ }
        y ↔
    x ≤ y

Tactic:
by

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

Goal state before:
pp: X Y : SSet
inst✝ : X.Finite
f : X ⟶ Y
hf : Epi f
d : ℕ
h✝ : X.HasDimensionLT d
this : Y.HasDimensionLT d
i : ℕ
hi : i < d
⊢ Finite (Y _⦋i⦌)

Tactic:
by

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

Goal state before:
pp: X Y : SSet
inst✝ : X.Finite
f : X ⟶ Y
hf : Epi f
⊢ Y.Finite

Tactic:
by

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

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

Goal state before:
pp: X : SSet
ι : Type u_1
inst✝ : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), (A i).toSSet.Finite
x✝ : (i : ι) × (A i).toSSet.N
i : ι
s : (A i).toSSet.N
⊢ (ConcreteCategory.hom ((Subcomplex.homOfLE ⋯).app (Opposite.op ⦋s.dim⦌))) s.simplex ∈
    (⨆ i, A i).toSSet.nonDegenerate s.dim

Tactic:
by

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

Goal state before:
pp: d : ℕ
n m : Truncated d
a b : n ⟶ m
⊢ Hom.toOrderHom a.hom = Hom.toOrderHom b.hom ↔ a = b

Tactic:
by

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

Goal state before:
pp: X : SSet
n m : ℕ
x : X _⦋n⦌
y : X _⦋m⦌
hx : x ∈ X.nonDegenerate n
hy : y ∈ X.nonDegenerate m
⊢ { dim := n, simplex := x } = { dim := m, simplex := y } ↔ Subcomplex.ofSimplex x = Subcomplex.ofSimplex y

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x✝ : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁ : ↑(X.nonDegenerate m)
hy₁ : x✝ = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : ↑(X.nonDegenerate m)
hy₂ : x✝ = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : Fin (m + 1) → Fin (n + 1) :=
  fun y ↦ if y = (SimplexCategory.Hom.toOrderHom f₁) x then x else (SimplexCategory.Hom.toOrderHom hf.section_) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁) (α y) = y
hα₂ : Monotone α
⊢ SimplexCategory.Hom.mk { toFun := α, monotone' := hα₂ } ≫ f₁ = 𝟙 ⦋m⦌

Tactic:
by

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

Goal state before:
pp: X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
hf : (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
⊢ x.subcomplex ≤ y.subcomplex

Tactic:
by

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

Goal state before:
pp: X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst✝ : Epi f
hf : (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
this : IsSplitEpi f
⊢ (ConcreteCategory.hom (X.map (section_ f).op)) x.simplex = y.simplex

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x✝ : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁ : ↑(X.nonDegenerate m)
hy₁ : x✝ = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : ↑(X.nonDegenerate m)
hy₂ : x✝ = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
x : Fin (⦋n⦌.len + 1)
hf : SplitEpi f₁
α : Fin (m + 1) → Fin (n + 1) :=
  fun y ↦ if y = (SimplexCategory.Hom.toOrderHom f₁) x then x else (SimplexCategory.Hom.toOrderHom hf.section_) y
hα₁ : ∀ (y : Fin (m + 1)), (SimplexCategory.Hom.toOrderHom f₁) (α y) = y
hα₂ : Monotone α
⊢ (SimplexCategory.Hom.toOrderHom
        { section_ := SimplexCategory.Hom.mk { toFun := α, monotone' := hα₂ }, id := ⋯ }.section_)
      ((SimplexCategory.Hom.toOrderHom f₁) x) =
    x

Tactic:
by

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

Goal state before:
pp: X : SSet
x y : X.S
f : ⦋x.dim⦌ ⟶ ⦋y.dim⦌
inst✝ : Epi f
hf : (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex
⊢ x.subcomplex = y.subcomplex

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
x : X _⦋n⦌
m : ℕ
f₁ : ⦋n⦌ ⟶ ⦋m⦌
inst✝ : Epi f₁
y₁ : ↑(X.nonDegenerate m)
hy₁ : x = (ConcreteCategory.hom (X.map f₁.op)) ↑y₁
f₂ : ⦋n⦌ ⟶ ⦋m⦌
y₂ : ↑(X.nonDegenerate m)
hy₂ : x = (ConcreteCategory.hom (X.map f₂.op)) ↑y₂
⊢ f₁ = f₂

Tactic:
by

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

Goal state before:
pp: X : SSet
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
y : ↑(X.nonDegenerate m)
this : IsSplitEpi f
⊢ Function.Injective ⇑(ConcreteCategory.hom (X.map f.op))

Tactic:
by

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

Goal state before:
pp: X : SSet
ι : Type u_1
inst✝ : Finite ι
A : ι → X.Subcomplex
h : ∀ (i : ι), (A i).toSSet.Finite
d : ℕ
s : X _⦋d⦌
h₁ : s ∈ (⨆ i, A i).obj (Opposite.op ⦋d⦌)
h₂✝ : ⟨s, h₁⟩ ∈ (⨆ i, A i).toSSet.nonDegenerate d
h₂ : ↑⟨s, h₁⟩ ∈ X.nonDegenerate d
i : ι
hi : s ∈ (A i).obj (Opposite.op ⦋d⦌)
⊢ ⟨s, hi⟩ ∈ (A i).toSSet.nonDegenerate d

Tactic:
by

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

Goal state before:
pp: X : SSet
ι : Type u_1
inst✝ : Finite ι
A : ι → X.Subcomplex
⊢ (⨆ i, A i).toSSet.Finite ↔ ∀ (i : ι), (A i).toSSet.Finite

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
n : ℕ
x : ↑(A.obj (op ⦋n⦌))
⊢ x ∈ A.toSSet.degenerate n ↔ ↑x ∈ X.degenerate n

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
n : ℕ
x : ↑(A.obj (op ⦋n⦌))
⊢ x ∈ A.toSSet.nonDegenerate n ↔ ↑x ∈ X.nonDegenerate n

Tactic:
by

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

Goal state before:
pp: X : SSet
x : X.S
⊢ ∃ x_1, x_1.subcomplex = x.subcomplex

Tactic:
by

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

Goal state before:
pp: X : SSet
x : X.S
y₁ y₂ : X.N
h₁ : y₁.subcomplex = x.subcomplex
h₂ : y₂.subcomplex = x.subcomplex
⊢ y₁.subcomplex = y₂.subcomplex

Tactic:
by

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

Goal state before:
pp: X : SSet
x : X.S
y : X.N
⊢ x.toN = y → y.subcomplex = x.subcomplex

Tactic:
by

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

Goal state before:
pp: X : SSet
x : X.S
y : X.N
h : y.subcomplex = x.subcomplex
⊢ x.toN.subcomplex = x.subcomplex

Tactic:
by

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
this✝ : 0 < n
Δ : SimplexCategory
this : Nonempty (CostructuredArrow (inclusion n) Δ)
Δ₁ : SimplexCategory
hΔ₁ : Δ₁.len ≤ n
f : (inclusion n).obj { obj := Δ₁, property := hΔ₁ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
Δ₂ : SimplexCategory
hΔ₂ : Δ₂.len ≤ n
f' : (inclusion n).obj { obj := Δ₂, property := hΔ₂ } ⟶ (Functor.fromPUnit Δ).obj { as := PUnit.unit }
hff' : (ConcreteCategory.hom f) 0 ≤ (ConcreteCategory.hom f') 0
⊢ Zigzag
    { left := { obj := ⦋1⦌, property := this✝ }, right := { as := PUnit.unit },
      hom := mkOfLe ((ConcreteCategory.hom f) 0) ((ConcreteCategory.hom f') 0) hff' }
    { left := { obj := Δ₂, property := hΔ₂ }, right := { as := PUnit.unit }, hom := f' }

Tactic:
· trans ⟨⦋0⦌ₙ, ⟨⟨⟩⟩, ⦋0⦌.const _ (f' 0)⟩
      · apply Zigzag.of_inv <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 1
      · apply Zigzag.of_hom <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 0

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

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

Tactic:
by

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

Goal state before:
pp: X : SSet
y : X.N
n m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
w✝ : Epi f
z : ↑(X.nonDegenerate m)
hy : { dim := n, simplex := (ConcreteCategory.hom (X.map f.op)) ↑z }.toN = y
⊢ y = N.mk ↑z ⋯

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
⊢ A = ⊤ ↔ ∀ (n : ℕ), X.nonDegenerate n ⊆ A.obj (op ⦋n⦌)

Tactic:
by

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

Goal state before:
pp: X : SSet
x : X.S
y : X.N
hy : x.toN = y
⊢ ∃! f, Epi f ∧ (ConcreteCategory.hom (X.map f.op)) y.simplex = x.simplex

Tactic:
by

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
n : ℕ
⊢ A.toSSet.degenerate n = ⊤ ↔ X.degenerate n ⊓ A.obj (op ⦋n⦌) = A.obj (op ⦋n⦌)

Tactic:
by

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

Goal state before:
pp: X : SSet
⊢ ⨆ x, ofSimplex ↑x.snd = ⊤

Tactic:
by

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

Goal state before:
pp: X Y : SSet
n : ℕ
f : X ⟶ Y
m : ℕ
hm : m < n
g : ⦋n⦌ ⟶ ⦋m⦌
y : X _⦋m⦌
⊢ (ConcreteCategory.hom (Y.map g.op)) ((ConcreteCategory.hom (f.app (op ⦋m⦌))) y) =
    (ConcreteCategory.hom (f.app (op ⦋n⦌))) ((ConcreteCategory.hom (X.map g.op)) y)

Tactic:
by

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

Goal state before:
pp: X Y : SSet
n : ℕ
x : X _⦋n⦌
hx : x ∈ X.degenerate n
f : X ⟶ Y
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n

Tactic:
by

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
n : ℕ
⊢ ⇑(ConcreteCategory.hom (f.app (op ⦋n⦌))) '' X.degenerate n ⊆ Y.degenerate n

Tactic:
by

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝ : IsIso f
n : ℕ
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n ↔ x ∈ X.degenerate n

Tactic:
by

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

Goal state before:
pp: X Y : SSet
f : X ⟶ Y
inst✝ : IsIso f
n : ℕ
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.nonDegenerate n ↔ x ∈ X.nonDegenerate n

Tactic:
by

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

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ (inclusion n).Initial

Tactic:
by

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

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

Goal state before:
pp: n m : ℕ
inst✝ : NeZero n
hm : n ≤ m
⊢ n ≤ m

Tactic:
by

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

Goal state before:
pp: n m : ℕ
inst✝ : NeZero n
hm : n ≤ m
⊢ (incl n m ⋯).Initial

Tactic:
by

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

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

Goal state before:
pp: ⊢ 2 = Fin.succ 1

Tactic:
by

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

Goal state before:
pp: ⊢ Fin.succ 0 < 2

Tactic:
by

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

Goal state before:
pp: ⊢ δ₂ 1 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3 =
    Hom.tr (⦋0⦌.const ⦋0 + 1⦌ 0) δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3

Tactic:
by

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

Goal state before:
pp: ⊢ δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3 =
    Hom.tr (⦋0⦌.const ⦋0 + 1⦌ 1) δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3

Tactic:
by

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

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

Goal state before:
pp: ⊢ δ₂ 0 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3 ≫
      δ₂ 2 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_δ₂_two._proof_1 =
    δ₂ 1 δ₂_zero_comp_σ₂_one._proof_4 δ₂_zero_comp_σ₂_one._proof_3 ≫
      δ₂ 0 δ₂_zero_comp_σ₂_one._proof_3 δ₂_zero_comp_δ₂_two._proof_1

Tactic:
by

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

Goal state before:
pp: X Y : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 1 _proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_3 _proof_1).op)) x) =
    x

Tactic:
by

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

Goal state before:
pp: X Y : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })
⊢ (ConcreteCategory.hom (X.map (δ₂ 0 _proof_1 _proof_3).op))
      ((ConcreteCategory.hom (X.map (σ₂ 0 _proof_3 _proof_1).op)) x) =
    x

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
Y : SSet
f : X ⟶ Y
inst✝ : Mono f
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.degenerate n ↔ x ∈ X.degenerate n

Tactic:
by

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

Goal state before:
pp: X : SSet
n : ℕ
Y : SSet
f : X ⟶ Y
inst✝ : Mono f
x : X _⦋n⦌
⊢ (ConcreteCategory.hom (f.app (op ⦋n⦌))) x ∈ Y.nonDegenerate n ↔ x ∈ X.nonDegenerate n

Tactic:
by

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

Goal state before:
pp: X Y : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })
e : Edge x₀ x₁
f : X ⟶ Y
⊢ (ConcreteCategory.hom (Y.map (δ₂ 1 _proof_1 _proof_3).op))
      ((ConcreteCategory.hom (f.app (Opposite.op { obj := ⦋1⦌, property := _proof_2 }))) e.edge) =
    (ConcreteCategory.hom (f.app (Opposite.op { obj := ⦋0⦌, property := _proof_1 }))) x₀

Tactic:
by

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

Goal state before:
pp: X Y : Truncated 2
x₀ x₁ : X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })
e : Edge x₀ x₁
f : X ⟶ Y
⊢ (ConcreteCategory.hom (Y.map (δ₂ 0 _proof_1 _proof_3).op))
      ((ConcreteCategory.hom (f.app (Opposite.op { obj := ⦋1⦌, property := _proof_2 }))) e.edge) =
    (ConcreteCategory.hom (f.app (Opposite.op { obj := ⦋0⦌, property := _proof_1 }))) x₁

Tactic:
by

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

Goal state before:
pp: X Y : Truncated 2
x : X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })
f : X ⟶ Y
⊢ (id x).map f = id ((ConcreteCategory.hom (f.app (Opposite.op { obj := ⦋0⦌, property := _proof_1 }))) x)

Tactic:
by

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

Goal state before:
pp: X Y : Truncated 2
inst✝ : Subsingleton (X.obj (Opposite.op { obj := ⦋1⦌, property := _proof_2 }))
x y : X.obj (Opposite.op { obj := ⦋0⦌, property := _proof_1 })
f g : Edge x y
⊢ f = g

Tactic:
by

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

Goal state before:
pp: X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ x₁ = y₁

Tactic:
by

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

Goal state before:
pp: X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ x₀ = y₀

Tactic:
by

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

Goal state before:
pp: X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ (id x₀).edge = (id y₀).edge

Tactic:
by

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

Goal state before:
pp: X Y : SSet
x₀ x₁ x₂ y₀ y₁ : X _⦋0⦌
hom : Edge x₀ x₁
hom' : Edge y₀ y₁
I : hom.InvStruct
hhom : hom.edge = hom'.edge
⊢ (id x₁).edge = (id y₁).edge

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
⊢ s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i)) ↔ s.obj i.castSucc = s.obj i.succ

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
hi : s.obj i.castSucc = s.obj i.succ
⊢ s ∈ Set.range ⇑(ConcreteCategory.hom (SimplicialObject.σ (nerve X) i))

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n + 1⦌
i : Fin (n + 1)
hi : s.obj i.castSucc = s.obj i.succ
⊢ s ∈ (nerve X).degenerate (n + 1)

Tactic:
by

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

Goal state before:
pp: X : Truncated 2
s : X.obj (Opposite.op { obj := ⦋2⦌, property := _proof_1 })
⊢ ∃ x₀ x₁ x₂ e₀₁ e₁₂ e₀₂ h, h.simplex = s

Tactic:
by

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

Goal state before:
pp: X : Type u_1
inst✝ : PartialOrder X
n : ℕ
s : nerve X _⦋n⦌
⊢ s ∈ (nerve X).nonDegenerate n ↔ StrictMono s.obj

Tactic:
by

Goal state after: