awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin n.succ
hi : Membership.mem (γ := Set (Fin (n + 1))) (Set.range castSucc) i
rw :
  (↑(castSucc
          (((Equiv.ofInjective castSucc ⋯).symm : (a : (↑(Set.range castSucc) : Type)) → Fin n)
            (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1))) (Set.range castSucc) x) i
              hi))) :
      ℕ) =
    (↑i : ℕ)
⊢ (↑(((Equiv.ofInjective castSucc ⋯).symm : (a : (↑(Set.range castSucc) : Type)) → Fin n)
          (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1))) (Set.range castSucc) x) i
            hi)) :
      ℕ) =
    (↑i : ℕ)

Tactic:
rw [← val_castSucc]

Premises used: Fin.val_castSucc
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin n.succ
hi : Membership.mem (γ := Set (Fin (n + 1))) (Set.range castSucc) i
⊢ (↑(castSucc
          (((Equiv.ofInjective castSucc ⋯).symm : (a : (↑(Set.range castSucc) : Type)) → Fin n)
            (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1))) (Set.range castSucc) x) i
              hi))) :
      ℕ) =
    (↑i : ℕ)

Tactic:
congr_arg val (Equiv.apply_ofInjective_symm _ _)

Premises used: Fin.val, congr_arg, Equiv.apply_ofInjective_symm
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin n.succ
hi : Membership.mem (γ := Set (Fin (n + 1))) (Set.range castSucc) i
⊢ (↑(castSucc
          (((Equiv.ofInjective castSucc ⋯).symm : (a : (↑(Set.range castSucc) : Type)) → Fin n)
            (Subtype.mk (p := fun (x : Fin (n + 1)) ↦ Membership.mem (γ := Set (Fin (n + 1))) (Set.range castSucc) x) i
              hi))) :
      ℕ) =
    (↑i : ℕ)

Tactic:
exact congr_arg val (Equiv.apply_ofInjective_symm _ _)

Premises used: Fin.val, congr_arg, Equiv.apply_ofInjective_symm
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
i : Fin n
⊢ (castAdd m i).castSucc = castAdd (m + 1) i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
i : Fin n
pos : ∀ (h : i.succ = last n), (castAdd m i).succ = natAdd n 0
neg : ∀ (h : ¬i.succ = last n), (castAdd m i).succ = castAdd (m + 1) ⟨(↑i : ℕ) + 1, ⋯⟩
⊢ (castAdd m i).succ = if h : i.succ = last n then natAdd n 0 else castAdd (m + 1) ⟨(↑i : ℕ) + 1, ⋯⟩

Tactic:
split_ifs with h
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
i : Fin n
h : i.succ = last n
⊢ (castAdd m i).succ = natAdd n 0

Tactic:
Fin.ext (congr_arg Fin.val h :)

Premises used: Fin.ext, Fin.val, congr_arg
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
i : Fin n
h : ¬i.succ = last n
⊢ (castAdd m i).succ = castAdd (m + 1) ⟨(↑i : ℕ) + 1, ⋯⟩

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
i : Fin n
h : i.succ = last n
⊢ (castAdd m i).succ = natAdd n 0

Tactic:
exacts [Fin.ext (congr_arg Fin.val h :), rfl]

Premises used: Fin.ext, Fin.val, congr_arg, rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
i : Fin m
⊢ (natAdd n i).succ = natAdd n i.succ

Tactic:
rfl

Premises used: Fin.natAdd, rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
h : Ne (α := Fin (n + 1)) 1 0
simp_rw : (↑(pred 1 h) : ℕ) = (↑0 : ℕ)
simp_rw₁ : (↑1 : ℕ) - 1 = (↑0 : ℕ)
simp_rw₂ : 1 % (n + 1) - 1 = (↑0 : ℕ)
simp_rw₃ : 1 % (n + 1) - 1 = 0
simp_rw₄ : 1 % (n + 1) ≤ 1
⊢ pred 1 h = 0

Tactic:
simp_rw [Fin.ext_iff, val_pred, val_one', val_zero, Nat.sub_eq_zero_iff_le, Nat.mod_le]

Premises used: Fin.ext_iff, Fin.val_one', Fin.val_pred, Nat.sub_eq_zero_iff_le, Nat.mod_le, Fin.val_zero
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
rw : (i.pred hi).succ < j.succ ↔ i < j.succ
rw₁ rw₂ : i < j.succ ↔ i < j.succ
⊢ i.pred hi < j ↔ i < j.succ

Tactic:
rw [← succ_lt_succ_iff, succ_pred]

Premises used: Fin.succ_lt_succ_iff, Fin.succ_pred
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
rw : j.succ < (i.pred hi).succ ↔ j.succ < i
rw₁ rw₂ : j.succ < i ↔ j.succ < i
⊢ j < i.pred hi ↔ j.succ < i

Tactic:
rw [← succ_lt_succ_iff, succ_pred]

Premises used: Fin.succ_lt_succ_iff, Fin.succ_pred
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
rw : (i.pred hi).succ ≤ j.succ ↔ i ≤ j.succ
rw₁ rw₂ : i ≤ j.succ ↔ i ≤ j.succ
⊢ i.pred hi ≤ j ↔ i ≤ j.succ

Tactic:
rw [← succ_le_succ_iff, succ_pred]

Premises used: Fin.succ_le_succ_iff, Fin.succ_pred
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
rw : j.succ ≤ (i.pred hi).succ ↔ j.succ ≤ i
rw₁ rw₂ : j.succ ≤ i ↔ j.succ ≤ i
⊢ j ≤ i.pred hi ↔ j.succ ≤ i

Tactic:
rw [← succ_le_succ_iff, succ_pred]

Premises used: Fin.succ_le_succ_iff, Fin.succ_pred
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin (n + 1)
ha : a ≠ 0
⊢ (a.pred ha).castSucc = a.castSucc.pred ⋯

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin (n + 1)
ha : a ≠ 0
⊢ (a.pred ha).castSucc + 1 = a

Tactic:
simp
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
rw : b.succ ≤ a.castSucc ↔ b < a
rw₁ rw₂ : b < a ↔ b < a
⊢ b ≤ a.castSucc.pred ha ↔ b < a

Tactic:
rw [le_pred_iff, succ_le_castSucc_iff]

Premises used: Fin.succ_le_castSucc_iff, Fin.le_pred_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
rw : a.castSucc < b.succ ↔ a ≤ b
rw₁ rw₂ : a ≤ b ↔ a ≤ b
⊢ a.castSucc.pred ha < b ↔ a ≤ b

Tactic:
rw [pred_lt_iff, castSucc_lt_succ_iff]

Premises used: Fin.pred_lt_iff, Fin.castSucc_lt_succ_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin (n + 1)
ha : a.castSucc ≠ 0
rw : a ≤ a
rw₁ rw₂ : (↑a : ℕ) ≤ (↑a : ℕ)
⊢ a.castSucc.pred ha < a

Tactic:
rw [pred_castSucc_lt_iff, le_def]

Premises used: Fin.le_def, Fin.pred_castSucc_lt_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
rw : b ≤ a.castSucc.pred ⋯ ↔ b < a
rw₁ rw₂ : b < a ↔ b < a
⊢ b ≤ (a.pred ha).castSucc ↔ b < a

Tactic:
rw [castSucc_pred_eq_pred_castSucc, le_pred_castSucc_iff]

Premises used: Fin.castSucc_pred_eq_pred_castSucc, Fin.le_pred_castSucc_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
rw : a.castSucc.pred ⋯ < b ↔ a ≤ b
rw₁ rw₂ : a ≤ b ↔ a ≤ b
⊢ (a.pred ha).castSucc < b ↔ a ≤ b

Tactic:
rw [castSucc_pred_eq_pred_castSucc, pred_castSucc_lt_iff]

Premises used: Fin.castSucc_pred_eq_pred_castSucc, Fin.pred_castSucc_lt_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin (n + 1)
ha : a ≠ 0
rw : a ≤ a
rw₁ rw₂ : (↑a : ℕ) ≤ (↑a : ℕ)
⊢ (a.pred ha).castSucc < a

Tactic:
rw [castSucc_pred_lt_iff, le_def]

Premises used: Fin.le_def, Fin.castSucc_pred_lt_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
h : i < last n
h' : ¬i = last n
⊢ i.castLT h = i.castPred h'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
h : i ≠ last n
⊢ (↑(i.castPred h) : ℕ) = (↑i : ℕ)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin n
h' : ¬i.castSucc = last n
⊢ i.castSucc.castPred h' = i

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
h : i ≠ last n
rcases : ∀ (y : Fin n) (h : y.castSucc ≠ last n), (y.castSucc.castPred h).castSucc = y.castSucc
⊢ (i.castPred h).castSucc = i

Tactic:
rcases exists_castSucc_eq.mpr h with ⟨y, rfl⟩

Premises used: Iff.mpr, Fin.exists_castSucc_eq, rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
y : Fin n
h : y.castSucc ≠ last n
rw rw₁ : y.castSucc = y.castSucc
⊢ (y.castSucc.castPred h).castSucc = y.castSucc

Tactic:
rw [castPred_castSucc]

Premises used: Iff.mpr, Fin.ext_iff, Fin.castPred_castSucc, Iff.not, Fin.castSucc_lt_last, LT.lt.ne
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
hi : i ≠ last n
j : Fin n
h : i.castPred hi = j
rw : i = (i.castPred hi).castSucc
rw₁ rw₂ : i = i
⊢ i = j.castSucc

Tactic:
rw [← h, castSucc_castPred]

Premises used: Fin.castSucc_castPred
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin (n + 1)
hi : i ≠ last n
j : Fin n
h : i = j.castSucc
simp_rw : j.castSucc.castPred ⋯ = j
⊢ i.castPred hi = j

Tactic:
simp_rw [h, castPred_castSucc]

Premises used: Iff.mpr, Fin.ext_iff, Fin.castPred_castSucc, Iff.not, Fin.castSucc_lt_last, LT.lt.ne
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n i : ℕ
h₁ : i < n
h₂ : i < n.succ
h₃ : (⟨i, h₂⟩ : Fin (n + 1)) ≠ last n
⊢ (⟨i, h₂⟩ : Fin (n + 1)).castPred h₃ = ⟨i, h₁⟩

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i j : Fin (n + 1)
hi : i ≠ last n
hj : j ≠ last n
⊢ i.castPred hi ≤ j.castPred hj ↔ i ≤ j

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
i j : Fin (n + 1)
h : i ≤ j
hj : j ≠ last n
rw : ∀ (hj : j < last n), i < last n
⊢ i ≠ last n

Tactic:
rw [← lt_last_iff_ne_last] at hj ⊢

Premises used: Fin.lt_last_iff_ne_last
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
i j : Fin (n + 1)
h : i ≤ j
hj : j < last n
⊢ i < last n

Tactic:
Fin.lt_of_le_of_lt h hj

Premises used: Fin.lt_of_le_of_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n m : ℕ
i j : Fin (n + 1)
h : i ≤ j
hj : j < last n
⊢ i < last n

Tactic:
exact Fin.lt_of_le_of_lt h hj

Premises used: Fin.lt_of_le_of_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i j : Fin (n + 1)
h : i ≤ j
hj : j ≠ last n
⊢ i.castPred ⋯ ≤ j.castPred hj

Tactic:
h
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i j : Fin (n + 1)
hi : i ≠ last n
hj : j ≠ last n
⊢ i.castPred hi < j.castPred hj ↔ i < j

Tactic:
Iff.rfl

Premises used: Iff.rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i j : Fin (n + 1)
h : i < j
hj : j ≠ last n
⊢ i.castPred ⋯ < j.castPred hj

Tactic:
h
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
rw : (i.castPred hi).castSucc < j.castSucc ↔ i < j.castSucc
rw₁ rw₂ : i < j.castSucc ↔ i < j.castSucc
⊢ i.castPred hi < j ↔ i < j.castSucc

Tactic:
rw [← castSucc_lt_castSucc_iff, castSucc_castPred]

Premises used: Fin.castSucc_lt_castSucc_iff, Fin.castSucc_castPred
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
rw : j.castSucc < (i.castPred hi).castSucc ↔ j.castSucc < i
rw₁ rw₂ : j.castSucc < i ↔ j.castSucc < i
⊢ j < i.castPred hi ↔ j.castSucc < i

Tactic:
rw [← castSucc_lt_castSucc_iff, castSucc_castPred]

Premises used: Fin.castSucc_lt_castSucc_iff, Fin.castSucc_castPred
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
rw : (i.castPred hi).castSucc ≤ j.castSucc ↔ i ≤ j.castSucc
rw₁ rw₂ : i ≤ j.castSucc ↔ i ≤ j.castSucc
⊢ i.castPred hi ≤ j ↔ i ≤ j.castSucc

Tactic:
rw [← castSucc_le_castSucc_iff, castSucc_castPred]

Premises used: Fin.castSucc_castPred, Fin.castSucc_le_castSucc_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
rw : j.castSucc ≤ (i.castPred hi).castSucc ↔ j.castSucc ≤ i
rw₁ rw₂ : j.castSucc ≤ i ↔ j.castSucc ≤ i
⊢ j ≤ i.castPred hi ↔ j.castSucc ≤ i

Tactic:
rw [← castSucc_le_castSucc_iff, castSucc_castPred]

Premises used: Fin.castSucc_castPred, Fin.castSucc_le_castSucc_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i j : Fin (n + 1)
hi : i ≠ last n
hj : j ≠ last n
simp_rw : (↑(i.castPred hi) : ℕ) = (↑(j.castPred hj) : ℕ) ↔ (↑i : ℕ) = (↑j : ℕ)
simp_rw₁ :
  (↑(i.castPred hi) : ℕ) ≤ (↑(j.castPred hj) : ℕ) ∧ (↑(j.castPred hj) : ℕ) ≤ (↑(i.castPred hi) : ℕ) ↔
    (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) ≤ (↑i : ℕ)
simp_rw₂ : i.castPred hi ≤ j.castPred hj ∧ j.castPred hj ≤ i.castPred hi ↔ i ≤ j ∧ j ≤ i
⊢ i.castPred hi = j.castPred hj ↔ i = j

Tactic:
simp_rw [Fin.ext_iff, le_antisymm_iff, ← le_def, castPred_le_castPred_iff]

Premises used: Fin.ext_iff, Fin.le_def, Fin.castPred_le_castPred_iff, le_antisymm_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Fin n) (castPred 0 ⋯) 0

Tactic:
rfl

Premises used: Fin.ofNat, Nat.mod, rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
h : i ≠ last n
rw : i.castPred h = castPred 0 ⋯ ↔ i = 0
rw₁ rw₂ : i = 0 ↔ i = 0
⊢ i.castPred h = 0 ↔ i = 0

Tactic:
rw [← castPred_zero, castPred_inj]

Premises used: Fin.castPred_inj, Fin.castPred_zero
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
h₁ : i ≠ last n
h₂ : i ≠ 0
⊢ i.castPred h₁ ≠ 0

Tactic:
(castPred_eq_zero h₁).not.mpr h₂

Premises used: Iff.mpr, Fin.castPred_eq_zero, Iff.not
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero n
zero : ∀ [inst : NeZero (R := ℕ) 0], Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 1)) (castPred 1 ⋯) 1
succ : ∀ (n : ℕ) [inst : NeZero (n + 1)], Eq (α := Fin (n + 1 + 1)) (castPred 1 ⋯) 1
⊢ Eq (α := Fin (n + 1)) (castPred 1 ⋯) 1

Tactic:
cases n
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
inst : NeZero (R := ℕ) 0
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 1)) (castPred 1 ⋯) 1

Tactic:
subsingleton_one.elim _ 1

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
inst : NeZero (R := ℕ) 0
⊢ Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 1)) (castPred 1 ⋯) 1

Tactic:
exact subsingleton_one.elim _ 1

Premises used: Subsingleton.elim, OfNat.ofNat
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
inst : NeZero (n + 1)
⊢ Eq (α := Fin (n + 1 + 1)) (castPred 1 ⋯) 1

Tactic:
rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin (n + 1)
ha : a ≠ last n
ha' : a.succ ≠ last (n + 1)
⊢ (a.castPred ha).succ = a.succ.castPred ha'

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Data.Fin.SuccPred
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
cast : ∀ (i : Fin n) (ha : i.castSucc ≠ Fin.last n), (i.castSucc.castPred ha).succ = i.castSucc + 1
⊢ (a.castPred ha).succ = a + 1

Tactic:
cases a using lastCases
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
ha : last n ≠ last n
⊢ ((last n).castPred ha).succ = last n + 1

Tactic:
(ha rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
ha : last n ≠ last n
⊢ ((last n).castPred ha).succ = last n + 1

Tactic:
exact (ha rfl).elim

Premises used: False.elim, rfl
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
i : Fin n
ha : i.castSucc ≠ last n
cast : i.succ = i.castSucc + 1
cast₁ cast₂ : i.succ = i.succ
⊢ (i.castSucc.castPred ha).succ = i.castSucc + 1

Tactic:
rw [castPred_castSucc, coeSucc_eq_succ]

Premises used: Iff.mpr, Fin.ext_iff, Fin.castPred_castSucc, Iff.not, Fin.castSucc_lt_last, Fin.coeSucc_eq_succ, LT.lt.ne
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
rw : a.succ ≤ b.castSucc ↔ a < b
rw₁ rw₂ : a < b ↔ a < b
⊢ a.succ.castPred ha ≤ b ↔ a < b

Tactic:
rw [castPred_le_iff, succ_le_castSucc_iff]

Premises used: Fin.castPred_le_iff, Fin.succ_le_castSucc_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
rw : b.castSucc < a.succ ↔ b ≤ a
rw₁ rw₂ : b ≤ a ↔ b ≤ a
⊢ b < a.succ.castPred ha ↔ b ≤ a

Tactic:
rw [lt_castPred_iff, castSucc_lt_succ_iff]

Premises used: Fin.lt_castPred_iff, Fin.castSucc_lt_succ_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin (n + 1)
ha : a.succ ≠ last (n + 1)
rw : a ≤ a
rw₁ rw₂ : (↑a : ℕ) ≤ (↑a : ℕ)
⊢ a < a.succ.castPred ha

Tactic:
rw [lt_castPred_succ_iff, le_def]

Premises used: Fin.le_def, Fin.lt_castPred_succ_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
rw : a.succ.castPred ⋯ ≤ b ↔ a < b
rw₁ rw₂ : a < b ↔ a < b
⊢ (a.castPred ha).succ ≤ b ↔ a < b

Tactic:
rw [succ_castPred_eq_castPred_succ ha, castpred_succ_le_iff]

Premises used: Fin.castpred_succ_le_iff, Iff.mpr, Fin.succ_castPred_eq_castPred_succ, Fin.succ_ne_last_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
rw : b < a.succ.castPred ⋯ ↔ b ≤ a
rw₁ rw₂ : b ≤ a ↔ b ≤ a
⊢ b < (a.castPred ha).succ ↔ b ≤ a

Tactic:
rw [succ_castPred_eq_castPred_succ ha, lt_castPred_succ_iff]

Premises used: Iff.mpr, Fin.succ_castPred_eq_castPred_succ, Fin.succ_ne_last_iff, Fin.lt_castPred_succ_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin (n + 1)
ha : a ≠ last n
rw : a ≤ a
rw₁ rw₂ : (↑a : ℕ) ≤ (↑a : ℕ)
⊢ a < (a.castPred ha).succ

Tactic:
rw [lt_succ_castPred_iff, le_def]

Premises used: Fin.le_def, Fin.lt_succ_castPred_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ last n
hb : b ≠ 0
rw : (a.castPred ha).succ ≤ b ↔ a < b
rw₁ rw₂ : a < b ↔ a < b
⊢ a.castPred ha ≤ b.pred hb ↔ a < b

Tactic:
rw [le_pred_iff, succ_castPred_le_iff]

Premises used: Fin.succ_castPred_le_iff, Fin.le_pred_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
hb : b ≠ last n
rw : (a.pred ha).castSucc < b ↔ a ≤ b
rw₁ rw₂ : a ≤ b ↔ a ≤ b
⊢ a.pred ha < b.castPred hb ↔ a ≤ b

Tactic:
rw [lt_castPred_iff, castSucc_pred_lt_iff ha]

Premises used: Fin.lt_castPred_iff, Fin.castSucc_pred_lt_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
a : Fin (n + 1)
h₁ : a ≠ 0
h₂ : a ≠ last n
rw : a ≤ a
rw₁ rw₂ : (↑a : ℕ) ≤ (↑a : ℕ)
⊢ a.pred h₁ < a.castPred h₂

Tactic:
rw [pred_lt_castPred_iff, le_def]

Premises used: Fin.pred_lt_castPred_iff, Fin.le_def
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.castSucc < p
⊢ p.succAbove i = i.castSucc

Tactic:
if_pos h

Premises used: Fin.succAbove, if_pos
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.succ ≤ p
⊢ p.succAbove i = i.castSucc

Tactic:
succAbove_of_castSucc_lt _ _ (castSucc_lt_iff_succ_le.mpr h)

Premises used: Iff.mpr, Fin.succAbove_of_castSucc_lt, Fin.castSucc_lt_iff_succ_le
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p ≤ i.castSucc
⊢ p.succAbove i = i.succ

Tactic:
if_neg (Fin.not_lt.2 h)

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

Tactic:
succAbove_of_le_castSucc _ _ (le_castSucc_iff.mpr h)

Premises used: Iff.mpr, Fin.succAbove_of_le_castSucc, Fin.le_castSucc_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
h : p < i
⊢ p.succ.succAbove i = i.succ

Tactic:
succAbove_of_lt_succ _ _ (succ_lt_succ_iff.mpr h)

Premises used: Iff.mpr, Fin.succ_lt_succ_iff, Fin.succAbove_of_lt_succ
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
h : i ≤ p
⊢ p.succ.succAbove i = i.castSucc

Tactic:
succAbove_of_succ_le _ _ (succ_le_succ_iff.mpr h)

Premises used: Iff.mpr, Fin.succ_le_succ_iff, Fin.succAbove_of_succ_le
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
j : Fin n
⊢ j.succ.succAbove j = j.castSucc

Tactic:
succAbove_succ_of_le _ _ Fin.le_rfl

Premises used: Fin.le_rfl, Fin.succAbove_succ_of_le
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
h : i < p
⊢ p.castSucc.succAbove i = i.castSucc

Tactic:
succAbove_of_castSucc_lt _ _ (castSucc_lt_castSucc_iff.2 h)

Premises used: Iff.mpr, Fin.castSucc_lt_castSucc_iff, Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin n
h : p ≤ i
⊢ p.castSucc.succAbove i = i.succ

Tactic:
succAbove_of_le_castSucc _ _ (castSucc_le_castSucc_iff.2 h)

Premises used: Iff.mpr, Fin.succAbove_of_le_castSucc, Fin.castSucc_le_castSucc_iff
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
j : Fin n
⊢ j.castSucc.succAbove j = j.succ

Tactic:
succAbove_castSucc_of_le _ _ Fin.le_rfl

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

Tactic:
rw [succAbove_of_lt_succ _ _ (succ_pred _ _ ▸ h), succ_pred]

Premises used: Fin.succAbove_of_lt_succ, Fin.succ_pred
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin (n + 1)
h : i ≤ p
hi : i ≠ 0
⊢ p.succAbove (i.pred hi) = (i.pred hi).castSucc

Tactic:
succAbove_of_succ_le _ _ (succ_pred _ _ ▸ h)

Premises used: Eq.rec, Fin.succAbove_of_succ_le, Eq.symm, Fin.succ_pred
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
h : p ≠ 0
⊢ p.succAbove (p.pred h) = (p.pred h).castSucc

Tactic:
succAbove_pred_of_le _ _ Fin.le_rfl h

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

Tactic:
rw [succAbove_of_castSucc_lt _ _ (castSucc_castPred _ _ ▸ h), castSucc_castPred]

Premises used: Fin.castSucc_castPred, Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p i : Fin (n + 1)
h : p ≤ i
hi : i ≠ last n
⊢ p.succAbove (i.castPred hi) = (i.castPred hi).succ

Tactic:
succAbove_of_le_castSucc _ _ (castSucc_castPred _ _ ▸ h)

Premises used: Fin.succAbove_of_le_castSucc, Eq.rec, Fin.castSucc_castPred, Eq.symm
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
h : p ≠ last n
⊢ p.succAbove (p.castPred h) = (p.castPred h).succ

Tactic:
succAbove_castPred_of_le _ _ Fin.le_rfl h

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

Tactic:
rcases p.castSucc_lt_or_lt_succ 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 : i.castSucc ≠ p
⊢ p.succAbove i ≠ p

Tactic:
rw [succAbove_of_castSucc_lt _ _ h]

Premises used: Fin.succAbove_of_castSucc_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.castSucc < p
⊢ i.castSucc ≠ p

Tactic:
Fin.ne_of_lt h

Premises used: Fin.ne_of_lt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
h : i.castSucc < p
⊢ i.castSucc ≠ p

Tactic:
exact Fin.ne_of_lt h

Premises used: Fin.ne_of_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

Tactic:
rw [succAbove_of_lt_succ _ _ h]

Premises used: Fin.succAbove_of_lt_succ
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p < i.succ
⊢ i.succ ≠ p

Tactic:
Fin.ne_of_gt h

Premises used: Fin.ne_of_gt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
h : p < i.succ
⊢ i.succ ≠ p

Tactic:
exact Fin.ne_of_gt h

Premises used: Fin.ne_of_gt
-- Module: Mathlib.Data.Fin.SuccPred
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ p ≠ p.succAbove i

Tactic:
(succAbove_ne _ _).symm

Premises used: Fin.succAbove_ne, Ne.symm
-- Module: Mathlib.Data.Fin.SuccPred
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
neg₁ : ∀ (hi : ¬i.castSucc < p) (hj : ¬j.castSucc < p) (hij : i.succ = j.succ), i = j
⊢ i = j

Tactic:
split_ifs at hij with hi hj 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.castSucc = j.castSucc
⊢ i = j

Tactic:
castSucc_injective _ hij

Premises used: Fin.castSucc_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.castSucc = j.castSucc
⊢ i = j

Tactic:
exact castSucc_injective _ hij

Premises used: Fin.castSucc_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.castSucc = j.succ
⊢ j.succ < p

Tactic:
rw [hij] at hi
-- 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.castSucc = j.succ
hi₁ : j.succ < p
⊢ ¬j.castSucc < p

Tactic:
rw [hij] at hi
-- 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.castSucc = j.succ
hi₁ : j.succ < p
hj₁ : ¬j.castSucc < p
⊢ i.castSucc = j.succ

Tactic:
rw [hij] at hi