awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 1)
ha : a ≠ last n
⊢ (a.castPred ha).succ = a + 1
have last : ∀ (ha : last n ≠ last n), ((last n).castPred ha).succ = last n + 1
Tactic: cases a using lastCases
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 1)
ha : a ≠ Fin.last n
last : ∀ (ha : Fin.last n ≠ Fin.last n), ((Fin.last n).castPred ha).succ = Fin.last n + 1
⊢ (a.castPred ha).succ = a + 1
have cast : ∀ (i : Fin n) (ha : i.castSucc ≠ Fin.last n), (i.castSucc.castPred ha).succ = i.castSucc + 1
Tactic: cases a using lastCases
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin n
ha : i.castSucc ≠ last n
⊢ (i.castSucc.castPred ha).succ = i.castSucc + 1
have cast : i.succ = i.castSucc + 1
Tactic: rw [castPred_castSucc, coeSucc_eq_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin n
ha : i.castSucc ≠ last n
cast : i.succ = i.castSucc + 1
⊢ (i.castSucc.castPred ha).succ = i.castSucc + 1
have cast₁ : i.succ = i.succ
Tactic: rw [castPred_castSucc, coeSucc_eq_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ a.succ.castPred ha ≤ b ↔ a < b
have rw : a.succ ≤ b.castSucc ↔ a < b
Tactic: rw [castPred_le_iff, succ_le_castSucc_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
rw : a.succ ≤ b.castSucc ↔ a < b
⊢ a.succ.castPred ha ≤ b ↔ a < b
have rw₁ : a < b ↔ a < b
Tactic: rw [castPred_le_iff, succ_le_castSucc_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ b < a.succ.castPred ha ↔ b ≤ a
have rw : b.castSucc < a.succ ↔ b ≤ a
Tactic: rw [lt_castPred_iff, castSucc_lt_succ_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
rw : b.castSucc < a.succ ↔ b ≤ a
⊢ b < a.succ.castPred ha ↔ b ≤ a
have rw₁ : b ≤ a ↔ b ≤ a
Tactic: rw [lt_castPred_iff, castSucc_lt_succ_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
⊢ a < a.succ.castPred ha
have rw : a ≤ a
Tactic: rw [lt_castPred_succ_iff, le_def]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
rw : a ≤ a
⊢ a < a.succ.castPred ha
have rw₁ : (↑a : ℕ) ≤ (↑a : ℕ)
Tactic: rw [lt_castPred_succ_iff, le_def]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
⊢ (a.castPred ha).succ ≤ b ↔ a < b
have rw : a.succ.castPred sorry ≤ b ↔ a < b
Tactic: rw [succ_castPred_eq_castPred_succ ha, castpred_succ_le_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
rw : a.succ.castPred ⋯ ≤ b ↔ a < b
⊢ (a.castPred ha).succ ≤ b ↔ a < b
have rw₁ : a < b ↔ a < b
Tactic: rw [succ_castPred_eq_castPred_succ ha, castpred_succ_le_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
⊢ b < (a.castPred ha).succ ↔ b ≤ a
have rw : b < a.succ.castPred sorry ↔ b ≤ a
Tactic: rw [succ_castPred_eq_castPred_succ ha, lt_castPred_succ_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
rw : b < a.succ.castPred ⋯ ↔ b ≤ a
⊢ b < (a.castPred ha).succ ↔ b ≤ a
have rw₁ : b ≤ a ↔ b ≤ a
Tactic: rw [succ_castPred_eq_castPred_succ ha, lt_castPred_succ_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 1)
ha : a ≠ last n
⊢ a < (a.castPred ha).succ
have rw : a ≤ a
Tactic: rw [lt_succ_castPred_iff, le_def]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 1)
ha : a ≠ last n
rw : a ≤ a
⊢ a < (a.castPred ha).succ
have rw₁ : (↑a : ℕ) ≤ (↑a : ℕ)
Tactic: rw [lt_succ_castPred_iff, le_def]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
hb : b ≠ 0
⊢ a.castPred ha ≤ b.pred hb ↔ a < b
have rw : (a.castPred ha).succ ≤ b ↔ a < b
Tactic: rw [le_pred_iff, succ_castPred_le_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
hb : b ≠ 0
rw : (a.castPred ha).succ ≤ b ↔ a < b
⊢ a.castPred ha ≤ b.pred hb ↔ a < b
have rw₁ : a < b ↔ a < b
Tactic: rw [le_pred_iff, succ_castPred_le_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ last n
⊢ a.pred ha < b.castPred hb ↔ a ≤ b
have rw : (a.pred ha).castSucc < b ↔ a ≤ b
Tactic: rw [lt_castPred_iff, castSucc_pred_lt_iff ha]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ last n
rw : (a.pred ha).castSucc < b ↔ a ≤ b
⊢ a.pred ha < b.castPred hb ↔ a ≤ b
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [lt_castPred_iff, castSucc_pred_lt_iff ha]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 1)
h₁ : a ≠ 0
h₂ : a ≠ last n
⊢ a.pred h₁ < a.castPred h₂
have rw : a ≤ a
Tactic: rw [pred_lt_castPred_iff, le_def]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 1)
h₁ : a ≠ 0
h₂ : a ≠ last n
rw : a ≤ a
⊢ a.pred h₁ < a.castPred h₂
have rw₁ : (↑a : ℕ) ≤ (↑a : ℕ)
Tactic: rw [pred_lt_castPred_iff, le_def]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin (n + 1)
h : p < i
⊢ p.succAbove (i.pred ⋯) = i
have rw : (i.pred sorry).succ = i
Tactic: rw [succAbove_of_lt_succ _ _ (succ_pred _ _ ▸ h), succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin (n + 1)
h : p < i
rw : (i.pred ⋯).succ = i
⊢ p.succAbove (i.pred ⋯) = i
have rw₁ : i = i
Tactic: rw [succAbove_of_lt_succ _ _ (succ_pred _ _ ▸ h), succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin (n + 1)
h : i < p
⊢ p.succAbove (i.castPred ⋯) = i
have rw : (i.castPred sorry).castSucc = i
Tactic: rw [succAbove_of_castSucc_lt _ _ (castSucc_castPred _ _ ▸ h), castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin (n + 1)
h : i < p
rw : (i.castPred ⋯).castSucc = i
⊢ p.succAbove (i.castPred ⋯) = i
have rw₁ : i = i
Tactic: rw [succAbove_of_castSucc_lt _ _ (castSucc_castPred _ _ ▸ h), castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i ≠ p
have inl : ∀ (h : i.castSucc < p), p.succAbove i ≠ p
Tactic: rcases p.castSucc_lt_or_lt_succ i with (h | h)
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
inl : ∀ (h : i.castSucc < p), p.succAbove i ≠ p
⊢ p.succAbove i ≠ p
have inr : ∀ (h : p < i.succ), p.succAbove i ≠ p
Tactic: rcases p.castSucc_lt_or_lt_succ i with (h | h)
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.castSucc < p
⊢ p.succAbove i ≠ p
have inl : i.castSucc ≠ p
Tactic: rw [succAbove_of_castSucc_lt _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p < i.succ
⊢ p.succAbove i ≠ p
have inr : i.succ ≠ p
Tactic: rw [succAbove_of_lt_succ _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i j : Fin n
hij : (if i.castSucc < p then i.castSucc else i.succ) = if j.castSucc < p then j.castSucc else j.succ
⊢ i = j
have pos : ∀ (hi : i.castSucc < p) (hj : j.castSucc < p) (hij : i.castSucc = j.castSucc), i = j
Tactic: split_ifs at hij with hi hj hj
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i j : Fin n
hij : (if i.castSucc < p then i.castSucc else i.succ) = if j.castSucc < p then j.castSucc else j.succ
pos : ∀ (hi : i.castSucc < p) (hj : j.castSucc < p) (hij : i.castSucc = j.castSucc), i = j
⊢ i = j
have neg : ∀ (hi : i.castSucc < p) (hj : ¬j.castSucc < p) (hij : i.castSucc = j.succ), i = j
Tactic: split_ifs at hij with hi hj hj
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i j : Fin n
hij : (if i.castSucc < p then i.castSucc else i.succ) = if j.castSucc < p then j.castSucc else j.succ
pos : ∀ (hi : i.castSucc < p) (hj : j.castSucc < p) (hij : i.castSucc = j.castSucc), i = j
neg : ∀ (hi : i.castSucc < p) (hj : ¬j.castSucc < p) (hij : i.castSucc = j.succ), i = j
⊢ i = j
have pos₁ : ∀ (hi : ¬i.castSucc < p) (hj : j.castSucc < p) (hij : i.succ = j.castSucc), i = j
Tactic: split_ifs at hij with hi hj hj
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i j : Fin n
hij : (if i.castSucc < p then i.castSucc else i.succ) = if j.castSucc < p then j.castSucc else j.succ
pos : ∀ (hi : i.castSucc < p) (hj : j.castSucc < p) (hij : i.castSucc = j.castSucc), i = j
neg : ∀ (hi : i.castSucc < p) (hj : ¬j.castSucc < p) (hij : i.castSucc = j.succ), i = j
pos₁ : ∀ (hi : ¬i.castSucc < p) (hj : j.castSucc < p) (hij : i.succ = j.castSucc), i = j
⊢ i = j
have neg₁ : ∀ (hi : ¬i.castSucc < p) (hj : ¬j.castSucc < p) (hij : i.succ = j.succ), i = j
Tactic: split_ifs at hij with hi hj hj
Cleared hypotheses: hij
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (hypothesis)
Goal:
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : i.castSucc < p
hj : ¬j.castSucc < p
hij : i.castSucc = j.succ
⊢ i = j
have hi₁ : j.succ < p
Tactic: rw [hij] at hi
Cleared hypotheses: hi, hj, hij
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (hypothesis)
Goal:
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : j.castSucc < p
hij : i.succ = j.castSucc
⊢ i = j
have hj₁ : i.succ < p
Tactic: rw [← hij] at hj
Cleared hypotheses: hj, hij
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ a.succAbove 0 = 0
have rw : Eq (α := Fin (n + 1)) (castSucc 0) 0
Tactic: rw [Fin.succAbove_of_castSucc_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
rw : Eq (α := Fin (n + 1)) (castSucc 0) 0
⊢ a.succAbove 0 = 0
have h : castSucc 0 < a
Tactic: rw [Fin.succAbove_of_castSucc_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
a : Fin (n + 1)
b : Fin n
ha : a ≠ 0
⊢ a.succAbove b = 0 ↔ b = 0
have rw : a.succAbove b = a.succAbove 0 ↔ b = 0
Tactic: rw [← succAbove_ne_zero_zero ha, succAbove_right_inj]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
a : Fin (n + 1)
b : Fin n
ha : a ≠ 0
rw : a.succAbove b = a.succAbove 0 ↔ b = 0
⊢ a.succAbove b = 0 ↔ b = 0
have rw₁ : b = 0 ↔ b = 0
Tactic: rw [← succAbove_ne_zero_zero ha, succAbove_right_inj]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin n
⊢ succAbove 0 i = i.succ
have rw : i.succ = i.succ
Tactic: rw [succAbove_zero]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 2)
h : a ≠ last (n + 1)
⊢ a.succAbove (last n) = last (n + 1)
have rw : (last n).succ = last (n + 1)
Tactic: rw [succAbove_of_lt_succ _ _ (succ_last _ ▸ lt_last_iff_ne_last.2 h), succ_last]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 2)
h : a ≠ last (n + 1)
rw : (last n).succ = last (n + 1)
⊢ a.succAbove (last n) = last (n + 1)
have rw₁ : Eq (α := Fin (n + 1 + 1)) (last n.succ) (last (n + 1))
Tactic: rw [succAbove_of_lt_succ _ _ (succ_last _ ▸ lt_last_iff_ne_last.2 h), succ_last]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
⊢ a.succAbove b = last (n + 1) ↔ b = last n
have rw : a.succAbove b = a.succAbove (last n) ↔ b = last n
Tactic: rw [← succAbove_ne_last_last ha, succAbove_right_inj]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
rw : a.succAbove b = a.succAbove (last n) ↔ b = last n
⊢ a.succAbove b = last (n + 1) ↔ b = last n
have rw₁ : b = last n ↔ b = last n
Tactic: rw [← succAbove_ne_last_last ha, succAbove_right_inj]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
⊢ (last n).succAbove = castSucc
have h : ∀ (x : Fin n), (↑((last n).succAbove x) : ℕ) = (↑x.castSucc : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin n
⊢ (last n).succAbove i = i.castSucc
have rw : i.castSucc = i.castSucc
Tactic: rw [succAbove_last]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i < p ↔ i.castSucc < p
have inl : ∀ (H : i.castSucc < p), p.succAbove i < p ↔ i.castSucc < p
Tactic: rcases castSucc_lt_or_lt_succ p i with H | H
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
inl : ∀ (H : i.castSucc < p), p.succAbove i < p ↔ i.castSucc < p
⊢ p.succAbove i < p ↔ i.castSucc < p
have inr : ∀ (H : p < i.succ), p.succAbove i < p ↔ i.castSucc < p
Tactic: rcases castSucc_lt_or_lt_succ p i with H | H
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ p.succAbove i < p ↔ i.castSucc < p
have inl : p.succAbove i < p
Tactic: rwa [iff_true_right H, succAbove_of_castSucc_lt _ _ H]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p.succAbove i < p ↔ i.castSucc < p
have inr : ¬i.succ < p
Tactic: rw [castSucc_lt_iff_succ_le, iff_false_right (Fin.not_le.2 H), succAbove_of_lt_succ _ _ H]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p.succAbove i < p ↔ i.succ ≤ p
have rw : i.castSucc < p ↔ i.succ ≤ p
Tactic: rw [succAbove_lt_iff_castSucc_lt, castSucc_lt_iff_succ_le]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
rw : i.castSucc < p ↔ i.succ ≤ p
⊢ p.succAbove i < p ↔ i.succ ≤ p
have rw₁ : i.succ ≤ p ↔ i.succ ≤ p
Tactic: rw [succAbove_lt_iff_castSucc_lt, castSucc_lt_iff_succ_le]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p < p.succAbove i ↔ p ≤ i.castSucc
have inl : ∀ (H : i.castSucc < p), p < p.succAbove i ↔ p ≤ i.castSucc
Tactic: rcases castSucc_lt_or_lt_succ p i with H | H
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
inl : ∀ (H : i.castSucc < p), p < p.succAbove i ↔ p ≤ i.castSucc
⊢ p < p.succAbove i ↔ p ≤ i.castSucc
have inr : ∀ (H : p < i.succ), p < p.succAbove i ↔ p ≤ i.castSucc
Tactic: rcases castSucc_lt_or_lt_succ p i with H | H
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ p < p.succAbove i ↔ p ≤ i.castSucc
have inl : ¬p < i.castSucc
Tactic: rw [iff_false_right (Fin.not_le.2 H), succAbove_of_castSucc_lt _ _ H]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ p < p.succAbove i ↔ p ≤ i.castSucc
have inr : p < i.succ ↔ p ≤ i.castSucc
Tactic: rwa [succAbove_of_lt_succ _ _ H, iff_true_left H, le_castSucc_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
inr : p < i.succ ↔ p ≤ i.castSucc
⊢ p < p.succAbove i ↔ p ≤ i.castSucc
have inr₁ : p ≤ i.castSucc
Tactic: rwa [succAbove_of_lt_succ _ _ H, iff_true_left H, le_castSucc_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p < p.succAbove i ↔ p < i.succ
have rw : p ≤ i.castSucc ↔ p < i.succ
Tactic: rw [lt_succAbove_iff_le_castSucc, le_castSucc_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
rw : p ≤ i.castSucc ↔ p < i.succ
⊢ p < p.succAbove i ↔ p < i.succ
have rw₁ : p < i.succ ↔ p < i.succ
Tactic: rw [lt_succAbove_iff_le_castSucc, le_castSucc_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
⊢ 0 < p.succAbove i
have pos : ∀ (H : i.castSucc < p), 0 < p.succAbove i
Tactic: by_cases H : castSucc i < p
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
pos : ∀ (H : i.castSucc < p), 0 < p.succAbove i
⊢ 0 < p.succAbove i
have neg : ∀ (H : ¬i.castSucc < p), 0 < p.succAbove i
Tactic: by_cases H : castSucc i < p
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
x : Fin n
y : Fin (n + 1)
h : x.castSucc < y
h' : y.succAbove x ≠ last n
⊢ (y.succAbove x).castPred h' = x
have rw : y.succAbove x = x.castSucc
Tactic: rw [castPred_eq_iff_eq_castSucc, succAbove_of_castSucc_lt _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
x : Fin n
y : Fin (n + 1)
h : x.castSucc < y
h' : y.succAbove x ≠ last n
rw : y.succAbove x = x.castSucc
⊢ (y.succAbove x).castPred h' = x
have rw₁ : x.castSucc = x.castSucc
Tactic: rw [castPred_eq_iff_eq_castSucc, succAbove_of_castSucc_lt _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
x y : Fin (n + 1)
h : x ≠ y
⊢ ∃ (z : Fin n), y.succAbove z = x
have inl : ∀ (hxy : x < y), ∃ (z : Fin n), y.succAbove z = x
Tactic: obtain hxy | hyx := Fin.lt_or_lt_of_ne h
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
x y : Fin (n + 1)
h : x ≠ y
inl : ∀ (hxy : x < y), ∃ (z : Fin n), y.succAbove z = x
⊢ ∃ (z : Fin n), y.succAbove z = x
have inr : ∀ (hyx : y < x), ∃ (z : Fin n), y.succAbove z = x
Tactic: obtain hxy | hyx := Fin.lt_or_lt_of_ne h
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
⊢ Eq (α := Set (Fin (n + 1))) (Set.range succ) {0}ᶜ
have rw : Eq (α := Set (Fin (n + 1))) (Set.range (succAbove 0)) {0}ᶜ
Tactic: rw [← succAbove_zero, range_succAbove]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
rw : Eq (α := Set (Fin (n + 1))) (Set.range (succAbove 0)) {0}ᶜ
⊢ Eq (α := Set (Fin (n + 1))) (Set.range succ) {0}ᶜ
have rw₁ : Eq (α := Set (Fin (n + 1))) {0}ᶜ {0}ᶜ
Tactic: rw [← succAbove_zero, range_succAbove]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ
have inl : ∀ (h : i < j.succ), i.succ.succAbove j.succ = (i.succAbove j).succ
Tactic: obtain h | h := i.lt_or_ge (succ j)
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
inl : ∀ (h : i < j.succ), i.succ.succAbove j.succ = (i.succAbove j).succ
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ
have inr : ∀ (h : j.succ ≤ i), i.succ.succAbove j.succ = (i.succAbove j).succ
Tactic: obtain h | h := i.lt_or_ge (succ j)
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i < j.succ
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ
have inl : i.succ.succAbove j.succ = j.succ.succ
Tactic: rw [succAbove_of_lt_succ _ _ h, succAbove_succ_of_lt _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i < j.succ
inl : i.succ.succAbove j.succ = j.succ.succ
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ
have inl₁ : j.succ.succ = j.succ.succ
Tactic: rw [succAbove_of_lt_succ _ _ h, succAbove_succ_of_lt _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.succ ≤ i
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ
have inr : i.succ.succAbove j.succ = j.castSucc.succ
Tactic: rwa [succAbove_of_castSucc_lt _ _ h, succAbove_succ_of_le, succ_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.succ ≤ i
inr : i.succ.succAbove j.succ = j.castSucc.succ
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ
have inr₁ : j.succ.castSucc = j.castSucc.succ
Tactic: rwa [succAbove_of_castSucc_lt _ _ h, succAbove_succ_of_le, succ_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.succ ≤ i
inr : i.succ.succAbove j.succ = j.castSucc.succ
inr₁ : j.succ.castSucc = j.castSucc.succ
inr₂ : j.succ ≤ i
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ
have inr₃ : j.succ.castSucc = j.succ.castSucc
Tactic: rwa [succAbove_of_castSucc_lt _ _ h, succAbove_succ_of_le, succ_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
have inl : ∀ (h : i ≤ j.castSucc), i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
Tactic: rcases i.le_or_gt (castSucc j) with (h | h)
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
inl : ∀ (h : i ≤ j.castSucc), i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
have inr : ∀ (h : j.castSucc < i), i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
Tactic: rcases i.le_or_gt (castSucc j) with (h | h)
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
have inl : i.castSucc.succAbove j.castSucc = j.succ.castSucc
Tactic: rw [succAbove_of_le_castSucc _ _ h, succAbove_castSucc_of_le _ _ h, succ_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
inl : i.castSucc.succAbove j.castSucc = j.succ.castSucc
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
have inl₁ : j.castSucc.succ = j.succ.castSucc
Tactic: rw [succAbove_of_le_castSucc _ _ h, succAbove_castSucc_of_le _ _ h, succ_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
inl : i.castSucc.succAbove j.castSucc = j.succ.castSucc
inl₁ : j.castSucc.succ = j.succ.castSucc
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
have inl₂ : j.succ.castSucc = j.succ.castSucc
Tactic: rw [succAbove_of_le_castSucc _ _ h, succAbove_castSucc_of_le _ _ h, succ_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
have inr : i.castSucc.succAbove j.castSucc = j.castSucc.castSucc
Tactic: rw [succAbove_of_castSucc_lt _ _ h, succAbove_castSucc_of_lt _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
inr : i.castSucc.succAbove j.castSucc = j.castSucc.castSucc
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
have inr₁ : j.castSucc.castSucc = j.castSucc.castSucc
Tactic: rw [succAbove_of_castSucc_lt _ _ h, succAbove_castSucc_of_lt _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : a.succAbove b ≠ 0
⊢ (a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk
have simp_rw : ((a.pred ha).succAbove (b.pred hb)).succ = ((a.succAbove b).pred hk).succ
Tactic: simp_rw [← succ_inj (b := pred (succAbove a b) hk), ← succ_succAbove_succ, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ 0
hk : a.succAbove b ≠ 0
simp_rw : ((a.pred ha).succAbove (b.pred hb)).succ = ((a.succAbove b).pred hk).succ
⊢ (a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk
have simp_rw₁ : (a.pred ha).succ.succAbove (b.pred hb).succ = ((a.succAbove b).pred hk).succ
Tactic: simp_rw [← succ_inj (b := pred (succAbove a b) hk), ← succ_succAbove_succ, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
hb : b ≠ last n
hk : a.succAbove b ≠ last (n + 1)
⊢ (a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk
have simp_rw : ((a.castPred ha).succAbove (b.castPred hb)).castSucc = ((a.succAbove b).castPred hk).castSucc
Tactic: simp_rw [← castSucc_inj (b := (a.succAbove b).castPred hk), ← castSucc_succAbove_castSucc,
    castSucc_castPred]