awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : (↑j : ℕ) ≤ i
k : Fin (⦋n⦌.len + 1)
h : (↑((⟨(↑k : ℕ) + (i + 1), ⋯⟩ : Fin (m + 1 + 1)).pred ⋯) : ℕ) = (↑(⟨(↑k : ℕ) + i, ⋯⟩ : Fin (m + 1)) : ℕ)
⊢ (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter (i + 1) hi ≫ σ j) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
          k) :
      ℕ) =
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (δ₀Iter i ⋯) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋m⦌.len + 1))
          k) :
      ℕ)

Tactic:
rw [dsimp% ConcreteCategory.comp_apply (δ₀Iter (i + 1)) (σ j),
    δ₀Iter_apply .., δ₀Iter_apply .., coe_σ,
    Fin.predAbove_of_castSucc_lt _ _ (by grind)]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, Fin.predAbove_of_castSucc_lt, SimplexCategory.σ, SimplexCategory.coe_σ, HAdd.hAdd, SimplexCategory.δ₀Iter, OfNat.ofNat, SimplexCategory.δ₀Iter_apply
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + (i + 1) = m + 1
hj : (↑j : ℕ) ≤ i
k : Fin (⦋n⦌.len + 1)
⊢ (↑((⟨(↑k : ℕ) + (i + 1), ⋯⟩ : Fin (m + 1 + 1)).pred ⋯) : ℕ) = (↑(⟨(↑k : ℕ) + i, ⋯⟩ : Fin (m + 1)) : ℕ)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi' : n + 0 = m
hj' : (↑j : ℕ) = (↑j' : ℕ) + 0
⊢ n = m

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi' : n + 0 = m
hj' : (↑j : ℕ) = (↑j' : ℕ) + 0
zero : ∀ (j : Fin (n + 1)) (hi' : n + 0 = n) (hj' : (↑j : ℕ) = (↑j' : ℕ) + 0), δ₀Iter 0 ⋯ ≫ σ j = σ j' ≫ δ₀Iter 0 hi'
⊢ δ₀Iter 0 ⋯ ≫ σ j = σ j' ≫ δ₀Iter 0 hi'

Tactic:
obtain rfl : n = m := by lia

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
j' j : Fin (n + 1)
hi' : n + 0 = n
hj' : (↑j : ℕ) = (↑j' : ℕ) + 0
⊢ j = j'

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
j' j : Fin (n + 1)
hi' : n + 0 = n
hj' : (↑j : ℕ) = (↑j' : ℕ) + 0
zero : ∀ (hj' : (↑j : ℕ) = (↑j : ℕ) + 0), δ₀Iter 0 ⋯ ≫ σ j = σ j ≫ δ₀Iter 0 hi'
⊢ δ₀Iter 0 ⋯ ≫ σ j = σ j' ≫ δ₀Iter 0 hi'

Tactic:
obtain rfl : j = j' := by lia

Premises used: rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
j : Fin (n + 1)
hi' : n + 0 = n
hj' : (↑j : ℕ) = (↑j : ℕ) + 0
⊢ δ₀Iter 0 ⋯ ≫ σ j = σ j ≫ δ₀Iter 0 hi'

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m) (hj' : (↑j : ℕ) = (↑j' : ℕ) + i),
    δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi' : n + (i + 1) = m
hj' : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)
succ :
  ∀ (j : Fin (HAdd.hAdd (α := ℕ) 0 1)) (hi' : n + (i + 1) = 0) (hj' : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)),
    δ₀Iter (i + 1) ⋯ ≫ σ j = σ j' ≫ δ₀Iter (i + 1) hi'
succ₁ :
  ∀ (m : ℕ) (j : Fin (m + 1 + 1)) (hi' : n + (i + 1) = m + 1) (hj' : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)),
    δ₀Iter (i + 1) ⋯ ≫ σ j = σ j' ≫ δ₀Iter (i + 1) hi'
⊢ δ₀Iter (i + 1) ⋯ ≫ σ j = σ j' ≫ δ₀Iter (i + 1) hi'

Tactic:
obtain _ | m := m
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m) (hj' : (↑j : ℕ) = (↑j' : ℕ) + i),
    δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
j : Fin (HAdd.hAdd (α := ℕ) 0 1)
hi' : n + (i + 1) = 0
hj' : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)
⊢ δ₀Iter (i + 1) ⋯ ≫ σ j = σ j' ≫ δ₀Iter (i + 1) hi'

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m) (hj' : (↑j : ℕ) = (↑j' : ℕ) + i),
    δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
hi' : n + (i + 1) = m + 1
hj' : 0 = (↑j' : ℕ) + (i + 1)
⊢ False

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m) (hj' : (↑j : ℕ) = (↑j' : ℕ) + i),
    δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
j : Fin (m + 1 + 1)
hi' : n + (i + 1) = m + 1
hj' : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)
succ :
  ∀ (j : Fin (m + 1)) (hj' : (↑j.succ : ℕ) = (↑j' : ℕ) + (i + 1)),
    δ₀Iter (i + 1) ⋯ ≫ σ j.succ = σ j' ≫ δ₀Iter (i + 1) hi'
⊢ δ₀Iter (i + 1) ⋯ ≫ σ j = σ j' ≫ δ₀Iter (i + 1) hi'

Tactic:
obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero
        (by rintro rfl; dsimp at hj'; lia)

Premises used: Fin.eq_succ_of_ne_zero, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m) (hj' : (↑j : ℕ) = (↑j' : ℕ) + i),
    δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
hi' : n + (i + 1) = m + 1
j : Fin (m + 1)
hj' : (↑j.succ : ℕ) = (↑j' : ℕ) + (i + 1)
⊢ 0 ≤ j.castSucc

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m) (hj' : (↑j : ℕ) = (↑j' : ℕ) + i),
    δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
hi' : n + (i + 1) = m + 1
j : Fin (m + 1)
hj' : (↑j.succ : ℕ) = (↑j' : ℕ) + (i + 1)
⊢ n + i = m

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m) (hj' : (↑j : ℕ) = (↑j' : ℕ) + i),
    δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
hi' : n + (i + 1) = m + 1
j : Fin (m + 1)
hj' : (↑j.succ : ℕ) = (↑j' : ℕ) + (i + 1)
⊢ (↑j : ℕ) = (↑j' : ℕ) + i

Tactic:
grind
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i : ℕ
hi :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m) (hj' : (↑j : ℕ) = (↑j' : ℕ) + i),
    δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'
n : ℕ
j' : Fin (n + 1)
m : ℕ
hi' : n + (i + 1) = m + 1
j : Fin (m + 1)
hj' : (↑j.succ : ℕ) = (↑j' : ℕ) + (i + 1)
succ : δ₀Iter i ⋯ ≫ δ 0 ≫ σ j.succ = σ j' ≫ δ₀Iter (i + 1) hi'
succ₁ : δ₀Iter i ⋯ ≫ δ 0 ≫ σ j.succ = σ j' ≫ δ₀Iter i ⋯ ≫ δ 0
succ₂ : δ₀Iter i ⋯ ≫ σ j ≫ δ 0 = σ j' ≫ δ₀Iter i ⋯ ≫ δ 0
succ₃ succ₄ : σ j' ≫ δ₀Iter i ⋯ ≫ δ 0 = σ j' ≫ δ₀Iter i ⋯ ≫ δ 0
⊢ δ₀Iter (i + 1) ⋯ ≫ σ j.succ = σ j' ≫ δ₀Iter (i + 1) hi'

Tactic:
rw [δ₀Iter_succ_assoc .., δ₀Iter_succ ..,
        dsimp% δ_comp_σ_of_le (i := 0) (j := j) (by simp),
        reassoc_of% hi j j' (by lia) (by grind)]

Premises used: SimplexCategory.δ₀Iter_succ_assoc, SimplexCategory.δ_comp_σ_of_le, SimplexCategory.δ₀Iter_succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
j' : Fin (n + 1)
hi' : n + i = m
hj' : (↑j : ℕ) = (↑j' : ℕ) + i
zero :
  ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + 0 = m) (hj' : (↑j : ℕ) = (↑j' : ℕ) + 0),
    δ₀Iter 0 ⋯ ≫ σ j = σ j' ≫ δ₀Iter 0 hi'
succ :
  ∀ (i : ℕ)
    (hi :
      ∀ {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + i = m) (hj' : (↑j : ℕ) = (↑j' : ℕ) + i),
        δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi')
    {n m : ℕ} (j : Fin (m + 1)) (j' : Fin (n + 1)) (hi' : n + (i + 1) = m) (hj' : (↑j : ℕ) = (↑j' : ℕ) + (i + 1)),
    δ₀Iter (i + 1) ⋯ ≫ σ j = σ j' ≫ δ₀Iter (i + 1) hi'
⊢ δ₀Iter i ⋯ ≫ σ j = σ j' ≫ δ₀Iter i hi'

Tactic:
induction i generalizing n m with
  | zero =>
    obtain rfl : n = m := by lia
    obtain rfl : j = j' := by lia
    simp
  | succ i hi =>
    obtain _ | m := m
    · grind
    · obtain ⟨j, rfl⟩ := j.eq_succ_of_ne_zero
        (by rintro rfl; dsimp at hj'; lia)
      rw [δ₀Iter_succ_assoc .., δ₀Iter_succ ..,
        dsimp% δ_comp_σ_of_le (i := 0) (j := j) (by simp),
        reassoc_of% hi j j' (by lia) (by grind)]

Premises used: Fin.eq_succ_of_ne_zero, SimplexCategory.δ₀Iter_succ_assoc, SimplexCategory.δ_comp_σ_of_le, rfl, SimplexCategory.δ₀Iter_succ
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
hi : n + i = m
j : Fin (⦋m⦌.len + 1)
⊢ (↑j : ℕ) - i < ⦋n⦌.len + 1

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
hi : n + i = m
x x_1 : Fin (⦋m⦌.len + 1)
h : x ≤ x_1
⊢ LE.le (α := Fin (⦋n⦌.len + 1))
    ((fun (j : Fin (⦋m⦌.len + 1)) ↦ if (↑j : ℕ) < i then 0 else (⟨(↑j : ℕ) - i, ⋯⟩ : Fin (⦋n⦌.len + 1))) x)
    ((fun (j : Fin (⦋m⦌.len + 1)) ↦ if (↑j : ℕ) < i then 0 else (⟨(↑j : ℕ) - i, ⋯⟩ : Fin (⦋n⦌.len + 1))) x_1)

Tactic:
grind [Fin.zero_le]

Premises used: Fin.zero_le
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) < i
⊢ (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter i hi) :
            (a : Fin (m + 1)) → Fin (n + 1))
          j) :
      ℕ) =
    0

Tactic:
simp [σ₀Iter, Hom.mk, ConcreteCategory.hom, Hom.toOrderHom, if_pos hj]

Premises used: CategoryTheory.ConcreteCategory.hom, SimplexCategory.σ₀Iter, if_pos, SimplexCategory.Hom.toOrderHom, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : i ≤ (↑j : ℕ)
dsimp : (↑(if (↑j : ℕ) < i then 0 else (⟨(↑j : ℕ) - i, ⋯⟩ : Fin (n + 1))) : ℕ) = (↑j : ℕ) - i
⊢ (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter i hi) :
            (a : Fin (m + 1)) → Fin (n + 1))
          j) :
      ℕ) =
    (↑j : ℕ) - i

Tactic:
dsimp [σ₀Iter, Hom.mk, ConcreteCategory.hom, Hom.toOrderHom]

Premises used: CategoryTheory.ConcreteCategory.hom, SimplexCategory.σ₀Iter, SimplexCategory.Hom.toOrderHom, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : i ≤ (↑j : ℕ)
⊢ ¬(↑j : ℕ) < i

Tactic:
lia
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : i ≤ (↑j : ℕ)
rw rw₁ : (↑(⟨(↑j : ℕ) - i, ⋯⟩ : Fin (n + 1)) : ℕ) = (↑j : ℕ) - i
⊢ (↑(if (↑j : ℕ) < i then 0 else (⟨(↑j : ℕ) - i, ⋯⟩ : Fin (n + 1))) : ℕ) = (↑j : ℕ) - i

Tactic:
rw [if_neg (by lia)]

Premises used: if_neg
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj : (↑j : ℕ) ≤ i
inl :
  ∀ (hi : n + (↑j : ℕ) = m) (hj : (↑j : ℕ) ≤ (↑j : ℕ)),
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter (↑j : ℕ) hi) :
              (a : Fin (m + 1)) → Fin (n + 1))
            j) :
        ℕ) =
      0
inr :
  ∀ (hj : (↑j : ℕ) < i),
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter i hi) :
              (a : Fin (m + 1)) → Fin (n + 1))
            j) :
        ℕ) =
      0
⊢ (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter i hi) :
            (a : Fin (m + 1)) → Fin (n + 1))
          j) :
      ℕ) =
    0

Tactic:
obtain rfl | hj := hj.eq_or_lt

Premises used: LE.le.eq_or_lt, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n m : ℕ
j : Fin (m + 1)
hi : n + (↑j : ℕ) = m
hj : (↑j : ℕ) ≤ (↑j : ℕ)
inl : (↑j : ℕ) - (↑j : ℕ) = 0
inl₁ inl₂ : Eq (α := ℕ) 0 0
⊢ (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter (↑j : ℕ) hi) :
            (a : Fin (m + 1)) → Fin (n + 1))
          j) :
      ℕ) =
    0

Tactic:
rw [σ₀Iter_coe_eq_of_ge .., tsub_self]

Premises used: tsub_self, SimplexCategory.σ₀Iter_coe_eq_of_ge
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj_1 : (↑j : ℕ) ≤ i
hj : (↑j : ℕ) < i
⊢ (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter i hi) :
            (a : Fin (m + 1)) → Fin (n + 1))
          j) :
      ℕ) =
    0

Tactic:
σ₀Iter_coe_eq_of_lt ..

Premises used: SimplexCategory.σ₀Iter_coe_eq_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
j : Fin (m + 1)
hi : n + i = m
hj_1 : (↑j : ℕ) ≤ i
hj : (↑j : ℕ) < i
⊢ (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter i hi) :
            (a : Fin (m + 1)) → Fin (n + 1))
          j) :
      ℕ) =
    0

Tactic:
exact σ₀Iter_coe_eq_of_lt ..

Premises used: SimplexCategory.σ₀Iter_coe_eq_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
a :
  ∀ (x : Fin (⦋n⦌.len + 1)),
    (↑((Hom.toOrderHom (σ₀Iter 0 ⋯) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ) =
      (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ)
⊢ σ₀Iter 0 ⋯ = 𝟙 ⦋n⦌

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
x : Fin (⦋n⦌.len + 1)
⊢ (↑((Hom.toOrderHom (σ₀Iter 0 ⋯) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ)

Tactic:
simp [σ₀Iter]

Premises used: SimplexCategory.σ₀Iter
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
⊢ Eq (α := ⦋n + 1⦌ ⟶ ⦋n⦌) (σ₀Iter 1 ⋯) (σ 0)

Tactic:
ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
refine :
  ∀ (k : Fin (⦋n + 1⦌.len + 1)),
    Eq (α := Fin (⦋n⦌.len + 1))
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n + 1⦌) (σ₀Iter 1 ⋯) :
            (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          k :
        Fin (⦋n⦌.len + 1))
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n + 1⦌) (σ 0) :
            (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          k :
        Fin (⦋n⦌.len + 1))
⊢ Eq (α := ⦋n + 1⦌ ⟶ ⦋n⦌) (σ₀Iter 1 ⋯) (σ 0)

Tactic:
refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
k : Fin (⦋n + 1⦌.len + 1)
h :
  (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n + 1⦌) (σ₀Iter 1 ⋯) :
            (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          k) :
      ℕ) =
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n + 1⦌) (σ 0) :
            (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          k) :
      ℕ)
⊢ Eq (α := Fin (⦋n⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n + 1⦌) (σ₀Iter 1 ⋯) :
          (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        k :
      Fin (⦋n⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n + 1⦌) (σ 0) :
          (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        k :
      Fin (⦋n⦌.len + 1))

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
k : Fin (⦋n + 1⦌.len + 1)
h :
  (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n + 1⦌) (σ₀Iter 1 ⋯) :
            (a : Fin (n + 1 + 1)) → Fin (n + 1))
          0) :
      ℕ) =
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n + 1⦌) (σ 0) :
            (a : Fin (n + 1 + 1)) → Fin (n + 1))
          0) :
      ℕ)
h₁ :
  ∀ (k : Fin ⦋n + 1⦌.len),
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n + 1⦌) (σ₀Iter 1 ⋯) :
              (a : Fin (n + 1 + 1)) → Fin (n + 1))
            k.succ) :
        ℕ) =
      (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n + 1⦌) (σ 0) :
              (a : Fin (n + 1 + 1)) → Fin (n + 1))
            k.succ) :
        ℕ)
⊢ (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n + 1⦌) (σ₀Iter 1 ⋯) :
            (a : Fin (n + 1 + 1)) → Fin (n + 1))
          k) :
      ℕ) =
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n + 1⦌) (σ 0) :
            (a : Fin (n + 1 + 1)) → Fin (n + 1))
          k) :
      ℕ)

Tactic:
obtain rfl | ⟨k, rfl⟩ := k.eq_zero_or_eq_succ

Premises used: Fin.eq_zero_or_eq_succ, rfl
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
⊢ (↑0 : ℕ) < 1

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
⊢ LE.le (α := Fin (n + 1 + 1)) 0 (Fin.castSucc 0)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
⊢ 0 = (↑(Fin.castPred 0 ⋯) : ℕ)

Tactic:
dsimp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
k : Fin ⦋n + 1⦌.len
h : (↑k.succ : ℕ) - 1 = (↑(Fin.predAbove 0 k.succ) : ℕ)
⊢ (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n + 1⦌) (σ₀Iter 1 ⋯) :
            (a : Fin (n + 1 + 1)) → Fin (n + 1))
          k.succ) :
      ℕ) =
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n + 1⦌) (σ 0) :
            (a : Fin (n + 1 + 1)) → Fin (n + 1))
          k.succ) :
      ℕ)

Tactic:
rw [σ₀Iter_coe_eq_of_ge .., coe_σ]

Premises used: SimplexCategory.coe_σ, SimplexCategory.σ₀Iter_coe_eq_of_ge
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
n : ℕ
k : Fin ⦋n + 1⦌.len
⊢ (↑k.succ : ℕ) - 1 = (↑(Fin.predAbove 0 k.succ) : ℕ)

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
h : n + (i + 1) = m
⊢ σ₀Iter (i + 1) h = σ₀Iter i ⋯ ≫ σ 0

Tactic:
ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
h : n + (i + 1) = m
refine :
  ∀ (k : Fin (⦋m⦌.len + 1)),
    Eq (α := Fin (⦋n⦌.len + 1))
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter (i + 1) h) :
            (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          k :
        Fin (⦋n⦌.len + 1))
      ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter i ⋯ ≫ σ 0) :
            (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          k :
        Fin (⦋n⦌.len + 1))
⊢ σ₀Iter (i + 1) h = σ₀Iter i ⋯ ≫ σ 0

Tactic:
refine ConcreteCategory.hom_ext _ _ (fun k ↦ ?_)

Premises used: CategoryTheory.ConcreteCategory.hom_ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
h₁ :
  (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter (i + 1) h) :
            (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          k) :
      ℕ) =
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter i ⋯ ≫ σ 0) :
            (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          k) :
      ℕ)
⊢ Eq (α := Fin (⦋n⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter (i + 1) h) :
          (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        k :
      Fin (⦋n⦌.len + 1))
    ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
            fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter i ⋯ ≫ σ 0) :
          (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        k :
      Fin (⦋n⦌.len + 1))

Tactic:
ext
-- Module: Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
Goal:
i n m : ℕ
h : n + (i + 1) = m
k : Fin (⦋m⦌.len + 1)
h₁ :
  (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter (i + 1) h) :
            (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          k) :
      ℕ) =
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (X := ⦋n + 1⦌) (σ 0) :
            (a : Fin (n + 1 + 1)) → Fin (n + 1))
          ((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
                fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter i ⋯) :
              (a : Fin (m + 1)) → Fin (n + 1 + 1))
            k)) :
      ℕ)
⊢ (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter (i + 1) h) :
            (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          k) :
      ℕ) =
    (↑((ConcreteCategory.hom (FC := fun (i j : SimplexCategory) ↦ Fin (i.len + 1) →o Fin (j.len + 1)) (CC :=
              fun (X : SimplexCategory) ↦ Fin (X.len + 1)) (σ₀Iter i ⋯ ≫ σ 0) :
            (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          k) :
      ℕ)

Tactic:
rw [dsimp% ConcreteCategory.comp_apply (σ₀Iter i) (σ 0)]

Premises used: CategoryTheory.ConcreteCategory.comp_apply, SimplexCategory.σ₀Iter, SimplexCategory.σ, OfNat.ofNat