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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
k : ℕ
hk :
  ∀ (i j : ℕ) (hij : i ≤ j) (hj : j ≤ n),
    i + k = j →
      (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
        (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x
i j : ℕ
hij : i ≤ j
hj : j ≤ n
hik : i + (k + 1) = j
α : StructuredArrow (op ⦋n⦌) (inclusion 2).op :=
  strArrowMk₂ (mkOfLeComp ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯ ⋯) fac_aux₂._proof_1_10
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i + k, ⋯⟩ ⟨j, ⋯⟩ ⋯) lift._proof_3
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) lift._proof_3
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨i + k, ⋯⟩ ⋯) lift._proof_3
β₀ : α ⟶ α₀ := homMk (Hom.tr (mkOfSucc 1) ⋯ ⋯).op ⋯
β₁ : α ⟶ α₁ := homMk (Hom.tr (SimplexCategory.δ 1) ⋯ ⋯).op ⋯
β₂ : α ⟶ α₂ := homMk (Hom.tr (mkOfSucc 0) ⋯ ⋯).op ⋯
h₀ : (ConcreteCategory.hom (X.map α₀.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₀)) x
h₂ : (ConcreteCategory.hom (X.map α₂.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α₂)) x
⊢ (ConcreteCategory.hom (X.map α.hom)) (lift sx s x) = (ConcreteCategory.hom (s.π.app α)) x

Tactic:
by

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

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
σ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 1)), W (σ d i ⋯ ⋯)
⊢ W = ⊤

Tactic:
by

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

Goal state before:
pp: X Y Z : Truncated 2
xyz : X.HomotopyCategory × Y.HomotopyCategory × Z.HomotopyCategory
⊢ (associativity'Iso X Y Z).hom.app xyz =
    𝟙
      (((prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).inverse ⋙
            (inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙ inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom).obj
        xyz)

Tactic:
by

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

Goal state before:
pp: W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
⊢ a.len ≤ max a.len b.len

Tactic:
by

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

Goal state before:
pp: W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
hW : ∀ (d : ℕ), W.inverseImage (Truncated.inclusion d) = ⊤
a b : SimplexCategory
f : a ⟶ b
⊢ b.len ≤ max a.len b.len

Tactic:
by

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

Goal state before:
pp: W : MorphismProperty SimplexCategory
inst✝ : W.IsMultiplicative
δ_mem : ∀ {n : ℕ} (i : Fin (n + 2)), W (δ i)
σ_mem : ∀ {n : ℕ} (i : Fin (n + 1)), W (σ i)
⊢ W = ⊤

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ : SemiSimplexCategory
a₁✝ a₂✝ : X✝ ⟶ Y✝
h : toSimplexCategory.map a₁✝ = toSimplexCategory.map a₂✝
⊢ a₁✝ = a₂✝

Tactic:
by

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

Goal state before:
pp: n m : SemiSimplexCategory
f : n ⟶ m
⊢ Mono (toSimplexCategory.map f)

Tactic:
by

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

Goal state before:
pp: n m : SemiSimplexCategory
f : n ⟶ m
Z✝ : SemiSimplexCategory
g₁ g₂ : Z✝ ⟶ n
h : g₁ ≫ f = g₂ ≫ f
⊢ g₁ = g₂

Tactic:
by

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

Goal state before:
pp: n m : SemiSimplexCategory
f : toSimplexCategory.obj n ⟶ toSimplexCategory.obj m
inst✝ : Mono f
⊢ Function.Injective ⇑(SimplexCategory.Hom.toOrderHom f)

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j₁ j₂ : Fin (⦋n⦌.len + 1)
h : j₁ ≤ j₂
⊢ (fun j ↦ if j.castSucc < i then 0 else 1) j₁ ≤ (fun j ↦ if j.castSucc < i then 0 else 1) j₂

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
⊢ (ConcreteCategory.hom (toMk₁ i)) j = 0 ↔ j.castSucc < i

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
⊢ (ConcreteCategory.hom (toMk₁ i)) j = 0

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
⊢ (ConcreteCategory.hom (toMk₁ i)) j = 1 ↔ i ≤ j.castSucc

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
⊢ (ConcreteCategory.hom (toMk₁ i)) j = 1

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: X Y Z : Truncated 2
xyz : (X.HomotopyCategory × Y.HomotopyCategory) × Z.HomotopyCategory
⊢ (associativityIso X Y Z).hom.app xyz =
    𝟙 (((inverse X Y).prod (𝟭 Z.HomotopyCategory) ⋙ inverse (X ⊗ Y) Z ⋙ mapHomotopyCategory (α_ X Y Z).hom).obj xyz)

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ : Truncated 2
x✝¹ : X✝ ⟶ Y✝
x✝ : Truncated 2
⊢ hoFunctor₂.map x✝¹ ▷ hoFunctor₂.obj x✝ ≫ (iso Y✝ x✝).symm.hom = (iso X✝ x✝).symm.hom ≫ hoFunctor₂.map (x✝¹ ▷ x✝)

Tactic:
by

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

Goal state before:
pp: X✝ Y✝ x✝¹ : Truncated 2
x✝ : X✝ ⟶ Y✝
⊢ hoFunctor₂.obj x✝¹ ◁ hoFunctor₂.map x✝ ≫ (iso x✝¹ Y✝).symm.hom = (iso x✝¹ X✝).symm.hom ≫ hoFunctor₂.map (x✝¹ ◁ x✝)

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : i ≤ k
⊢ i.castSucc ≤ k.castSucc

Tactic:
by

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

Goal state before:
pp: x✝² x✝¹ x✝ : Truncated 2
⊢ (iso x✝² x✝¹).symm.hom ▷ hoFunctor₂.obj x✝ ≫ (iso (x✝² ⊗ x✝¹) x✝).symm.hom ≫ hoFunctor₂.map (α_ x✝² x✝¹ x✝).hom =
    (α_ (hoFunctor₂.obj x✝²) (hoFunctor₂.obj x✝¹) (hoFunctor₂.obj x✝)).hom ≫
      hoFunctor₂.obj x✝² ◁ (iso x✝¹ x✝).symm.hom ≫ (iso x✝² (x✝¹ ⊗ x✝)).symm.hom

Tactic:
by

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

Goal state before:
pp: Y : Truncated 2
⊢ (λ_ (hoFunctor₂.obj Y)).hom =
    (HomotopyCategory.isoTerminal (𝟙_ (Truncated 2))).symm.hom ▷ hoFunctor₂.obj Y ≫
      (iso (𝟙_ (Truncated 2)) Y).symm.hom ≫ hoFunctor₂.map (λ_ Y).hom

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
⊢ σ j ≫ toMk₁ i = toMk₁ i.castSucc

Tactic:
by

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

Goal state before:
pp: X : Truncated 2
⊢ (ρ_ (hoFunctor₂.obj X)).hom =
    hoFunctor₂.obj X ◁ (HomotopyCategory.isoTerminal (𝟙_ (Truncated 2))).symm.hom ≫
      (iso X (𝟙_ (Truncated 2))).symm.hom ≫ hoFunctor₂.map (ρ_ X).hom

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
⊢ k.castSucc < i.succ

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LE α
⊢ (IsRelUpperSet s fun x ↦ True) ↔ IsUpperSet s

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
s : Set α
inst✝ : LE α
⊢ (IsRelLowerSet s fun x ↦ True) ↔ IsLowerSet s

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
s t : Set α
P : α → Prop
inst✝ : LE α
hs : IsRelUpperSet s P
ht : IsRelUpperSet t P
b : α
mb : b ∈ s ∪ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∪ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
s t : Set α
P : α → Prop
inst✝ : LE α
hs : IsRelLowerSet s P
ht : IsRelLowerSet t P
b : α
mb : b ∈ s ∪ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∪ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
s t : Set α
P : α → Prop
inst✝ : LE α
hs : IsRelUpperSet s P
ht : IsRelUpperSet t P
b : α
x✝ : b ∈ s ∩ t
bs : b ∈ s
bt : b ∈ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ s ∩ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
s t : Set α
P : α → Prop
inst✝ : LE α
hs : IsRelLowerSet s P
ht : IsRelLowerSet t P
b : α
x✝ : b ∈ s ∩ t
bs : b ∈ s
bt : b ∈ t
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ s ∩ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
S : Set (Set α)
hS : S.Nonempty
hf : ∀ (s : Set α), s ∈ S → IsRelUpperSet s P
b : α
mb : b ∈ ⋂₀ S
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b ≤ b_1 → P b_1 → b_1 ∈ ⋂₀ S

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
S : Set (Set α)
hS : S.Nonempty
hf : ∀ (s : Set α), s ∈ S → IsRelLowerSet s P
b : α
mb : b ∈ ⋂₀ S
⊢ P b ∧ ∀ ⦃b_1 : α⦄, b_1 ≤ b → P b_1 → b_1 ∈ ⋂₀ S

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsUpperSet s
a : { x // P x }
ma : a ∈ s
b : α
x : ↑a ≤ b
y : P b
⊢ b ∈ Subtype.val '' s

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsRelUpperSet (Subtype.val '' s) P
a b : { x // P x }
x : a ≤ b
y : a ∈ s
⊢ ↑a ∈ Subtype.val '' s

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
⊢ IsUpperSet s ↔ IsRelUpperSet (Subtype.val '' s) P

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsLowerSet s
a : { x // P x }
ma : a ∈ s
b : α
x : b ≤ ↑a
y : P b
⊢ b ∈ Subtype.val '' s

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : k ≤ i
hk' : k ≤ j.castSucc
⊢ (k.castPred ⋯).castSucc ≤ j.castSucc

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
h : IsRelLowerSet (Subtype.val '' s) P
a b : { x // P x }
x : b ≤ a
y : a ∈ s
⊢ ↑a ∈ Subtype.val '' s

Tactic:
by

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

Goal state before:
pp: n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
⊢ σ j ≫ toMk₁ i = toMk₁ i.succ

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
P : α → Prop
inst✝ : LE α
s : Set { x // P x }
⊢ IsLowerSet s ↔ IsRelLowerSet (Subtype.val '' s) P

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s✝ t✝ : Set α
a b : α
P : α → Prop
inst✝ : LE α
s t : RelUpperSet P
h : s.carrier = t.carrier
⊢ s = t

Tactic:
by

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : toMk₁ i = toMk₁ j
hij : i < j
⊢ ↑j ≤ ⦋n⦌.len + 1

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Function.Injective toMk₁

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s✝ t✝ : Set α
a b : α
P : α → Prop
inst✝ : LE α
s t : RelLowerSet P
h : s.carrier = t.carrier
⊢ s = t

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
c x✝ : α
b : x✝ ∈ Icc a c
⊢ (fun x ↦ x ≤ c) x✝ ∧ ∀ ⦃b : α⦄, x✝ ≤ b → (fun x ↦ x ≤ c) b → b ∈ Icc a c

Tactic:
by

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

Goal state before:
pp: n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : S.Nonempty
i : Fin (⦋n⦌.len + 1)
h : i.castSucc < (S.min' hS).castSucc
hi : i ∈ S
⊢ False

Tactic:
by

Goal state after:
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: α : Type u_1
a : α
inst✝ : Preorder α
c x✝ : α
b : x✝ ∈ Icc c a
⊢ (fun x ↦ c ≤ x) x✝ ∧ ∀ ⦃b : α⦄, b ≤ x✝ → (fun x ↦ c ≤ x) b → b ∈ Icc c a

Tactic:
by

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

Goal state before:
pp: n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
⊢ i.castSucc < Fin.last (n + 1)

Tactic:
by

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

Goal state before:
pp: n : ℕ
f : ⦋n⦌ ⟶ ⦋1⦌
S : Finset (Fin (n + 1)) := {i | (ConcreteCategory.hom f) i = 1}
hS : ¬S.Nonempty
i : Fin (⦋n⦌.len + 1)
hj : (ConcreteCategory.hom f) i = (fun i ↦ i) ⟨1, ⋯⟩
⊢ i ∈ S

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ Function.Surjective toMk₁

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
K x✝¹ : PreAbstractSimplicialComplex ι
x✝ : (fun K ↦ K.faces) K = (fun K ↦ K.faces) x✝¹
⊢ K = x✝¹

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Set (PreAbstractSimplicialComplex ι)
x✝¹ : Finset ι
x✝ : x✝¹ ∈ (⋂ K ∈ s, K.faces) ∩ {t | t.Nonempty}
hx : x✝¹ ∈ ⋂ K ∈ s, K.faces
hn : x✝¹ ∈ {t | t.Nonempty}
⊢ x✝¹.Nonempty ∧ ∀ ⦃b : Finset ι⦄, b ⊆ x✝¹ → b.Nonempty → b ∈ (⋂ K ∈ s, K.faces) ∩ {t | t.Nonempty}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
α : Type u_2
β : Type u_3
inst✝ : DecidableEq β
K : PreAbstractSimplicialComplex α
f : α → β
x : Finset β
h : x ∈ (fun s ↦ Finset.image f s) '' K.faces
⊢ x.Nonempty ∧ ∀ ⦃b : Finset β⦄, b ⊆ x → b.Nonempty → b ∈ (fun s ↦ Finset.image f s) '' K.faces

Tactic:
by

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i j : ℕ
hij : i ≤ j
hj : j ≤ n
⊢ (ConcreteCategory.hom (X.map (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij).op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ (mkOfLe ⟨i, ⋯⟩ ⟨j, ⋯⟩ hij) fac_aux₁._proof_1))) x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty ∧ ∀ ⦃b : Finset ι⦄, b ⊆ x → b.Nonempty → b ∈ {s | ∃ v, s = {v}}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
x✝² x✝¹ : AbstractSimplicialComplex ι
x✝ : (fun K ↦ K.faces) x✝² = (fun K ↦ K.faces) x✝¹
⊢ x✝² = x✝¹

Tactic:
by

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
φ : ⦋1⦌ ⟶ ⦋n⦌
⊢ 0 ≤ 1

Tactic:
by

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i j : Fin (n + 1)
hij : i ≤ j
⊢ ↑j ≤ n

Tactic:
by

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
φ : ⦋1⦌ ⟶ ⦋n⦌
⊢ (ConcreteCategory.hom (X.map φ.op)) (lift sx s x) =
    (ConcreteCategory.hom (s.π.app (strArrowMk₂ φ fac_aux₁._proof_1))) x

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty ∧ ∀ ⦃b : Finset ι⦄, b ⊆ x → b.Nonempty → b ∈ {t | ∃ v, t = {v}}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x✝¹ : Finset ι
x✝ : x✝¹ ∈ (⋂ K ∈ s, K.faces) ∩ {t | t.Nonempty}
hx : x✝¹ ∈ ⋂ K ∈ s, K.faces
hn : x✝¹ ∈ {t | t.Nonempty}
⊢ x✝¹.Nonempty ∧ ∀ ⦃b : Finset ι⦄, b ⊆ x✝¹ → b.Nonempty → b ∈ (⋂ K ∈ s, K.faces) ∩ {t | t.Nonempty}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
v : ι
⊢ {v} ∈ (⋂ K ∈ s, K.faces) ∩ {t | t.Nonempty}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ x.Nonempty ∧ ∀ ⦃b : Finset ι⦄, b ⊆ x → b.Nonempty → b ∈ {s | ∃ v, s = {v}}

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
x✝ : Set (AbstractSimplicialComplex ι)
⊢ IsLUB x✝ (sSup x✝)

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
K : AbstractSimplicialComplex ι
x✝ : Finset ι
ht : x✝ ∈ (fun K ↦ K.faces) ⊥
⊢ x✝ ∈ (fun K ↦ K.faces) K

Tactic:
by

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin (i + 1)
⊢ Fin (⦋i⦌.len + 1)

Tactic:
by

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin (i + 1)
⊢ (strArrowMk₂ f hi).hom ≫ (inclusion 2).op.map (Hom.tr (⦋0⦌.const ⦋i⦌ k) ⋯ hi).op =
    (strArrowMk₂ (⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom f) k))
        SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_1).hom

Tactic:
by

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
x : s.pt
i : ℕ
hi : i ≤ 2
f : unop ((inclusion 2).op.obj (op { obj := ⦋i⦌, property := hi })) ⟶ unop (op ⦋n⦌)
k : Fin i
⊢ (strArrowMk₂ f (SSet.StrictSegal.isPointwiseRightKanExtensionAt._proof_1 i hi)).hom ≫
      (inclusion 2).op.map (Hom.tr (mkOfSucc k) ⋯ hi).op =
    (strArrowMk₂ (mkOfSucc k ≫ f) SSet.StrictSegal.isPointwiseRightKanExtensionAt.lift._proof_3).hom

Tactic:
by

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
j : StructuredArrow (op ⦋n⦌) (inclusion 2).op
⊢ (↾fun x ↦ lift sx s x) ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y : SimplexCategory
h : WithInitial.of x = WithInitial.of y
⊢ x.len = y.len

Tactic:
by

Goal state after:
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

Goal state before:
pp: x y : SimplexCategory
h : WithInitial.of x = WithInitial.of y
⊢ x = y

Tactic:
by

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
m : s.pt ⟶ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).pt
hm :
  ∀ (j : StructuredArrow (op ⦋n⦌) (inclusion 2).op),
    m ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j
⊢ m = ↾fun x ↦ lift sx s x

Tactic:
ext x
    apply sx.spineInjective (X := X)
    -- simp? [spineEquiv] says:
    simp only [spineEquiv, RightExtension.coneAt_pt, rightExtensionInclusion_left,
      TypeCat.Fun.toFun_apply, Equiv.coe_fn_mk, lift, Nat.reduceAdd, ObjectProperty.ι_obj,
      const_obj_obj, comp_obj, proj_obj, mk_right, op_obj, TypeCat.hom_ofHom, TypeCat.Fun.coe_mk,
      spine_spineToSimplex_apply]
    ext i
    · exact ConcreteCategory.congr_hom (hm (StructuredArrow.mk
        (Y := op ⦋0⦌2) (⦋0⦌.const ⦋n⦌ i).op)) x
    · exact ConcreteCategory.congr_hom (hm (.mk (Y := op ⦋1⦌2)
        (.op (mkOfLe _ _ (Fin.castSucc_le_succ i))))) x

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

Goal state before:
pp: X : SSet
sx : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (inclusion 2).op ⋙ (inclusion 2).op ⋙ X)
m : s.pt ⟶ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).pt
hm :
  ∀ (j : StructuredArrow (op ⦋n⦌) (inclusion 2).op),
    m ≫ ((rightExtensionInclusion X 2).coneAt (op ⦋n⦌)).π.app j = s.π.app j
⊢ m = ↾fun x ↦ lift sx s x

Tactic:
by

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

Goal state before:
pp: X : Cat
⊢ (nerveFunctor₂.obj X).IsStrictSegal

Tactic:
by

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

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
i : Fin (n + 2)
⊢ i ∈ finset f x ↔ i = Fin.last (n + 1) ∨ ∃ (h : i ≠ Fin.last (n + 1)), x ≤ (f (i.castPred h)).castSucc

Tactic:
by

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

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ Fin.last (n + 1) ∈ finset f x

Tactic:
by

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

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
i : Fin (n + 1)
⊢ i.castSucc ∈ finset f x ↔ x ≤ (f i).castSucc

Tactic:
by

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

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
h : ∀ b ∈ finset f x, b = Fin.last (n + 1)
i : Fin (n + 1)
this : x ≤ (f i).castSucc
⊢ i.castSucc ∈ finset f x

Tactic:
by

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

Goal state before:
pp: n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x : Fin (m + 2)
⊢ map' f x = Fin.last (n + 1) ↔ ∀ (i : Fin (n + 1)), (f i).castSucc < x

Tactic:
by

Goal state after: