awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : i ≤ k
hjk : j.castSucc < k
⊢ i ≤ (j.predAbove k).castSucc
have a : i < k
Tactic: rw [Fin.le_castSucc_iff, Fin.predAbove_of_castSucc_lt _ _ hjk, Fin.succ_pred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
⊢ j.succ.predAbove (i.castSucc.succAbove k) = i.succAbove (j.predAbove k)
have a : j.succ.predAbove k.castSucc = i.succAbove (j.predAbove k)
Tactic: rw [Fin.succAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hik)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
⊢ j.succ.predAbove k.castSucc = i.succAbove (j.predAbove k)
have hjk : k < j.castSucc
Tactic: have hjk := H.trans_lt' hik
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : i ≤ j.castSucc
k : Fin (⦋n + 1⦌.len + 1)
hik : k < i
hjk : k < j.castSucc
⊢ j.succ.predAbove k.castSucc = i.succAbove (j.predAbove k)
have a : (k.castPred sorry).castSucc < i
Tactic: rw [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr
      (hjk.trans Fin.castSucc_lt_succ).le),
      Fin.predAbove_of_le_castSucc _ _ hjk.le, Fin.castPred_castSucc, Fin.succAbove_of_castSucc_lt,
      Fin.castSucc_castPred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ δ i.castSucc ≫ σ i = 𝟙 ⦋n⦌
have rcases : ∀ (i : ℕ) (hi : i < n + 1), δ (⟨i, hi⟩ : Fin (n + 1)).castSucc ≫ σ (⟨i, hi⟩ : Fin (n + 1)) = 𝟙 ⦋n⦌
Tactic: rcases i with ⟨i, hi⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
hi : i < n + 1
⊢ δ (⟨i, hi⟩ : Fin (n + 1)).castSucc ≫ σ (⟨i, hi⟩ : Fin (n + 1)) = 𝟙 ⦋n⦌
have a : ∀ (j : ℕ) (hj : j < ⦋n⦌.len + 1),
  (↑((Hom.toOrderHom (δ (⟨i, hi⟩ : Fin (n + 1)).castSucc ≫ σ (⟨i, hi⟩ : Fin (n + 1))) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          (⟨j, hj⟩ : Fin (⦋n⦌.len + 1))) :
      ℕ) =
    (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) ⟨j, hj⟩) : ℕ)
Tactic: ext ⟨j, hj⟩
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
⊢ (↑((Hom.toOrderHom (δ (⟨i, hi⟩ : Fin (n + 1)).castSucc ≫ σ (⟨i, hi⟩ : Fin (n + 1))) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          (⟨j, hj⟩ : Fin (⦋n⦌.len + 1))) :
      ℕ) =
    (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) ⟨j, hj⟩) : ℕ)
have a : (↑(if h :
          (⟨i, sorry⟩ : Fin (n + 1 + 1)) <
            if (⟨j, sorry⟩ : Fin (n + 1 + 1)) < (⟨i, sorry⟩ : Fin (n + 1 + 1)) then (⟨j, sorry⟩ : Fin (n + 1 + 1))
            else (⟨j + 1, sorry⟩ : Fin (n + 1 + 1)) then
        (if (⟨j, sorry⟩ : Fin (n + 1 + 1)) < (⟨i, sorry⟩ : Fin (n + 1 + 1)) then (⟨j, sorry⟩ : Fin (n + 1 + 1))
            else (⟨j + 1, sorry⟩ : Fin (n + 1 + 1))).pred
          sorry
      else
        (if (⟨j, sorry⟩ : Fin (n + 1 + 1)) < (⟨i, sorry⟩ : Fin (n + 1 + 1)) then (⟨j, sorry⟩ : Fin (n + 1 + 1))
            else (⟨j + 1, sorry⟩ : Fin (n + 1 + 1))).castPred
          sorry) :
    ℕ) =
  j
Tactic: dsimp [σ, δ, Fin.predAbove, Fin.succAbove]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
⊢ (↑(if h :
            (⟨i, ⋯⟩ : Fin (n + 1 + 1)) <
              if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)) then
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).pred
            ⋯
        else
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).castPred
            ⋯) :
      ℕ) =
    j
have a : (if h : i < if j < i then j else j + 1 then (if j < i then j else j + 1) - 1
  else (↑((if j < i then (⟨j, sorry⟩ : Fin (n + 1 + 1)) else (⟨j + 1, sorry⟩ : Fin (n + 1 + 1))).castPred sorry) : ℕ)) =
  j
Tactic: simp only [Fin.lt_def, Fin.dite_val, Fin.ite_val, Fin.val_pred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
⊢ (if h : i < if j < i then j else j + 1 then (if j < i then j else j + 1) - 1
    else (↑((if j < i then (⟨j, ⋯⟩ : Fin (n + 1 + 1)) else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).castPred ⋯) : ℕ)) =
    j
have pos : j < i → i < j → j - 1 = j
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
pos : j < i → i < j → j - 1 = j
⊢ (if h : i < if j < i then j else j + 1 then (if j < i then j else j + 1) - 1
    else (↑((if j < i then (⟨j, ⋯⟩ : Fin (n + 1 + 1)) else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).castPred ⋯) : ℕ)) =
    j
have neg : ∀ (h : j < i) (h_1 : ¬i < j), (↑((⟨j, sorry⟩ : Fin (n + 1 + 1)).castPred sorry) : ℕ) = j
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
pos : j < i → i < j → j - 1 = j
neg : ∀ (h : j < i) (h_1 : ¬i < j), (↑((⟨j, ⋯⟩ : Fin (n + 1 + 1)).castPred ⋯) : ℕ) = j
⊢ (if h : i < if j < i then j else j + 1 then (if j < i then j else j + 1) - 1
    else (↑((if j < i then (⟨j, ⋯⟩ : Fin (n + 1 + 1)) else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).castPred ⋯) : ℕ)) =
    j
have pos₁ : ¬j < i → i < j + 1 → j + 1 - 1 = j
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
pos : j < i → i < j → j - 1 = j
neg : ∀ (h : j < i) (h_1 : ¬i < j), (↑((⟨j, ⋯⟩ : Fin (n + 1 + 1)).castPred ⋯) : ℕ) = j
pos₁ : ¬j < i → i < j + 1 → j + 1 - 1 = j
⊢ (if h : i < if j < i then j else j + 1 then (if j < i then j else j + 1) - 1
    else (↑((if j < i then (⟨j, ⋯⟩ : Fin (n + 1 + 1)) else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).castPred ⋯) : ℕ)) =
    j
have neg₁ : ∀ (h : ¬j < i) (h_1 : ¬i < j + 1), (↑((⟨j + 1, sorry⟩ : Fin (n + 1 + 1)).castPred sorry) : ℕ) = j
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
hi : i < n + 1
j : ℕ
hj : j < ⦋n⦌.len + 1
h : ¬j < i
h_1 : ¬i < j + 1
⊢ (↑((⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)).castPred ⋯) : ℕ) = j
have neg : False
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.castSucc
⊢ δ j ≫ σ i = 𝟙 ⦋n⦌
have subst : δ i.castSucc ≫ σ i = 𝟙 ⦋n⦌
Tactic: subst H
Cleared hypotheses: j, H
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ δ i.castSucc ≫ σ i = 𝟙 ⦋n⦌
have rw : 𝟙 ⦋n⦌ = 𝟙 ⦋n⦌
Tactic: rw [δ_comp_σ_self]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ δ i.succ ≫ σ i = 𝟙 ⦋n⦌
have a : ∀ (j : Fin (⦋n⦌.len + 1)),
  (↑((Hom.toOrderHom (δ i.succ ≫ σ i) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) j) : ℕ) =
    (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) j) : ℕ)
Tactic: ext j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin (⦋n⦌.len + 1)
⊢ (↑((Hom.toOrderHom (δ i.succ ≫ σ i) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) j) : ℕ) =
    (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) j) : ℕ)
have a : ∀ (i : ℕ) (isLt : i < n + 1),
  (↑((Hom.toOrderHom (δ (⟨i, isLt⟩ : Fin (n + 1)).succ ≫ σ (⟨i, isLt⟩ : Fin (n + 1))) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          j) :
      ℕ) =
    (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) j) : ℕ)
Tactic: rcases i with ⟨i, _⟩
Cleared hypotheses: i
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
j : Fin (⦋n⦌.len + 1)
i : ℕ
isLt : i < n + 1
⊢ (↑((Hom.toOrderHom (δ (⟨i, isLt⟩ : Fin (n + 1)).succ ≫ σ (⟨i, isLt⟩ : Fin (n + 1))) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          j) :
      ℕ) =
    (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) j) : ℕ)
have a : ∀ (j : ℕ) (isLt_1 : j < ⦋n⦌.len + 1),
  (↑((Hom.toOrderHom (δ (⟨i, isLt⟩ : Fin (n + 1)).succ ≫ σ (⟨i, isLt⟩ : Fin (n + 1))) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          (⟨j, isLt_1⟩ : Fin (⦋n⦌.len + 1))) :
      ℕ) =
    (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) ⟨j, isLt_1⟩) : ℕ)
Tactic: rcases j with ⟨j, _⟩
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
⊢ (↑((Hom.toOrderHom (δ (⟨i, isLt⟩ : Fin (n + 1)).succ ≫ σ (⟨i, isLt⟩ : Fin (n + 1))) :
            (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1))
          (⟨j, isLt_1⟩ : Fin (⦋n⦌.len + 1))) :
      ℕ) =
    (↑((Hom.toOrderHom (𝟙 ⦋n⦌) : (a : Fin (⦋n⦌.len + 1)) → Fin (⦋n⦌.len + 1)) ⟨j, isLt_1⟩) : ℕ)
have a : (↑(if h :
          (⟨i, sorry⟩ : Fin (n + 1 + 1)) <
            if (⟨j, sorry⟩ : Fin (n + 1 + 1)) < (⟨i + 1, sorry⟩ : Fin (n + 1 + 1)) then (⟨j, sorry⟩ : Fin (n + 1 + 1))
            else (⟨j + 1, sorry⟩ : Fin (n + 1 + 1)) then
        (if (⟨j, sorry⟩ : Fin (n + 1 + 1)) < (⟨i + 1, sorry⟩ : Fin (n + 1 + 1)) then (⟨j, sorry⟩ : Fin (n + 1 + 1))
            else (⟨j + 1, sorry⟩ : Fin (n + 1 + 1))).pred
          sorry
      else
        (if (⟨j, sorry⟩ : Fin (n + 1 + 1)) < (⟨i + 1, sorry⟩ : Fin (n + 1 + 1)) then (⟨j, sorry⟩ : Fin (n + 1 + 1))
            else (⟨j + 1, sorry⟩ : Fin (n + 1 + 1))).castPred
          sorry) :
    ℕ) =
  j
Tactic: dsimp [δ, σ, Fin.succAbove, Fin.predAbove]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
⊢ (↑(if h :
            (⟨i, ⋯⟩ : Fin (n + 1 + 1)) <
              if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)) then
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).pred
            ⋯
        else
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).castPred
            ⋯) :
      ℕ) =
    j
have pos : ∀ (h : (⟨j, sorry⟩ : Fin (n + 1 + 1)) < ⟨i + 1, sorry⟩) (h_1 : (⟨i, sorry⟩ : Fin (n + 1 + 1)) < ⟨j, sorry⟩),
  (↑((⟨j, sorry⟩ : Fin (n + 1 + 1)).pred sorry) : ℕ) = j
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
pos :
  ∀ (h : (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩) (h_1 : (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j, ⋯⟩),
    (↑((⟨j, ⋯⟩ : Fin (n + 1 + 1)).pred ⋯) : ℕ) = j
⊢ (↑(if h :
            (⟨i, ⋯⟩ : Fin (n + 1 + 1)) <
              if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)) then
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).pred
            ⋯
        else
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).castPred
            ⋯) :
      ℕ) =
    j
have neg : ∀ (h : (⟨j, sorry⟩ : Fin (n + 1 + 1)) < ⟨i + 1, sorry⟩) (h_1 : ¬(⟨i, sorry⟩ : Fin (n + 1 + 1)) < ⟨j, sorry⟩),
  (↑((⟨j, sorry⟩ : Fin (n + 1 + 1)).castPred sorry) : ℕ) = j
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
pos :
  ∀ (h : (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩) (h_1 : (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j, ⋯⟩),
    (↑((⟨j, ⋯⟩ : Fin (n + 1 + 1)).pred ⋯) : ℕ) = j
neg :
  ∀ (h : (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩) (h_1 : ¬(⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j, ⋯⟩),
    (↑((⟨j, ⋯⟩ : Fin (n + 1 + 1)).castPred ⋯) : ℕ) = j
⊢ (↑(if h :
            (⟨i, ⋯⟩ : Fin (n + 1 + 1)) <
              if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)) then
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).pred
            ⋯
        else
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).castPred
            ⋯) :
      ℕ) =
    j
have pos₁ : ∀ (h : ¬(⟨j, sorry⟩ : Fin (n + 1 + 1)) < ⟨i + 1, sorry⟩) (h_1 : (⟨i, sorry⟩ : Fin (n + 1 + 1)) < ⟨j + 1, sorry⟩),
  (↑((⟨j + 1, sorry⟩ : Fin (n + 1 + 1)).pred sorry) : ℕ) = j
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
pos :
  ∀ (h : (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩) (h_1 : (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j, ⋯⟩),
    (↑((⟨j, ⋯⟩ : Fin (n + 1 + 1)).pred ⋯) : ℕ) = j
neg :
  ∀ (h : (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩) (h_1 : ¬(⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j, ⋯⟩),
    (↑((⟨j, ⋯⟩ : Fin (n + 1 + 1)).castPred ⋯) : ℕ) = j
pos₁ :
  ∀ (h : ¬(⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩) (h_1 : (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j + 1, ⋯⟩),
    (↑((⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)).pred ⋯) : ℕ) = j
⊢ (↑(if h :
            (⟨i, ⋯⟩ : Fin (n + 1 + 1)) <
              if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)) then
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).pred
            ⋯
        else
          (if (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < (⟨i + 1, ⋯⟩ : Fin (n + 1 + 1)) then (⟨j, ⋯⟩ : Fin (n + 1 + 1))
              else (⟨j + 1, ⋯⟩ : Fin (n + 1 + 1))).castPred
            ⋯) :
      ℕ) =
    j
have neg₁ : ∀ (h : ¬(⟨j, sorry⟩ : Fin (n + 1 + 1)) < ⟨i + 1, sorry⟩) (h_1 : ¬(⟨i, sorry⟩ : Fin (n + 1 + 1)) < ⟨j + 1, sorry⟩),
  (↑((⟨j + 1, sorry⟩ : Fin (n + 1 + 1)).castPred sorry) : ℕ) = j
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
h : (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩
h_1 : (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j, ⋯⟩
⊢ (↑((⟨j, ⋯⟩ : Fin (n + 1 + 1)).pred ⋯) : ℕ) = j
have pos : j - 1 = j
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
h : ¬(⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩
h_1 : ¬(⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j + 1, ⋯⟩
⊢ (↑((⟨j + 1, ⋯⟩ : Fin (n + 1 + 1)).castPred ⋯) : ℕ) = j
have neg : False
Tactic: simp
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
h : (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩
h_1 : (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j, ⋯⟩
⊢ j - 1 = j
have h : j < i + 1
Tactic: simp at *
Cleared hypotheses: h, h_1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
h_1 : (⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩
h_2 : (⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j, ⋯⟩
h : j < i + 1
⊢ j - 1 = j
have h₁ : i < j
Tactic: simp at *
Cleared hypotheses: h_1, h_2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
h : ¬(⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩
h_1 : ¬(⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j + 1, ⋯⟩
⊢ False
have h : i + 1 ≤ j
Tactic: simp at *
Cleared hypotheses: h, h_1
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
n i : ℕ
isLt : i < n + 1
j : ℕ
isLt_1 : j < ⦋n⦌.len + 1
h_1 : ¬(⟨j, ⋯⟩ : Fin (n + 1 + 1)) < ⟨i + 1, ⋯⟩
h_2 : ¬(⟨i, ⋯⟩ : Fin (n + 1 + 1)) < ⟨j + 1, ⋯⟩
h : i + 1 ≤ j
⊢ False
have h₁ : j + 1 ≤ i
Tactic: simp at *
Cleared hypotheses: h_1, h_2
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
j : Fin (n + 2)
i : Fin (n + 1)
H : j = i.succ
⊢ δ j ≫ σ i = 𝟙 ⦋n⦌
have subst : δ i.succ ≫ σ i = 𝟙 ⦋n⦌
Tactic: subst H
Cleared hypotheses: j, H
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ δ i.succ ≫ σ i = 𝟙 ⦋n⦌
have rw : 𝟙 ⦋n⦌ = 𝟙 ⦋n⦌
Tactic: rw [δ_comp_σ_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
⊢ δ i.succ ≫ σ j.castSucc = σ j ≫ δ i
have a : ∀ (k : Fin (⦋n + 1⦌.len + 1)),
  Eq (α := Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom (δ i.succ ≫ σ j.castSucc) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k :
      Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom (σ j ≫ δ i) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
Tactic: ext k : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
⊢ Eq (α := Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom (δ i.succ ≫ σ j.castSucc) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k :
      Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom (σ j ≫ δ i) : (a : Fin (⦋n + 1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
have a : j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)
Tactic: dsimp [δ, σ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
⊢ j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)
have a : ∀ (hik : k ≤ i), j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)
Tactic: rcases le_or_gt k i with (hik | hik)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
a : ∀ (hik : k ≤ i), j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)
⊢ j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)
have a₁ : ∀ (hik : i < k), j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)
Tactic: rcases le_or_gt k i with (hik | hik)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
⊢ j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)
have a : j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)
Tactic: rw [Fin.succAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_succ_iff.mpr hik)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)
have a : ∀ (hjk : k ≤ j.castSucc), j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)
Tactic: rcases le_or_gt k (j.castSucc) with (hjk | hjk)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
a : ∀ (hjk : k ≤ j.castSucc), j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)
have a₁ : ∀ (hjk : j.castSucc < k), j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)
Tactic: rcases le_or_gt k (j.castSucc) with (hjk | hjk)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : k ≤ j.castSucc
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)
have a : (k.castPred sorry).castSucc < i
Tactic: rw [Fin.predAbove_of_le_castSucc _ _
      (Fin.castSucc_le_castSucc_iff.mpr hjk), Fin.castPred_castSucc,
      Fin.predAbove_of_le_castSucc _ _ hjk, Fin.succAbove_of_castSucc_lt, Fin.castSucc_castPred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : k ≤ j.castSucc
⊢ (k.castPred ⋯).castSucc < i
have a : k < i
Tactic: rw [Fin.castSucc_castPred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : j.castSucc < k
⊢ j.castSucc.predAbove k.castSucc = i.succAbove (j.predAbove k)
have a : (k.pred sorry).castSucc < i
Tactic: rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hjk),
      Fin.predAbove_of_castSucc_lt _ _ hjk, Fin.succAbove_of_castSucc_lt,
      Fin.castSucc_pred_eq_pred_castSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : k ≤ i
hjk : j.castSucc < k
⊢ (k.pred ⋯).castSucc < i
have a : (k.pred sorry).succ ≤ i
Tactic: rwa [Fin.castSucc_lt_iff_succ_le, Fin.succ_pred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
⊢ j.castSucc.predAbove (i.succ.succAbove k) = i.succAbove (j.predAbove k)
have a : j.castSucc.predAbove k.succ = i.succAbove (j.predAbove k)
Tactic: rw [Fin.succAbove_of_le_castSucc _ _ (Fin.succ_le_castSucc_iff.mpr hik)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (hypothesis)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
⊢ j.castSucc.predAbove k.succ = i.succAbove (j.predAbove k)
have hjk : j.castSucc < k
Tactic: have hjk := H.trans hik
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
H : j.castSucc < i
k : Fin (⦋n + 1⦌.len + 1)
hik : i < k
hjk : j.castSucc < k
⊢ j.castSucc.predAbove k.succ = i.succAbove (j.predAbove k)
have a : i ≤ (k.pred sorry).castSucc
Tactic: rw [Fin.predAbove_of_castSucc_lt _ _ hjk, Fin.predAbove_of_castSucc_lt _ _
      (Fin.castSucc_lt_succ_iff.mpr hjk.le),
    Fin.pred_succ, Fin.succAbove_of_le_castSucc, Fin.succ_pred]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
⊢ δ i ≫ σ j = σ (j.castLT ⋯) ≫ δ (i.pred ⋯)
have rw : δ i ≫ σ j = δ (i.pred sorry).succ ≫ σ (Fin.castSucc (j.castLT sorry))
Tactic: rw [← δ_comp_σ_of_gt]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin (n + 3)
j : Fin (n + 2)
H : j.succ < i
rw : δ i ≫ σ j = δ (i.pred ⋯).succ ≫ σ (Fin.castSucc (j.castLT ⋯))
⊢ δ i ≫ σ j = σ (j.castLT ⋯) ≫ δ (i.pred ⋯)
have rw₁ : Fin.castSucc (j.castLT sorry) < i.pred sorry
Tactic: rw [← δ_comp_σ_of_gt]