awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
x : α
n : ℕ
zero : succ^[0] x = x + (↑0 : α)
⊢ succ^[n] x = x + (↑n : α)
have succ : ∀ (n : ℕ) (IH : succ^[n] x = x + (↑n : α)), succ^[n + 1] x = x + (↑(n + 1) : α)
Tactic: induction n with
  | zero =>
    rw [Function.iterate_zero_apply, Nat.cast_zero, add_zero]
  | succ n IH =>
    rw [Function.iterate_succ_apply', IH, Nat.cast_add, succ_eq_add_one, Nat.cast_one, add_assoc]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
x : α
⊢ pred^[0] x = x - (↑0 : α)
have zero : x = x - (↑0 : α)
Tactic: rw [Function.iterate_zero_apply, Nat.cast_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
x : α
zero : x = x - (↑0 : α)
⊢ pred^[0] x = x - (↑0 : α)
have zero₁ : x = x - 0
Tactic: rw [Function.iterate_zero_apply, Nat.cast_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
x : α
zero : x = x - (↑0 : α)
zero₁ : x = x - 0
⊢ pred^[0] x = x - (↑0 : α)
have zero₂ : x = x
Tactic: rw [Function.iterate_zero_apply, Nat.cast_zero, sub_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - (↑n : α)
⊢ pred^[n + 1] x = x - (↑(n + 1) : α)
have succ : pred (pred^[n] x) = x - (↑(n + 1) : α)
Tactic: rw [Function.iterate_succ_apply', IH, Nat.cast_add, pred_eq_sub_one, Nat.cast_one, sub_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - (↑n : α)
succ : pred (pred^[n] x) = x - (↑(n + 1) : α)
⊢ pred^[n + 1] x = x - (↑(n + 1) : α)
have succ₁ : pred (x - (↑n : α)) = x - (↑(n + 1) : α)
Tactic: rw [Function.iterate_succ_apply', IH, Nat.cast_add, pred_eq_sub_one, Nat.cast_one, sub_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - (↑n : α)
succ : pred (pred^[n] x) = x - (↑(n + 1) : α)
succ₁ : pred (x - (↑n : α)) = x - (↑(n + 1) : α)
⊢ pred^[n + 1] x = x - (↑(n + 1) : α)
have succ₂ : pred (x - (↑n : α)) = x - HAdd.hAdd (α := α) (↑n : α) (↑1 : α)
Tactic: rw [Function.iterate_succ_apply', IH, Nat.cast_add, pred_eq_sub_one, Nat.cast_one, sub_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - (↑n : α)
succ : pred (pred^[n] x) = x - (↑(n + 1) : α)
succ₁ : pred (x - (↑n : α)) = x - (↑(n + 1) : α)
succ₂ : pred (x - (↑n : α)) = x - HAdd.hAdd (α := α) (↑n : α) (↑1 : α)
⊢ pred^[n + 1] x = x - (↑(n + 1) : α)
have succ₃ : x - (↑n : α) - 1 = x - HAdd.hAdd (α := α) (↑n : α) (↑1 : α)
Tactic: rw [Function.iterate_succ_apply', IH, Nat.cast_add, pred_eq_sub_one, Nat.cast_one, sub_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - (↑n : α)
succ : pred (pred^[n] x) = x - (↑(n + 1) : α)
succ₁ : pred (x - (↑n : α)) = x - (↑(n + 1) : α)
succ₂ : pred (x - (↑n : α)) = x - HAdd.hAdd (α := α) (↑n : α) (↑1 : α)
succ₃ : x - (↑n : α) - 1 = x - HAdd.hAdd (α := α) (↑n : α) (↑1 : α)
⊢ pred^[n + 1] x = x - (↑(n + 1) : α)
have succ₄ : x - (↑n : α) - 1 = x - HAdd.hAdd (α := α) (↑n : α) 1
Tactic: rw [Function.iterate_succ_apply', IH, Nat.cast_add, pred_eq_sub_one, Nat.cast_one, sub_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
x : α
n : ℕ
IH : pred^[n] x = x - (↑n : α)
succ : pred (pred^[n] x) = x - (↑(n + 1) : α)
succ₁ : pred (x - (↑n : α)) = x - (↑(n + 1) : α)
succ₂ : pred (x - (↑n : α)) = x - HAdd.hAdd (α := α) (↑n : α) (↑1 : α)
succ₃ : x - (↑n : α) - 1 = x - HAdd.hAdd (α := α) (↑n : α) (↑1 : α)
succ₄ : x - (↑n : α) - 1 = x - HAdd.hAdd (α := α) (↑n : α) 1
⊢ pred^[n + 1] x = x - (↑(n + 1) : α)
have succ₅ : x - HAdd.hAdd (α := α) (↑n : α) 1 = x - HAdd.hAdd (α := α) (↑n : α) 1
Tactic: rw [Function.iterate_succ_apply', IH, Nat.cast_add, pred_eq_sub_one, Nat.cast_one, sub_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
x : α
n : ℕ
⊢ pred^[n] x = x - (↑n : α)
have zero : pred^[0] x = x - (↑0 : α)
Tactic: induction n with
  | zero =>
    rw [Function.iterate_zero_apply, Nat.cast_zero, sub_zero]
  | succ n IH =>
    rw [Function.iterate_succ_apply', IH, Nat.cast_add, pred_eq_sub_one, Nat.cast_one, sub_sub]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
x : α
n : ℕ
zero : pred^[0] x = x - (↑0 : α)
⊢ pred^[n] x = x - (↑n : α)
have succ : ∀ (n : ℕ) (IH : pred^[n] x = x - (↑n : α)), pred^[n + 1] x = x - (↑(n + 1) : α)
Tactic: induction n with
  | zero =>
    rw [Function.iterate_zero_apply, Nat.cast_zero, sub_zero]
  | succ n IH =>
    rw [Function.iterate_succ_apply', IH, Nat.cast_add, pred_eq_sub_one, Nat.cast_one, sub_sub]
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : Zero α
inst_2 : One α
inst_3 : ZeroLEOneClass α
inst_4 : NeZero.{u_1} (R := α) 1
⊢ ¬IsMax.{u_1} (α := α) 0
have rw : ∃ (b : α), 0 < b
Tactic: rw [not_isMax_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : SuccAddOrder α
⊢ 1 ≤ x ↔ 0 < x
have rw : 1 ≤ x ↔ succ 0 ≤ x
Tactic: rw [← succ_le_iff_of_not_isMax not_isMax_zero, succ_eq_add_one, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : SuccAddOrder α
rw : 1 ≤ x ↔ succ 0 ≤ x
⊢ 1 ≤ x ↔ 0 < x
have rw₁ : 1 ≤ x ↔ HAdd.hAdd (α := α) 0 1 ≤ x
Tactic: rw [← succ_le_iff_of_not_isMax not_isMax_zero, succ_eq_add_one, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : SuccAddOrder α
rw : 1 ≤ x ↔ succ 0 ≤ x
rw₁ : 1 ≤ x ↔ HAdd.hAdd (α := α) 0 1 ≤ x
⊢ 1 ≤ x ↔ 0 < x
have rw₂ : 1 ≤ x ↔ 1 ≤ x
Tactic: rw [← succ_le_iff_of_not_isMax not_isMax_zero, succ_eq_add_one, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NeZero.{u_1} (R := α) 1
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
⊢ 1 ≤ x ↔ x ≠ 0
have rw : 0 < x ↔ x ≠ 0
Tactic: rw [Order.one_le_iff_pos, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NeZero.{u_1} (R := α) 1
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
rw : 0 < x ↔ x ≠ 0
⊢ 1 ≤ x ↔ x ≠ 0
have rw₁ : x ≠ 0 ↔ x ≠ 0
Tactic: rw [Order.one_le_iff_pos, pos_iff_ne_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
inst_4 : NoMaxOrder α
⊢ x ⋖ y ↔ x + 1 = y
have rw : x ⋖ y ↔ succ x = y
Tactic: rw [← succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
inst_4 : NoMinOrder α
⊢ x ⋖ y ↔ y - 1 = x
have rw : x ⋖ y ↔ pred y = x
Tactic: rw [← pred_eq_sub_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
⊢ y + 1 < x
have rw : succ y < x
Tactic: rw [← succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
⊢ x < y - 1
have rw : x < pred y
Tactic: rw [← pred_eq_sub_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
hx : IsSuccPrelimit x
hy : y < x
n : ℕ
⊢ y + (↑(n + 1) : α) < x
have rw : y + (↑n : α) + 1 < x
Tactic: rw [Nat.cast_add_one, ← add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x y : α
inst : PartialOrder α
inst_1 : AddCommGroupWithOne α
inst_2 : PredSubOrder α
hx : IsPredPrelimit x
hy : x < y
n : ℕ
⊢ x < y - (↑(n + 1) : α)
have rw : x < y - (↑n : α) - 1
Tactic: rw [Nat.cast_add_one, ← sub_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddZeroClass α
inst_2 : OrderBot α
inst_3 : IsBotZeroClass α
inst_4 : One α
inst_5 : NoMaxOrder α
inst_6 : SuccAddOrder α
a : WithBot α
⊢ a.succ = 0 ↔ a = ⊥
have bot : Eq.{u_1 + 1} (α := α) (WithBot.succ ⊥) 0 ↔ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddZeroClass α
inst_2 : OrderBot α
inst_3 : IsBotZeroClass α
inst_4 : One α
inst_5 : NoMaxOrder α
inst_6 : SuccAddOrder α
a : WithBot α
bot : Eq.{u_1 + 1} (α := α) (WithBot.succ ⊥) 0 ↔ Eq.{u_1 + 1} (α := WithBot α) ⊥ ⊥
⊢ a.succ = 0 ↔ a = ⊥
have coe : ∀ (a : α), (↑a : WithBot α).succ = 0 ↔ (↑a : WithBot α) = ⊥
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : PartialOrder α
inst_1 : AddZeroClass α
inst_2 : OrderBot α
inst_3 : IsBotZeroClass α
inst_4 : One α
inst_5 : NoMaxOrder α
inst_6 : SuccAddOrder α
a : α
⊢ (↑a : WithBot α).succ = 0 ↔ (↑a : WithBot α) = ⊥
have coe : ¬a + 1 = 0
Tactic: simp only [WithBot.succ_coe, WithBot.coe_ne_bot, iff_false, succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (hypothesis)
Goal:
α : Type u_1
x y : α
inst : LinearOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
h : x < y + 1
⊢ x ≤ y
have h₁ : x < succ y
Tactic: rw [← succ_eq_add_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x y : α
inst : LinearOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
hy : ¬IsMax y
⊢ x < y + 1 ↔ x ≤ y
have rw : x < succ y ↔ x ≤ y
Tactic: rw [← succ_eq_add_one, lt_succ_iff_of_not_isMax hy]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x y : α
inst : LinearOrder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
hy : ¬IsMax y
rw : x < succ y ↔ x ≤ y
⊢ x < y + 1 ↔ x ≤ y
have rw₁ : x ≤ y ↔ x ≤ y
Tactic: rw [← succ_eq_add_one, lt_succ_iff_of_not_isMax hy]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
⊢ x < 1 ↔ x = 0
have rw : x < HAdd.hAdd (α := α) 0 1 ↔ x = 0
Tactic: rw [← zero_add 1, lt_add_one_iff, nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
rw : x < HAdd.hAdd (α := α) 0 1 ↔ x = 0
⊢ x < 1 ↔ x = 0
have rw₁ : x ≤ 0 ↔ x = 0
Tactic: rw [← zero_add 1, lt_add_one_iff, nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
rw : x < HAdd.hAdd (α := α) 0 1 ↔ x = 0
rw₁ : x ≤ 0 ↔ x = 0
⊢ x < 1 ↔ x = 0
have rw₂ : x = 0 ↔ x = 0
Tactic: rw [← zero_add 1, lt_add_one_iff, nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
⊢ x ≤ 1 ↔ x = 0 ∨ x = 1
have rw : x < 1 ∨ x = 1 ↔ x = 0 ∨ x = 1
Tactic: rw [le_iff_lt_or_eq, lt_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
rw : x < 1 ∨ x = 1 ↔ x = 0 ∨ x = 1
⊢ x ≤ 1 ↔ x = 0 ∨ x = 1
have rw₁ : x = 0 ∨ x = 1 ↔ x = 0 ∨ x = 1
Tactic: rw [le_iff_lt_or_eq, lt_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
⊢ Eq (α := Set α) (Set.Iio 1) {0}
have h : ∀ (x : α), Membership.mem (γ := Set α) (Set.Iio 1) x ↔ Membership.mem (γ := Set α) {0} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
⊢ Eq (α := Set α) (Set.Iic 1) {0, 1}
have h : ∀ (x : α), Membership.mem (γ := Set α) (Set.Iic 1) x ↔ Membership.mem (γ := Set α) {0, 1} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
⊢ x < 2 ↔ x ≤ 1
have rw : x < HAdd.hAdd (α := α) 1 1 ↔ x ≤ 1
Tactic: rw [← one_add_one_eq_two, lt_add_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
rw : x < HAdd.hAdd (α := α) 1 1 ↔ x ≤ 1
⊢ x < 2 ↔ x ≤ 1
have rw₁ : x ≤ 1 ↔ x ≤ 1
Tactic: rw [← one_add_one_eq_two, lt_add_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
⊢ x ≤ 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
have rw : x < 2 ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
Tactic: rw [le_iff_lt_or_eq, lt_two_iff, le_one_iff, or_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
rw : x < 2 ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
⊢ x ≤ 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
have rw₁ : x ≤ 1 ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
Tactic: rw [le_iff_lt_or_eq, lt_two_iff, le_one_iff, or_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
rw : x < 2 ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
rw₁ : x ≤ 1 ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
⊢ x ≤ 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
have rw₂ : (x = 0 ∨ x = 1) ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
Tactic: rw [le_iff_lt_or_eq, lt_two_iff, le_one_iff, or_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
rw : x < 2 ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
rw₁ : x ≤ 1 ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
rw₂ : (x = 0 ∨ x = 1) ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
⊢ x ≤ 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
have rw₃ : x = 0 ∨ x = 1 ∨ x = 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
Tactic: rw [le_iff_lt_or_eq, lt_two_iff, le_one_iff, or_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
⊢ Eq (α := Set α) (Set.Iio 2) {0, 1}
have h : ∀ (x : α), Membership.mem (γ := Set α) (Set.Iio 2) x ↔ Membership.mem (γ := Set α) {0, 1} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : NoMaxOrder α
inst_3 : SuccAddOrder α
inst_4 : IsBotZeroClass α
⊢ Eq (α := Set α) (Set.Iic 2) {0, 1, 2}
have h : ∀ (x : α), Membership.mem (γ := Set α) (Set.Iic 2) x ↔ Membership.mem (γ := Set α) {0, 1, 2} x
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (hypothesis)
Goal:
α : Type u_1
x y : α
inst : LinearOrder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
h : x - 1 < y
⊢ x ≤ y
have h₁ : pred x < y
Tactic: rw [← pred_eq_sub_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x y : α
inst : LinearOrder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
hx : ¬IsMin x
⊢ x - 1 < y ↔ x ≤ y
have rw : pred x < y ↔ x ≤ y
Tactic: rw [← pred_eq_sub_one, pred_lt_iff_of_not_isMin hx]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x y : α
inst : LinearOrder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
hx : ¬IsMin x
rw : pred x < y ↔ x ≤ y
⊢ x - 1 < y ↔ x ≤ y
have rw₁ : x ≤ y ↔ x ≤ y
Tactic: rw [← pred_eq_sub_one, pred_lt_iff_of_not_isMin hx]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : SuccAddOrder α
⊢ x < 1 ↔ x ≤ 0
have rw : x < 1 ↔ x < succ 0
Tactic: rw [← lt_succ_iff_of_not_isMax not_isMax_zero, succ_eq_add_one, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : SuccAddOrder α
rw : x < 1 ↔ x < succ 0
⊢ x < 1 ↔ x ≤ 0
have rw₁ : x < 1 ↔ x < HAdd.hAdd (α := α) 0 1
Tactic: rw [← lt_succ_iff_of_not_isMax not_isMax_zero, succ_eq_add_one, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x : α
inst : LinearOrder α
inst_1 : AddMonoidWithOne α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_1} (R := α) 1
inst_4 : SuccAddOrder α
rw : x < 1 ↔ x < succ 0
rw₁ : x < 1 ↔ x < HAdd.hAdd (α := α) 0 1
⊢ x < 1 ↔ x ≤ 0
have rw₂ : x < 1 ↔ x < 1
Tactic: rw [← lt_succ_iff_of_not_isMax not_isMax_zero, succ_eq_add_one, zero_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
b : α
⊢ toIcoMod hp 0 b ∈ Set.Ico 0 p
have h : p = 0 + p
Tactic: convert! toIcoMod_mem_Ico hp 0 b
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoDiv hp a b • p - b = -toIcoMod hp a b
have rw : toIcoDiv hp a b • p - b = -(b - toIcoDiv hp a b • p)
Tactic: rw [toIcoMod, neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
rw : toIcoDiv hp a b • p - b = -(b - toIcoDiv hp a b • p)
⊢ toIcoDiv hp a b • p - b = -toIcoMod hp a b
have rw₁ : toIcoDiv hp a b • p - b = toIcoDiv hp a b • p - b
Tactic: rw [toIcoMod, neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocDiv hp a b • p - b = -toIocMod hp a b
have rw : toIocDiv hp a b • p - b = -(b - toIocDiv hp a b • p)
Tactic: rw [toIocMod, neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
rw : toIocDiv hp a b • p - b = -(b - toIocDiv hp a b • p)
⊢ toIocDiv hp a b • p - b = -toIocMod hp a b
have rw₁ : toIocDiv hp a b • p - b = toIocDiv hp a b • p - b
Tactic: rw [toIocMod, neg_sub]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIcoMod hp a b - b = -toIcoDiv hp a b • p
have rw : b - toIcoDiv hp a b • p - b = -toIcoDiv hp a b • p
Tactic: rw [toIcoMod, sub_sub_cancel_left, neg_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
rw : b - toIcoDiv hp a b • p - b = -toIcoDiv hp a b • p
⊢ toIcoMod hp a b - b = -toIcoDiv hp a b • p
have rw₁ : -(toIcoDiv hp a b • p) = -toIcoDiv hp a b • p
Tactic: rw [toIcoMod, sub_sub_cancel_left, neg_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
rw : b - toIcoDiv hp a b • p - b = -toIcoDiv hp a b • p
rw₁ : -(toIcoDiv hp a b • p) = -toIcoDiv hp a b • p
⊢ toIcoMod hp a b - b = -toIcoDiv hp a b • p
have rw₂ : -(toIcoDiv hp a b • p) = -(toIcoDiv hp a b • p)
Tactic: rw [toIcoMod, sub_sub_cancel_left, neg_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ toIocMod hp a b - b = -toIocDiv hp a b • p
have rw : b - toIocDiv hp a b • p - b = -toIocDiv hp a b • p
Tactic: rw [toIocMod, sub_sub_cancel_left, neg_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
rw : b - toIocDiv hp a b • p - b = -toIocDiv hp a b • p
⊢ toIocMod hp a b - b = -toIocDiv hp a b • p
have rw₁ : -(toIocDiv hp a b • p) = -toIocDiv hp a b • p
Tactic: rw [toIocMod, sub_sub_cancel_left, neg_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
rw : b - toIocDiv hp a b • p - b = -toIocDiv hp a b • p
rw₁ : -(toIocDiv hp a b • p) = -toIocDiv hp a b • p
⊢ toIocMod hp a b - b = -toIocDiv hp a b • p
have rw₂ : -(toIocDiv hp a b • p) = -(toIocDiv hp a b • p)
Tactic: rw [toIocMod, sub_sub_cancel_left, neg_smul]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
⊢ b - toIcoMod hp a b = toIcoDiv hp a b • p
have rw : b - (b - toIcoDiv hp a b • p) = toIcoDiv hp a b • p
Tactic: rw [toIcoMod, sub_sub_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.ToIntervalMod (goal)
Goal:
α : Type u_1
inst : AddCommGroup α
inst_1 : LinearOrder α
inst_2 : IsOrderedAddMonoid α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
rw : b - (b - toIcoDiv hp a b • p) = toIcoDiv hp a b • p
⊢ b - toIcoMod hp a b = toIcoDiv hp a b • p
have rw₁ : toIcoDiv hp a b • p = toIcoDiv hp a b • p
Tactic: rw [toIcoMod, sub_sub_cancel]