awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ σ i.castSucc ≫ σ j = σ j.succ ≫ σ i
have a : ∀ (k : Fin (⦋n + 1 + 1⦌.len + 1)),
  Eq (α := Fin (⦋n⦌.len + 1))
    ((Hom.toOrderHom (σ i.castSucc ≫ σ j) : (a : Fin (⦋n + 1 + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1)) k : Fin (⦋n⦌.len + 1))
    ((Hom.toOrderHom (σ j.succ ≫ σ i) : (a : Fin (⦋n + 1 + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1)) k : Fin (⦋n⦌.len + 1))
Tactic: ext k : 3
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (⦋n + 1 + 1⦌.len + 1)
⊢ Eq (α := Fin (⦋n⦌.len + 1))
    ((Hom.toOrderHom (σ i.castSucc ≫ σ j) : (a : Fin (⦋n + 1 + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1)) k : Fin (⦋n⦌.len + 1))
    ((Hom.toOrderHom (σ j.succ ≫ σ i) : (a : Fin (⦋n + 1 + 1⦌.len + 1)) → Fin (⦋n⦌.len + 1)) k : Fin (⦋n⦌.len + 1))
have a : j.predAbove (i.castSucc.predAbove k) = i.predAbove (j.succ.predAbove k)
Tactic: dsimp [σ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
⊢ j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)
have a : ∀ (h : i ≤ k), j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)
Tactic: rcases le_or_gt i k with (h | h)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
a : ∀ (h : i ≤ k), j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)
⊢ j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)
have a₁ : ∀ (h : k < i), j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)
Tactic: rcases le_or_gt i k with (h | h)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)
have a : j.predAbove k.castSucc = i.predAbove (j.predAbove k.castSucc).succ
Tactic: simp_rw [Fin.predAbove_of_castSucc_lt i.castSucc _ (Fin.castSucc_lt_castSucc_iff.mpr
        (Fin.castSucc_lt_succ_iff.mpr h)), ← Fin.succ_castSucc, Fin.pred_succ,
        Fin.succ_predAbove_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ j.predAbove k.castSucc = i.predAbove (j.predAbove k.castSucc).succ
have rw : i ≤ j.predAbove k.castSucc
Tactic: rw [Fin.predAbove_of_castSucc_lt i _ (Fin.castSucc_lt_succ_iff.mpr _), Fin.pred_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
⊢ i ≤ j.predAbove k.castSucc
have inl : ∀ (hkj : k ≤ j), i ≤ j.predAbove k.castSucc
Tactic: rcases le_or_gt k j with (hkj | hkj)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
inl : ∀ (hkj : k ≤ j), i ≤ j.predAbove k.castSucc
⊢ i ≤ j.predAbove k.castSucc
have inr : ∀ (hkj : j < k), i ≤ j.predAbove k.castSucc
Tactic: rcases le_or_gt k j with (hkj | hkj)
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : k ≤ j
⊢ i ≤ j.predAbove k.castSucc
have inl : i ≤ k.castSucc.castPred sorry
Tactic: rwa [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hkj),
          Fin.castPred_castSucc]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : i ≤ k
hkj : j < k
⊢ i ≤ j.predAbove k.castSucc
have inr : i < k
Tactic: rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hkj),
          Fin.le_pred_iff,
          Fin.succ_le_castSucc_iff]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
⊢ j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)
have a : j.predAbove k.succ = i.predAbove (j.predAbove k.castSucc).succ
Tactic: simp_rw [Fin.predAbove_of_le_castSucc i.castSucc _ (Fin.castSucc_le_castSucc_iff.mpr
        (Fin.succ_le_castSucc_iff.mpr h)), Fin.castPred_castSucc, ← Fin.succ_castSucc,
        Fin.succ_predAbove_succ]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
⊢ j.predAbove k.succ = i.predAbove (j.predAbove k.castSucc).succ
have a : j.predAbove k.succ = i.predAbove (k.castSucc.castPred sorry).succ
Tactic: rw [Fin.predAbove_of_le_castSucc _ k.castSucc
        (Fin.castSucc_le_castSucc_iff.mpr (h.le.trans H)),
        Fin.castPred_castSucc, Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr (H.trans_lt' h)), Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr h)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
a : j.predAbove k.succ = i.predAbove (k.castSucc.castPred ⋯).succ
⊢ j.predAbove k.succ = i.predAbove (j.predAbove k.castSucc).succ
have a₁ : j.predAbove k.succ = i.predAbove k.succ
Tactic: rw [Fin.predAbove_of_le_castSucc _ k.castSucc
        (Fin.castSucc_le_castSucc_iff.mpr (h.le.trans H)),
        Fin.castPred_castSucc, Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr (H.trans_lt' h)), Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr h)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
a : j.predAbove k.succ = i.predAbove (k.castSucc.castPred ⋯).succ
a₁ : j.predAbove k.succ = i.predAbove k.succ
⊢ j.predAbove k.succ = i.predAbove (j.predAbove k.castSucc).succ
have a₂ : k.succ.castPred sorry = i.predAbove k.succ
Tactic: rw [Fin.predAbove_of_le_castSucc _ k.castSucc
        (Fin.castSucc_le_castSucc_iff.mpr (h.le.trans H)),
        Fin.castPred_castSucc, Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr (H.trans_lt' h)), Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr h)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (n + 1)
h : k < i
a : j.predAbove k.succ = i.predAbove (k.castSucc.castPred ⋯).succ
a₁ : j.predAbove k.succ = i.predAbove k.succ
a₂ : k.succ.castPred ⋯ = i.predAbove k.succ
⊢ j.predAbove k.succ = i.predAbove (j.predAbove k.castSucc).succ
have a₃ : k.succ.castPred sorry = k.succ.castPred sorry
Tactic: rw [Fin.predAbove_of_le_castSucc _ k.castSucc
        (Fin.castSucc_le_castSucc_iff.mpr (h.le.trans H)),
        Fin.castPred_castSucc, Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr (H.trans_lt' h)), Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr h)]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin ⦋n + 1 + 1⦌.len
⊢ j.predAbove (i.castSucc.predAbove k.castSucc) = i.predAbove (j.succ.predAbove k.castSucc)
have a : j.predAbove (i.castSucc.predAbove (Fin.castSucc 0)) = i.predAbove (j.succ.predAbove (Fin.castSucc 0))
Tactic: cases k using Fin.cases with
    | zero =>
      simp
    | succ k =>
      rcases le_or_gt i k with (h | h)
      · simp_rw [Fin.predAbove_of_castSucc_lt i.castSucc _ (Fin.castSucc_lt_castSucc_iff.mpr
        (Fin.castSucc_lt_succ_iff.mpr h)), ← Fin.succ_castSucc, Fin.pred_succ,
        Fin.succ_predAbove_succ]
        rw [Fin.predAbove_of_castSucc_lt i _ (Fin.castSucc_lt_succ_iff.mpr _), Fin.pred_succ]
        rcases le_or_gt k j with (hkj | hkj)
        · rwa [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hkj),
          Fin.castPred_castSucc]
        · rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hkj),
          Fin.le_pred_iff,
          Fin.succ_le_castSucc_iff]
          exact H.trans_lt hkj
      · simp_rw [Fin.predAbove_of_le_castSucc i.castSucc _ (Fin.castSucc_le_castSucc_iff.mpr
        (Fin.succ_le_castSucc_iff.mpr h)), Fin.castPred_castSucc, ← Fin.succ_castSucc,
        Fin.succ_predAbove_succ]
        rw [Fin.predAbove_of_le_castSucc _ k.castSucc
        (Fin.castSucc_le_castSucc_iff.mpr (h.le.trans H)),
        Fin.castPred_castSucc, Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr (H.trans_lt' h)), Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr h)]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin ⦋n + 1 + 1⦌.len
a : j.predAbove (i.castSucc.predAbove (Fin.castSucc 0)) = i.predAbove (j.succ.predAbove (Fin.castSucc 0))
⊢ j.predAbove (i.castSucc.predAbove k.castSucc) = i.predAbove (j.succ.predAbove k.castSucc)
have a₁ : ∀ (k : Fin (n + 1)), j.predAbove (i.castSucc.predAbove k.succ.castSucc) = i.predAbove (j.succ.predAbove k.succ.castSucc)
Tactic: cases k using Fin.cases with
    | zero =>
      simp
    | succ k =>
      rcases le_or_gt i k with (h | h)
      · simp_rw [Fin.predAbove_of_castSucc_lt i.castSucc _ (Fin.castSucc_lt_castSucc_iff.mpr
        (Fin.castSucc_lt_succ_iff.mpr h)), ← Fin.succ_castSucc, Fin.pred_succ,
        Fin.succ_predAbove_succ]
        rw [Fin.predAbove_of_castSucc_lt i _ (Fin.castSucc_lt_succ_iff.mpr _), Fin.pred_succ]
        rcases le_or_gt k j with (hkj | hkj)
        · rwa [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hkj),
          Fin.castPred_castSucc]
        · rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hkj),
          Fin.le_pred_iff,
          Fin.succ_le_castSucc_iff]
          exact H.trans_lt hkj
      · simp_rw [Fin.predAbove_of_le_castSucc i.castSucc _ (Fin.castSucc_le_castSucc_iff.mpr
        (Fin.succ_le_castSucc_iff.mpr h)), Fin.castPred_castSucc, ← Fin.succ_castSucc,
        Fin.succ_predAbove_succ]
        rw [Fin.predAbove_of_le_castSucc _ k.castSucc
        (Fin.castSucc_le_castSucc_iff.mpr (h.le.trans H)),
        Fin.castPred_castSucc, Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr (H.trans_lt' h)), Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr h)]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (⦋n + 1 + 1⦌.len + 1)
⊢ j.predAbove (i.castSucc.predAbove k) = i.predAbove (j.succ.predAbove k)
have a : j.predAbove (i.castSucc.predAbove (Fin.last ⦋n + 1 + 1⦌.len)) =
  i.predAbove (j.succ.predAbove (Fin.last ⦋n + 1 + 1⦌.len))
Tactic: cases k using Fin.lastCases with
  | last => simp only [len_mk, Fin.predAbove_right_last]
  | cast k =>
    cases k using Fin.cases with
    | zero =>
      simp
    | succ k =>
      rcases le_or_gt i k with (h | h)
      · simp_rw [Fin.predAbove_of_castSucc_lt i.castSucc _ (Fin.castSucc_lt_castSucc_iff.mpr
        (Fin.castSucc_lt_succ_iff.mpr h)), ← Fin.succ_castSucc, Fin.pred_succ,
        Fin.succ_predAbove_succ]
        rw [Fin.predAbove_of_castSucc_lt i _ (Fin.castSucc_lt_succ_iff.mpr _), Fin.pred_succ]
        rcases le_or_gt k j with (hkj | hkj)
        · rwa [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hkj),
          Fin.castPred_castSucc]
        · rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hkj),
          Fin.le_pred_iff,
          Fin.succ_le_castSucc_iff]
          exact H.trans_lt hkj
      · simp_rw [Fin.predAbove_of_le_castSucc i.castSucc _ (Fin.castSucc_le_castSucc_iff.mpr
        (Fin.succ_le_castSucc_iff.mpr h)), Fin.castPred_castSucc, ← Fin.succ_castSucc,
        Fin.succ_predAbove_succ]
        rw [Fin.predAbove_of_le_castSucc _ k.castSucc
        (Fin.castSucc_le_castSucc_iff.mpr (h.le.trans H)),
        Fin.castPred_castSucc, Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr (H.trans_lt' h)), Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr h)]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
k : Fin (⦋n + 1 + 1⦌.len + 1)
a :
  j.predAbove (i.castSucc.predAbove (Fin.last ⦋n + 1 + 1⦌.len)) =
    i.predAbove (j.succ.predAbove (Fin.last ⦋n + 1 + 1⦌.len))
⊢ j.predAbove (i.castSucc.predAbove k) = i.predAbove (j.succ.predAbove k)
have a₁ : ∀ (k : Fin ⦋n + 1 + 1⦌.len), j.predAbove (i.castSucc.predAbove k.castSucc) = i.predAbove (j.succ.predAbove k.castSucc)
Tactic: cases k using Fin.lastCases with
  | last => simp only [len_mk, Fin.predAbove_right_last]
  | cast k =>
    cases k using Fin.cases with
    | zero =>
      simp
    | succ k =>
      rcases le_or_gt i k with (h | h)
      · simp_rw [Fin.predAbove_of_castSucc_lt i.castSucc _ (Fin.castSucc_lt_castSucc_iff.mpr
        (Fin.castSucc_lt_succ_iff.mpr h)), ← Fin.succ_castSucc, Fin.pred_succ,
        Fin.succ_predAbove_succ]
        rw [Fin.predAbove_of_castSucc_lt i _ (Fin.castSucc_lt_succ_iff.mpr _), Fin.pred_succ]
        rcases le_or_gt k j with (hkj | hkj)
        · rwa [Fin.predAbove_of_le_castSucc _ _ (Fin.castSucc_le_castSucc_iff.mpr hkj),
          Fin.castPred_castSucc]
        · rw [Fin.predAbove_of_castSucc_lt _ _ (Fin.castSucc_lt_castSucc_iff.mpr hkj),
          Fin.le_pred_iff,
          Fin.succ_le_castSucc_iff]
          exact H.trans_lt hkj
      · simp_rw [Fin.predAbove_of_le_castSucc i.castSucc _ (Fin.castSucc_le_castSucc_iff.mpr
        (Fin.succ_le_castSucc_iff.mpr h)), Fin.castPred_castSucc, ← Fin.succ_castSucc,
        Fin.succ_predAbove_succ]
        rw [Fin.predAbove_of_le_castSucc _ k.castSucc
        (Fin.castSucc_le_castSucc_iff.mpr (h.le.trans H)),
        Fin.castPred_castSucc, Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr (H.trans_lt' h)), Fin.predAbove_of_le_castSucc _ k.succ
        (Fin.succ_le_castSucc_iff.mpr h)]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
j : Fin (n + 2)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k ≠ j
⊢ factor_δ f j ≫ δ j = f
have a : ∀ (k : Fin (⦋m⦌.len + 1)),
  Eq (α := Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom (factor_δ f j ≫ δ j) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom f : (a : Fin (⦋m⦌.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:
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
j : Fin (n + 2)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k ≠ j
k : Fin (⦋m⦌.len + 1)
⊢ Eq (α := Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom (factor_δ f j ≫ δ j) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
have a : ∀
  (hj :
    ∀ (k : Fin (m + 1)),
      Ne (α := Fin (⦋n + 1⦌.len + 1))
        ((Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
        (0 : Fin (n + 1 + 1))),
  Eq (α := Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom (factor_δ f 0 ≫ δ 0) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
Tactic: cases j using Fin.cases
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
m n : ℕ
f : ⦋m⦌ ⟶ ⦋n + 1⦌
j : Fin (n + 2)
hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k ≠ j
k : Fin (⦋m⦌.len + 1)
a :
  ∀
    (hj :
      ∀ (k : Fin (m + 1)),
        Ne (α := Fin (⦋n + 1⦌.len + 1))
          ((Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
          (0 : Fin (n + 1 + 1))),
    Eq (α := Fin (⦋n + 1⦌.len + 1))
      ((Hom.toOrderHom (factor_δ f 0 ≫ δ 0) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k :
        Fin (⦋n + 1⦌.len + 1))
      ((Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
⊢ Eq (α := Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom (factor_δ f j ≫ δ j) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
have a₁ : ∀ (i : Fin (n + 1))
  (hj : ∀ (k : Fin (m + 1)), (Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k ≠ i.succ),
  Eq (α := Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom (factor_δ f i.succ ≫ δ i.succ) : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k :
      Fin (⦋n + 1⦌.len + 1))
    ((Hom.toOrderHom f : (a : Fin (⦋m⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) k : Fin (⦋n + 1⦌.len + 1))
Tactic: cases j using Fin.cases
Cleared hypotheses: j, hj
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
⊢ δ 0 ≫ mkOfSucc i = ⦋0⦌.const ⦋n⦌ i.succ
have a : ∀ (x : Fin (⦋0⦌.len + 1)),
  (↑((Hom.toOrderHom (δ 0 ≫ mkOfSucc i) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.succ) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
x : Fin (⦋0⦌.len + 1)
⊢ (↑((Hom.toOrderHom (δ 0 ≫ mkOfSucc i) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.succ) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ)
have a : (↑((Hom.toOrderHom (δ 0 ≫ mkOfSucc i) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋0⦌.len + 1)))) :
    ℕ) =
  (↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.succ) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, sorry⟩)) :
    ℕ)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
⊢ δ 1 ≫ mkOfSucc i = ⦋0⦌.const ⦋n⦌ i.castSucc
have a : ∀ (x : Fin (⦋0⦌.len + 1)),
  (↑((Hom.toOrderHom (δ 1 ≫ mkOfSucc i) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.castSucc) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
x : Fin (⦋0⦌.len + 1)
⊢ (↑((Hom.toOrderHom (δ 1 ≫ mkOfSucc i) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.castSucc) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1)) x) : ℕ)
have a : (↑((Hom.toOrderHom (δ 1 ≫ mkOfSucc i) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋0⦌.len + 1)))) :
    ℕ) =
  (↑((Hom.toOrderHom (⦋0⦌.const ⦋n⦌ i.castSucc) : (a : Fin (⦋0⦌.len + 1)) → Fin (⦋n⦌.len + 1))
        ((fun (i : Fin (⦋0⦌.len + 1)) ↦ i) ⟨0, sorry⟩)) :
    ℕ)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
⊢ mkOfSucc i ≫ δ j = mkOfSucc i.castSucc
have a : ∀ (x : Fin (⦋1⦌.len + 1)),
  (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.castSucc) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
x : Fin (⦋1⦌.len + 1)
⊢ (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.castSucc) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ)
have a : (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋1⦌.len + 1)))) :
    ℕ) =
  (↑((Hom.toOrderHom (mkOfSucc i.castSucc) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, sorry⟩)) :
    ℕ)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : i.succ.castSucc < j
x : Fin (⦋1⦌.len + 1)
a :
  (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (⦋1⦌.len + 1)))) :
      ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.castSucc) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, ⋯⟩)) :
      ℕ)
⊢ (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.castSucc) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ)
have a₁ : (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨1, sorry⟩ : Fin (⦋1⦌.len + 1)))) :
    ℕ) =
  (↑((Hom.toOrderHom (mkOfSucc i.castSucc) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1))
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨1, sorry⟩)) :
    ℕ)
Tactic: fin_cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
⊢ mkOfSucc i ≫ δ j = mkOfSucc i.succ
have a : ∀ (x : Fin (⦋1⦌.len + 1)),
  (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ)
Tactic: ext x
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
⊢ (↑((Hom.toOrderHom (mkOfSucc i ≫ δ j) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (⦋1⦌.len + 1)) → Fin (⦋n + 1⦌.len + 1)) x) : ℕ)
have a : (↑(j.succAbove ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1)) x)) : ℕ) =
  (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1)) x) : ℕ)
Tactic: simp only [δ, len_mk, mkHom, comp_toOrderHom, Hom.toOrderHom_mk, OrderHom.comp_coe,
    OrderEmbedding.toOrderHom_coe, Function.comp_apply, Fin.succAboveOrderEmb_apply]
-- Lean 4 proof step from Mathlib.AlgebraicTopology.SimplexCategory.Basic (goal)
Goal:
n : ℕ
i : Fin n
j : Fin (n + 2)
h : j < i.succ.castSucc
x : Fin (⦋1⦌.len + 1)
⊢ (↑(j.succAbove ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1)) x)) : ℕ) =
    (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1)) x) : ℕ)
have a : (↑(j.succAbove
        ((Hom.toOrderHom (mkOfSucc i) : (a : Fin (1 + 1)) → Fin (n + 1))
          ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) (⟨0, sorry⟩ : Fin (⦋1⦌.len + 1))))) :
    ℕ) =
  (↑((Hom.toOrderHom (mkOfSucc i.succ) : (a : Fin (1 + 1)) → Fin (n + 1 + 1))
        ((fun (i : Fin (⦋1⦌.len + 1)) ↦ i) ⟨0, sorry⟩)) :
    ℕ)
Tactic: fin_cases x
Cleared hypotheses: x