awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
inl : p.rev.predAbove i = (i.rev.pred ⋯).rev
inl₁ : p.rev.predAbove i = i.rev.rev.castPred ⋯
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev
have inl₂ : i.castPred sorry = i.rev.rev.castPred sorry
Tactic: rw [predAbove_of_succ_le _ _ h, rev_pred,
      predAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), castPred_inj, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
inl : p.rev.predAbove i = (i.rev.pred ⋯).rev
inl₁ : p.rev.predAbove i = i.rev.rev.castPred ⋯
inl₂ : i.castPred ⋯ = i.rev.rev.castPred ⋯
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev
have inl₃ : i = i.rev.rev
Tactic: rw [predAbove_of_succ_le _ _ h, rev_pred,
      predAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), castPred_inj, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : p.succ ≤ i.rev
inl : p.rev.predAbove i = (i.rev.pred ⋯).rev
inl₁ : p.rev.predAbove i = i.rev.rev.castPred ⋯
inl₂ : i.castPred ⋯ = i.rev.rev.castPred ⋯
inl₃ : i = i.rev.rev
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev
have inl₄ : i = i
Tactic: rw [predAbove_of_succ_le _ _ h, rev_pred,
      predAbove_of_le_castSucc _ _ (rev_succ _ ▸ (le_rev_iff.mpr h)), castPred_inj, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev
have inr : p.rev.predAbove i = (i.rev.castPred sorry).rev
Tactic: rw [predAbove_of_le_castSucc _ _ h, rev_castPred,
      predAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), pred_inj, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
inr : p.rev.predAbove i = (i.rev.castPred ⋯).rev
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev
have inr₁ : p.rev.predAbove i = i.rev.rev.pred sorry
Tactic: rw [predAbove_of_le_castSucc _ _ h, rev_castPred,
      predAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), pred_inj, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
inr : p.rev.predAbove i = (i.rev.castPred ⋯).rev
inr₁ : p.rev.predAbove i = i.rev.rev.pred ⋯
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev
have inr₂ : i.pred sorry = i.rev.rev.pred sorry
Tactic: rw [predAbove_of_le_castSucc _ _ h, rev_castPred,
      predAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), pred_inj, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
inr : p.rev.predAbove i = (i.rev.castPred ⋯).rev
inr₁ : p.rev.predAbove i = i.rev.rev.pred ⋯
inr₂ : i.pred ⋯ = i.rev.rev.pred ⋯
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev
have inr₃ : i = i.rev.rev
Tactic: rw [predAbove_of_le_castSucc _ _ h, rev_castPred,
      predAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), pred_inj, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
h : i.rev ≤ p.castSucc
inr : p.rev.predAbove i = (i.rev.castPred ⋯).rev
inr₁ : p.rev.predAbove i = i.rev.rev.pred ⋯
inr₂ : i.pred ⋯ = i.rev.rev.pred ⋯
inr₃ : i = i.rev.rev
⊢ p.rev.predAbove i = (p.predAbove i.rev).rev
have inr₄ : i = i
Tactic: rw [predAbove_of_le_castSucc _ _ h, rev_castPred,
      predAbove_of_succ_le _ _ (rev_castSucc _ ▸ (rev_le_iff.mpr h)), pred_inj, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ p.predAbove i.rev = (p.rev.predAbove i).rev
have rw : p.predAbove i.rev = (p.predAbove i.rev).rev.rev
Tactic: rw [predAbove_rev_left, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
rw : p.predAbove i.rev = (p.predAbove i.rev).rev.rev
⊢ p.predAbove i.rev = (p.rev.predAbove i).rev
have rw₁ : p.predAbove i.rev = p.predAbove i.rev
Tactic: rw [predAbove_rev_left, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
⊢ (p.predAbove i).rev = p.rev.predAbove i.rev
have rw : (p.predAbove i).rev = (p.predAbove i.rev.rev).rev
Tactic: rw [predAbove_rev_left, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
p : Fin n
i : Fin (n + 1)
rw : (p.predAbove i).rev = (p.predAbove i.rev.rev).rev
⊢ (p.predAbove i).rev = p.rev.predAbove i.rev
have rw₁ : (p.predAbove i).rev = (p.predAbove i).rev
Tactic: rw [predAbove_rev_left, rev_rev]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
j : Fin (n + 1)
⊢ (↑j : ℕ) + (↑j.rev : ℕ) = n
have obtain : ∀ (j : ℕ) (hj : j < n + 1), (↑(⟨j, hj⟩ : Fin (n + 1)) : ℕ) + (↑(⟨j, hj⟩ : Fin (n + 1)).rev : ℕ) = n
Tactic: obtain ⟨j, hj⟩ := j
Cleared hypotheses: j
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
j : Fin (n + 1)
⊢ (↑j.rev : ℕ) + (↑j : ℕ) = n
have rw : (↑j : ℕ) + (↑j.rev : ℕ) = n
Tactic: rw [Nat.add_comm, j.add_rev_cast]
-- Lean 4 proof step from Mathlib.Data.Fin.Rev (goal)
Goal:
n : ℕ
j : Fin (n + 1)
rw : (↑j : ℕ) + (↑j.rev : ℕ) = n
⊢ (↑j.rev : ℕ) + (↑j : ℕ) = n
have rw₁ : n = n
Tactic: rw [Nat.add_comm, j.add_rev_cast]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Fin (n + 1)) (succ 0) 1
have zero : ∀ [inst : NeZero (R := ℕ) 0], Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 1)) (succ 0) 1
Tactic: cases n
Cleared hypotheses: n, inst
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
zero : ∀ [inst : NeZero (R := ℕ) 0], Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 1)) (succ 0) 1
⊢ Eq (α := Fin (n + 1)) (succ 0) 1
have succ : ∀ (n : ℕ) [inst : NeZero (n + 1)], Eq (α := Fin (n + 1 + 1)) (succ 0) 1
Tactic: cases n
Cleared hypotheses: n, inst
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Fin (n + 1 + 1)) (succ 1) 2
have zero : ∀ [NeZero (R := ℕ) 0], Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 1 + 1)) (succ 1) 2
Tactic: cases n
Cleared hypotheses: n, inst
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
zero : ∀ [NeZero (R := ℕ) 0], Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 1 + 1)) (succ 1) 2
⊢ Eq (α := Fin (n + 1 + 1)) (succ 1) 2
have succ : ∀ (n : ℕ) [NeZero (n + 1)], Eq (α := Fin (n + 1 + 1 + 1)) (succ 1) 2
Tactic: cases n
Cleared hypotheses: n, inst
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
k : Fin n
h : k ≤ 0
⊢ (↑k : ℕ) = (↑0 : ℕ)
have rw : 0 = (↑0 : ℕ)
Tactic: rw [Nat.eq_zero_of_le_zero h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n k : ℕ
h : n ≤ k
i : Fin k
hi : i ∈ Set.range (castLE h)
⊢ (↑(((Equiv.ofInjective (castLE h) ⋯).symm : (a : (↑(Set.range (castLE h)) : Type)) → Fin n)
          (Subtype.mk (p := fun (x : Fin k) ↦ x ∈ Set.range (castLE h)) i hi)) :
      ℕ) =
    (↑i : ℕ)
have rw : (↑(castLE h
        (((Equiv.ofInjective (castLE h) sorry).symm : (a : (↑(Set.range (castLE h)) : Type)) → Fin n)
          (Subtype.mk (p := fun (x : Fin k) ↦ x ∈ Set.range (castLE h)) i hi))) :
    ℕ) =
  (↑i : ℕ)
Tactic: rw [← val_castLE h]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
h : n = n
⊢ finCongr h = Equiv.refl (Fin n)
have H : ∀ (x : Fin n), (↑((finCongr h : (a : Fin n) → Fin n) x) : ℕ) = (↑((Equiv.refl (Fin n) : (a : Fin n) → Fin n) x) : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n m : ℕ
h : n = m
⊢ finCongr h = Equiv.cast ⋯
have subst : finCongr sorry = Equiv.cast sorry
Tactic: subst h
Cleared hypotheses: m, h
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin n
⊢ a.succ ≤ b.castSucc ↔ a < b
have rw : a.succ < b.succ ↔ a < b
Tactic: rw [le_castSucc_iff, succ_lt_succ_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin n
rw : a.succ < b.succ ↔ a < b
⊢ a.succ ≤ b.castSucc ↔ a < b
have rw₁ : a < b ↔ a < b
Tactic: rw [le_castSucc_iff, succ_lt_succ_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin n
⊢ a.castSucc < b.succ ↔ a ≤ b
have rw : a.succ ≤ b.succ ↔ a ≤ b
Tactic: rw [castSucc_lt_iff_succ_le, succ_le_succ_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin n
rw : a.succ ≤ b.succ ↔ a ≤ b
⊢ a.castSucc < b.succ ↔ a ≤ b
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [castSucc_lt_iff_succ_le, succ_le_succ_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (hypothesis)
Goal:
n : ℕ
a b : Fin (n + 1)
i : Fin n
hl : i.castSucc < a
hu : b < i.succ
⊢ b < a
have hl₁ : (↑i : ℕ) < (↑a : ℕ)
Tactic: simp [Fin.lt_def, -val_fin_lt] at *
Cleared hypotheses: hl, hu
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (hypothesis)
Goal:
n : ℕ
a b : Fin (n + 1)
i : Fin n
hl : i.castSucc < a
hu : b < i.succ
hl₁ : (↑i : ℕ) < (↑a : ℕ)
⊢ b < a
have hu₁ : (↑b : ℕ) < (↑i : ℕ) + 1
Tactic: simp [Fin.lt_def, -val_fin_lt] at *
Cleared hypotheses: hl, hu
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.castSucc < p ∨ p < i.succ
have simp : (↑i : ℕ) < (↑p : ℕ) ∨ (↑p : ℕ) < (↑i : ℕ) + 1
Tactic: simp [Fin.lt_def, -val_fin_lt]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p : Fin (n + 1)
i : Fin n
⊢ i.succ ≤ p ∨ p ≤ i.castSucc
have rw : i.castSucc < p ∨ p < i.succ
Tactic: rw [le_castSucc_iff, ← castSucc_lt_iff_succ_le]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin n
h : p < i
⊢ i.castSucc ≠ 0
have zero : ∀ {p i : Fin 0} (h : p < i), i.castSucc ≠ 0
Tactic: cases n
Cleared hypotheses: n, p, i, h
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
p i : Fin n
h : p < i
zero : ∀ {p i : Fin 0} (h : p < i), i.castSucc ≠ 0
⊢ i.castSucc ≠ 0
have succ : ∀ (n : ℕ) {p i : Fin (n + 1)} (h : p < i), i.castSucc ≠ 0
Tactic: cases n
Cleared hypotheses: n, p, i, h
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin n
⊢ (↑(↑a : ℕ) : Fin (n + 1)) = a.castSucc
have h : (↑(↑(↑a : ℕ) : Fin (n + 1)) : ℕ) = (↑a.castSucc : ℕ)
Tactic: ext
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin n.succ
hi : Membership.mem (γ := Set (Fin (n + 1))) (Set.range castSucc) 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 : ℕ)
have rw : (↑(castSucc
        (((Equiv.ofInjective castSucc sorry).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]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n m : ℕ
i : Fin n
⊢ (castAdd m i).succ = if h : i.succ = last n then natAdd n 0 else castAdd (m + 1) ⟨(↑i : ℕ) + 1, ⋯⟩
have pos : ∀ (h : i.succ = last n), (castAdd m i).succ = natAdd n 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n m : ℕ
i : Fin n
pos : ∀ (h : i.succ = last n), (castAdd m i).succ = natAdd n 0
⊢ (castAdd m i).succ = if h : i.succ = last n then natAdd n 0 else castAdd (m + 1) ⟨(↑i : ℕ) + 1, ⋯⟩
have neg : ∀ (h : ¬i.succ = last n), (castAdd m i).succ = castAdd (m + 1) ⟨(↑i : ℕ) + 1, sorry⟩
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
h : Ne (α := Fin (n + 1)) 1 0
⊢ pred 1 h = 0
have simp_rw : (↑(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]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
h : Ne (α := Fin (n + 1)) 1 0
simp_rw : (↑(pred 1 h) : ℕ) = (↑0 : ℕ)
⊢ pred 1 h = 0
have simp_rw₁ : (↑1 : ℕ) - 1 = (↑0 : ℕ)
Tactic: simp_rw [Fin.ext_iff, val_pred, val_one', val_zero, Nat.sub_eq_zero_iff_le, Nat.mod_le]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
h : Ne (α := Fin (n + 1)) 1 0
simp_rw : (↑(pred 1 h) : ℕ) = (↑0 : ℕ)
simp_rw₁ : (↑1 : ℕ) - 1 = (↑0 : ℕ)
⊢ pred 1 h = 0
have simp_rw₂ : 1 % (n + 1) - 1 = (↑0 : ℕ)
Tactic: simp_rw [Fin.ext_iff, val_pred, val_one', val_zero, Nat.sub_eq_zero_iff_le, Nat.mod_le]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
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 : ℕ)
⊢ pred 1 h = 0
have simp_rw₃ : 1 % (n + 1) - 1 = 0
Tactic: simp_rw [Fin.ext_iff, val_pred, val_one', val_zero, Nat.sub_eq_zero_iff_le, Nat.mod_le]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
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
⊢ pred 1 h = 0
have simp_rw₄ : 1 % (n + 1) ≤ 1
Tactic: simp_rw [Fin.ext_iff, val_pred, val_one', val_zero, Nat.sub_eq_zero_iff_le, Nat.mod_le]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ i.pred hi < j ↔ i < j.succ
have rw : (i.pred hi).succ < j.succ ↔ i < j.succ
Tactic: rw [← succ_lt_succ_iff, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
rw : (i.pred hi).succ < j.succ ↔ i < j.succ
⊢ i.pred hi < j ↔ i < j.succ
have rw₁ : i < j.succ ↔ i < j.succ
Tactic: rw [← succ_lt_succ_iff, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ j < i.pred hi ↔ j.succ < i
have rw : j.succ < (i.pred hi).succ ↔ j.succ < i
Tactic: rw [← succ_lt_succ_iff, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
rw : j.succ < (i.pred hi).succ ↔ j.succ < i
⊢ j < i.pred hi ↔ j.succ < i
have rw₁ : j.succ < i ↔ j.succ < i
Tactic: rw [← succ_lt_succ_iff, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ i.pred hi ≤ j ↔ i ≤ j.succ
have rw : (i.pred hi).succ ≤ j.succ ↔ i ≤ j.succ
Tactic: rw [← succ_le_succ_iff, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
rw : (i.pred hi).succ ≤ j.succ ↔ i ≤ j.succ
⊢ i.pred hi ≤ j ↔ i ≤ j.succ
have rw₁ : i ≤ j.succ ↔ i ≤ j.succ
Tactic: rw [← succ_le_succ_iff, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
⊢ j ≤ i.pred hi ↔ j.succ ≤ i
have rw : j.succ ≤ (i.pred hi).succ ↔ j.succ ≤ i
Tactic: rw [← succ_le_succ_iff, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ 0
rw : j.succ ≤ (i.pred hi).succ ↔ j.succ ≤ i
⊢ j ≤ i.pred hi ↔ j.succ ≤ i
have rw₁ : j.succ ≤ i ↔ j.succ ≤ i
Tactic: rw [← succ_le_succ_iff, succ_pred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ b ≤ a.castSucc.pred ha ↔ b < a
have rw : b.succ ≤ a.castSucc ↔ b < a
Tactic: rw [le_pred_iff, succ_le_castSucc_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
rw : b.succ ≤ a.castSucc ↔ b < a
⊢ b ≤ a.castSucc.pred ha ↔ b < a
have rw₁ : b < a ↔ b < a
Tactic: rw [le_pred_iff, succ_le_castSucc_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ a.castSucc.pred ha < b ↔ a ≤ b
have rw : a.castSucc < b.succ ↔ a ≤ b
Tactic: rw [pred_lt_iff, castSucc_lt_succ_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a.castSucc ≠ 0
rw : a.castSucc < b.succ ↔ a ≤ b
⊢ a.castSucc.pred ha < b ↔ a ≤ b
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [pred_lt_iff, castSucc_lt_succ_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 1)
ha : a.castSucc ≠ 0
⊢ a.castSucc.pred ha < a
have rw : a ≤ a
Tactic: rw [pred_castSucc_lt_iff, le_def]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 1)
ha : a.castSucc ≠ 0
rw : a ≤ a
⊢ a.castSucc.pred ha < a
have rw₁ : (↑a : ℕ) ≤ (↑a : ℕ)
Tactic: rw [pred_castSucc_lt_iff, le_def]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
⊢ b ≤ (a.pred ha).castSucc ↔ b < a
have rw : b ≤ a.castSucc.pred sorry ↔ b < a
Tactic: rw [castSucc_pred_eq_pred_castSucc, le_pred_castSucc_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
rw : b ≤ a.castSucc.pred ⋯ ↔ b < a
⊢ b ≤ (a.pred ha).castSucc ↔ b < a
have rw₁ : b < a ↔ b < a
Tactic: rw [castSucc_pred_eq_pred_castSucc, le_pred_castSucc_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
⊢ (a.pred ha).castSucc < b ↔ a ≤ b
have rw : a.castSucc.pred sorry < b ↔ a ≤ b
Tactic: rw [castSucc_pred_eq_pred_castSucc, pred_castSucc_lt_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a b : Fin (n + 1)
ha : a ≠ 0
rw : a.castSucc.pred ⋯ < b ↔ a ≤ b
⊢ (a.pred ha).castSucc < b ↔ a ≤ b
have rw₁ : a ≤ b ↔ a ≤ b
Tactic: rw [castSucc_pred_eq_pred_castSucc, pred_castSucc_lt_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 1)
ha : a ≠ 0
⊢ (a.pred ha).castSucc < a
have rw : a ≤ a
Tactic: rw [castSucc_pred_lt_iff, le_def]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
a : Fin (n + 1)
ha : a ≠ 0
rw : a ≤ a
⊢ (a.pred ha).castSucc < a
have rw₁ : (↑a : ℕ) ≤ (↑a : ℕ)
Tactic: rw [castSucc_pred_lt_iff, le_def]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
h : i ≠ last n
⊢ (i.castPred h).castSucc = i
have rcases : ∀ (y : Fin n) (h : y.castSucc ≠ last n), (y.castSucc.castPred h).castSucc = y.castSucc
Tactic: rcases exists_castSucc_eq.mpr h with ⟨y, rfl⟩
Cleared hypotheses: i, h
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
y : Fin n
h : y.castSucc ≠ last n
⊢ (y.castSucc.castPred h).castSucc = y.castSucc
have rw : y.castSucc = y.castSucc
Tactic: rw [castPred_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
hi : i ≠ last n
j : Fin n
h : i.castPred hi = j
⊢ i = j.castSucc
have rw : i = (i.castPred hi).castSucc
Tactic: rw [← h, castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
hi : i ≠ last n
j : Fin n
h : i.castPred hi = j
rw : i = (i.castPred hi).castSucc
⊢ i = j.castSucc
have rw₁ : i = i
Tactic: rw [← h, castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i : Fin (n + 1)
hi : i ≠ last n
j : Fin n
h : i = j.castSucc
⊢ i.castPred hi = j
have simp_rw : j.castSucc.castPred sorry = j
Tactic: simp_rw [h, castPred_castSucc]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n m : ℕ
i j : Fin (n + 1)
h : i ≤ j
hj : j ≠ last n
⊢ i ≠ last n
have rw : ∀ (hj : j < last n), i < last n
Tactic: rw [← lt_last_iff_ne_last] at hj ⊢
Cleared hypotheses: hj
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ i.castPred hi < j ↔ i < j.castSucc
have rw : (i.castPred hi).castSucc < j.castSucc ↔ i < j.castSucc
Tactic: rw [← castSucc_lt_castSucc_iff, castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
rw : (i.castPred hi).castSucc < j.castSucc ↔ i < j.castSucc
⊢ i.castPred hi < j ↔ i < j.castSucc
have rw₁ : i < j.castSucc ↔ i < j.castSucc
Tactic: rw [← castSucc_lt_castSucc_iff, castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ j < i.castPred hi ↔ j.castSucc < i
have rw : j.castSucc < (i.castPred hi).castSucc ↔ j.castSucc < i
Tactic: rw [← castSucc_lt_castSucc_iff, castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
rw : j.castSucc < (i.castPred hi).castSucc ↔ j.castSucc < i
⊢ j < i.castPred hi ↔ j.castSucc < i
have rw₁ : j.castSucc < i ↔ j.castSucc < i
Tactic: rw [← castSucc_lt_castSucc_iff, castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ i.castPred hi ≤ j ↔ i ≤ j.castSucc
have rw : (i.castPred hi).castSucc ≤ j.castSucc ↔ i ≤ j.castSucc
Tactic: rw [← castSucc_le_castSucc_iff, castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
rw : (i.castPred hi).castSucc ≤ j.castSucc ↔ i ≤ j.castSucc
⊢ i.castPred hi ≤ j ↔ i ≤ j.castSucc
have rw₁ : i ≤ j.castSucc ↔ i ≤ j.castSucc
Tactic: rw [← castSucc_le_castSucc_iff, castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
⊢ j ≤ i.castPred hi ↔ j.castSucc ≤ i
have rw : j.castSucc ≤ (i.castPred hi).castSucc ↔ j.castSucc ≤ i
Tactic: rw [← castSucc_le_castSucc_iff, castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
j : Fin n
i : Fin (n + 1)
hi : i ≠ last n
rw : j.castSucc ≤ (i.castPred hi).castSucc ↔ j.castSucc ≤ i
⊢ j ≤ i.castPred hi ↔ j.castSucc ≤ i
have rw₁ : j.castSucc ≤ i ↔ j.castSucc ≤ i
Tactic: rw [← castSucc_le_castSucc_iff, castSucc_castPred]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
i j : Fin (n + 1)
hi : i ≠ last n
hj : j ≠ last n
⊢ i.castPred hi = j.castPred hj ↔ i = j
have simp_rw : (↑(i.castPred hi) : ℕ) = (↑(j.castPred hj) : ℕ) ↔ (↑i : ℕ) = (↑j : ℕ)
Tactic: simp_rw [Fin.ext_iff, le_antisymm_iff, ← le_def, castPred_le_castPred_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
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 : ℕ)
⊢ i.castPred hi = j.castPred hj ↔ i = j
have simp_rw₁ : (↑(i.castPred hi) : ℕ) ≤ (↑(j.castPred hj) : ℕ) ∧ (↑(j.castPred hj) : ℕ) ≤ (↑(i.castPred hi) : ℕ) ↔
  (↑i : ℕ) ≤ (↑j : ℕ) ∧ (↑j : ℕ) ≤ (↑i : ℕ)
Tactic: simp_rw [Fin.ext_iff, le_antisymm_iff, ← le_def, castPred_le_castPred_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
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 : ℕ)
⊢ i.castPred hi = j.castPred hj ↔ i = j
have simp_rw₂ : i.castPred hi ≤ j.castPred hj ∧ j.castPred hj ≤ i.castPred hi ↔ i ≤ j ∧ j ≤ i
Tactic: simp_rw [Fin.ext_iff, le_antisymm_iff, ← le_def, castPred_le_castPred_iff]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
h : i ≠ last n
⊢ i.castPred h = 0 ↔ i = 0
have rw : i.castPred h = castPred 0 sorry ↔ i = 0
Tactic: rw [← castPred_zero, castPred_inj]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
i : Fin (n + 1)
h : i ≠ last n
rw : i.castPred h = castPred 0 ⋯ ↔ i = 0
⊢ i.castPred h = 0 ↔ i = 0
have rw₁ : i = 0 ↔ i = 0
Tactic: rw [← castPred_zero, castPred_inj]
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
⊢ Eq (α := Fin (n + 1)) (castPred 1 ⋯) 1
have zero : ∀ [inst : NeZero (R := ℕ) 0], Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 1)) (castPred 1 sorry) 1
Tactic: cases n
Cleared hypotheses: n, inst
-- Lean 4 proof step from Mathlib.Data.Fin.SuccPred (goal)
Goal:
n : ℕ
inst : NeZero n
zero : ∀ [inst : NeZero (R := ℕ) 0], Eq (α := Fin (HAdd.hAdd (α := ℕ) 0 1)) (castPred 1 ⋯) 1
⊢ Eq (α := Fin (n + 1)) (castPred 1 ⋯) 1
have succ : ∀ (n : ℕ) [inst : NeZero (n + 1)], Eq (α := Fin (n + 1 + 1)) (castPred 1 sorry) 1
Tactic: cases n
Cleared hypotheses: n, inst