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 := ⋯
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).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✝
t : Fin (1 + 1)
x : Fin ((unop (op ⦋1⦌)).len + 1)
⊢ ↑((Hom.toOrderHom (α.hom ≫ (mkOfSucc 1).op).unop) x) = ↑((Hom.toOrderHom α₀.hom.unop) x)

Tactic:
;

Goal state after:
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 := ⋯
α₀ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₁ : StructuredArrow (op ⦋n⦌) (inclusion 2).op := ⋯
α₂ : StructuredArrow (op ⦋n⦌) (inclusion 2).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✝
t : Fin (1 + 1)
x : Fin ((unop (op ⦋1⦌)).len + 1)
⊢ ↑((Hom.toOrderHom (α.hom ≫ (mkOfSucc 1).op).unop) x) = ↑((Hom.toOrderHom α₀.hom.unop) x)
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
⊢ ({ toFunctor := functor X Y } ≫ { toFunctor := inverse X Y }).toFunctor =
    (𝟙 (Cat.of (X ⊗ Y).HomotopyCategory)).toFunctor

Tactic:
;

Goal state after:
X X' Y Y' Z : Truncated 2
⊢ ({ toFunctor := functor X Y } ≫ { toFunctor := inverse X Y }).toFunctor =
    (𝟙 (Cat.of (X ⊗ Y).HomotopyCategory)).toFunctor
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

Goal state before:
pp: X X' Y Y' Z : Truncated 2
⊢ ({ toFunctor := inverse X Y } ≫ { toFunctor := functor X Y }).toFunctor =
    (𝟙 (Cat.of (X.HomotopyCategory × Y.HomotopyCategory))).toFunctor

Tactic:
;

Goal state after:
X X' Y Y' Z : Truncated 2
⊢ ({ toFunctor := inverse X Y } ≫ { toFunctor := functor X Y }).toFunctor =
    (𝟙 (Cat.of (X.HomotopyCategory × Y.HomotopyCategory))).toFunctor
Module: Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.NormalForms

Goal state before:
pp: m✝ : ℕ
L✝ : List ℕ
x y : SimplexCategoryGenRel
f : x ⟶ y
hf : P_σ f
L : List ℕ
m b : ℕ
h₁ : mk m = y
h₂ : x = mk (m + b)
h : L.length = b
⊢ (mk m).1 + b = (mk (m + b)).1

Tactic:
;

Goal state after:
m✝ : ℕ
L✝ : List ℕ
x y : SimplexCategoryGenRel
f : x ⟶ y
hf : P_σ f
L : List ℕ
m b : ℕ
h₁ : mk m = y
h₂ : x = mk (m + b)
h : L.length = b
⊢ (mk m).1 + b = (mk (m + b)).1
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
n : ℕ
hn : n < d
i : Fin (n + 2)
⊢ n ≤ d

Tactic:
;

Goal state after:
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
n : ℕ
hn : n < d
i : Fin (n + 2)
⊢ n ≤ d
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
n : ℕ
hn : n < d
i : Fin (n + 2)
⊢ n + 1 ≤ d

Tactic:
;

Goal state after:
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
n : ℕ
hn : n < d
i : Fin (n + 2)
⊢ n + 1 ≤ d
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 ⋯ ⋯)
n : ℕ
hn : n < d
i : Fin (n + 1)
⊢ n + 1 ≤ d

Tactic:
;

Goal state after:
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
n : ℕ
hn : n < d
i : Fin (n + 1)
⊢ n + 1 ≤ d
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 ⋯ ⋯)
n : ℕ
hn : n < d
i : Fin (n + 1)
⊢ n ≤ d

Tactic:
;

Goal state after:
d : ℕ
W : MorphismProperty (Truncated d)
inst✝ : W.IsMultiplicative
δ_mem : ∀ (n : ℕ) (hn : n < d) (i : Fin (n + 2)), W (δ d i ⋯ ⋯)
n : ℕ
hn : n < d
i : Fin (n + 1)
⊢ n ≤ d
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: case pos
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 ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
⊢ W f

pp: case neg
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 ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : ¬Function.Surjective ⇑(Hom.toOrderHom f.hom)
⊢ W f

Tactic:
;

Goal state after:
case pos
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 ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
⊢ W f

case neg
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 ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : ¬Function.Surjective ⇑(Hom.toOrderHom f.hom)
⊢ W f
Module: Mathlib.AlgebraicTopology.SimplexCategory.MorphismProperty

Goal state before:
pp: case pos
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 ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f

pp: case neg
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 ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : ¬Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f

Tactic:
;

Goal state after:
case pos
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 ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f

case neg
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 ⋯ ⋯)
c : ℕ
hc :
  ∀ (a : ℕ) (ha : a ≤ d) (b : ℕ) (hb : b ≤ d)
    (f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }), a + b = c → W f
a : ℕ
ha : a ≤ d
b : ℕ
hb : b ≤ d
f : { obj := { len := a }, property := ha } ⟶ { obj := { len := b }, property := hb }
h : a + b = c + 1
h₁ : Function.Surjective ⇑(Hom.toOrderHom f.hom)
h₂ : ¬Function.Injective ⇑(Hom.toOrderHom f.hom)
⊢ W f
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : k < i
⊢ (ConcreteCategory.hom (toMk₁ i)) (j.predAbove k) = (ConcreteCategory.hom (toMk₁ i.castSucc)) k

Tactic:
;

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hk : k < i
⊢ (ConcreteCategory.hom (toMk₁ i)) (j.predAbove k) = (ConcreteCategory.hom (toMk₁ i.castSucc)) k
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).toFunctor =
    ((iso X✝ x✝).symm.hom ≫ hoFunctor₂.map (x✝¹ ▷ x✝)).toFunctor

Tactic:
;

Goal state after:
X✝ Y✝ : Truncated 2
x✝¹ : X✝ ⟶ Y✝
x✝ : Truncated 2
⊢ (hoFunctor₂.map x✝¹ ▷ hoFunctor₂.obj x✝ ≫ (iso Y✝ x✝).symm.hom).toFunctor =
    ((iso X✝ x✝).symm.hom ≫ hoFunctor₂.map (x✝¹ ▷ x✝)).toFunctor
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).toFunctor =
    ((iso x✝¹ X✝).symm.hom ≫ hoFunctor₂.map (x✝¹ ◁ x✝)).toFunctor

Tactic:
;

Goal state after:
X✝ Y✝ x✝¹ : Truncated 2
x✝ : X✝ ⟶ Y✝
⊢ (hoFunctor₂.obj x✝¹ ◁ hoFunctor₂.map x✝ ≫ (iso x✝¹ Y✝).symm.hom).toFunctor =
    ((iso x✝¹ X✝).symm.hom ≫ hoFunctor₂.map (x✝¹ ◁ x✝)).toFunctor
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).toFunctor =
    ((α_ (hoFunctor₂.obj x✝²) (hoFunctor₂.obj x✝¹) (hoFunctor₂.obj x✝)).hom ≫
        hoFunctor₂.obj x✝² ◁ (iso x✝¹ x✝).symm.hom ≫ (iso x✝² (x✝¹ ⊗ x✝)).symm.hom).toFunctor

Tactic:
;

Goal state after:
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).toFunctor =
    ((α_ (hoFunctor₂.obj x✝²) (hoFunctor₂.obj x✝¹) (hoFunctor₂.obj x✝)).hom ≫
        hoFunctor₂.obj x✝² ◁ (iso x✝¹ x✝).symm.hom ≫ (iso x✝² (x✝¹ ⊗ x✝)).symm.hom).toFunctor
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

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

Tactic:
;

Goal state after:
Y : Truncated 2
⊢ (λ_ (hoFunctor₂.obj Y)).hom.toFunctor =
    ((HomotopyCategory.isoTerminal (𝟙_ (Truncated 2))).symm.hom ▷ hoFunctor₂.obj Y ≫
        (iso (𝟙_ (Truncated 2)) Y).symm.hom ≫ hoFunctor₂.map (λ_ Y).hom).toFunctor
Module: Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal

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

Tactic:
;

Goal state after:
X : Truncated 2
⊢ (ρ_ (hoFunctor₂.obj X)).hom.toFunctor =
    (hoFunctor₂.obj X ◁ (HomotopyCategory.isoTerminal (𝟙_ (Truncated 2))).symm.hom ≫
        (iso X (𝟙_ (Truncated 2))).symm.hom ≫ hoFunctor₂.map (ρ_ X).hom).toFunctor
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : i < k
⊢ (ConcreteCategory.hom (toMk₁ i)) (j.predAbove k) = (ConcreteCategory.hom (toMk₁ i.succ)) k

Tactic:
;

Goal state after:
case pos
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
h : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hk : i < k
⊢ (ConcreteCategory.hom (toMk₁ i)) (j.predAbove k) = (ConcreteCategory.hom (toMk₁ i.succ)) k
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case mk
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t✝ : Set α
a b : α
P : α → Prop
inst✝ : LE α
t : RelUpperSet P
carrier✝ : Set α
isRelUpperSet'✝ : IsRelUpperSet carrier✝ P
h : { carrier := carrier✝, isRelUpperSet' := isRelUpperSet'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, isRelUpperSet' := isRelUpperSet'✝ } = t

Tactic:
;

Goal state after:
case mk
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t✝ : Set α
a b : α
P : α → Prop
inst✝ : LE α
t : RelUpperSet P
carrier✝ : Set α
isRelUpperSet'✝ : IsRelUpperSet carrier✝ P
h : { carrier := carrier✝, isRelUpperSet' := isRelUpperSet'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, isRelUpperSet' := isRelUpperSet'✝ } = t
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case mk.mk
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t : Set α
a b : α
P : α → Prop
inst✝ : LE α
carrier✝¹ : Set α
isRelUpperSet'✝¹ : IsRelUpperSet carrier✝¹ P
carrier✝ : Set α
isRelUpperSet'✝ : IsRelUpperSet carrier✝ P
h :
  { carrier := carrier✝¹, isRelUpperSet' := isRelUpperSet'✝¹ }.carrier =
    { carrier := carrier✝, isRelUpperSet' := isRelUpperSet'✝ }.carrier
⊢ { carrier := carrier✝¹, isRelUpperSet' := isRelUpperSet'✝¹ } =
    { carrier := carrier✝, isRelUpperSet' := isRelUpperSet'✝ }

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t : Set α
a b : α
P : α → Prop
inst✝ : LE α
carrier✝¹ : Set α
isRelUpperSet'✝¹ : IsRelUpperSet carrier✝¹ P
carrier✝ : Set α
isRelUpperSet'✝ : IsRelUpperSet carrier✝ P
h :
  { carrier := carrier✝¹, isRelUpperSet' := isRelUpperSet'✝¹ }.carrier =
    { carrier := carrier✝, isRelUpperSet' := isRelUpperSet'✝ }.carrier
⊢ { carrier := carrier✝¹, isRelUpperSet' := isRelUpperSet'✝¹ } =
    { carrier := carrier✝, isRelUpperSet' := isRelUpperSet'✝ }
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 + 1

Tactic:
;

Goal state after:
n : ℕ
i j : Fin (n + 2)
h : toMk₁ i = toMk₁ j
hij : i < j
⊢ ↑j ≤ n + 1
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case mk
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t✝ : Set α
a b : α
P : α → Prop
inst✝ : LE α
t : RelLowerSet P
carrier✝ : Set α
isRelLowerSet'✝ : IsRelLowerSet carrier✝ P
h : { carrier := carrier✝, isRelLowerSet' := isRelLowerSet'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, isRelLowerSet' := isRelLowerSet'✝ } = t

Tactic:
;

Goal state after:
case mk
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t✝ : Set α
a b : α
P : α → Prop
inst✝ : LE α
t : RelLowerSet P
carrier✝ : Set α
isRelLowerSet'✝ : IsRelLowerSet carrier✝ P
h : { carrier := carrier✝, isRelLowerSet' := isRelLowerSet'✝ }.carrier = t.carrier
⊢ { carrier := carrier✝, isRelLowerSet' := isRelLowerSet'✝ } = t
Module: Mathlib.Order.UpperLower.Relative

Goal state before:
pp: case mk.mk
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t : Set α
a b : α
P : α → Prop
inst✝ : LE α
carrier✝¹ : Set α
isRelLowerSet'✝¹ : IsRelLowerSet carrier✝¹ P
carrier✝ : Set α
isRelLowerSet'✝ : IsRelLowerSet carrier✝ P
h :
  { carrier := carrier✝¹, isRelLowerSet' := isRelLowerSet'✝¹ }.carrier =
    { carrier := carrier✝, isRelLowerSet' := isRelLowerSet'✝ }.carrier
⊢ { carrier := carrier✝¹, isRelLowerSet' := isRelLowerSet'✝¹ } =
    { carrier := carrier✝, isRelLowerSet' := isRelLowerSet'✝ }

Tactic:
;

Goal state after:
case mk.mk
α : Type u_1
ι : Sort u_2
κ : ι → Sort u_3
s t : Set α
a b : α
P : α → Prop
inst✝ : LE α
carrier✝¹ : Set α
isRelLowerSet'✝¹ : IsRelLowerSet carrier✝¹ P
carrier✝ : Set α
isRelLowerSet'✝ : IsRelLowerSet carrier✝ P
h :
  { carrier := carrier✝¹, isRelLowerSet' := isRelLowerSet'✝¹ }.carrier =
    { carrier := carrier✝, isRelLowerSet' := isRelLowerSet'✝ }.carrier
⊢ { carrier := carrier✝¹, isRelLowerSet' := isRelLowerSet'✝¹ } =
    { carrier := carrier✝, isRelLowerSet' := isRelLowerSet'✝ }
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
this : S.min' ⋯ ≤ i
⊢ False

Tactic:
;

Goal state after:
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
this : S.min' ⋯ ≤ i
⊢ False
Module: Mathlib.AlgebraicTopology.SimplexCategory.ToMkOne

Goal state before:
pp: case pos
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 : ¬(ConcreteCategory.hom f) i = 1
⊢ 0 = (ConcreteCategory.hom f) i

Tactic:
;

Goal state after:
case pos
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 : ¬(ConcreteCategory.hom f) i = 1
⊢ 0 = (ConcreteCategory.hom f) i
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case left
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty

Tactic:
;

Goal state after:
case left
ι : Type u_1
K : PreAbstractSimplicialComplex ι
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

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

Tactic:
intro t hts ht
        cases Finset.subset_singleton_iff.mp (hv ▸ hts) with
        | inl h => exact (ht.ne_empty h).elim
        | inr h => exact ⟨v, h⟩

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
    ext
    grind

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

Goal state before:
pp: case left
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty

Tactic:
;

Goal state after:
case left
ι : Type u_1
s : Set (AbstractSimplicialComplex ι)
x : Finset ι
x✝ : x ∈ {t | ∃ v, t = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty
Module: Mathlib.AlgebraicTopology.SimplicialComplex.Basic

Goal state before:
pp: case left
ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty

Tactic:
;

Goal state after:
case left
ι : Type u_1
x : Finset ι
x✝ : x ∈ {s | ∃ v, s = {v}}
v : ι
hv : x = {v}
⊢ {v}.Nonempty
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)
⊢ f.op ≫ (⦋0⦌.const ⦋i⦌ k).op = (⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom f) k)).op

Tactic:
;

Goal state after:
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)
⊢ f.op ≫ (⦋0⦌.const ⦋i⦌ k).op = (⦋0⦌.const ⦋n⦌ ((Hom.toOrderHom f) k)).op
Module: Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal

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

Tactic:
;

Goal state after:
x y : SimplexCategory
h : x = y
⊢ x.len = y.len
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
X✝ Y✝ : SimplicialThickening J
f : X✝ ⟶ Y✝
t✝ : J
⊢ t✝ ∈ (𝟙 X✝ ≫ f).I ↔ t✝ ∈ f.I

Tactic:
;

Goal state after:
J : Type u_1
inst✝ : LinearOrder J
X✝ Y✝ : SimplicialThickening J
f : X✝ ⟶ Y✝
t✝ : J
⊢ t✝ ∈ (𝟙 X✝ ≫ f).I ↔ t✝ ∈ f.I
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
X✝ Y✝ : SimplicialThickening J
f : X✝ ⟶ Y✝
t✝ : J
⊢ t✝ ∈ (f ≫ 𝟙 Y✝).I ↔ t✝ ∈ f.I

Tactic:
;

Goal state after:
J : Type u_1
inst✝ : LinearOrder J
X✝ Y✝ : SimplicialThickening J
f : X✝ ⟶ Y✝
t✝ : J
⊢ t✝ ∈ (f ≫ 𝟙 Y✝).I ↔ t✝ ∈ f.I
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
x✝³ : SimplicialThickening J
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (↾fun x ↦ (Functor.const (Fin ((Opposite.unop x✝¹).len + 1))).obj (𝟙 x✝³)) =
    (↾fun x ↦ (Functor.const (Fin ((Opposite.unop x✝²).len + 1))).obj (𝟙 x✝³)) ≫ (nerve (x✝³ ⟶ x✝³)).map x✝

Tactic:
;

Goal state after:
J : Type u_1
inst✝ : LinearOrder J
x✝³ : SimplicialThickening J
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (↾fun x ↦ (Functor.const (Fin ((Opposite.unop x✝¹).len + 1))).obj (𝟙 x✝³)) =
    (↾fun x ↦ (Functor.const (Fin ((Opposite.unop x✝²).len + 1))).obj (𝟙 x✝³)) ≫ (nerve (x✝³ ⟶ x✝³)).map x✝
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (((nerve (i ⟶ j)).map x✝ ⊗ₘ (nerve (j ⟶ k)).map x✝) ≫ ↾fun x ↦ Functor.prod' x.1 x.2 ⋙ i.compFunctor j k) =
    (↾fun x ↦ Functor.prod' x.1 x.2 ⋙ i.compFunctor j k) ≫ (nerve (i ⟶ k)).map x✝

Tactic:
;

Goal state after:
J : Type u_1
inst✝ : LinearOrder J
i j k : SimplicialThickening J
x✝² x✝¹ : SimplexCategoryᵒᵖ
x✝ : x✝² ⟶ x✝¹
⊢ (((nerve (i ⟶ j)).map x✝ ⊗ₘ (nerve (j ⟶ k)).map x✝) ≫ ↾fun x ↦ Functor.prod' x.1 x.2 ⋙ i.compFunctor j k) =
    (↾fun x ↦ Functor.prod' x.1 x.2 ⋙ i.compFunctor j k) ≫ (nerve (i ⟶ k)).map x✝
Module: Mathlib.AlgebraicTopology.SimplicialNerve

Goal state before:
pp: J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
k : J
hk : k ∈ I.I
⊢ { as := f i.as }.as ≤ f k

Tactic:
;

Goal state after:
J K : Type u
inst✝¹ : LinearOrder J
inst✝ : LinearOrder K
f : J →o K
i j : SimplicialThickening J
I : i ⟶ j
k : J
hk : k ∈ I.I
⊢ { as := f i.as }.as ≤ f k