awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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)
simp_rw : ((a.castPred ha).succAbove (b.castPred hb)).castSucc = ((a.succAbove b).castPred hk).castSucc
⊢ (a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk
have simp_rw₁ : (a.castPred ha).castSucc.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]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
⊢ i.succ.succAbove 1 = (i.succAbove 0).succ
have rw : i.succ.succAbove (succ 0) = (i.succAbove 0).succ
Tactic: rw [← succ_zero_eq_one']
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (hypothesis)
Goal:
n : ℕ
j : Fin n
⊢ succAbove 1 j.succ = j.succ.succ
have this : succAbove (succ 0) j.succ = (succAbove 0 j).succ
Tactic: have := succ_succAbove_succ 0 j
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
this : succAbove (succ 0) j.succ = (succAbove 0 j).succ
⊢ succAbove 1 j.succ = j.succ.succ
have rwa : ∀ (this : succAbove 1 j.succ = (succAbove 0 j).succ), succAbove 1 j.succ = j.succ.succ
Tactic: rwa [succ_zero_eq_one, zero_succAbove] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
this : succAbove (succ 0) j.succ = (succAbove 0 j).succ
rwa : ∀ (this : succAbove 1 j.succ = (succAbove 0 j).succ), succAbove 1 j.succ = j.succ.succ
⊢ succAbove 1 j.succ = j.succ.succ
have rwa₁ : ∀ (this : succAbove 1 j.succ = j.succ.succ), succAbove 1 j.succ = j.succ.succ
Tactic: rwa [succ_zero_eq_one, zero_succAbove] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin n
h : i < p
⊢ p.predAbove i.succ = i.succ.castPred ⋯
have rw : i.succ.castPred sorry = i.succ.castPred sorry
Tactic: rw [predAbove_of_lt_succ _ _ (succ_lt_succ_iff.mpr h)]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin n
h : p ≤ i
⊢ p.predAbove i.succ = i
have rw : i.succ.pred sorry = i
Tactic: rw [predAbove_of_succ_le _ _ (succ_le_succ_iff.mpr h), pred_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin n
h : p ≤ i
rw : i.succ.pred ⋯ = i
⊢ p.predAbove i.succ = i
have rw₁ : i = i
Tactic: rw [predAbove_of_succ_le _ _ (succ_le_succ_iff.mpr h), pred_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin n
h : p < i
⊢ p.predAbove i.castSucc = i.castSucc.pred ⋯
have rw : i.castSucc.pred sorry = i.castSucc.pred sorry
Tactic: rw [predAbove_of_castSucc_lt _ _ (castSucc_lt_castSucc_iff.2 h)]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin n
h : i ≤ p
⊢ p.predAbove i.castSucc = i
have rw : i.castSucc.castPred sorry = i
Tactic: rw [predAbove_of_le_castSucc _ _ (castSucc_le_castSucc_iff.mpr h), castPred_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin n
h : i ≤ p
rw : i.castSucc.castPred ⋯ = i
⊢ p.predAbove i.castSucc = i
have rw₁ : i = i
Tactic: rw [predAbove_of_le_castSucc _ _ (castSucc_le_castSucc_iff.mpr h), castPred_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin (n + 1)
h : i < p
⊢ (p.pred ⋯).predAbove i = i.castPred ⋯
have rw : i.castPred sorry = i.castPred sorry
Tactic: rw [predAbove_of_lt_succ _ _ (succ_pred _ _ ▸ h)]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin (n + 1)
h : p ≤ i
hp : p ≠ 0
⊢ (p.pred hp).predAbove i = i.pred ⋯
have rw : i.pred sorry = i.pred sorry
Tactic: rw [predAbove_of_succ_le _ _ (succ_pred _ _ ▸ h)]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin (n + 1)
h : p < i
⊢ (p.castPred ⋯).predAbove i = i.pred ⋯
have rw : i.pred sorry = i.pred sorry
Tactic: rw [predAbove_of_castSucc_lt _ _ (castSucc_castPred _ _ ▸ h)]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin (n + 1)
h : i ≤ p
hp : p ≠ last n
⊢ (p.castPred hp).predAbove i = i.castPred ⋯
have rw : i.castPred sorry = i.castPred sorry
Tactic: rw [predAbove_of_le_castSucc _ _ (castSucc_castPred _ _ ▸ h)]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin n
⊢ i.predAbove 0 = 0
have zero : ∀ [inst : NeZero (R := ℕ) 0] {i : Fin 0}, i.predAbove 0 = 0
Tactic: cases n
Cleared hypotheses: n, inst, i
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin n
zero : ∀ [inst : NeZero (R := ℕ) 0] {i : Fin 0}, i.predAbove 0 = 0
⊢ i.predAbove 0 = 0
have succ : ∀ (n : ℕ) [inst : NeZero (n + 1)] {i : Fin (n + 1)}, i.predAbove 0 = 0
Tactic: cases n
Cleared hypotheses: n, inst, i
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero (n + 1)
i : Fin (n + 1)
⊢ i.predAbove 0 = 0
have succ : castPred 0 sorry = 0
Tactic: rw [predAbove_of_le_castSucc _ _ (zero_le _), castPred_zero]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero (n + 1)
i : Fin (n + 1)
succ : castPred 0 ⋯ = 0
⊢ i.predAbove 0 = 0
have succ₁ : Eq (α := Fin (n + 1)) 0 0
Tactic: rw [predAbove_of_le_castSucc _ _ (zero_le _), castPred_zero]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin n
⊢ predAbove 0 i.succ = i
have rw : i = i
Tactic: rw [predAbove_succ_of_le _ _ (Fin.zero_le _)]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
hi : i ≠ 0
⊢ predAbove 0 i = i.pred hi
have obtain : ∀ (y : Fin n) (hi : y.succ ≠ 0), predAbove 0 y.succ = y.succ.pred hi
Tactic: obtain ⟨y, rfl⟩ := exists_succ_eq.2 hi
Cleared hypotheses: i, hi
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
⊢ predAbove 0 i = if hi : i = 0 then 0 else i.pred hi
have pos : ∀ (hi : i = 0), predAbove 0 i = 0
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
pos : ∀ (hi : i = 0), predAbove 0 i = 0
⊢ predAbove 0 i = if hi : i = 0 then 0 else i.pred hi
have neg : ∀ (hi : ¬i = 0), predAbove 0 i = i.pred hi
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
hi : i = 0
⊢ predAbove 0 i = 0
have pos : Eq (α := Fin n) (predAbove 0 0) 0
Tactic: rw [hi, predAbove_right_zero]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
hi : i = 0
pos : Eq (α := Fin n) (predAbove 0 0) 0
⊢ predAbove 0 i = 0
have pos₁ : Eq (α := Fin n) 0 0
Tactic: rw [hi, predAbove_right_zero]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
hi : ¬i = 0
⊢ predAbove 0 i = i.pred hi
have neg : i.pred hi = i.pred hi
Tactic: rw [predAbove_zero_of_ne_zero hi]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ i.predAbove (last (n + 1)) = last n
have rw : pred (last (n + 1)) sorry = last n
Tactic: rw [predAbove_of_castSucc_lt _ _ (castSucc_lt_last _), pred_last]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
rw : pred (last (n + 1)) ⋯ = last n
⊢ i.predAbove (last (n + 1)) = last n
have rw₁ : last n = last n
Tactic: rw [predAbove_of_castSucc_lt _ _ (castSucc_lt_last _), pred_last]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
⊢ (last n).predAbove i.castSucc = i
have rw : i.castSucc.castPred sorry = i
Tactic: rw [predAbove_of_le_castSucc _ _ (castSucc_le_castSucc_iff.mpr (le_last _)), castPred_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
rw : i.castSucc.castPred ⋯ = i
⊢ (last n).predAbove i.castSucc = i
have rw₁ : i = i
Tactic: rw [predAbove_of_le_castSucc _ _ (castSucc_le_castSucc_iff.mpr (le_last _)), castPred_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (hypothesis)
Goal:
n : ℕ
i : Fin (n + 2)
hi : i ≠ last (n + 1)
⊢ (last n).predAbove i = i.castPred hi
have hi₁ : ∃ (j : Fin (n + 1)), j.castSucc = i
Tactic: rw [← exists_castSucc_eq] at hi
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
hi_1 : i ≠ last (n + 1)
hi : ∃ (j : Fin (n + 1)), j.castSucc = i
⊢ (last n).predAbove i = i.castPred hi_1
have rcases : ∀ (y : Fin (n + 1)) (hi : y.castSucc ≠ last (n + 1)), (last n).predAbove y.castSucc = y.castSucc.castPred hi
Tactic: rcases hi with ⟨y, rfl⟩
Cleared hypotheses: i, hi_1, hi
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
⊢ (last n).predAbove i = if hi : i = last (n + 1) then last n else i.castPred hi
have pos : ∀ (hi : i = last (n + 1)), (last n).predAbove i = last n
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
pos : ∀ (hi : i = last (n + 1)), (last n).predAbove i = last n
⊢ (last n).predAbove i = if hi : i = last (n + 1) then last n else i.castPred hi
have neg : ∀ (hi : ¬i = last (n + 1)), (last n).predAbove i = i.castPred hi
Tactic: split_ifs with hi
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
hi : i = last (n + 1)
⊢ (last n).predAbove i = last n
have pos : (last n).predAbove (last (n + 1)) = last n
Tactic: rw [hi, predAbove_right_last]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
hi : i = last (n + 1)
pos : (last n).predAbove (last (n + 1)) = last n
⊢ (last n).predAbove i = last n
have pos₁ : last n = last n
Tactic: rw [hi, predAbove_right_last]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 2)
hi : ¬i = last (n + 1)
⊢ (last n).predAbove i = i.castPred hi
have neg : i.castPred hi = i.castPred hi
Tactic: rw [predAbove_last_of_ne_last hi]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin n
⊢ ∃ (a : Fin (n + 1)), p.predAbove a = i
have pos : ∀ (hi : i ≤ p), ∃ (a : Fin (n + 1)), p.predAbove a = i
Tactic: by_cases hi : i ≤ p
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin n
pos : ∀ (hi : i ≤ p), ∃ (a : Fin (n + 1)), p.predAbove a = i
⊢ ∃ (a : Fin (n + 1)), p.predAbove a = i
have neg : ∀ (hi : ¬i ≤ p), ∃ (a : Fin (n + 1)), p.predAbove a = i
Tactic: by_cases hi : i ≤ p
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (hypothesis)
Goal:
n : ℕ
p i : Fin n
hi : ¬i ≤ p
⊢ ∃ (a : Fin (n + 1)), p.predAbove a = i
have hi₁ : p < i
Tactic: rw [Fin.not_le] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i ≠ p.castSucc
⊢ p.castSucc.succAbove (p.predAbove i) = i
have inl : ∀ (h : i < p.castSucc), p.castSucc.succAbove (p.predAbove i) = i
Tactic: obtain h | h := Fin.lt_or_lt_of_ne h
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
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
⊢ p.castSucc.succAbove (p.predAbove i) = i
have inr : ∀ (h : p.castSucc < i), p.castSucc.succAbove (p.predAbove i) = i
Tactic: obtain h | h := Fin.lt_or_lt_of_ne h
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h_1 : i ≠ p.castSucc
h : i < p.castSucc
⊢ p.castSucc.succAbove (p.predAbove i) = i
have inl : p.castSucc.succAbove (i.castPred sorry) = i
Tactic: rw [predAbove_of_le_castSucc _ _ (Fin.le_of_lt h), succAbove_castPred_of_lt _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
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
⊢ p.castSucc.succAbove (p.predAbove i) = i
have inl₁ : i = i
Tactic: rw [predAbove_of_le_castSucc _ _ (Fin.le_of_lt h), succAbove_castPred_of_lt _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h_1 : i ≠ p.castSucc
h : p.castSucc < i
⊢ p.castSucc.succAbove (p.predAbove i) = i
have inr : p.castSucc.succAbove (i.pred sorry) = i
Tactic: rw [predAbove_of_castSucc_lt _ _ h, succAbove_pred_of_lt _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
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
⊢ p.castSucc.succAbove (p.predAbove i) = i
have inr₁ : i = i
Tactic: rw [predAbove_of_castSucc_lt _ _ h, succAbove_pred_of_lt _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i ≠ p.succ
⊢ p.succ.succAbove (p.predAbove i) = i
have inl : ∀ (h : i < p.succ), p.succ.succAbove (p.predAbove i) = i
Tactic: obtain h | h := Fin.lt_or_lt_of_ne h
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
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
⊢ p.succ.succAbove (p.predAbove i) = i
have inr : ∀ (h : p.succ < i), p.succ.succAbove (p.predAbove i) = i
Tactic: obtain h | h := Fin.lt_or_lt_of_ne h
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h_1 : i ≠ p.succ
h : i < p.succ
⊢ p.succ.succAbove (p.predAbove i) = i
have inl : p.succ.succAbove (i.castPred sorry) = i
Tactic: rw [predAbove_of_le_castSucc _ _ (le_castSucc_iff.2 h),
      succAbove_castPred_of_lt _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
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
⊢ p.succ.succAbove (p.predAbove i) = i
have inl₁ : i = i
Tactic: rw [predAbove_of_le_castSucc _ _ (le_castSucc_iff.2 h),
      succAbove_castPred_of_lt _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h_1 : i ≠ p.succ
h : p.succ < i
⊢ p.succ.succAbove (p.predAbove i) = i
have inr : p.succ.succAbove (i.pred sorry) = i
Tactic: rw [predAbove_of_castSucc_lt _ _ (Fin.lt_of_le_of_lt (p.castSucc_le_succ) h),
      succAbove_pred_of_lt _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
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
⊢ p.succ.succAbove (p.predAbove i) = i
have inr₁ : i = i
Tactic: rw [predAbove_of_castSucc_lt _ _ (Fin.lt_of_le_of_lt (p.castSucc_le_succ) h),
      succAbove_pred_of_lt _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin n
⊢ p.predAbove (p.castSucc.succAbove i) = i
have inl : ∀ (h : p ≤ i), p.predAbove (p.castSucc.succAbove i) = i
Tactic: obtain h | h := p.le_or_gt i
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin n
inl : ∀ (h : p ≤ i), p.predAbove (p.castSucc.succAbove i) = i
⊢ p.predAbove (p.castSucc.succAbove i) = i
have inr : ∀ (h : i < p), p.predAbove (p.castSucc.succAbove i) = i
Tactic: obtain h | h := p.le_or_gt i
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin n
h : p ≤ i
⊢ p.predAbove (p.castSucc.succAbove i) = i
have inl : p.predAbove i.succ = i
Tactic: rw [succAbove_castSucc_of_le _ _ h, predAbove_succ_of_le _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin n
h : p ≤ i
inl : p.predAbove i.succ = i
⊢ p.predAbove (p.castSucc.succAbove i) = i
have inl₁ : i = i
Tactic: rw [succAbove_castSucc_of_le _ _ h, predAbove_succ_of_le _ _ h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin n
h : i < p
⊢ p.predAbove (p.castSucc.succAbove i) = i
have inr : p.predAbove i.castSucc = i
Tactic: rw [succAbove_castSucc_of_lt _ _ h, predAbove_castSucc_of_le _ _ <| Fin.le_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin n
h : i < p
inr : p.predAbove i.castSucc = i
⊢ p.predAbove (p.castSucc.succAbove i) = i
have inr₁ : i = i
Tactic: rw [succAbove_castSucc_of_lt _ _ h, predAbove_castSucc_of_le _ _ <| Fin.le_of_lt h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ
have inl : ∀ (h : a.succ ≤ b), a.succ.predAbove b.succ = (a.predAbove b).succ
Tactic: obtain h | h := Fin.le_or_gt (succ a) b
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
inl : ∀ (h : a.succ ≤ b), a.succ.predAbove b.succ = (a.predAbove b).succ
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ
have inr : ∀ (h : b < a.succ), a.succ.predAbove b.succ = (a.predAbove b).succ
Tactic: obtain h | h := Fin.le_or_gt (succ a) b
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.succ ≤ b
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ
have inl : a.succ.predAbove b.succ = (b.pred sorry).succ
Tactic: rw [predAbove_of_castSucc_lt _ _ h, predAbove_succ_of_le _ _ h, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.succ ≤ b
inl : a.succ.predAbove b.succ = (b.pred ⋯).succ
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ
have inl₁ : b = (b.pred sorry).succ
Tactic: rw [predAbove_of_castSucc_lt _ _ h, predAbove_succ_of_le _ _ h, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
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
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ
have inl₂ : b = b
Tactic: rw [predAbove_of_castSucc_lt _ _ h, predAbove_succ_of_le _ _ h, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b < a.succ
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ
have inr : a.succ.predAbove b.succ = (b.castPred sorry).succ
Tactic: rw [predAbove_of_lt_succ _ _ h, predAbove_succ_of_lt _ _ h, succ_castPred_eq_castPred_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b < a.succ
inr : a.succ.predAbove b.succ = (b.castPred ⋯).succ
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ
have inr₁ : b.succ.castPred sorry = (b.castPred sorry).succ
Tactic: rw [predAbove_of_lt_succ _ _ h, predAbove_succ_of_lt _ _ h, succ_castPred_eq_castPred_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
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
⊢ a.succ.predAbove b.succ = (a.predAbove b).succ
have inr₂ : b.succ.castPred sorry = b.succ.castPred sorry
Tactic: rw [predAbove_of_lt_succ _ _ h, predAbove_succ_of_lt _ _ h, succ_castPred_eq_castPred_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
have inl : ∀ (h : a.castSucc < b), a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
Tactic: obtain h | h := a.castSucc.lt_or_ge b
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
inl : ∀ (h : a.castSucc < b), a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
have inr : ∀ (h : b ≤ a.castSucc), a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
Tactic: obtain h | h := a.castSucc.lt_or_ge b
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.castSucc < b
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
have inl : a.castSucc.predAbove b.castSucc = (b.pred sorry).castSucc
Tactic: rw [predAbove_of_castSucc_lt _ _ h, predAbove_castSucc_of_lt _ _ h,
      castSucc_pred_eq_pred_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
h : a.castSucc < b
inl : a.castSucc.predAbove b.castSucc = (b.pred ⋯).castSucc
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
have inl₁ : b.castSucc.pred sorry = (b.pred sorry).castSucc
Tactic: rw [predAbove_of_castSucc_lt _ _ h, predAbove_castSucc_of_lt _ _ h,
      castSucc_pred_eq_pred_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
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
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
have inl₂ : b.castSucc.pred sorry = b.castSucc.pred sorry
Tactic: rw [predAbove_of_castSucc_lt _ _ h, predAbove_castSucc_of_lt _ _ h,
      castSucc_pred_eq_pred_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b ≤ a.castSucc
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
have inr : a.castSucc.predAbove b.castSucc = (b.castPred sorry).castSucc
Tactic: rw [predAbove_of_le_castSucc _ _ h, predAbove_castSucc_of_le _ _ h, castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin n
b : Fin (n + 1)
h : b ≤ a.castSucc
inr : a.castSucc.predAbove b.castSucc = (b.castPred ⋯).castSucc
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
have inr₁ : b = (b.castPred sorry).castSucc
Tactic: rw [predAbove_of_le_castSucc _ _ h, predAbove_castSucc_of_le _ _ h, castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
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
⊢ a.castSucc.predAbove b.castSucc = (a.predAbove b).castSucc
have inr₂ : b = b
Tactic: rw [predAbove_of_le_castSucc _ _ h, predAbove_castSucc_of_le _ _ h, castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ (j.predAbove i).predAbove (i.succAbove j) = j
have inl : j.castSucc ≤ (i.pred sorry).castSucc
Tactic: rw [predAbove_of_castSucc_lt _ _ h, succAbove_of_castSucc_lt _ _ h, predAbove_of_le_castSucc,
      castPred_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ j.castSucc ≤ (i.pred ⋯).castSucc
have inl : j.castSucc < (i.pred sorry).succ
Tactic: rwa [le_castSucc_iff, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ (j.predAbove i).predAbove (i.succAbove j) = j
have inr : (i.castPred sorry).castSucc < j.succ
Tactic: rw [predAbove_of_le_castSucc _ _ h, succAbove_of_le_castSucc _ _ h, predAbove_of_castSucc_lt,
      pred_succ]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i ≤ j.castSucc
⊢ (i.castPred ⋯).castSucc < j.succ
have inr : i < j.succ
Tactic: rwa [castSucc_castPred, ← le_castSucc_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (hypothesis)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
⊢ (j.predAbove i).predAbove (i.succAbove j) = j
have x : 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]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
⊢ (i.succAbove j).succAbove (j.predAbove i) = i
have inl : j.castSucc.succAbove (j.predAbove i) = i
Tactic: rw [succAbove_of_castSucc_lt _ _ h, succAbove_predAbove (Fin.ne_of_gt h)]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
inl : j.castSucc.succAbove (j.predAbove i) = i
⊢ (i.succAbove j).succAbove (j.predAbove i) = i
have inl₁ : i = i
Tactic: rw [succAbove_of_castSucc_lt _ _ h, succAbove_predAbove (Fin.ne_of_gt h)]