awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
pos : ∀ (hi : i = 0), predAbove 0 i = 0
neg : ∀ (hi : ¬i = 0), predAbove 0 i = i.pred hi
⊢ predAbove 0 i = if hi : i = 0 then 0 else i.pred hi

Tactic:
split_ifs with hi
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
hi : i = 0
pos : Eq (α := Fin n) (predAbove 0 0) 0
pos₁ pos₂ : Eq (α := Fin n) 0 0
⊢ predAbove 0 i = 0

Tactic:
rw [hi, predAbove_right_zero]

Premises used: Fin.predAbove_right_zero
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
hi : ¬i = 0
neg neg₁ : i.pred hi = i.pred hi
⊢ predAbove 0 i = i.pred hi

Tactic:
rw [predAbove_zero_of_ne_zero hi]

Premises used: Fin.predAbove_zero_of_ne_zero
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
rw : pred (last (n + 1)) ⋯ = last n
rw₁ rw₂ : last n = last n
⊢ i.predAbove (last (n + 1)) = last n

Tactic:
rw [predAbove_of_castSucc_lt _ _ (castSucc_lt_last _), pred_last]

Premises used: Iff.mpr, Fin.ext_iff, Fin.predAbove_of_castSucc_lt, Iff.not, Fin.pred_last, LT.lt.ne', Fin.castSucc_lt_last, Fin.last_pos'
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
rw : i.castSucc.castPred ⋯ = i
rw₁ rw₂ : i = i
⊢ (last n).predAbove i.castSucc = i

Tactic:
rw [predAbove_of_le_castSucc _ _ (castSucc_le_castSucc_iff.mpr (le_last _)), castPred_castSucc]

Premises used: Iff.mpr, Fin.ext_iff, Fin.castPred_castSucc, Iff.not, Fin.castSucc_lt_last, Fin.predAbove_of_le_castSucc, Fin.castSucc_le_castSucc_iff, LT.lt.ne, Fin.le_last
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
hi : i ≠ last (n + 1)
⊢ ∃ (j : Fin (n + 1)), j.castSucc = i

Tactic:
rw [← exists_castSucc_eq] at hi

Premises used: Fin.exists_castSucc_eq
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
hi_1 : i ≠ last (n + 1)
hi : ∃ (j : Fin (n + 1)), j.castSucc = i
rcases : ∀ (y : Fin (n + 1)) (hi : y.castSucc ≠ last (n + 1)), (last n).predAbove y.castSucc = y.castSucc.castPred hi
⊢ (last n).predAbove i = i.castPred hi_1

Tactic:
rcases hi with ⟨y, rfl⟩

Premises used: rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
y : Fin (n + 1)
hi : y.castSucc ≠ last (n + 1)
⊢ (last n).predAbove y.castSucc = y.castSucc.castPred hi

Tactic:
predAbove_last_castSucc

Premises used: Fin.predAbove_last_castSucc
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
y : Fin (n + 1)
hi : y.castSucc ≠ last (n + 1)
⊢ (last n).predAbove y.castSucc = y.castSucc.castPred hi

Tactic:
exact predAbove_last_castSucc

Premises used: Fin.predAbove_last_castSucc
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
pos : ∀ (hi : i = last (n + 1)), (last n).predAbove i = last n
neg : ∀ (hi : ¬i = last (n + 1)), (last n).predAbove i = i.castPred hi
⊢ (last n).predAbove i = if hi : i = last (n + 1) then last n else i.castPred hi

Tactic:
split_ifs with hi
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
hi : i = last (n + 1)
pos : (last n).predAbove (last (n + 1)) = last n
pos₁ pos₂ : last n = last n
⊢ (last n).predAbove i = last n

Tactic:
rw [hi, predAbove_right_last]

Premises used: Fin.predAbove_right_last
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
hi : ¬i = last (n + 1)
neg neg₁ : i.castPred hi = i.castPred hi
⊢ (last n).predAbove i = i.castPred hi

Tactic:
rw [predAbove_last_of_ne_last hi]

Premises used: Fin.predAbove_last_of_ne_last
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
pos : ∀ (hi : i ≤ p), ∃ (a : Fin (n + 1)), p.predAbove a = i
neg : ∀ (hi : ¬i ≤ p), ∃ (a : Fin (n + 1)), p.predAbove a = i
⊢ ∃ (a : Fin (n + 1)), p.predAbove a = i

Tactic:
by_cases hi : i ≤ p
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
hi : i ≤ p
⊢ ∃ (a : Fin (n + 1)), p.predAbove a = i

Tactic:
⟨i.castSucc, predAbove_castSucc_of_le p i hi⟩

Premises used: Fin.predAbove_castSucc_of_le, Exists.intro, Fin.castSucc
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
hi : i ≤ p
⊢ ∃ (a : Fin (n + 1)), p.predAbove a = i

Tactic:
exact ⟨i.castSucc, predAbove_castSucc_of_le p i hi⟩
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
hi : ¬i ≤ p
⊢ p < i

Tactic:
rw [Fin.not_le] at hi

Premises used: Fin.not_le
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
hi : p < i
⊢ ∃ (a : Fin (n + 1)), p.predAbove a = i

Tactic:
⟨i.succ, predAbove_succ_of_le p i (Fin.le_of_lt hi)⟩

Premises used: Fin.succ, Fin.le_of_lt, Fin.predAbove_succ_of_le, Exists.intro
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
hi : p < i
⊢ ∃ (a : Fin (n + 1)), p.predAbove a = i

Tactic:
exact ⟨i.succ, predAbove_succ_of_le p i (Fin.le_of_lt hi)⟩
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i ≠ p.castSucc
inl : ∀ (h : i < p.castSucc), p.castSucc.succAbove (p.predAbove i) = i
inr : ∀ (h : p.castSucc < i), p.castSucc.succAbove (p.predAbove i) = i
⊢ p.castSucc.succAbove (p.predAbove i) = i

Tactic:
obtain h | h := Fin.lt_or_lt_of_ne h

Premises used: Fin.lt_or_lt_of_ne
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h_1 : i ≠ p.castSucc
h : i < p.castSucc
inl : p.castSucc.succAbove (i.castPred ⋯) = i
inl₁ inl₂ : i = i
⊢ p.castSucc.succAbove (p.predAbove i) = i

Tactic:
rw [predAbove_of_le_castSucc _ _ (Fin.le_of_lt h), succAbove_castPred_of_lt _ _ h]

Premises used: Fin.le_of_lt, Fin.predAbove_of_le_castSucc, Fin.succAbove_castPred_of_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h_1 : i ≠ p.castSucc
h : p.castSucc < i
inr : p.castSucc.succAbove (i.pred ⋯) = i
inr₁ inr₂ : i = i
⊢ p.castSucc.succAbove (p.predAbove i) = i

Tactic:
rw [predAbove_of_castSucc_lt _ _ h, succAbove_pred_of_lt _ _ h]

Premises used: Fin.predAbove_of_castSucc_lt, Fin.succAbove_pred_of_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i ≠ p.succ
inl : ∀ (h : i < p.succ), p.succ.succAbove (p.predAbove i) = i
inr : ∀ (h : p.succ < i), p.succ.succAbove (p.predAbove i) = i
⊢ p.succ.succAbove (p.predAbove i) = i

Tactic:
obtain h | h := Fin.lt_or_lt_of_ne h

Premises used: Fin.lt_or_lt_of_ne
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h_1 : i ≠ p.succ
h : i < p.succ
inl : p.succ.succAbove (i.castPred ⋯) = i
inl₁ inl₂ : i = i
⊢ p.succ.succAbove (p.predAbove i) = i

Tactic:
rw [predAbove_of_le_castSucc _ _ (le_castSucc_iff.2 h),
      succAbove_castPred_of_lt _ _ h]

Premises used: Iff.mpr, Fin.predAbove_of_le_castSucc, Fin.le_castSucc_iff, Fin.succAbove_castPred_of_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h_1 : i ≠ p.succ
h : p.succ < i
inr : p.succ.succAbove (i.pred ⋯) = i
inr₁ inr₂ : i = i
⊢ p.succ.succAbove (p.predAbove i) = i

Tactic:
rw [predAbove_of_castSucc_lt _ _ (Fin.lt_of_le_of_lt (p.castSucc_le_succ) h),
      succAbove_pred_of_lt _ _ h]

Premises used: Fin.castSucc_le_succ, Fin.predAbove_of_castSucc_lt, Fin.succAbove_pred_of_lt, Fin.lt_of_le_of_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
inl : ∀ (h : p ≤ i), p.predAbove (p.castSucc.succAbove i) = i
inr : ∀ (h : i < p), p.predAbove (p.castSucc.succAbove i) = i
⊢ p.predAbove (p.castSucc.succAbove i) = i

Tactic:
obtain h | h := p.le_or_gt i

Premises used: Fin.le_or_gt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
h : p ≤ i
inl : p.predAbove i.succ = i
inl₁ inl₂ : i = i
⊢ p.predAbove (p.castSucc.succAbove i) = i

Tactic:
rw [succAbove_castSucc_of_le _ _ h, predAbove_succ_of_le _ _ h]

Premises used: Fin.succAbove_castSucc_of_le, Fin.predAbove_succ_of_le
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
h : i < p
inr : p.predAbove i.castSucc = i
inr₁ inr₂ : i = i
⊢ p.predAbove (p.castSucc.succAbove i) = i

Tactic:
rw [succAbove_castSucc_of_lt _ _ h, predAbove_castSucc_of_le _ _ <| Fin.le_of_lt h]

Premises used: Fin.predAbove_castSucc_of_le, Fin.succAbove_castSucc_of_lt, Fin.le_of_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
inl : ∀ (h : a.succ ≤ b), a.succ.predAbove b.succ = (a.predAbove b).succ
inr : ∀ (h : b < a.succ), a.succ.predAbove b.succ = (a.predAbove b).succ
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ

Tactic:
obtain h | h := Fin.le_or_gt (succ a) b

Premises used: Fin.succ, Fin.le_or_gt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.succ ≤ b
inl : a.succ.predAbove b.succ = (b.pred ⋯).succ
inl₁ : b = (b.pred ⋯).succ
inl₂ inl₃ : b = b
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ

Tactic:
rw [predAbove_of_castSucc_lt _ _ h, predAbove_succ_of_le _ _ h, succ_pred]

Premises used: Fin.predAbove_of_castSucc_lt, Fin.predAbove_succ_of_le, Fin.succ_pred
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b < a.succ
inr : a.succ.predAbove b.succ = (b.castPred ⋯).succ
inr₁ : b.succ.castPred ⋯ = (b.castPred ⋯).succ
inr₂ inr₃ : b.succ.castPred ⋯ = b.succ.castPred ⋯
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ

Tactic:
rw [predAbove_of_lt_succ _ _ h, predAbove_succ_of_lt _ _ h, succ_castPred_eq_castPred_succ]

Premises used: Iff.mpr, Fin.succ_castPred_eq_castPred_succ, Fin.predAbove_succ_of_lt, Fin.succ_ne_last_iff, Fin.predAbove_of_lt_succ
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
inl : ∀ (h : a.castSucc < b), a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
inr : ∀ (h : b ≤ a.castSucc), a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

Tactic:
obtain h | h := a.castSucc.lt_or_ge b

Premises used: Fin.lt_or_ge, Fin.castSucc
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.castSucc < b
inl : a.castSucc.predAbove b.castSucc = (b.pred ⋯).castSucc
inl₁ : b.castSucc.pred ⋯ = (b.pred ⋯).castSucc
inl₂ inl₃ : b.castSucc.pred ⋯ = b.castSucc.pred ⋯
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

Tactic:
rw [predAbove_of_castSucc_lt _ _ h, predAbove_castSucc_of_lt _ _ h,
      castSucc_pred_eq_pred_castSucc]

Premises used: Fin.predAbove_of_castSucc_lt, Fin.castSucc_pred_eq_pred_castSucc, Fin.predAbove_castSucc_of_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b ≤ a.castSucc
inr : a.castSucc.predAbove b.castSucc = (b.castPred ⋯).castSucc
inr₁ : b = (b.castPred ⋯).castSucc
inr₂ inr₃ : b = b
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc

Tactic:
rw [predAbove_of_le_castSucc _ _ h, predAbove_castSucc_of_le _ _ h, castSucc_castPred]

Premises used: Fin.predAbove_castSucc_of_le, Fin.castSucc_castPred, Fin.predAbove_of_le_castSucc
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
inl : j.castSucc ≤ (i.pred ⋯).castSucc
⊢ (j.predAbove i).predAbove (i.succAbove j) = j

Tactic:
rw [predAbove_of_castSucc_lt _ _ h, succAbove_of_castSucc_lt _ _ h, predAbove_of_le_castSucc,
      castPred_castSucc]

Premises used: Iff.mpr, Fin.ext_iff, Fin.castPred_castSucc, Fin.predAbove_of_castSucc_lt, Iff.not, Fin.castSucc_lt_last, Fin.predAbove_of_le_castSucc, Fin.succAbove_of_castSucc_lt, LT.lt.ne
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
inl : j.castSucc < (i.pred ⋯).succ
inl₁ inl₂ inl₃ inl₄ : j.castSucc < i
⊢ j.castSucc ≤ (i.pred ⋯).castSucc

Tactic:
rwa [le_castSucc_iff, succ_pred]

Premises used: Fin.le_castSucc_iff, Fin.succ_pred
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
inr : (i.castPred ⋯).castSucc < j.succ
⊢ (j.predAbove i).predAbove (i.succAbove j) = j

Tactic:
rw [predAbove_of_le_castSucc _ _ h, succAbove_of_le_castSucc _ _ h, predAbove_of_castSucc_lt,
      pred_succ]

Premises used: Fin.succAbove_of_le_castSucc, Fin.predAbove_of_castSucc_lt, Fin.pred_succ, Fin.predAbove_of_le_castSucc
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
inr : i < j.succ
inr₁ inr₂ inr₃ inr₄ : i ≤ j.castSucc
⊢ (i.castPred ⋯).castSucc < j.succ

Tactic:
rwa [castSucc_castPred, ← le_castSucc_iff]

Premises used: Fin.castSucc_castPred, Fin.le_castSucc_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ j.castSucc < i ∨ i ≤ j.castSucc

Tactic:
cases j.castSucc.lt_or_le i with
  | inl h =>
    rw [predAbove_of_castSucc_lt _ _ h, succAbove_of_castSucc_lt _ _ h, predAbove_of_le_castSucc,
      castPred_castSucc]
    rwa [le_castSucc_iff, succ_pred]
  | inr h =>
    rw [predAbove_of_le_castSucc _ _ h, succAbove_of_le_castSucc _ _ h, predAbove_of_castSucc_lt,
      pred_succ]
    rwa [castSucc_castPred, ← le_castSucc_iff]

Premises used: Iff.mpr, Fin.lt_or_le, Fin.ext_iff, Fin.castPred_castSucc, Fin.predAbove_of_castSucc_lt, Iff.not, Fin.pred_succ, Fin.castSucc_lt_last, Fin.castSucc_castPred, Fin.predAbove_of_le_castSucc, Fin.le_castSucc_iff, Fin.castSucc, Fin.succ_pred, LT.lt.ne
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
inl : j.castSucc.succAbove (j.predAbove i) = i
inl₁ inl₂ : i = i
⊢ (i.succAbove j).succAbove (j.predAbove i) = i

Tactic:
rw [succAbove_of_castSucc_lt _ _ h, succAbove_predAbove (Fin.ne_of_gt h)]

Premises used: Fin.ne_of_gt, Fin.succAbove_predAbove, Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
inr : j.succ.succAbove (j.predAbove i) = i
inr₁ inr₂ : i = i
⊢ (i.succAbove j).succAbove (j.predAbove i) = i

Tactic:
rw [succAbove_of_le_castSucc _ _ h,
      succ_succAbove_predAbove (Fin.ne_of_lt <| le_castSucc_iff.mp h)]

Premises used: Fin.succAbove_of_le_castSucc, Fin.ne_of_lt, Fin.succ_succAbove_predAbove, Iff.mp, Fin.le_castSucc_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ j.castSucc < i ∨ i ≤ j.castSucc

Tactic:
cases Fin.lt_or_le j.castSucc i with
  | inl h => rw [succAbove_of_castSucc_lt _ _ h, succAbove_predAbove (Fin.ne_of_gt h)]
  | inr h =>
    rw [succAbove_of_le_castSucc _ _ h,
      succ_succAbove_predAbove (Fin.ne_of_lt <| le_castSucc_iff.mp h)]

Premises used: Fin.lt_or_le, Fin.castSucc
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : (↑((i.succAbove j).succAbove ((j.predAbove i).succAbove k)) : ℕ) = (↑(i.succAbove (j.succAbove k)) : ℕ)
⊢ (i.succAbove j).succAbove ((j.predAbove i).succAbove k) = i.succAbove (j.succAbove k)

Tactic:
ext
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h :
  (if
        (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) <
          if (↑j : ℕ) < (↑i : ℕ) then (↑j : ℕ) else (↑j : ℕ) + 1 then
      if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < if (↑j : ℕ) < (↑i : ℕ) then (↑i : ℕ) - 1 else (↑i : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1) =
    if (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) < (↑i : ℕ) then
      if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1
    else (if (↑k : ℕ) < (↑j : ℕ) then (↑k : ℕ) else (↑k : ℕ) + 1) + 1
⊢ (↑((i.succAbove j).succAbove ((j.predAbove i).succAbove k)) : ℕ) = (↑(i.succAbove (j.succAbove k)) : ℕ)

Tactic:
simp only [succAbove, predAbove, lt_def, val_castSucc, apply_dite Fin.val, val_pred, coe_castPred,
    dite_eq_ite, apply_ite Fin.val, val_succ]

Premises used: Fin.succAbove, apply_dite, Fin.val_pred, apply_ite, Fin.val_succ, Fin.predAbove, Fin.val, Fin.coe_castPred, Fin.lt_def, dite_eq_ite, Fin.val_castSucc
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
h_1 : (↑k : ℕ) < (↑i : ℕ) - 1
h_2 : (↑k : ℕ) < (↑j : ℕ)
h_3 : (↑k : ℕ) < (↑i : ℕ)
⊢ (↑k : ℕ) = (↑k : ℕ)

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
h_1 : (↑k : ℕ) < (↑i : ℕ) - 1
h_2 : (↑k : ℕ) < (↑j : ℕ)
h_3 : ¬(↑k : ℕ) < (↑i : ℕ)
⊢ (↑k : ℕ) = (↑k : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
h_1 : (↑k : ℕ) < (↑i : ℕ) - 1
h_2 : ¬(↑k : ℕ) < (↑j : ℕ)
h_3 : (↑k : ℕ) + 1 < (↑i : ℕ)
⊢ (↑k : ℕ) + 1 = (↑k : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
h_1 : (↑k : ℕ) < (↑i : ℕ) - 1
h_2 : ¬(↑k : ℕ) < (↑j : ℕ)
h_3 : ¬(↑k : ℕ) + 1 < (↑i : ℕ)
⊢ (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
h_1 : ¬(↑k : ℕ) < (↑i : ℕ) - 1
h_2 : (↑k : ℕ) + 1 < (↑j : ℕ)
h_3 : (↑k : ℕ) < (↑j : ℕ)
h_4 : (↑k : ℕ) < (↑i : ℕ)
⊢ (↑k : ℕ) + 1 = (↑k : ℕ)

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
h_1 : ¬(↑k : ℕ) < (↑i : ℕ) - 1
h_2 : (↑k : ℕ) + 1 < (↑j : ℕ)
h_3 : (↑k : ℕ) < (↑j : ℕ)
h_4 : ¬(↑k : ℕ) < (↑i : ℕ)
⊢ (↑k : ℕ) + 1 = (↑k : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
h_1 : ¬(↑k : ℕ) < (↑i : ℕ) - 1
h_2 : (↑k : ℕ) + 1 < (↑j : ℕ)
h_3 : ¬(↑k : ℕ) < (↑j : ℕ)
h_4 : (↑k : ℕ) + 1 < (↑i : ℕ)
⊢ (↑k : ℕ) + 1 = (↑k : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
h_1 : ¬(↑k : ℕ) < (↑i : ℕ) - 1
h_2 : (↑k : ℕ) + 1 < (↑j : ℕ)
h_3 : ¬(↑k : ℕ) < (↑j : ℕ)
h_4 : ¬(↑k : ℕ) + 1 < (↑i : ℕ)
⊢ (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
h_1 : ¬(↑k : ℕ) < (↑i : ℕ) - 1
h_2 : ¬(↑k : ℕ) + 1 < (↑j : ℕ)
h_3 : (↑k : ℕ) < (↑j : ℕ)
h_4 : (↑k : ℕ) < (↑i : ℕ)
⊢ (↑k : ℕ) + 1 + 1 = (↑k : ℕ)

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
h_1 : ¬(↑k : ℕ) < (↑i : ℕ) - 1
h_2 : ¬(↑k : ℕ) + 1 < (↑j : ℕ)
h_3 : (↑k : ℕ) < (↑j : ℕ)
h_4 : ¬(↑k : ℕ) < (↑i : ℕ)
⊢ (↑k : ℕ) + 1 + 1 = (↑k : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
h_1 : ¬(↑k : ℕ) < (↑i : ℕ) - 1
h_2 : ¬(↑k : ℕ) + 1 < (↑j : ℕ)
h_3 : ¬(↑k : ℕ) < (↑j : ℕ)
h_4 : (↑k : ℕ) + 1 < (↑i : ℕ)
⊢ (↑k : ℕ) + 1 + 1 = (↑k : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : (↑j : ℕ) < (↑i : ℕ)
h_1 : ¬(↑k : ℕ) < (↑i : ℕ) - 1
h_2 : ¬(↑k : ℕ) + 1 < (↑j : ℕ)
h_3 : ¬(↑k : ℕ) < (↑j : ℕ)
h_4 : ¬(↑k : ℕ) + 1 < (↑i : ℕ)
⊢ (↑k : ℕ) + 1 + 1 = (↑k : ℕ) + 1 + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : ¬(↑j : ℕ) < (↑i : ℕ)
h_1 : (↑k : ℕ) < (↑i : ℕ)
h_2 : (↑k : ℕ) < (↑j : ℕ) + 1
h_3 : (↑k : ℕ) < (↑j : ℕ)
⊢ (↑k : ℕ) = (↑k : ℕ)

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : ¬(↑j : ℕ) < (↑i : ℕ)
h_1 : (↑k : ℕ) < (↑i : ℕ)
h_2 : (↑k : ℕ) < (↑j : ℕ) + 1
h_3 : ¬(↑k : ℕ) < (↑j : ℕ)
h_4 : (↑k : ℕ) + 1 < (↑i : ℕ)
⊢ (↑k : ℕ) = (↑k : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : ¬(↑j : ℕ) < (↑i : ℕ)
h_1 : (↑k : ℕ) < (↑i : ℕ)
h_2 : (↑k : ℕ) < (↑j : ℕ) + 1
h_3 : ¬(↑k : ℕ) < (↑j : ℕ)
h_4 : ¬(↑k : ℕ) + 1 < (↑i : ℕ)
⊢ (↑k : ℕ) = (↑k : ℕ) + 1 + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : ¬(↑j : ℕ) < (↑i : ℕ)
h_1 : (↑k : ℕ) < (↑i : ℕ)
h_2 : ¬(↑k : ℕ) < (↑j : ℕ) + 1
h_3 : (↑k : ℕ) < (↑j : ℕ)
⊢ (↑k : ℕ) + 1 = (↑k : ℕ)

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : ¬(↑j : ℕ) < (↑i : ℕ)
h_1 : (↑k : ℕ) < (↑i : ℕ)
h_2 : ¬(↑k : ℕ) < (↑j : ℕ) + 1
h_3 : ¬(↑k : ℕ) < (↑j : ℕ)
h_4 : (↑k : ℕ) + 1 < (↑i : ℕ)
⊢ (↑k : ℕ) + 1 = (↑k : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : ¬(↑j : ℕ) < (↑i : ℕ)
h_1 : (↑k : ℕ) < (↑i : ℕ)
h_2 : ¬(↑k : ℕ) < (↑j : ℕ) + 1
h_3 : ¬(↑k : ℕ) < (↑j : ℕ)
h_4 : ¬(↑k : ℕ) + 1 < (↑i : ℕ)
⊢ (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : ¬(↑j : ℕ) < (↑i : ℕ)
h_1 : ¬(↑k : ℕ) < (↑i : ℕ)
h_2 : (↑k : ℕ) + 1 < (↑j : ℕ) + 1
h_3 : (↑k : ℕ) < (↑j : ℕ)
⊢ (↑k : ℕ) + 1 = (↑k : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : ¬(↑j : ℕ) < (↑i : ℕ)
h_1 : ¬(↑k : ℕ) < (↑i : ℕ)
h_2 : (↑k : ℕ) + 1 < (↑j : ℕ) + 1
h_3 : ¬(↑k : ℕ) < (↑j : ℕ)
h_4 : (↑k : ℕ) + 1 < (↑i : ℕ)
⊢ (↑k : ℕ) + 1 = (↑k : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : ¬(↑j : ℕ) < (↑i : ℕ)
h_1 : ¬(↑k : ℕ) < (↑i : ℕ)
h_2 : (↑k : ℕ) + 1 < (↑j : ℕ) + 1
h_3 : ¬(↑k : ℕ) < (↑j : ℕ)
h_4 : ¬(↑k : ℕ) + 1 < (↑i : ℕ)
⊢ (↑k : ℕ) + 1 = (↑k : ℕ) + 1 + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : ¬(↑j : ℕ) < (↑i : ℕ)
h_1 : ¬(↑k : ℕ) < (↑i : ℕ)
h_2 : ¬(↑k : ℕ) + 1 < (↑j : ℕ) + 1
h_3 : (↑k : ℕ) < (↑j : ℕ)
⊢ (↑k : ℕ) + 1 + 1 = (↑k : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : ¬(↑j : ℕ) < (↑i : ℕ)
h_1 : ¬(↑k : ℕ) < (↑i : ℕ)
h_2 : ¬(↑k : ℕ) + 1 < (↑j : ℕ) + 1
h_3 : ¬(↑k : ℕ) < (↑j : ℕ)
h_4 : (↑k : ℕ) + 1 < (↑i : ℕ)
⊢ (↑k : ℕ) + 1 + 1 = (↑k : ℕ) + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 2)
j : Fin (n + 1)
k : Fin n
h : ¬(↑j : ℕ) < (↑i : ℕ)
h_1 : ¬(↑k : ℕ) < (↑i : ℕ)
h_2 : ¬(↑k : ℕ) + 1 < (↑j : ℕ) + 1
h_3 : ¬(↑k : ℕ) < (↑j : ℕ)
h_4 : ¬(↑k : ℕ) + 1 < (↑i : ℕ)
⊢ (↑k : ℕ) + 1 + 1 = (↑k : ℕ) + 1 + 1

Tactic:
lia
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
le_succ : ∀ (a : Fin 0), a ≤ a.elim0
max_of_succ_le : ∀ {a : Fin 0}, a.elim0 ≤ a → IsMax a
succ_le_of_lt : ∀ {a b : Fin 0}, a < b → a.elim0 ≤ b
succ : Fin 0 → Fin 0
⊢ SuccOrder (Fin 0)

Tactic:
constructor
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
a : Fin 0
⊢ a ≤ a.elim0

Tactic:
elim0 a

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
a : Fin 0
⊢ a ≤ a.elim0

Tactic:
exact elim0 a

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
a : Fin 0
⊢ a.elim0 ≤ a → IsMax a

Tactic:
elim0 a

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
a : Fin 0
⊢ a.elim0 ≤ a → IsMax a

Tactic:
exact elim0 a

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
a b : Fin 0
⊢ a < b → a.elim0 ≤ b

Tactic:
elim0 a

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
a : Fin 0
⊢ ∀ {b : Fin 0}, a < b → a.elim0 ≤ b

Tactic:
exact elim0 a

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
a : Fin 0
⊢ Fin 0

Tactic:
exact elim0 a

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
i : Fin (n + 1)
hi : ¬IsMax i
j : Fin (n + 1)
⊢ i ≠ last n

Tactic:
simpa using hi
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
i : Fin (n + 1)
hi : ¬IsMax i
j : Fin (n + 1)
obtain :
  ∀ (i : Fin n) (hi : ¬IsMax i.castSucc),
    i.castSucc < j ↔
      (fun (i : Fin (n + 1)) ↦
            (lastCases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) (last n) succ i : Fin (n + 1)))
          i.castSucc ≤
        j
⊢ i < j ↔
    (fun (i : Fin (n + 1)) ↦ (lastCases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) (last n) succ i : Fin (n + 1)))
        i ≤
      j

Tactic:
obtain ⟨i, rfl⟩ := Fin.eq_castSucc_of_ne_last (by simpa using hi)

Premises used: Fin.eq_castSucc_of_ne_last, rfl
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
j : Fin (n + 1)
i : Fin n
hi : ¬IsMax i.castSucc
⊢ i.castSucc < j ↔
    (fun (i : Fin (n + 1)) ↦ (lastCases (motive := fun (x : Fin (n + 1)) ↦ Fin (n + 1)) (last n) succ i : Fin (n + 1)))
        i.castSucc ≤
      j

Tactic:
simp [castSucc_lt_iff_succ_le]

Premises used: Fin.castSucc_lt_iff_succ_le
-- Module: Mathlib.Data.Fin.SuccPredOrder
Goal:
n : ℕ
i : Fin (n + 1)
hi : IsMax i
⊢ i = last n

Tactic:
simpa using hi