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

Goal state before:
pp: i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : i < ↑k
⊢ j.castSucc < k

Tactic:
grind

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

Goal state before:
pp: case pos
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : ↑j ≤ i
k : Fin (⦋m + 1⦌.len + 1)
hk : i < ↑k
⊢ ↑(k.pred ⋯) - i = ↑k - (i + 1)

Tactic:
grind

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

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

Tactic:
grind

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

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

Tactic:
rfl

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

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

Tactic:
| succ i hi' =>

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

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

Tactic:
| succ i hi' =>

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

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

Tactic:
rfl

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

Goal state before:
pp: X : SSet
d : ℕ
w✝ : X _⦋d⦌
⊢ { dim := d, simplex := w✝ }.cast ⋯ = { dim := d, simplex := w✝ }

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case a
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
G : F ⟶ Augmented.toArrow.obj X
x y : SimplexCategory
f : x ⟶ y
j✝ : Fin (x.len + 1)
⊢ Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const y ((SimplexCategory.Hom.toOrderHom f) j✝)) =
    Arrow.Hom.right G ≫ X.right.map (⦋0⦌.const x j✝ ≫ f)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

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

Tactic:
rfl

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

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

Tactic:
rfl

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

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

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: case h₂.refine_1
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : ∀ (n : ℕ) (f : Arrow C), HasWidePushout f.left (fun x ↦ f.right) fun x ↦ f.hom
F : Arrow C
X : Augmented C
A : F.augmentedCechConerve ⟶ X
x : SimplexCategory
j : Fin (x.len + 1)
⊢ WidePushout.ι (fun x ↦ F.hom) ((SimplexCategory.Hom.toOrderHom (⦋0⦌.const x j)) 0) ≫ A.right.app x =
    WidePushout.ι (fun x ↦ F.hom) j ≫ A.right.app x

Tactic:
rfl

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

Goal state before:
pp: X : SSet
x : X _⦋0⦌
n : SimplexCategoryᵒᵖ
⊢ (ConcreteCategory.hom ((ofSimplex x).ι.app n)).toFun
      ⟨(ConcreteCategory.hom (X.map (Opposite.op ((Opposite.unop n).const (Opposite.unop (Opposite.op ⦋0⦌)) 0)))) x,
        ⋯⟩ =
    (ConcreteCategory.hom ((const x).app n)).toFun
      ⟨(ConcreteCategory.hom (X.map (Opposite.op ((Opposite.unop n).const (Opposite.unop (Opposite.op ⦋0⦌)) 0)))) x, ⋯⟩

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

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

Tactic:
rfl

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

Goal state before:
pp: X : SSet
x : X.N
⊢ x.subcomplex = x.subcomplex

Tactic:
rfl

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

Goal state before:
pp: X : SSet
s : X.N
⊢ s.cast ⋯ = s

Tactic:
rfl

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

Goal state before:
pp: X : SSet
d : ℕ
s : X _⦋d⦌
hs : s ∈ X.nonDegenerate d
⊢ Subcomplex.ofSimplex ↑⟨d, ⟨s, hs⟩⟩.snd ≤ (mk s hs).subcomplex

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.CechNerve

Goal state before:
pp: C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasTerminal C
ι : Type w
inst✝¹ : HasFiniteProducts C
inst✝ : Finite ι
X : C
⊢ HasWidePullback (Arrow.mk (terminal.from X)).right (fun x ↦ (Arrow.mk (terminal.from X)).left) fun x ↦
    (Arrow.mk (terminal.from X)).hom

Tactic:
by
  cases nonempty_fintype ι
  exact ⟨⟨wideCospan.limitCone ι X⟩⟩

Goal state after:
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
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
y : ↑(X.nonDegenerate m)
⊢ ∃ a, φ a = (ConcreteCategory.hom (X.map f.op)) ↑y

Tactic:
have := SimplexCategory.le_of_epi f

Goal state after:
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
m : ℕ
f : ⦋n⦌ ⟶ ⦋m⦌
hf : Epi f
y : ↑(X.nonDegenerate m)
this : m ≤ n
⊢ ∃ a, φ a = (ConcreteCategory.hom (X.map f.op)) ↑y
Module: Mathlib.AlgebraicTopology.SimplicialSet.Finite

Goal state before:
pp: X : SSet
inst✝ : X.Finite
A : X.Subcomplex
d : ℕ
h✝ : X.HasDimensionLT d
i : ℕ
hi : i < d
x : X _⦋i⦌
property✝³ : x ∈ A.obj (Opposite.op ⦋i⦌)
property✝² : ⟨x, property✝³⟩ ∈ A.toSSet.nonDegenerate i
property✝¹ : (fun a ↦ ↑↑a) ⟨⟨x, property✝³⟩, property✝²⟩ ∈ A.obj (Opposite.op ⦋i⦌)
property✝ : ⟨(fun a ↦ ↑↑a) ⟨⟨x, property✝³⟩, property✝²⟩, property✝¹⟩ ∈ A.toSSet.nonDegenerate i
⊢ ⟨⟨x, property✝³⟩, property✝²⟩ = ⟨⟨(fun a ↦ ↑↑a) ⟨⟨x, property✝³⟩, property✝²⟩, property✝¹⟩, property✝⟩

Tactic:
rfl

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
⊢ N.mk x hx ≤ N.mk y hy ∧ N.mk y hy ≤ N.mk x hx ↔
    Subcomplex.ofSimplex x ≤ Subcomplex.ofSimplex y ∧ Subcomplex.ofSimplex y ≤ Subcomplex.ofSimplex x

Tactic:
rfl

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 := ⦋0⦌, property := ⋯ }, right := { as := PUnit.unit },
      hom := ⦋0⦌.const ((Functor.fromPUnit Δ).obj { as := PUnit.unit }) ((ConcreteCategory.hom f') 0) }

Tactic:
apply Zigzag.of_inv <| CostructuredArrow.homMk <| Hom.tr <| ⦋0⦌.const _ 1

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:
constructor
  · intro hy
    simpa [← comp_apply, ← NatTrans.comp_app] using degenerate_app_apply hy (inv f)
  · exact fun hx ↦ degenerate_app_apply hx f

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x : C
⊢ ((ConcreteCategory.hom (SimplicialObject.σ (nerve C) 0)) (ComposableArrows.mk₀ x)).hom = eqToHom ⋯

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 2)) (ComposableArrows.mk₂ f g)) = f

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) (ComposableArrows.mk₂ f g)) = g

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) (ComposableArrows.mk₂ f g)) = f ≫ g

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : ComposableArrows C 0
e : Edge x y
⊢ ComposableArrows.left e.edge = nerveEquiv ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 1)) e.edge)

Tactic:
rfl

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

Goal state before:
pp: C : Type u
inst✝ : Category.{v, u} C
x y : ComposableArrows C 0
e : Edge x y
⊢ ComposableArrows.right e.edge = nerveEquiv ((ConcreteCategory.hom (SimplicialObject.δ (nerve C) 0)) e.edge)

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case zero
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
j : ℕ
⊢ (C.augment f w).d (0 + 1) (j + 1) = C.d 0 j

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Homology.Augment

Goal state before:
pp: case succ
V : Type u
inst✝¹ : Category.{v, u} V
inst✝ : HasZeroMorphisms V
C : ChainComplex V ℕ
X : V
f : C.X 0 ⟶ X
w : C.d 1 0 ≫ f = 0
j n✝ : ℕ
⊢ (C.augment f w).d (n✝ + 1 + 1) (j + 1) = C.d (n✝ + 1) j

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
m : SimplexCategory
f : ⦋n + 1⦌ ⟶ m
i : Fin (n + 2)
⊢ (ConcreteCategory.hom (SimplicialObject.δ (stdSimplex.obj m) i)) (objEquiv.symm f) = objEquiv.symm (δ i ≫ f)

Tactic:
rfl

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

Goal state before:
pp: n : ℕ
m : SimplexCategory
f : ⦋n⦌ ⟶ m
i : Fin (n + 1)
⊢ (ConcreteCategory.hom (SimplicialObject.σ (stdSimplex.obj m) i)) (objEquiv.symm f) = objEquiv.symm (σ i ≫ f)

Tactic:
rfl

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

Goal state before:
pp: m₁ m₂ : SimplexCategoryᵒᵖ
f : m₁ ⟶ m₂
n : SimplexCategory
x : (stdSimplex.obj n).obj m₁
⊢ (ConcreteCategory.hom ((stdSimplex.obj n).map f)) x = objEquiv.symm (f.unop ≫ objEquiv x)

Tactic:
rfl

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

Goal state before:
pp: X : SSet
n : SimplexCategory
x : X.obj (op n)
m : SimplexCategoryᵒᵖ
y : (stdSimplex.obj n).obj m
⊢ (ConcreteCategory.hom (X.map (objEquiv y).op)) x = (ConcreteCategory.hom ((yonedaEquiv.symm x).app m)) y

Tactic:
rfl

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

Goal state before:
pp: case «0»
n : ℕ
x : Δ[n] _⦋0⦌
⊢ ((fun i ↦ const n i (op ⦋0⦌)) ((fun x ↦ x 0) x)) ((fun i ↦ i) ⟨0, ⋯⟩) = x ((fun i ↦ i) ⟨0, ⋯⟩)

Tactic:
rfl

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

Goal state before:
pp: X : SSet
A : X.Subcomplex
n : SimplexCategory
f : stdSimplex.obj n ⟶ A.toSSet
⊢ ↑(yonedaEquiv f) = yonedaEquiv (f ≫ A.ι)

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
⊢ ↑i.rev + ↑i = n

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
⊢ ↑i.rev + 1 + ↑i = n + 1

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
j : ℕ
hj : autoParam (j = ↑i.rev) h_eq._auto_1
⊢ j + ↑i = n

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
j : ℕ
hj : autoParam (j = ↑i.rev) h_eq._auto_1
⊢ j + 1 + ↑i = n + 1

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
⊢ h ed i = X.left.δ₀Iter ↑i ⋯ ≫ ed.s ↑i.rev ≫ X.left.σ₀Iter ↑i ⋯

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
⊢ 0 + ↑(Fin.last n) = n

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
k : Fin (n + 1 + 1)
hk : j.succ.rev = k
⊢ ↑k + 1 + (↑j + 1) = n + 1 + 1

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : i ≤ j.castSucc
k : Fin (n + 1 + 1)
hk : j.succ.rev = k
⊢ ↑k + ↑j = n

Tactic:
grind

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

Goal state before:
pp: n d : ℕ
s : Δ[n] _⦋d⦌
⊢ StrictMono ((ConcreteCategory.hom ((isoNerve.{u} n).hom.app (op ⦋d⦌))) s).obj ↔ StrictMono ⇑s

Tactic:
rfl

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ ↑k + (↑i + 1) = n + 1

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ ↑k + 1 + ↑i = n + 1

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ ↑i < ↑i.castSucc.succ

Tactic:
grind

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

Goal state before:
pp: n : ℕ
i j : Fin (n + 2)
h : i.castSucc < j.succ
⊢ i ≤ j

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ ↑i + 1 = 1 + ↑i

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
⊢ ↑k + 1 + (↑i + 1) = n + 1 + 1

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : ↑j.succ ≤ ↑i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j.succ + l = ↑i
⊢ ↑i = ↑j + 1 + l

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑i = ↑j + 1 + l
⊢ l + 1 < ↑k + 2

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑i = ↑j + 1 + l
this :
  ed.s (↑k + 1) ≫ X.left.δ ⟨l + 1 + 1, ⋯⟩ =
    X.left.δ ⟨l + 1, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_24 n i j k hk l hl⟩ ≫
      ed.s ↑k
⊢ l + 2 < ↑k + 1 + 2

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑i = ↑j + 1 + l
this :
  ed.s (↑k + 1) ≫ X.left.δ ⟨l + 1 + 1, ⋯⟩ =
    X.left.δ ⟨l + 1, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_24 n i j k hk l hl⟩ ≫
      ed.s ↑k
⊢ ↑k + 1 + ↑j.castSucc = n + 1

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑i = ↑j + 1 + l
this :
  ed.s (↑k + 1) ≫ X.left.δ ⟨l + 1 + 1, ⋯⟩ =
    X.left.δ ⟨l + 1, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy._proof_24 n i j k hk l hl⟩ ≫
      ed.s ↑k
⊢ ↑k + ↑j.castSucc = n

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
k : Fin (n + 1)
hk : j.rev = k
⊢ ↑k + (↑j + 1) = n + 1

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
k : Fin (n + 1)
hk : j.rev = k
⊢ ↑k + 1 + ↑j = n + 1

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j + l = ↑i
⊢ l < ↑k + 1

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j + l = ↑i
⊢ ↑k + ↑j.castSucc = n

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j + l = ↑i
⊢ l + 1 < ↑k + 1 + 1

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: C : Type u_1
inst✝ : Category.{v_1, u_1} C
X : Augmented C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
l : ℕ
hl : ↑j + l = ↑i
⊢ ↑k + 1 + ↑j = n + 1

Tactic:
grind

Goal state after:
Module: Mathlib.AlgebraicTopology.ExtraDegeneracy

Goal state before:
pp: case «0»
Δ : SimplexCategory
x : SSet.stdSimplex.obj Δ _⦋0⦌
⊢ ↑((SimplexCategory.Hom.toOrderHom
          (objEquiv
            ((ConcreteCategory.hom
                  ((↾fun f ↦
                      objEquiv.symm
                        (SimplexCategory.Hom.mk
                          { toFun := shiftFun ⇑(SimplexCategory.Hom.toOrderHom (objEquiv f)), monotone' := ⋯ })) ≫
                    SimplicialObject.δ (SSet.stdSimplex.obj Δ) 1)).toFun
              x)))
        ((fun i ↦ i) ⟨0, ⋯⟩)) =
    ↑((SimplexCategory.Hom.toOrderHom
          (objEquiv
            ((ConcreteCategory.hom
                  (Limits.terminal.from (SSet.stdSimplex.obj Δ _⦋0⦌) ≫
                    ↾fun x ↦ objMk ((OrderHom.const (Fin 1)) 0))).toFun
              x)))
        ((fun i ↦ i) ⟨0, ⋯⟩))

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Homology.HomologicalBicomplex

Goal state before:
pp: C : Type u_1
inst✝¹ : Category.{v_1, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
x₁ : I₁
x₂ : I₂
⊢ (K.X x₁).X x₂ = (K.X x₁).X x₂

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : c₁.Rel i₁ (c₁.next i₁)
⊢ K.d₁ c₁₂ i₁ i₂ i₁₂ =
    c₁.ε₁ c₂ c₁₂ (i₁, i₂) •
      (K.d i₁ (c₁.next i₁)).f i₂ ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (c₁.next i₁, i₂) i₁₂

Tactic:
rfl

Goal state after:
Module: Mathlib.Algebra.Homology.TotalComplex

Goal state before:
pp: C : Type u_1
inst✝⁴ : Category.{v_1, u_1} C
inst✝³ : Preadditive C
I₁ : Type u_2
I₂ : Type u_3
I₁₂ : Type u_4
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
c₁₂ : ComplexShape I₁₂
inst✝² : TotalComplexShape c₁ c₂ c₁₂
inst✝¹ : DecidableEq I₁₂
inst✝ : K.HasTotal c₁₂
i₁ : I₁
i₂ : I₂
i₁₂ : I₁₂
h : c₂.Rel i₂ (c₂.next i₂)
⊢ K.d₂ c₁₂ i₁ i₂ i₁₂ =
    c₁.ε₂ c₂ c₁₂ (i₁, i₂) •
      (K.X i₁).d i₂ (c₂.next i₂) ≫ K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, c₂.next i₂) i₁₂

Tactic:
rfl

Goal state after: