awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : j.succ < p
hj : ¬j.castSucc < p
hij : i.castSucc = j.succ
⊢ i = j

Tactic:
cases hj <| Nat.lt_trans j.castSucc_lt_succ hi

Premises used: Fin.castSucc_lt_succ, Nat.lt_trans
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : j.castSucc < p
hij : i.succ = j.castSucc
⊢ i.succ < p

Tactic:
rw [← hij] at hj
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : j.castSucc < p
hij : i.succ = j.castSucc
hj₁ : i.succ < p
⊢ i.succ = j.castSucc

Tactic:
rw [← hij] at hj
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : i.succ < p
hij : i.succ = j.castSucc
⊢ i = j

Tactic:
cases hi <| Nat.lt_trans i.castSucc_lt_succ hj

Premises used: Fin.castSucc_lt_succ, Nat.lt_trans
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : ¬j.castSucc < p
hij : i.succ = j.succ
⊢ i = j

Tactic:
succ_injective _ hij

Premises used: Fin.succ_injective
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i j : Fin n
hi : ¬i.castSucc < p
hj : ¬j.castSucc < p
hij : i.succ = j.succ
⊢ i = j

Tactic:
exact succ_injective _ hij

Premises used: Fin.succ_injective
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i j : Fin n
⊢ p.succAbove i = p.succAbove j ↔ i = j

Tactic:
succAbove_right_injective.eq_iff

Premises used: Function.Injective.eq_iff, Fin.succAbove_right_injective
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
rw : Eq (α := Fin (n + 1)) (castSucc 0) 0
h : castSucc 0 < a
⊢ a.succAbove 0 = 0

Tactic:
rw [Fin.succAbove_of_castSucc_lt]

Premises used: Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ Eq (α := Fin (n + 1)) (castSucc 0) 0

Tactic:
castSucc_zero'

Premises used: Fin.castSucc_zero'
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ Eq (α := Fin (n + 1)) (castSucc 0) 0

Tactic:
exact castSucc_zero'

Premises used: Fin.castSucc_zero'
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 < a

Tactic:
Fin.pos_iff_ne_zero.2 ha

Premises used: Iff.mpr, Fin.pos_iff_ne_zero, Nat.mod
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
a : Fin (n + 1)
ha : a ≠ 0
⊢ castSucc 0 < a

Tactic:
exact Fin.pos_iff_ne_zero.2 ha

Premises used: Iff.mpr, Fin.pos_iff_ne_zero
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
a : Fin (n + 1)
b : Fin n
ha : a ≠ 0
rw : a.succAbove b = a.succAbove 0 ↔ b = 0
rw₁ rw₂ : b = 0 ↔ b = 0
⊢ a.succAbove b = 0 ↔ b = 0

Tactic:
rw [← succAbove_ne_zero_zero ha, succAbove_right_inj]

Premises used: Fin.succAbove_right_inj, Fin.succAbove_ne_zero_zero
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
a : Fin (n + 1)
b : Fin n
ha : a ≠ 0
hb : b ≠ 0
⊢ a.succAbove b ≠ 0

Tactic:
mt (succAbove_eq_zero_iff ha).mp hb

Premises used: Fin.succAbove_eq_zero_iff, mt, Iff.mp
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
⊢ Eq (α := (i : Fin n) → Fin (n + 1)) (succAbove 0) succ

Tactic:
rfl

Premises used: Fin.succAbove, Fin.succ, rfl, ite
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin n
rw rw₁ : i.succ = i.succ
⊢ succAbove 0 i = i.succ

Tactic:
rw [succAbove_zero]

Premises used: Fin.succAbove_zero
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin (n + 2)
h : a ≠ last (n + 1)
rw : (last n).succ = last (n + 1)
rw₁ rw₂ : Eq (α := Fin (n + 1 + 1)) (last n.succ) (last (n + 1))
⊢ a.succAbove (last n) = last (n + 1)

Tactic:
rw [succAbove_of_lt_succ _ _ (succ_last _ ▸ lt_last_iff_ne_last.2 h), succ_last]

Premises used: Fin.succAbove_of_lt_succ, Fin.succ_last
-- Module: Mathlib.Data.Fin.SuccPred
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
rw₁ rw₂ : b = last n ↔ b = last n
⊢ a.succAbove b = last (n + 1) ↔ b = last n

Tactic:
rw [← succAbove_ne_last_last ha, succAbove_right_inj]

Premises used: Fin.succAbove_ne_last_last, Fin.succAbove_right_inj
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin (n + 2)
b : Fin (n + 1)
ha : a ≠ last (n + 1)
hb : b ≠ last n
⊢ a.succAbove b ≠ last (n + 1)

Tactic:
mt (succAbove_eq_last_iff ha).mp hb

Premises used: mt, Fin.succAbove_eq_last_iff, Iff.mp
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
h : ∀ (x : Fin n), (↑((last n).succAbove x) : ℕ) = (↑x.castSucc : ℕ)
⊢ (last n).succAbove = castSucc

Tactic:
ext
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
x : Fin n
⊢ (↑((last n).succAbove x) : ℕ) = (↑x.castSucc : ℕ)

Tactic:
simp only [succAbove_of_castSucc_lt, castSucc_lt_last]

Premises used: Fin.castSucc_lt_last, Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin n
rw rw₁ : i.castSucc = i.castSucc
⊢ (last n).succAbove i = i.castSucc

Tactic:
rw [succAbove_last]

Premises used: Fin.succAbove_last
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
inl : ∀ (H : i.castSucc < p), p.succAbove i < p ↔ i.castSucc < p
inr : ∀ (H : p < i.succ), p.succAbove i < p ↔ i.castSucc < p
⊢ p.succAbove i < p ↔ i.castSucc < p

Tactic:
rcases castSucc_lt_or_lt_succ p i with H | H

Premises used: Fin.castSucc_lt_or_lt_succ
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
inl : p.succAbove i < p
inl₁ inl₂ inl₃ inl₄ : i.castSucc < p
⊢ p.succAbove i < p ↔ i.castSucc < p

Tactic:
rwa [iff_true_right H, succAbove_of_castSucc_lt _ _ H]

Premises used: iff_true_right, Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
inr : ¬i.succ < p
⊢ p.succAbove i < p ↔ i.castSucc < p

Tactic:
rw [castSucc_lt_iff_succ_le, iff_false_right (Fin.not_le.2 H), succAbove_of_lt_succ _ _ H]

Premises used: Iff.mpr, Fin.not_le, Fin.succAbove_of_lt_succ, iff_false_right, Fin.castSucc_lt_iff_succ_le
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ ¬i.succ < p

Tactic:
Fin.not_lt.2 <| Fin.le_of_lt H

Premises used: Iff.mpr, Fin.le_of_lt, Fin.not_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
⊢ ¬i.succ < p

Tactic:
exact Fin.not_lt.2 <| Fin.le_of_lt H

Premises used: Iff.mpr, Fin.le_of_lt, Fin.not_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
rw : i.castSucc < p ↔ i.succ ≤ p
rw₁ rw₂ : i.succ ≤ p ↔ i.succ ≤ p
⊢ p.succAbove i < p ↔ i.succ ≤ p

Tactic:
rw [succAbove_lt_iff_castSucc_lt, castSucc_lt_iff_succ_le]

Premises used: Fin.succAbove_lt_iff_castSucc_lt, Fin.castSucc_lt_iff_succ_le
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
inl : ∀ (H : i.castSucc < p), p < p.succAbove i ↔ p ≤ i.castSucc
inr : ∀ (H : p < i.succ), p < p.succAbove i ↔ p ≤ i.castSucc
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

Tactic:
rcases castSucc_lt_or_lt_succ p i with H | H

Premises used: Fin.castSucc_lt_or_lt_succ
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
inl : ¬p < i.castSucc
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

Tactic:
rw [iff_false_right (Fin.not_le.2 H), succAbove_of_castSucc_lt _ _ H]

Premises used: Iff.mpr, Fin.not_le, Fin.succAbove_of_castSucc_lt, iff_false_right
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ ¬p < i.castSucc

Tactic:
Fin.not_lt.2 <| Fin.le_of_lt H

Premises used: Iff.mpr, Fin.le_of_lt, Fin.not_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
H : i.castSucc < p
⊢ ¬p < i.castSucc

Tactic:
exact Fin.not_lt.2 <| Fin.le_of_lt H

Premises used: Iff.mpr, Fin.le_of_lt, Fin.not_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
H : p < i.succ
inr : p < i.succ ↔ p ≤ i.castSucc
inr₁ : p ≤ i.castSucc
inr₂ inr₃ inr₄ inr₅ : p < i.succ
⊢ p < p.succAbove i ↔ p ≤ i.castSucc

Tactic:
rwa [succAbove_of_lt_succ _ _ H, iff_true_left H, le_castSucc_iff]

Premises used: Fin.le_castSucc_iff, Fin.succAbove_of_lt_succ, iff_true_left
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
rw : p ≤ i.castSucc ↔ p < i.succ
rw₁ rw₂ : p < i.succ ↔ p < i.succ
⊢ p < p.succAbove i ↔ p < i.succ

Tactic:
rw [lt_succAbove_iff_le_castSucc, le_castSucc_iff]

Premises used: Fin.lt_succAbove_iff_le_castSucc, Fin.le_castSucc_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
pos : ∀ (H : i.castSucc < p), 0 < p.succAbove i
neg : ∀ (H : ¬i.castSucc < p), 0 < p.succAbove i
⊢ 0 < p.succAbove i

Tactic:
by_cases H : castSucc i < p

Premises used: Fin.castSucc
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
H : i.castSucc < p
⊢ 0 < p.succAbove i

Tactic:
simpa [succAbove_of_castSucc_lt _ _ H] using castSucc_pos' h

Premises used: Fin.succAbove_of_castSucc_lt, Fin.castSucc_pos'
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
p : Fin (n + 1)
i : Fin n
h : 0 < i
H : ¬i.castSucc < p
⊢ 0 < p.succAbove i

Tactic:
simp [succAbove_of_le_castSucc _ _ (Fin.not_lt.1 H)]

Premises used: Fin.succAbove_of_le_castSucc, Iff.mp, Fin.not_lt
-- Module: Mathlib.Data.Fin.SuccPred
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
rw₁ rw₂ : x.castSucc = x.castSucc
⊢ (y.succAbove x).castPred h' = x

Tactic:
rw [castPred_eq_iff_eq_castSucc, succAbove_of_castSucc_lt _ _ h]

Premises used: Fin.succAbove_of_castSucc_lt, Fin.castPred_eq_iff_eq_castSucc
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
x : Fin n
y : Fin (n + 1)
h : y ≤ x.castSucc
h' : y.succAbove x ≠ 0
⊢ (y.succAbove x).pred h' = x

Tactic:
simp only [succAbove_of_le_castSucc _ _ h, pred_succ]

Premises used: Fin.succAbove_of_le_castSucc, Fin.pred_succ
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
x y : Fin (n + 1)
h : x ≠ y
inl : ∀ (hxy : x < y), ∃ (z : Fin n), y.succAbove z = x
inr : ∀ (hyx : y < x), ∃ (z : Fin n), y.succAbove z = x
⊢ ∃ (z : Fin n), y.succAbove z = x

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

Premises used: Fin.lt_or_lt_of_ne
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
x y : Fin (n + 1)
h : x ≠ y
hxy : x < y
⊢ ∃ (z : Fin n), y.succAbove z = x

Tactic:
⟨_, succAbove_castPred_of_lt _ _ hxy⟩

Premises used: Exists.intro, Fin.succAbove_castPred_of_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
x y : Fin (n + 1)
h : x ≠ y
hyx : y < x
⊢ ∃ (z : Fin n), y.succAbove z = x

Tactic:
⟨_, succAbove_pred_of_lt _ _ hyx⟩

Premises used: Fin.succAbove_pred_of_lt, Exists.intro
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
x y : Fin (n + 1)
h : x ≠ y
hxy : x < y
⊢ ∃ (z : Fin n), y.succAbove z = x

Tactic:
exacts [⟨_, succAbove_castPred_of_lt _ _ hxy⟩, ⟨_, succAbove_pred_of_lt _ _ hyx⟩]
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
x : Fin (n + 1)
y : Fin n
⊢ x.succAbove y ≠ x

Tactic:
succAbove_ne _ _

Premises used: Fin.succAbove_ne
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
x : Fin (n + 1)
y : Fin n
⊢ x.succAbove y ≠ x

Tactic:
exact succAbove_ne _ _

Premises used: Fin.succAbove_ne
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
⊢ Set.range p.succAbove = {p}ᶜ

Tactic:
Set.ext fun _ => exists_succAbove_eq_iff

Premises used: Set.ext, Fin.exists_succAbove_eq_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
rw : Eq (α := Set (Fin (n + 1))) (Set.range (succAbove 0)) {0}ᶜ
rw₁ rw₂ : Eq (α := Set (Fin (n + 1))) {0}ᶜ {0}ᶜ
⊢ Eq (α := Set (Fin (n + 1))) (Set.range succ) {0}ᶜ

Tactic:
rw [← succAbove_zero, range_succAbove]

Premises used: Fin.range_succAbove, Fin.succAbove_zero
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
x x_1 : Fin (n + 1)
h : x.succAbove = x_1.succAbove
⊢ x = x_1

Tactic:
simpa [range_succAbove] using congr_arg (fun f : Fin n → Fin (n + 1) => (Set.range f)ᶜ) h

Premises used: Compl.compl, congr_arg, Fin.range_succAbove, Set.range
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
x y : Fin (n + 1)
⊢ x.succAbove = y.succAbove ↔ x = y

Tactic:
succAbove_left_injective.eq_iff

Premises used: Function.Injective.eq_iff, Fin.succAbove_left_injective
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin n
⊢ succAbove 0 i = i.succ

Tactic:
rfl

Premises used: Fin.succAbove, Fin.succ, rfl, ite
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
i : Fin n
⊢ i.succ.succAbove 0 = 0

Tactic:
simp
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
inl : ∀ (h : i < j.succ), i.succ.succAbove j.succ = (i.succAbove j).succ
inr : ∀ (h : j.succ ≤ i), i.succ.succAbove j.succ = (i.succAbove j).succ
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ

Tactic:
obtain h | h := i.lt_or_ge (succ j)

Premises used: Fin.succ, Fin.lt_or_ge
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : i < j.succ
inl : i.succ.succAbove j.succ = j.succ.succ
inl₁ inl₂ : j.succ.succ = j.succ.succ
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ

Tactic:
rw [succAbove_of_lt_succ _ _ h, succAbove_succ_of_lt _ _ h]

Premises used: Fin.succAbove_succ_of_lt, Fin.succAbove_of_lt_succ
-- Module: Mathlib.Data.Fin.SuccPred
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
inr₃ : j.succ.castSucc = j.succ.castSucc
inr₄ : j.succ ≤ i
inr₅ : j.succ.castSucc = j.succ.castSucc
inr₆ inr₇ inr₈ : j.succ ≤ i
⊢ i.succ.succAbove j.succ = (i.succAbove j).succ

Tactic:
rwa [succAbove_of_castSucc_lt _ _ h, succAbove_succ_of_le, succ_castSucc]

Premises used: Fin.succAbove_of_castSucc_lt, Fin.succ_castSucc, Fin.succAbove_succ_of_le
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
inl : ∀ (h : i ≤ j.castSucc), i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
inr : ∀ (h : j.castSucc < i), i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

Tactic:
rcases i.le_or_gt (castSucc j) with (h | h)

Premises used: Fin.le_or_gt, Fin.castSucc
-- Module: Mathlib.Data.Fin.SuccPred
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
inl₂ inl₃ : j.succ.castSucc = j.succ.castSucc
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

Tactic:
rw [succAbove_of_le_castSucc _ _ h, succAbove_castSucc_of_le _ _ h, succ_castSucc]

Premises used: Fin.succAbove_of_le_castSucc, Fin.succAbove_castSucc_of_le, Fin.succ_castSucc
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
j : Fin n
h : j.castSucc < i
inr : i.castSucc.succAbove j.castSucc = j.castSucc.castSucc
inr₁ inr₂ : j.castSucc.castSucc = j.castSucc.castSucc
⊢ i.castSucc.succAbove j.castSucc = (i.succAbove j).castSucc

Tactic:
rw [succAbove_of_castSucc_lt _ _ h, succAbove_castSucc_of_lt _ _ h]

Premises used: Fin.succAbove_castSucc_of_lt, Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.Data.Fin.SuccPred
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
simp_rw₁ : (a.pred ha).succ.succAbove (b.pred hb).succ = ((a.succAbove b).pred hk).succ
⊢ (a.pred ha).succAbove (b.pred hb) = (a.succAbove b).pred hk

Tactic:
simp_rw [← succ_inj (b := pred (succAbove a b) hk), ← succ_succAbove_succ, succ_pred]

Premises used: Fin.succ_succAbove_succ, Fin.succ_inj, Fin.succ_pred
-- Module: Mathlib.Data.Fin.SuccPred
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
simp_rw₁ : (a.castPred ha).castSucc.succAbove (b.castPred hb).castSucc = ((a.succAbove b).castPred hk).castSucc
⊢ (a.castPred ha).succAbove (b.castPred hb) = (a.succAbove b).castPred hk

Tactic:
simp_rw [← castSucc_inj (b := (a.succAbove b).castPred hk), ← castSucc_succAbove_castSucc,
    castSucc_castPred]

Premises used: Fin.castSucc_succAbove_castSucc, Fin.castSucc_castPred, Fin.castSucc_inj
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
⊢ Eq (α := Fin (n + 1 + 1)) (succAbove 1 0) 0

Tactic:
rfl

Premises used: Fin.succAbove, Fin.ofNat, Nat.mod, rfl, ite
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
rw : i.succ.succAbove (succ 0) = (i.succAbove 0).succ
⊢ i.succ.succAbove 1 = (i.succAbove 0).succ

Tactic:
rw [← succ_zero_eq_one']

Premises used: Fin.succ_zero_eq_one'
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
⊢ i.succ.succAbove (succ 0) = (i.succAbove 0).succ

Tactic:
succ_succAbove_succ i 0

Premises used: Fin.succ_succAbove_succ, OfNat.ofNat
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
⊢ i.succ.succAbove (succ 0) = (i.succAbove 0).succ

Tactic:
exact succ_succAbove_succ i 0

Premises used: Fin.succ_succAbove_succ, OfNat.ofNat
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
j : Fin n
⊢ succAbove (succ 0) j.succ = (succAbove 0 j).succ

Tactic:
have := succ_succAbove_succ 0 j
-- Module: Mathlib.Data.Fin.SuccPred
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : succAbove 1 j.succ = j.succ.succ), succAbove 1 j.succ = j.succ.succ
⊢ succAbove 1 j.succ = j.succ.succ

Tactic:
rwa [succ_zero_eq_one, zero_succAbove] at this

Premises used: Fin.zero_succAbove, Fin.succ_zero_eq_one
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
⊢ Eq (α := Fin (n + 2 + 1)) (succAbove 1 1) 2

Tactic:
simpa only [succ_zero_eq_one, val_zero, zero_succAbove, succ_one_eq_two]
    using succ_succAbove_succ (0 : Fin (n + 2)) (0 : Fin (n + 1))

Premises used: Fin.succ_succAbove_succ, Fin.zero_succAbove, Fin.succ_zero_eq_one, OfNat.ofNat, Fin.val_zero, Fin.succ_one_eq_two
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i ≤ p.castSucc
⊢ p.predAbove i = i.castPred ⋯

Tactic:
dif_neg <| Fin.not_lt.2 h

Premises used: Iff.mpr, Fin.predAbove, dif_neg, Fin.not_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i < p.succ
⊢ p.predAbove i = i.castPred ⋯

Tactic:
predAbove_of_le_castSucc _ _ (le_castSucc_iff.mpr h)

Premises used: Iff.mpr, Fin.predAbove_of_le_castSucc, Fin.le_castSucc_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.castSucc < i
⊢ p.predAbove i = i.pred ⋯

Tactic:
dif_pos h

Premises used: dif_pos, Fin.predAbove
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i
⊢ p.predAbove i = i.pred ⋯

Tactic:
predAbove_of_castSucc_lt _ _ (castSucc_lt_iff_succ_le.mpr h)

Premises used: Iff.mpr, Fin.predAbove_of_castSucc_lt, Fin.castSucc_lt_iff_succ_le
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
h : i < p
rw rw₁ : i.succ.castPred ⋯ = i.succ.castPred ⋯
⊢ p.predAbove i.succ = i.succ.castPred ⋯

Tactic:
rw [predAbove_of_lt_succ _ _ (succ_lt_succ_iff.mpr h)]

Premises used: Iff.mpr, Fin.succ_lt_succ_iff, Fin.predAbove_of_lt_succ
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
h : p ≤ i
rw : i.succ.pred ⋯ = i
rw₁ rw₂ : i = i
⊢ p.predAbove i.succ = i

Tactic:
rw [predAbove_of_succ_le _ _ (succ_le_succ_iff.mpr h), pred_succ]

Premises used: Iff.mpr, Fin.succ_le_succ_iff, Fin.pred_succ, Fin.predAbove_of_succ_le
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin n
⊢ p.predAbove p.succ = p

Tactic:
predAbove_succ_of_le _ _ Fin.le_rfl

Premises used: Fin.le_rfl, Fin.predAbove_succ_of_le
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
h : p < i
rw rw₁ : i.castSucc.pred ⋯ = i.castSucc.pred ⋯
⊢ p.predAbove i.castSucc = i.castSucc.pred ⋯

Tactic:
rw [predAbove_of_castSucc_lt _ _ (castSucc_lt_castSucc_iff.2 h)]

Premises used: Iff.mpr, Fin.predAbove_of_castSucc_lt, Fin.castSucc_lt_castSucc_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
h : i ≤ p
rw : i.castSucc.castPred ⋯ = i
rw₁ rw₂ : i = i
⊢ p.predAbove i.castSucc = i

Tactic:
rw [predAbove_of_le_castSucc _ _ (castSucc_le_castSucc_iff.mpr h), 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
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin n
⊢ p.predAbove p.castSucc = p

Tactic:
predAbove_castSucc_of_le _ _ Fin.le_rfl

Premises used: Fin.predAbove_castSucc_of_le, Fin.le_rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin (n + 1)
h : i < p
rw rw₁ : i.castPred ⋯ = i.castPred ⋯
⊢ (p.pred ⋯).predAbove i = i.castPred ⋯

Tactic:
rw [predAbove_of_lt_succ _ _ (succ_pred _ _ ▸ h)]

Premises used: Fin.predAbove_of_lt_succ
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin (n + 1)
h : p ≤ i
hp : p ≠ 0
rw rw₁ : i.pred ⋯ = i.pred ⋯
⊢ (p.pred hp).predAbove i = i.pred ⋯

Tactic:
rw [predAbove_of_succ_le _ _ (succ_pred _ _ ▸ h)]

Premises used: Fin.predAbove_of_succ_le
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
hp : p ≠ 0
⊢ (p.pred hp).predAbove p = p.pred hp

Tactic:
predAbove_pred_of_le _ _ Fin.le_rfl hp

Premises used: Fin.le_rfl, Fin.predAbove_pred_of_le
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin (n + 1)
h : p < i
rw rw₁ : i.pred ⋯ = i.pred ⋯
⊢ (p.castPred ⋯).predAbove i = i.pred ⋯

Tactic:
rw [predAbove_of_castSucc_lt _ _ (castSucc_castPred _ _ ▸ h)]

Premises used: Fin.predAbove_of_castSucc_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin (n + 1)
h : i ≤ p
hp : p ≠ last n
rw rw₁ : i.castPred ⋯ = i.castPred ⋯
⊢ (p.castPred hp).predAbove i = i.castPred ⋯

Tactic:
rw [predAbove_of_le_castSucc _ _ (castSucc_castPred _ _ ▸ h)]

Premises used: Fin.predAbove_of_le_castSucc
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
hp : p ≠ last n
⊢ (p.castPred hp).predAbove p = p.castPred hp

Tactic:
predAbove_castPred_of_le _ _ Fin.le_rfl hp

Premises used: Fin.predAbove_castPred_of_le, Fin.le_rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
i : Fin n
zero : ∀ [inst : NeZero (R := ℕ) 0] {i : Fin 0}, i.predAbove 0 = 0
succ : ∀ (n : ℕ) [inst : NeZero (n + 1)] {i : Fin (n + 1)}, i.predAbove 0 = 0
⊢ i.predAbove 0 = 0

Tactic:
cases n
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
inst : NeZero (R := ℕ) 0
i : Fin 0
⊢ i.predAbove 0 = 0

Tactic:
i.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
inst : NeZero (R := ℕ) 0
i : Fin 0
⊢ i.predAbove 0 = 0

Tactic:
exact i.elim0

Premises used: Fin.elim0
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero (n + 1)
i : Fin (n + 1)
succ : castPred 0 ⋯ = 0
succ₁ succ₂ : Eq (α := Fin (n + 1)) 0 0
⊢ i.predAbove 0 = 0

Tactic:
rw [predAbove_of_le_castSucc _ _ (zero_le _), castPred_zero]

Premises used: Fin.zero_le, Fin.predAbove_of_le_castSucc, Fin.castPred_zero
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
i : Fin n
rw rw₁ : i = i
⊢ predAbove 0 i.succ = i

Tactic:
rw [predAbove_succ_of_le _ _ (Fin.zero_le _)]

Premises used: Fin.zero_le, Fin.predAbove_succ_of_le
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
hi : i ≠ 0
obtain : ∀ (y : Fin n) (hi : y.succ ≠ 0), predAbove 0 y.succ = y.succ.pred hi
⊢ predAbove 0 i = i.pred hi

Tactic:
obtain ⟨y, rfl⟩ := exists_succ_eq.2 hi

Premises used: Iff.mpr, Fin.exists_succ_eq, rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
y : Fin n
hi : y.succ ≠ 0
⊢ predAbove 0 y.succ = y.succ.pred hi

Tactic:
predAbove_zero_succ

Premises used: Fin.predAbove_zero_succ, Nat.pred
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
y : Fin n
hi : y.succ ≠ 0
⊢ predAbove 0 y.succ = y.succ.pred hi

Tactic:
exact predAbove_zero_succ

Premises used: Fin.predAbove_zero_succ
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
j : Fin (n + 1)
h : j ≠ 0
⊢ (predAbove 0 j).succ = j

Tactic:
simp [h]