awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
rw :
  X.left.δ₀Iter ((↑j : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯ =
    X.left.δ i ≫ X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯
rw₁ rw₂ :
  X.left.δ₀Iter ((↑j : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯ =
    X.left.δ₀Iter ((↑j : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯
⊢ X.left.δ₀Iter ((↑j : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑j : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc =
    X.left.δ i ≫ X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯

Tactic:
rw [X.left.σ₀Iter_δ _ _ (by grind), X.left.δ_δ₀Iter_assoc _ _ (by grind)]

Premises used: CategoryTheory.Comma.left, CategoryTheory.SimplicialObject.δ_δ₀Iter_assoc, CategoryTheory.SimplicialObject.σ₀Iter_δ
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
generalize :
  ∀ (k : Fin (n + 1 + 1)) (hk : i.succ.rev = k),
    h ed i.succ ≫ X.left.δ i.castSucc.succ = h ed i.castSucc ≫ X.left.δ i.castSucc.succ
⊢ h ed i.succ ≫ X.left.δ i.castSucc.succ = h ed i.castSucc ≫ X.left.δ i.castSucc.succ

Tactic:
generalize hk : i.succ.rev = k

Premises used: Fin.succ, Fin.rev
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
dsimp : h ed i.succ ≫ X.left.δ i.castSucc.succ = h ed i.castSucc ≫ X.left.δ i.castSucc.succ
⊢ h ed i.succ ≫ X.left.δ i.castSucc.succ = h ed i.castSucc ≫ X.left.δ i.castSucc.succ

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
rw :
  X.left.δ₀Iter (↑i.succ : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑i.succ : ℕ) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i.castSucc : ℕ) ⋯ ≫
      ed.s ((↑k : ℕ) + 1) ≫ X.left.σ₀Iter (↑i.castSucc : ℕ) ⋯ ≫ X.left.δ i.castSucc.succ
⊢ h ed i.succ ≫ X.left.δ i.castSucc.succ = h ed i.castSucc ≫ X.left.δ i.castSucc.succ

Tactic:
rw [h_eq_assoc _ _ k, h_eq_assoc _ _ (k + 1)]

Premises used: Fin.val, HAdd.hAdd, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq_assoc, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
dsimp :
  X.left.δ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ ed.s ((↑k : ℕ) + 1) ≫ X.left.σ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ i.castSucc.succ
⊢ X.left.δ₀Iter (↑i.succ : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑i.succ : ℕ) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i.castSucc : ℕ) ⋯ ≫
      ed.s ((↑k : ℕ) + 1) ≫ X.left.σ₀Iter (↑i.castSucc : ℕ) ⋯ ≫ X.left.δ i.castSucc.succ

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 1)
k : Fin (n + 1 + 1)
hk : i.succ.rev = k
rw :
  X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ ed.s ((↑k : ℕ) + 1) ≫ X.left.σ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ i.castSucc.succ
rw₁ :
  X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ ed.s ((↑k : ℕ) + 1) ≫ X.left.δ 1 ≫ X.left.σ₀Iter (↑i : ℕ) ⋯
rw₂ :
  X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑i : ℕ) ⋯
rw₃ rw₄ :
  X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑i : ℕ) ⋯ =
    X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ 0 ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑i : ℕ) ⋯
⊢ X.left.δ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑i : ℕ) + 1) ⋯ ≫ X.left.δ i.castSucc.succ =
    X.left.δ₀Iter (↑i : ℕ) ⋯ ≫ ed.s ((↑k : ℕ) + 1) ≫ X.left.σ₀Iter (↑i : ℕ) ⋯ ≫ X.left.δ i.castSucc.succ

Tactic:
rw [X.left.δ₀Iter_succ'_assoc _ (by grind),
      X.left.σ₀Iter_δ' i.castSucc.succ i.val (m := k.val + 1)
        (i' := 1) (by grind) (by grind) (by simp; grind),
      dsimp% ed.s_comp_δ_assoc k.val 0, X.left.σ₀Iter_δ _ _ (by grind)]

Premises used: Fin.succ, CategoryTheory.SimplicialObject.σ₀Iter_δ', CategoryTheory.Comma.left, CategoryTheory.SimplicialObject.δ₀Iter_succ'_assoc, Fin.val, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_δ_assoc, Fin.castSucc, OfNat.ofNat, CategoryTheory.SimplicialObject.σ₀Iter_δ
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
hij : j.castSucc < i
generalize :
  ∀ (k : Fin (n + 1)) (hk : j.rev = k),
    h ed j.castSucc ≫ X.left.δ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).δ i ≫ h ed j
⊢ h ed j.castSucc ≫ X.left.δ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).δ i ≫ h ed j

Tactic:
generalize hk : j.rev = k

Premises used: Fin.rev
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
rw : ∀ (hij : (↑j.succ : ℕ) ≤ (↑i : ℕ)) (k : Fin (n + 1)) (hk : j.rev = k), ∃ (l : ℕ), (↑i : ℕ) = (↑j : ℕ) + 1 + l
⊢ ∃ (l : ℕ), (↑i : ℕ) = (↑j : ℕ) + 1 + l

Tactic:
rw [Fin.castSucc_lt_iff_succ_le, Fin.le_def] at hij

Premises used: Fin.le_def, Fin.castSucc_lt_iff_succ_le
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
obtain : ∀ (l : ℕ) (hl : (↑j.succ : ℕ) + l = (↑i : ℕ)), ∃ (l : ℕ), (↑i : ℕ) = (↑j : ℕ) + 1 + l
⊢ ∃ (l : ℕ), (↑i : ℕ) = (↑j : ℕ) + 1 + l

Tactic:
obtain ⟨l, hl⟩ := Nat.le.dest hij

Premises used: Nat.le.dest
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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 : ℕ)
⊢ ∃ (l : ℕ), (↑i : ℕ) = (↑j : ℕ) + 1 + l

Tactic:
exact ⟨l, by grind⟩
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
obtain :
  ∀ (l : ℕ) (hl : (↑i : ℕ) = (↑j : ℕ) + 1 + l),
    h ed j.castSucc ≫ X.left.δ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).δ i ≫ h ed j
⊢ h ed j.castSucc ≫ X.left.δ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).δ i ≫ h ed j

Tactic:
obtain ⟨l, hl⟩ : ∃ l, i.val = j + 1 + l := by
      rw [Fin.castSucc_lt_iff_succ_le, Fin.le_def] at hij
      obtain ⟨l, hl⟩ := Nat.le.dest hij
      exact ⟨l, by grind⟩

Premises used: Fin.val
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
⊢ ed.s ((↑k : ℕ) + 1) ≫ X.left.δ (⟨l + 1, ⋯⟩ : Fin ((↑k : ℕ) + 2)).succ =
    X.left.δ (⟨l + 1, ⋯⟩ : Fin ((↑k : ℕ) + 2)) ≫ ed.s (↑k : ℕ)

Tactic:
have := ed.s_comp_δ k ⟨l + 1, by grind⟩
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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, ⋯⟩ : Fin ((↑k : ℕ) + 2)).succ =
    X.left.δ (⟨l + 1, ⋯⟩ : Fin ((↑k : ℕ) + 2)) ≫ ed.s (↑k : ℕ)
dsimp : h ed j.castSucc ≫ X.left.δ i.succ = X.left.δ i ≫ h ed j
⊢ h ed j.castSucc ≫ X.left.δ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).δ i ≫ h ed j

Tactic:
dsimp at this ⊢
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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, ⋯⟩ : Fin ((↑k : ℕ) + 2 + 1)) =
    X.left.δ (⟨l + 1, ⋯⟩ : Fin ((↑k : ℕ) + 2)) ≫ ed.s (↑k : ℕ)
⊢ l + 2 < (↑k : ℕ) + 1 + 2

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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, ⋯⟩ : Fin ((↑k : ℕ) + 2 + 1)) =
    X.left.δ (⟨l + 1, ⋯⟩ : Fin ((↑k : ℕ) + 2)) ≫ ed.s (↑k : ℕ)
⊢ (↑k : ℕ) + 1 + (↑j.castSucc : ℕ) = n + 1

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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, ⋯⟩ : Fin ((↑k : ℕ) + 2 + 1)) =
    X.left.δ (⟨l + 1, ⋯⟩ : Fin ((↑k : ℕ) + 2)) ≫ ed.s (↑k : ℕ)
⊢ (↑k : ℕ) + (↑j.castSucc : ℕ) = n

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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, ⋯⟩ : Fin ((↑k : ℕ) + 2 + 1)) =
    X.left.δ (⟨l + 1, ⋯⟩ : Fin ((↑k : ℕ) + 2)) ≫ ed.s (↑k : ℕ)
rw :
  X.left.δ i ≫ X.left.δ₀Iter (↑j.castSucc : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j.castSucc : ℕ) ⋯ =
    X.left.δ i ≫ X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯
⊢ h ed j.castSucc ≫ X.left.δ i.succ = X.left.δ i ≫ h ed j

Tactic:
rw [h_eq_assoc _ _ (k + 1), h_eq _ _ k,
      X.left.σ₀Iter_δ' _ _ ⟨l + 2, by grind⟩ (by grind),
      reassoc_of% this, ← X.left.δ_δ₀Iter'_assoc _ _ i (by grind)]

Premises used: CategoryTheory.SimplicialObject.σ₀Iter_δ', CategoryTheory.Comma.left, Fin.mk, Fin.val, CategoryTheory.SimplicialObject.δ_δ₀Iter'_assoc, HAdd.hAdd, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq_assoc, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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, ⋯⟩ : Fin ((↑k : ℕ) + 2 + 1)) =
    X.left.δ (⟨l + 1, ⋯⟩ : Fin ((↑k : ℕ) + 2)) ≫ ed.s (↑k : ℕ)
⊢ X.left.δ i ≫ X.left.δ₀Iter (↑j.castSucc : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j.castSucc : ℕ) ⋯ =
    X.left.δ i ≫ X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
generalize :
  ∀ (k : Fin (n + 1)) (hk : j.rev = k),
    h ed j ≫ X.left.σ i.castSucc = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).σ i ≫ h ed j.succ
⊢ h ed j ≫ X.left.σ i.castSucc = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).σ i ≫ h ed j.succ

Tactic:
generalize hk : j.rev = k

Premises used: Fin.rev
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
k : Fin (n + 1)
hk : j.rev = k
dsimp : h ed j ≫ X.left.σ i.castSucc = X.left.σ i ≫ h ed j.succ
⊢ h ed j ≫ X.left.σ i.castSucc = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).σ i ≫ h ed j.succ

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
k : Fin (n + 1)
hk : j.rev = k
rw :
  X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯ ≫ X.left.σ i.castSucc =
    X.left.σ i ≫ X.left.δ₀Iter (↑j.succ : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j.succ : ℕ) ⋯
⊢ h ed j ≫ X.left.σ i.castSucc = X.left.σ i ≫ h ed j.succ

Tactic:
rw [h_eq_assoc _ _ k, h_eq _ _ k]

Premises used: Fin.val, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq_assoc
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
k : Fin (n + 1)
hk : j.rev = k
dsimp :
  X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯ ≫ X.left.σ i.castSucc =
    X.left.σ i ≫ X.left.δ₀Iter ((↑j : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑j : ℕ) + 1) ⋯
⊢ X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯ ≫ X.left.σ i.castSucc =
    X.left.σ i ≫ X.left.δ₀Iter (↑j.succ : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j.succ : ℕ) ⋯

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : i ≤ j
k : Fin (n + 1)
hk : j.rev = k
rw :
  X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯ ≫ X.left.σ i.castSucc =
    X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑j : ℕ) + 1) ⋯
rw₁ rw₂ :
  X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑j : ℕ) + 1) ⋯ =
    X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑j : ℕ) + 1) ⋯
⊢ X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯ ≫ X.left.σ i.castSucc =
    X.left.σ i ≫ X.left.δ₀Iter ((↑j : ℕ) + 1) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ₀Iter ((↑j : ℕ) + 1) ⋯

Tactic:
rw [X.left.σ_δ₀Iter_assoc _ _ (by grind), X.left.σ₀Iter_σ _ _ (by grind)]

Premises used: CategoryTheory.SimplicialObject.σ₀Iter_σ, CategoryTheory.SimplicialObject.σ_δ₀Iter_assoc, CategoryTheory.Comma.left
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
generalize :
  ∀ (k : Fin (n + 1)) (hk : j.rev = k),
    h ed j ≫ X.left.σ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).σ i ≫ h ed j.castSucc
⊢ h ed j ≫ X.left.σ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).σ i ≫ h ed j.castSucc

Tactic:
generalize hk : j.rev = k

Premises used: Fin.rev
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} C
ed : X.ExtraDegeneracy
n : ℕ
i j : Fin (n + 1)
hij : j ≤ i
k : Fin (n + 1)
hk : j.rev = k
obtain :
  ∀ (l : ℕ) (hl : (↑j : ℕ) + l = (↑i : ℕ)),
    h ed j ≫ X.left.σ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).σ i ≫ h ed j.castSucc
⊢ h ed j ≫ X.left.σ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).σ i ≫ h ed j.castSucc

Tactic:
obtain ⟨l, hl⟩ := Nat.le.dest (Fin.le_def.1 hij)

Premises used: Fin.le_def, Iff.mp, Nat.le.dest
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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 : ℕ)
dsimp : h ed j ≫ X.left.σ i.succ = X.left.σ i ≫ h ed j.castSucc
⊢ h ed j ≫ X.left.σ i.succ = (Functor.obj (𝟭 (SimplicialObject.{v_1, u_1} C)) X.left).σ i ≫ h ed j.castSucc

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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 : ℕ)
rw :
  X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ (⟨l + 1, ⋯⟩ : Fin ((↑k : ℕ) + 1 + 1)) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯ =
    X.left.δ₀Iter (↑j.castSucc : ℕ) ⋯ ≫
      ed.s (↑k : ℕ) ≫ X.left.σ (⟨l, ⋯⟩ : Fin ((↑k : ℕ) + 1)).succ ≫ X.left.σ₀Iter (↑j.castSucc : ℕ) ⋯
⊢ h ed j ≫ X.left.σ i.succ = X.left.σ i ≫ h ed j.castSucc

Tactic:
rw [h_eq_assoc _ _ k, h_eq _ _ (k + 1),
      X.left.σ_δ₀Iter'_assoc _ _ ⟨l, by grind⟩
        (by grind),
      ← ed.s_comp_σ_assoc,
      X.left.σ₀Iter_σ' j i.succ ⟨l + 1, by grind⟩ (by grind)]

Premises used: Fin.succ, CategoryTheory.SimplicialObject.σ_δ₀Iter'_assoc, CategoryTheory.Comma.left, Fin.mk, CategoryTheory.SimplicialObject.σ₀Iter_σ', Fin.val, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s_comp_σ_assoc, HAdd.hAdd, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq, CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.homotopy.h_eq_assoc, OfNat.ofNat
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
X : Augmented.{v_1, u_1} 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 : ℕ)
⊢ X.left.δ₀Iter (↑j : ℕ) ⋯ ≫ ed.s (↑k : ℕ) ≫ X.left.σ (⟨l + 1, ⋯⟩ : Fin ((↑k : ℕ) + 1 + 1)) ≫ X.left.σ₀Iter (↑j : ℕ) ⋯ =
    X.left.δ₀Iter (↑j.castSucc : ℕ) ⋯ ≫
      ed.s (↑k : ℕ) ≫ X.left.σ (⟨l, ⋯⟩ : Fin ((↑k : ℕ) + 1)).succ ≫ X.left.σ₀Iter (↑j.castSucc : ℕ) ⋯

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
n : ℕ
X : Type u_1
inst : Zero X
f : Fin n → X
⊢ shiftFun f 0 = 0

Tactic:
rfl

Premises used: Eq.mpr, SSet.Augmented.StandardSimplex.shiftFun, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
n : ℕ
X : Type u_1
inst : Zero X
f : Fin n → X
i : Fin n
⊢ shiftFun f i.succ = f i

Tactic:
rfl

Premises used: SSet.Augmented.StandardSimplex.shiftFun, Fin.cons, Fin.induction.go, Fin.induction, Fin.cases, Matrix.vecCons, rfl
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
pos :
  ∀ (h₁ : i₁ = 0),
    LE.le (α := Fin (Δ.len + 1))
      (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₁)
      (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₂)
neg :
  ∀ (h₁ : ¬i₁ = 0),
    LE.le (α := Fin (Δ.len + 1))
      (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₁)
      (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₂)
⊢ LE.le (α := Fin (Δ.len + 1))
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₁)
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₂)

Tactic:
by_cases h₁ : i₁ = 0
-- Module: Mathlib.AlgebraicTopology.ExtraDegeneracy
Goal:
n : ℕ
Δ : SimplexCategory
f : ⦋n⦌ ⟶ Δ
i₁ i₂ : Fin (⦋n + 1⦌.len + 1)
hi : i₁ ≤ i₂
h₁ : i₁ = 0
pos :
  ∀ (hi : 0 ≤ i₂),
    LE.le (α := Fin (Δ.len + 1))
      (shiftFun (n := ⦋n + 1⦌.len) (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) 0)
      (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₂)
⊢ LE.le (α := Fin (Δ.len + 1))
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₁)
    (shiftFun (⇑(SimplexCategory.Hom.toOrderHom f) : (a : Fin (⦋n⦌.len + 1)) → Fin (Δ.len + 1)) i₂)

Tactic:
subst h₁