mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: case inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
h : Even n
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) n

pp: case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
h : Odd n
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) n

Tactic:
·

Goal state after:
case inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
h : Even n
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) n
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: case inl.zero
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
h : Even 0
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) 0

pp: case inl.succ
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
h : Even (n + 1)
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) (n + 1)

Tactic:
·

Goal state after:
case inl.zero
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
h : Even 0
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) 0
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: case inl.succ
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
h : Even (n + 1)
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) (n + 1)

Tactic:
·

Goal state after:
case inl.succ
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
h : Even (n + 1)
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) (n + 1)
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
h : Odd n
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) n

Tactic:
·

Goal state after:
case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
h : Odd n
⊢ HomologicalComplex.HasHomology (alternatingConst.obj X) n
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: case inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : n ≠ 0
h : Even n
⊢ HomologicalComplex.ExactAt (alternatingConst.obj X) n

pp: case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : n ≠ 0
h : Odd n
⊢ HomologicalComplex.ExactAt (alternatingConst.obj X) n

Tactic:
·

Goal state after:
case inl
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : n ≠ 0
h : Even n
⊢ HomologicalComplex.ExactAt (alternatingConst.obj X) n
Module: Mathlib.Algebra.Homology.AlternatingConst

Goal state before:
pp: case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : n ≠ 0
h : Odd n
⊢ HomologicalComplex.ExactAt (alternatingConst.obj X) n

Tactic:
·

Goal state after:
case inr
C : Type u_1
inst✝² : Category.{v_1, u_1} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasZeroObject C
X : C
n : ℕ
hn : n ≠ 0
h : Odd n
⊢ HomologicalComplex.ExactAt (alternatingConst.obj X) n
Module: Mathlib.CategoryTheory.GradedObject.Bifunctor

Goal state before:
pp: C₁ : Type u_1
C₂ : Type u_2
C₃ : Type u_3
inst✝³ : Category.{v_1, u_1} C₁
inst✝² : Category.{v_2, u_2} C₂
inst✝¹ : Category.{v_3, u_3} C₃
F : C₁ ⥤ C₂ ⥤ C₃
I : Type u_4
J : Type u_5
K : Type u_6
p : I × J → K
X : GradedObject I C₁
Y : GradedObject J C₂
A : C₃
k : K
inst✝ : (((mapBifunctor F I J).obj X).obj Y).HasMap p
f : (i : I) → (j : J) → p (i, j) = k → ((F.obj (X i)).obj (Y j) ⟶ A)
i : I
j : J
hij : p (i, j) = k
⊢ ιMapBifunctorMapObj F p X Y i j k hij ≫ mapBifunctorMapObjDesc f = f i j hij

Tactic:
apply ι_descMapObj

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

Goal state before:
pp: case a
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
⊢ face S ≤ Subcomplex.ofSimplex (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom))

pp: case a
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
⊢ Subcomplex.ofSimplex (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom)) ≤ face S

Tactic:
·

Goal state after:
case a
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
⊢ face S ≤ Subcomplex.ofSimplex (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom))
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
⊢ f ≫ C.d 0 (0 + 1) = 0

pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
n✝ : ℕ
⊢ f ≫ C.d 0 (n✝ + 1 + 1) = 0

Tactic:
·

Goal state after:
case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
⊢ f ≫ C.d 0 (0 + 1) = 0
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
n✝ : ℕ
⊢ f ≫ C.d 0 (n✝ + 1 + 1) = 0

Tactic:
·

Goal state after:
case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : CochainComplex V ℕ
X : V
f : X ⟶ C.X 0
w : f ≫ C.d 0 1 = 0
i j k : ℕ
hij : (ComplexShape.up ℕ).Rel i j
hjk : (ComplexShape.up ℕ).Rel j k
n✝ : ℕ
⊢ f ≫ C.d 0 (n✝ + 1 + 1) = 0
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case a
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
⊢ Subcomplex.ofSimplex (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom)) ≤ face S

Tactic:
·

Goal state after:
case a
n : ℕ
S : Finset (Fin (n + 1))
m : ℕ
e : Fin (m + 1) ≃o ↥S
⊢ Subcomplex.ofSimplex (objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom)) ≤ face S
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case inl
n d : ℕ
s : Δ[n] _⦋d⦌
h : Function.Injective ⇑(Hom.toOrderHom (objEquiv s))
i : Fin d
h' : (fun j ↦ s j) i.castSucc < (fun j ↦ s j) i.succ
⊢ s i.castSucc < s i.succ

pp: case inr
n d : ℕ
s : Δ[n] _⦋d⦌
h : Function.Injective ⇑(Hom.toOrderHom (objEquiv s))
i : Fin d
h' : (fun j ↦ s j) i.castSucc = (fun j ↦ s j) i.succ
⊢ s i.castSucc < s i.succ

Tactic:
·

Goal state after:
case inl
n d : ℕ
s : Δ[n] _⦋d⦌
h : Function.Injective ⇑(Hom.toOrderHom (objEquiv s))
i : Fin d
h' : (fun j ↦ s j) i.castSucc < (fun j ↦ s j) i.succ
⊢ s i.castSucc < s i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case inr
n d : ℕ
s : Δ[n] _⦋d⦌
h : Function.Injective ⇑(Hom.toOrderHom (objEquiv s))
i : Fin d
h' : (fun j ↦ s j) i.castSucc = (fun j ↦ s j) i.succ
⊢ s i.castSucc < s i.succ

Tactic:
·

Goal state after:
case inr
n d : ℕ
s : Δ[n] _⦋d⦌
h : Function.Injective ⇑(Hom.toOrderHom (objEquiv s))
i : Fin d
h' : (fun j ↦ s j) i.castSucc = (fun j ↦ s j) i.succ
⊢ s i.castSucc < s i.succ
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case refine_1
n : ℕ
i j : Fin (n + 2)
h : i < j
k : Fin n
⊢ j.succAbove ((i.castPred ⋯).succAbove k) ∈ {i, j}ᶜ

pp: case refine_2
n : ℕ
i j : Fin (n + 2)
h : i < j
x✝¹ x✝ : Fin n
hk :
  (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) x✝¹ =
    (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) x✝
⊢ x✝¹ = x✝

pp: case refine_3
n : ℕ
i j : Fin (n + 2)
h : i < j
x✝ : ↥{i, j}ᶜ
l : Fin (n + 2)
hl : l ∈ {i, j}ᶜ
⊢ ∃ a, (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) a = ⟨l, hl⟩

Tactic:
·

Goal state after:
case refine_1
n : ℕ
i j : Fin (n + 2)
h : i < j
k : Fin n
⊢ j.succAbove ((i.castPred ⋯).succAbove k) ∈ {i, j}ᶜ
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case refine_2
n : ℕ
i j : Fin (n + 2)
h : i < j
x✝¹ x✝ : Fin n
hk :
  (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) x✝¹ =
    (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) x✝
⊢ x✝¹ = x✝

pp: case refine_3
n : ℕ
i j : Fin (n + 2)
h : i < j
x✝ : ↥{i, j}ᶜ
l : Fin (n + 2)
hl : l ∈ {i, j}ᶜ
⊢ ∃ a, (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) a = ⟨l, hl⟩

Tactic:
·

Goal state after:
case refine_2
n : ℕ
i j : Fin (n + 2)
h : i < j
x✝¹ x✝ : Fin n
hk :
  (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) x✝¹ =
    (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) x✝
⊢ x✝¹ = x✝
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case refine_3
n : ℕ
i j : Fin (n + 2)
h : i < j
x✝ : ↥{i, j}ᶜ
l : Fin (n + 2)
hl : l ∈ {i, j}ᶜ
⊢ ∃ a, (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) a = ⟨l, hl⟩

Tactic:
·

Goal state after:
case refine_3
n : ℕ
i j : Fin (n + 2)
h : i < j
x✝ : ↥{i, j}ᶜ
l : Fin (n + 2)
hl : l ∈ {i, j}ᶜ
⊢ ∃ a, (fun k ↦ ⟨j.succAbove ((i.castPred ⋯).succAbove k), ⋯⟩) a = ⟨l, hl⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case left
n m : ℕ
⊢ Function.Injective fun x ↦
    match x with
    | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩

pp: case right
n m : ℕ
⊢ Function.Surjective fun x ↦
    match x with
    | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩

Tactic:
·

Goal state after:
case left
n m : ℕ
⊢ Function.Injective fun x ↦
    match x with
    | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case right
n m : ℕ
⊢ Function.Surjective fun x ↦
    match x with
    | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩

Tactic:
·

Goal state after:
case right
n m : ℕ
⊢ Function.Surjective fun x ↦
    match x with
    | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case right.refine_1
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
⊢ objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom) ∈ Δ[n].nonDegenerate m

pp: case right.refine_2
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
⊢ (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
      ⟨objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom), ?right.refine_1⟩ =
    ⟨S, hS⟩

Tactic:
·

Goal state after:
case right.refine_1
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
⊢ objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom) ∈ Δ[n].nonDegenerate m
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case right.refine_2
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
⊢ (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
      ⟨objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom), ⋯⟩ =
    ⟨S, hS⟩

Tactic:
·

Goal state after:
case right.refine_2
n m : ℕ
S : Finset (Fin (n + 1))
hS : #S = m + 1
e : Fin (m + 1) ≃o ↥S := monoEquivOfFin ↥S ⋯
⊢ (fun x ↦
        match x with
        | ⟨x, hx⟩ => ⟨Finset.image (⇑(Hom.toOrderHom (objEquiv x))) univ, ⋯⟩)
      ⟨objMk ((OrderHom.Subtype.val fun x ↦ x ∈ S).comp e.toOrderEmbedding.toOrderHom), ⋯⟩ =
    ⟨S, hS⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case left
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
⊢ Function.Injective fun i ↦ ⟨↑x i, ⋯⟩

pp: case right
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
⊢ Function.Surjective fun i ↦ ⟨↑x i, ⋯⟩

Tactic:
·

Goal state after:
case left
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
⊢ Function.Injective fun i ↦ ⟨↑x i, ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case right
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
⊢ Function.Surjective fun i ↦ ⟨↑x i, ⋯⟩

Tactic:
·

Goal state after:
case right
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
⊢ Function.Surjective fun i ↦ ⟨↑x i, ⋯⟩
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

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

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

Tactic:
·

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

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

pp: case mp.inr
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a b : Fin (d + 1)
h : ¬↑x b < ↑x a
h' : b < a
h'' : (fun j ↦ ↑x j) b = (fun j ↦ ↑x j) a
⊢ ↑x b < ↑x a

Tactic:
·

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

Goal state before:
pp: case mp.inr
n d : ℕ
x : ↑(Δ[n].nonDegenerate d)
this : Function.Injective ⇑(Hom.toOrderHom (objEquiv ↑x))
a b : Fin (d + 1)
h : ¬↑x b < ↑x a
h' : b < a
h'' : (fun j ↦ ↑x j) b = (fun j ↦ ↑x j) a
⊢ ↑x b < ↑x a

Tactic:
·

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

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

Tactic:
·

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

Goal state before:
pp: case zero
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
hm : #S = 0
⊢ (face S).toSSet.HasDimensionLT d

pp: case succ
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
m : ℕ
hm : #S = m + 1
⊢ (face S).toSSet.HasDimensionLT d

Tactic:
·

Goal state after:
case zero
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
hm : #S = 0
⊢ (face S).toSSet.HasDimensionLT d
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case succ
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
m : ℕ
hm : #S = m + 1
⊢ (face S).toSSet.HasDimensionLT d

Tactic:
·

Goal state after:
case succ
n : ℕ
S : Finset (Fin (n + 1))
d : ℕ
hd : #S ≤ d
m : ℕ
hm : #S = m + 1
⊢ (face S).toSSet.HasDimensionLT d
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case refine_1
n : ℕ
x : Δ[n] _⦋n⦌
h : x ∈ Δ[n].nonDegenerate n
⊢ x = objEquiv.symm (𝟙 ⦋n⦌)

pp: case refine_2
n : ℕ
x : Δ[n] _⦋n⦌
⊢ x = objEquiv.symm (𝟙 ⦋n⦌) → x ∈ Δ[n].nonDegenerate n

Tactic:
·

Goal state after:
case refine_1
n : ℕ
x : Δ[n] _⦋n⦌
h : x ∈ Δ[n].nonDegenerate n
⊢ x = objEquiv.symm (𝟙 ⦋n⦌)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case refine_2
n : ℕ
x : Δ[n] _⦋n⦌
⊢ x = objEquiv.symm (𝟙 ⦋n⦌) → x ∈ Δ[n].nonDegenerate n

Tactic:
·

Goal state after:
case refine_2
n : ℕ
x : Δ[n] _⦋n⦌
⊢ x = objEquiv.symm (𝟙 ⦋n⦌) → x ∈ Δ[n].nonDegenerate n
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case pos
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
h₁ : i₁ = 0
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₁ ≤ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₂

pp: case neg
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₁ ≤ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₂

Tactic:
·

Goal state after:
case pos
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
h₁ : i₁ = 0
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₁ ≤ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₂
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case neg
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₁ ≤ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₂

Tactic:
·

Goal state after:
case neg
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
h₁ : ¬i₁ = 0
⊢ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₁ ≤ shiftFun (⇑(SimplexCategory.Hom.toOrderHom f)) i₂
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case mp
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ IsIso (toOfSimplex x) → Mono (yonedaEquiv.symm x)

pp: case mpr
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ Mono (yonedaEquiv.symm x) → IsIso (toOfSimplex x)

Tactic:
·

Goal state after:
case mp
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ IsIso (toOfSimplex x) → Mono (yonedaEquiv.symm x)
Module: Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex

Goal state before:
pp: case mp
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ IsIso (toOfSimplex x) → Mono (yonedaEquiv.symm x)

Tactic:
intro
    rw [← toOfSimplex_ι]
    infer_instance

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

Goal state before:
pp: case mpr
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ Mono (yonedaEquiv.symm x) → IsIso (toOfSimplex x)

Tactic:
·

Goal state after:
case mpr
X : SSet
n : ℕ
x : X _⦋n⦌
⊢ Mono (yonedaEquiv.symm x) → IsIso (toOfSimplex x)
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
j : Fin 1
⊢ (ExtraDegeneracy.s f S 0 ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i ↦ WidePullback.π (fun x ↦ f.hom) (Fin.succAbove 1 i))
          ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) j =
    ((WidePullback.base fun x ↦ f.hom) ≫ S.section_ ≫ WidePullback.lift f.hom (fun x ↦ 𝟙 f.left) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) j

pp: case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
⊢ ((ExtraDegeneracy.s f S 0 ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i ↦ WidePullback.π (fun x ↦ f.hom) (Fin.succAbove 1 i))
          ⋯) ≫
      WidePullback.base fun x ↦ f.hom) =
    ((WidePullback.base fun x ↦ f.hom) ≫ S.section_ ≫ WidePullback.lift f.hom (fun x ↦ 𝟙 f.left) ⋯) ≫
      WidePullback.base fun x ↦ f.hom

Tactic:
·

Goal state after:
case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
j : Fin 1
⊢ (ExtraDegeneracy.s f S 0 ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i ↦ WidePullback.π (fun x ↦ f.hom) (Fin.succAbove 1 i))
          ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) j =
    ((WidePullback.base fun x ↦ f.hom) ≫ S.section_ ≫ WidePullback.lift f.hom (fun x ↦ 𝟙 f.left) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) j
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
⊢ ((ExtraDegeneracy.s f S 0 ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i ↦ WidePullback.π (fun x ↦ f.hom) (Fin.succAbove 1 i))
          ⋯) ≫
      WidePullback.base fun x ↦ f.hom) =
    ((WidePullback.base fun x ↦ f.hom) ≫ S.section_ ≫ WidePullback.lift f.hom (fun x ↦ 𝟙 f.left) ⋯) ≫
      WidePullback.base fun x ↦ f.hom

Tactic:
·

Goal state after:
case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
⊢ ((ExtraDegeneracy.s f S 0 ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i ↦ WidePullback.π (fun x ↦ f.hom) (Fin.succAbove 1 i))
          ⋯) ≫
      WidePullback.base fun x ↦ f.hom) =
    ((WidePullback.base fun x ↦ f.hom) ≫ S.section_ ≫ WidePullback.lift f.hom (fun x ↦ 𝟙 f.left) ⋯) ≫
      WidePullback.base fun x ↦ f.hom
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1 + 1)
⊢ (ExtraDegeneracy.s f S (n + 1) ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.succAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) j =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S n) ≫
      WidePullback.π (fun x ↦ f.hom) j

pp: case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
⊢ ((ExtraDegeneracy.s f S (n + 1) ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.succAbove i_1)) ⋯) ≫
      WidePullback.base fun x ↦ f.hom) =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S n) ≫
      WidePullback.base fun x ↦ f.hom

Tactic:
·

Goal state after:
case a
C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
f : Arrow C
inst✝ : ∀ (n : ℕ), HasWidePullback f.right (fun x ↦ f.left) fun x ↦ f.hom
S : SplitEpi f.hom
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1 + 1)
⊢ (ExtraDegeneracy.s f S (n + 1) ≫
        WidePullback.lift (WidePullback.base fun x ↦ f.hom)
          (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succ.succAbove i_1)) ⋯) ≫
      WidePullback.π (fun x ↦ f.hom) j =
    (WidePullback.lift (WidePullback.base fun x ↦ f.hom) (fun i_1 ↦ WidePullback.π (fun x ↦ f.hom) (i.succAbove i_1))
          ⋯ ≫
        ExtraDegeneracy.s f S n) ≫
      WidePullback.π (fun x ↦ f.hom) j