awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
pos : ∀ (hx : x.castSucc < i), x.castSucc ≤ i.succAbove x
pos₁ : ∀ (hx : x.castSucc ≤ x.castSucc), x.castSucc ≤ x.castSucc.succAbove x
⊢ x.castSucc ≤ i.succAbove x

Tactic:
obtain hx | rfl := hx.lt_or_eq

Premises used: LE.le.lt_or_eq, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx_1 : x.castSucc ≤ i
hx : x.castSucc < i
pos : x.castSucc ≤ x.castSucc
pos₁ : x.castSucc < i
pos₂ : x.castSucc ≤ x.castSucc
pos₃ pos₄ pos₅ : x.castSucc < i
⊢ x.castSucc ≤ i.succAbove x

Tactic:
rwa [Fin.succAbove_of_castSucc_lt]

Premises used: Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
x : Fin (n + 1)
hx : x.castSucc ≤ x.castSucc
⊢ x.castSucc ≤ x.castSucc.succAbove x

Tactic:
simpa only [Fin.succAbove_castSucc_self] using Fin.castSucc_le_succ x

Premises used: Fin.castSucc_le_succ, Fin.succAbove_castSucc_self
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
j : Fin (n + 1)
hj : j < x
⊢ j.castSucc < x.castSucc

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : x.castSucc ≤ i
j : Fin (n + 1)
hj : j < x
pos : j.castSucc < x.castSucc
pos₁ pos₂ pos₃ pos₄ : j < x
⊢ i.succAbove j < x.castSucc

Tactic:
rwa [Fin.succAbove_of_castSucc_lt _ _ (lt_of_lt_of_le (by simpa) hx),
            Fin.castSucc_lt_castSucc_iff]

Premises used: Fin.castSucc_lt_castSucc_iff, Fin.succAbove_of_castSucc_lt, lt_of_lt_of_le
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 2)
hx : Fin.last (n + 1) ≤ i
⊢ i = Fin.last (n + 1)

Tactic:
Fin.last_le_iff.1 hx

Premises used: Fin.last_le_iff, Iff.mp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 2)
hx : Fin.last (n + 1) ≤ i
pos :
  ∀ (hx : LE.le (α := Fin (n + 2)) (Fin.last (n + 1)) (Fin.last (n + 1))),
    Eq (α := Fin (n + 2))
      (map' (OrderEmbedding.toOrderHom (Fin.succAboveOrderEmb (Fin.last (n + 1)))) (Fin.castSucc (Fin.last (n + 1))))
      (Fin.last (n + 1))
⊢ map' i.succAboveOrderEmb.toOrderHom (Fin.castSucc (Fin.last (n + 1))) = Fin.last (n + 1)

Tactic:
obtain rfl : i = Fin.last _ := Fin.last_le_iff.1 hx

Premises used: Fin.last, Fin.last_le_iff, Iff.mp, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
hx : LE.le (α := Fin (n + 2)) (Fin.last (n + 1)) (Fin.last (n + 1))
⊢ Eq (α := Fin (n + 2))
    (map' (OrderEmbedding.toOrderHom (Fin.succAboveOrderEmb (Fin.last (n + 1)))) (Fin.castSucc (Fin.last (n + 1))))
    (Fin.last (n + 1))

Tactic:
simp [map'_eq_last_iff]

Premises used: SimplexCategory.II.map'_eq_last_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 2)
hx : i < x
neg :
  ∀ (x : Fin (n + 1)) (hx : i < x.succ),
    map' i.succAboveOrderEmb.toOrderHom x.succ.castSucc = i.predAbove x.succ.castSucc
⊢ map' i.succAboveOrderEmb.toOrderHom x.castSucc = i.predAbove x.castSucc

Tactic:
obtain ⟨x, rfl⟩ := Fin.eq_succ_of_ne_zero (Fin.ne_zero_of_lt hx)

Premises used: Fin.eq_succ_of_ne_zero, Fin.ne_zero_of_lt, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
⊢ i.castSucc < x.succ.castSucc

Tactic:
simpa [Fin.le_castSucc_iff]

Premises used: Fin.le_castSucc_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
neg :
  x.succ.castSucc ≤ Fin.castSucc ((i.succAboveOrderEmb.toOrderHom : (a : Fin (n + 1)) → Fin (n + 1 + 1)) x) ∧
    ∀ i_1 < x,
      Fin.castSucc ((i.succAboveOrderEmb.toOrderHom : (a : Fin (n + 1)) → Fin (n + 1 + 1)) i_1) < x.succ.castSucc
⊢ map' i.succAboveOrderEmb.toOrderHom x.succ.castSucc = i.predAbove x.succ.castSucc

Tactic:
rw [Fin.predAbove_of_castSucc_lt _ _ (by simpa [Fin.le_castSucc_iff]),
        Fin.pred_castSucc_succ, map'_eq_castSucc_iff]

Premises used: Fin.predAbove_of_castSucc_lt, SimplexCategory.II.map'_eq_castSucc_iff, Fin.pred_castSucc_succ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
neg : ∀ i_1 < x, i.succAbove i_1 < x.succ
⊢ x.succ.castSucc ≤ Fin.castSucc ((i.succAboveOrderEmb.toOrderHom : (a : Fin (n + 1)) → Fin (n + 1 + 1)) x) ∧
    ∀ i_1 < x,
      Fin.castSucc ((i.succAboveOrderEmb.toOrderHom : (a : Fin (n + 1)) → Fin (n + 1 + 1)) i_1) < x.succ.castSucc

Tactic:
simp only [Fin.succAbove_of_lt_succ _ _ hx,
        OrderEmbedding.toOrderHom_coe, Fin.succAboveOrderEmb_apply,
        le_refl, Fin.castSucc_lt_castSucc_iff, true_and]

Premises used: le_refl, OrderEmbedding.toOrderHom_coe, Fin.castSucc_lt_castSucc_iff, Fin.succAbove_of_lt_succ, true_and, Fin.succAboveOrderEmb_apply
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
pos : ∀ (h : j.castSucc < i), i.succAbove j < x.succ
neg : ∀ (h : i ≤ j.castSucc), i.succAbove j < x.succ
⊢ i.succAbove j < x.succ

Tactic:
by_cases! h : j.castSucc < i

Premises used: Fin.castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
h : j.castSucc < i
⊢ i.succAbove j < x.succ

Tactic:
simpa [Fin.succAbove_of_castSucc_lt _ _ h] using hj.le

Premises used: LT.lt.le, Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 2)
x : Fin (n + 1)
hx : i < x.succ
j : Fin (n + 1)
hj : j < x
h : i ≤ j.castSucc
neg : j.succ < x.succ
neg₁ neg₂ neg₃ neg₄ : j < x
⊢ i.succAbove j < x.succ

Tactic:
rwa [Fin.succAbove_of_le_castSucc _ _ h, Fin.succ_lt_succ_iff]

Premises used: Fin.succAbove_of_le_castSucc, Fin.succ_lt_succ_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 2)
⊢ map' i.succAboveOrderEmb.toOrderHom (Fin.last (n + 2)) = i.predAbove (Fin.last (n + 2))

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 1)
x : Fin (n + 2)
inl :
  ∀ (x : Fin (n + 1)),
    map' { toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } x.castSucc =
      i.succ.castSucc.succAbove x.castSucc
inr :
  map' { toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } (Fin.last (n + 1)) =
    i.succ.castSucc.succAbove (Fin.last (n + 1))
⊢ map' { toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } x = i.succ.castSucc.succAbove x

Tactic:
obtain ⟨x, rfl⟩ | rfl := x.eq_castSucc_or_eq_last

Premises used: Fin.eq_castSucc_or_eq_last, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
pos :
  ∀ (hi : i < x),
    map' { toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } x.castSucc =
      i.succ.castSucc.succAbove x.castSucc
neg :
  ∀ (hi : x ≤ i),
    map' { toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } x.castSucc =
      i.succ.castSucc.succAbove x.castSucc
⊢ map' { toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } x.castSucc =
    i.succ.castSucc.succAbove x.castSucc

Tactic:
by_cases! hi : i < x
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ i.succ.castSucc ≤ x.castSucc.castSucc

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
pos :
  x.castSucc ≤
      Fin.castSucc
        (({ toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } :
            (a : Fin (n + 1 + 1)) → Fin (n + 1))
          x.succ) ∧
    ∀ i_1 < x.succ,
      Fin.castSucc
          (({ toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } :
              (a : Fin (n + 1 + 1)) → Fin (n + 1))
            i_1) <
        x.castSucc
⊢ map' { toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } x.castSucc =
    i.succ.castSucc.succAbove x.castSucc

Tactic:
rw [Fin.succAbove_of_le_castSucc _ _ (by simpa), Fin.succ_castSucc, map'_eq_castSucc_iff]

Premises used: Fin.succAbove_of_le_castSucc, SimplexCategory.II.map'_eq_castSucc_iff, Fin.succ_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
pos : x ≤ i.predAbove x.succ ∧ ∀ i_1 < x.succ, i.predAbove i_1 < x
⊢ x.castSucc ≤
      Fin.castSucc
        (({ toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } :
            (a : Fin (n + 1 + 1)) → Fin (n + 1))
          x.succ) ∧
    ∀ i_1 < x.succ,
      Fin.castSucc
          (({ toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } :
              (a : Fin (n + 1 + 1)) → Fin (n + 1))
            i_1) <
        x.castSucc

Tactic:
simp only [OrderHom.coe_mk, Fin.castSucc_le_castSucc_iff, Fin.castSucc_lt_castSucc_iff]

Premises used: Fin.castSucc_lt_castSucc_iff, OrderHom.coe_mk, Fin.castSucc_le_castSucc_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
pos : x ≤ i.predAbove x.succ
pos₁ : ∀ i_1 < x.succ, i.predAbove i_1 < x
⊢ x ≤ i.predAbove x.succ ∧ ∀ i_1 < x.succ, i.predAbove i_1 < x

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
⊢ i.castSucc < x.succ

Tactic:
simpa only [Fin.castSucc_lt_succ_iff] using hi.le

Premises used: LT.lt.le, Fin.castSucc_lt_succ_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
pos : x ≤ x.succ.pred ⋯
pos₁ pos₂ : x ≤ x
⊢ x ≤ i.predAbove x.succ

Tactic:
rw [Fin.predAbove_of_castSucc_lt _ _
          (by simpa only [Fin.castSucc_lt_succ_iff] using hi.le), Fin.pred_succ]

Premises used: Fin.predAbove_of_castSucc_lt, Fin.pred_succ
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
pos : ∀ (h : i.castSucc < j), i.predAbove j < x
neg : ∀ (h : j ≤ i.castSucc), i.predAbove j < x
⊢ i.predAbove j < x

Tactic:
by_cases! h : i.castSucc < j

Premises used: Fin.castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : i.castSucc < j
pos : j.pred ⋯ < x
pos₁ : (j.pred ⋯).succ < x.succ
pos₂ pos₃ pos₄ pos₅ : j < x.succ
⊢ i.predAbove j < x

Tactic:
rwa [Fin.predAbove_of_castSucc_lt _ _ h, ← Fin.succ_lt_succ_iff,
            Fin.succ_pred]

Premises used: Fin.succ_lt_succ_iff, Fin.predAbove_of_castSucc_lt, Fin.succ_pred
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : j ≤ i.castSucc
neg : j < x.castSucc
⊢ i.predAbove j < x

Tactic:
rw [Fin.predAbove_of_le_castSucc _ _ h, ← Fin.castSucc_lt_castSucc_iff,
            Fin.castSucc_castPred]

Premises used: Fin.castSucc_lt_castSucc_iff, Fin.castSucc_castPred, Fin.predAbove_of_le_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : j ≤ i.castSucc
⊢ j < x.castSucc

Tactic:
lt_of_le_of_lt h hi

Premises used: lt_of_le_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : i < x
j : Fin (n + 1 + 1)
hj : j < x.succ
h : j ≤ i.castSucc
⊢ j < x.castSucc

Tactic:
exact lt_of_le_of_lt h hi

Premises used: lt_of_le_of_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ x.castSucc.castSucc < i.succ.castSucc

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
neg :
  x.castSucc ≤
      Fin.castSucc
        (({ toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } :
            (a : Fin (n + 1 + 1)) → Fin (n + 1))
          x.castSucc) ∧
    ∀ i_1 < x.castSucc,
      Fin.castSucc
          (({ toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } :
              (a : Fin (n + 1 + 1)) → Fin (n + 1))
            i_1) <
        x.castSucc
⊢ map' { toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } x.castSucc =
    i.succ.castSucc.succAbove x.castSucc

Tactic:
rw [Fin.succAbove_of_castSucc_lt _ _ (by simpa), map'_eq_castSucc_iff]

Premises used: SimplexCategory.II.map'_eq_castSucc_iff, Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
neg : x ≤ i.predAbove x.castSucc ∧ ∀ i_1 < x.castSucc, i.predAbove i_1 < x
⊢ x.castSucc ≤
      Fin.castSucc
        (({ toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } :
            (a : Fin (n + 1 + 1)) → Fin (n + 1))
          x.castSucc) ∧
    ∀ i_1 < x.castSucc,
      Fin.castSucc
          (({ toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } :
              (a : Fin (n + 1 + 1)) → Fin (n + 1))
            i_1) <
        x.castSucc

Tactic:
simp only [OrderHom.coe_mk, Fin.castSucc_le_castSucc_iff, Fin.castSucc_lt_castSucc_iff]

Premises used: Fin.castSucc_lt_castSucc_iff, OrderHom.coe_mk, Fin.castSucc_le_castSucc_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
neg : x ≤ i.predAbove x.castSucc
neg₁ : ∀ i_1 < x.castSucc, i.predAbove i_1 < x
⊢ x ≤ i.predAbove x.castSucc ∧ ∀ i_1 < x.castSucc, i.predAbove i_1 < x

Tactic:
constructor
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ x.castSucc ≤ i.castSucc

Tactic:
simpa
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
⊢ x ≤ i.predAbove x.castSucc

Tactic:
simp only [i.predAbove_of_le_castSucc x.castSucc (by simpa),
          Fin.castPred_castSucc, le_refl]

Premises used: Iff.mpr, le_refl, Fin.ext_iff, Fin.castPred_castSucc, Iff.not, Fin.castSucc_lt_last, Fin.predAbove_of_le_castSucc, Fin.castSucc, LT.lt.ne
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
pos : ∀ (h : i.castSucc < j), i.predAbove j < x
neg : ∀ (h : j ≤ i.castSucc), i.predAbove j < x
⊢ i.predAbove j < x

Tactic:
by_cases! h : i.castSucc < j

Premises used: Fin.castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
h : i.castSucc < j
pos : j < x.succ
⊢ i.predAbove j < x

Tactic:
rw [Fin.predAbove_of_castSucc_lt _ _ h, ← Fin.succ_lt_succ_iff, Fin.succ_pred]

Premises used: Fin.succ_lt_succ_iff, Fin.predAbove_of_castSucc_lt, Fin.succ_pred
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
h : i.castSucc < j
⊢ j < x.succ

Tactic:
hj.trans x.castSucc_lt_succ

Premises used: Fin.castSucc_lt_succ, LT.lt.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
h : i.castSucc < j
⊢ j < x.succ

Tactic:
exact hj.trans x.castSucc_lt_succ

Premises used: Fin.castSucc_lt_succ, LT.lt.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i x : Fin (n + 1)
hi : x ≤ i
j : Fin (n + 1 + 1)
hj : j < x.castSucc
h : j ≤ i.castSucc
neg : j.castPred ⋯ < x
neg₁ : (j.castPred ⋯).castSucc < x.castSucc
neg₂ neg₃ neg₄ neg₅ : j < x.castSucc
⊢ i.predAbove j < x

Tactic:
rwa [Fin.predAbove_of_le_castSucc _ _ h, ← Fin.castSucc_lt_castSucc_iff,
            Fin.castSucc_castPred]

Premises used: Fin.castSucc_lt_castSucc_iff, Fin.castSucc_castPred, Fin.predAbove_of_le_castSucc
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : ℕ
i : Fin (n + 1)
⊢ map' { toFun := i.predAbove, monotone' := ⋯ : Fin (n + 1 + 1) →o Fin (n + 1) } (Fin.last (n + 1)) =
    i.succ.castSucc.succAbove (Fin.last (n + 1))

Tactic:
simp [map'_last]

Premises used: SimplexCategory.II.map'_last
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
z : Fin (n + 2)
hz : z ∈ finset f y
inl : ∀ (z : Fin (n + 1)) (hz : z.castSucc ∈ finset f y), z.castSucc ∈ finset f x
inr : ∀ (hz : Fin.last (n + 1) ∈ finset f y), Fin.last (n + 1) ∈ finset f x
⊢ z ∈ finset f x

Tactic:
obtain ⟨z, rfl⟩ | rfl := z.eq_castSucc_or_eq_last

Premises used: Fin.eq_castSucc_or_eq_last, rfl
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
z : Fin (n + 1)
hz : z.castSucc ∈ finset f y
inl :
  ∀ (hz : y ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) z)),
    x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) z)
⊢ z.castSucc ∈ finset f x

Tactic:
simp only [castSucc_mem_finset_iff] at hz ⊢

Premises used: SimplexCategory.II.castSucc_mem_finset_iff
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
z : Fin (n + 1)
hz : y ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) z)
⊢ x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) z)

Tactic:
hxy.trans hz

Premises used: LE.le.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
z : Fin (n + 1)
hz : y ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) z)
⊢ x ≤ Fin.castSucc ((f : (a : Fin (n + 1)) → Fin (m + 1)) z)

Tactic:
exact hxy.trans hz

Premises used: LE.le.trans
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
hz : Fin.last (n + 1) ∈ finset f y
⊢ Fin.last (n + 1) ∈ finset f x

Tactic:
simp
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n m : ℕ
f : Fin (n + 1) →o Fin (m + 1)
x y : Fin (m + 2)
hxy : x ≤ y
⊢ map' f x ≤ map' f y

Tactic:
exact Finset.min'_subset _ (fun z hz ↦ by
    obtain ⟨z, rfl⟩ | rfl := z.eq_castSucc_or_eq_last
    · simp only [castSucc_mem_finset_iff] at hz ⊢
      exact hxy.trans hz
    · simp)

Premises used: Finset.min'_subset
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : SimplexCategory
a :
  ∀ (x : Fin ((unop (op ⦋n.len + 1⦌)).len + 1)),
    Eq (α := Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
      ((Hom.toOrderHom
              (Quiver.Hom.unop
                (op
                  (Hom.mk
                    { toFun := II.map' (Hom.toOrderHom (𝟙 n)), monotone' := ⋯ :
                      Fin ((unop (op ⦋n.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋n.len + 1⦌)).len + 1) }))) :
            (a : Fin ((unop (op ⦋n.len + 1⦌)).len + 1)) → Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
          x :
        Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
      ((Hom.toOrderHom (Quiver.Hom.unop (𝟙 (op ⦋n.len + 1⦌))) :
            (a : Fin ((unop (op ⦋n.len + 1⦌)).len + 1)) → Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
          x :
        Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
⊢ Quiver.Hom.unop
      (op
        (Hom.mk
          { toFun := II.map' (Hom.toOrderHom (𝟙 n)), monotone' := ⋯ :
            Fin ((unop (op ⦋n.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋n.len + 1⦌)).len + 1) })) =
    Quiver.Hom.unop (𝟙 (op ⦋n.len + 1⦌))

Tactic:
ext x : 3
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : SimplexCategory
x : Fin ((unop (op ⦋n.len + 1⦌)).len + 1)
⊢ Eq (α := Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
    ((Hom.toOrderHom
            (Quiver.Hom.unop
              (op
                (Hom.mk
                  { toFun := II.map' (Hom.toOrderHom (𝟙 n)), monotone' := ⋯ :
                    Fin ((unop (op ⦋n.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋n.len + 1⦌)).len + 1) }))) :
          (a : Fin ((unop (op ⦋n.len + 1⦌)).len + 1)) → Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
        x :
      Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
    ((Hom.toOrderHom (Quiver.Hom.unop (𝟙 (op ⦋n.len + 1⦌))) :
          (a : Fin ((unop (op ⦋n.len + 1⦌)).len + 1)) → Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
        x :
      Fin ((unop (op ⦋n.len + 1⦌)).len + 1))

Tactic:
II.map'_id x

Premises used: Finset.min', OrderHom.id, Finset.inf', SimplexCategory.II.map', SimplexCategory.Hom.id, WithTop.untop, SimplexCategory.Hom.toOrderHom, SimplexCategory.II.map'_id, SimplexCategory.Hom.mk
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
n : SimplexCategory
x : Fin ((unop (op ⦋n.len + 1⦌)).len + 1)
⊢ Eq (α := Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
    ((Hom.toOrderHom
            (Quiver.Hom.unop
              (op
                (Hom.mk
                  { toFun := II.map' (Hom.toOrderHom (𝟙 n)), monotone' := ⋯ :
                    Fin ((unop (op ⦋n.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋n.len + 1⦌)).len + 1) }))) :
          (a : Fin ((unop (op ⦋n.len + 1⦌)).len + 1)) → Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
        x :
      Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
    ((Hom.toOrderHom (Quiver.Hom.unop (𝟙 (op ⦋n.len + 1⦌))) :
          (a : Fin ((unop (op ⦋n.len + 1⦌)).len + 1)) → Fin ((unop (op ⦋n.len + 1⦌)).len + 1))
        x :
      Fin ((unop (op ⦋n.len + 1⦌)).len + 1))

Tactic:
exact II.map'_id x

Premises used: SimplexCategory.II.map'_id
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
m n p : SimplexCategory
f : m ⟶ n
g : n ⟶ p
a :
  ∀ (x : Fin ((unop (op ⦋p.len + 1⦌)).len + 1)),
    Eq (α := Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
      ((Hom.toOrderHom
              (Quiver.Hom.unop
                (op
                  (Hom.mk
                    { toFun := II.map' (Hom.toOrderHom (f ≫ g)), monotone' := ⋯ :
                      Fin ((unop (op ⦋p.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋m.len + 1⦌)).len + 1) }))) :
            (a : Fin ((unop (op ⦋p.len + 1⦌)).len + 1)) → Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
          x :
        Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
      ((Hom.toOrderHom
              (Quiver.Hom.unop
                (op
                    (Hom.mk
                      { toFun := II.map' (Hom.toOrderHom f), monotone' := ⋯ :
                        Fin ((unop (op ⦋n.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋m.len + 1⦌)).len + 1) }) ≫
                  op (Hom.mk { toFun := II.map' (Hom.toOrderHom g), monotone' := ⋯ }))) :
            (a : Fin ((unop (op ⦋p.len + 1⦌)).len + 1)) → Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
          x :
        Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
⊢ Quiver.Hom.unop
      (op
        (Hom.mk
          { toFun := II.map' (Hom.toOrderHom (f ≫ g)), monotone' := ⋯ :
            Fin ((unop (op ⦋p.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋m.len + 1⦌)).len + 1) })) =
    Quiver.Hom.unop
      (op
          (Hom.mk
            { toFun := II.map' (Hom.toOrderHom f), monotone' := ⋯ :
              Fin ((unop (op ⦋n.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋m.len + 1⦌)).len + 1) }) ≫
        op (Hom.mk { toFun := II.map' (Hom.toOrderHom g), monotone' := ⋯ }))

Tactic:
ext x : 3
-- Module: Mathlib.AlgebraicTopology.SimplicialObject.II
Goal:
m n p : SimplexCategory
f : m ⟶ n
g : n ⟶ p
x : Fin ((unop (op ⦋p.len + 1⦌)).len + 1)
⊢ Eq (α := Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
    ((Hom.toOrderHom
            (Quiver.Hom.unop
              (op
                (Hom.mk
                  { toFun := II.map' (Hom.toOrderHom (f ≫ g)), monotone' := ⋯ :
                    Fin ((unop (op ⦋p.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋m.len + 1⦌)).len + 1) }))) :
          (a : Fin ((unop (op ⦋p.len + 1⦌)).len + 1)) → Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
        x :
      Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
    ((Hom.toOrderHom
            (Quiver.Hom.unop
              (op
                  (Hom.mk
                    { toFun := II.map' (Hom.toOrderHom f), monotone' := ⋯ :
                      Fin ((unop (op ⦋n.len + 1⦌)).len + 1) →o Fin ((unop (op ⦋m.len + 1⦌)).len + 1) }) ≫
                op (Hom.mk { toFun := II.map' (Hom.toOrderHom g), monotone' := ⋯ }))) :
          (a : Fin ((unop (op ⦋p.len + 1⦌)).len + 1)) → Fin ((unop (op ⦋m.len + 1⦌)).len + 1))
        x :
      Fin ((unop (op ⦋m.len + 1⦌)).len + 1))

Tactic:
(II.map'_map' _ _ _).symm

Premises used: Finset.min', Finset.inf', SimplexCategory.II.map', SimplexCategory.II.map'_map', OrderHom.comp, WithTop.untop, SimplexCategory.Hom.comp, SimplexCategory.Hom.toOrderHom, Eq.symm, SimplexCategory.Hom.mk