awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Unbundled.Hom (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : PartialOrder β
inst_7 : AddCommSemigroup β
inst_8 : Sub β
inst_9 : OrderedSub β
inst_10 : AddLeftReflectLE β
inst_11 : FunLike F α β
inst_12 : AddHomClass F α β
f : F
a b : α
h : b ≤ a
| HSub.hSub (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) = (f : (a : α) → β) (a - b)
have lhs : HSub.hSub (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
Tactic: lhs
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Unbundled.Hom (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : PartialOrder β
inst_7 : AddCommSemigroup β
inst_8 : Sub β
inst_9 : OrderedSub β
inst_10 : AddLeftReflectLE β
inst_11 : FunLike F α β
inst_12 : AddHomClass F α β
f : F
a b : α
h : b ≤ a
| HSub.hSub (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β)
have rw : HSub.hSub (α := β) (β := β) ((f : (a : α) → β) (a - b + b) : β) ((f : (a : α) → β) b : β)
Tactic: rw [← tsub_add_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Unbundled.Hom (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : PartialOrder β
inst_7 : AddCommSemigroup β
inst_8 : Sub β
inst_9 : OrderedSub β
inst_10 : AddLeftReflectLE β
inst_11 : FunLike F α β
inst_12 : AddHomClass F α β
f : F
a b : α
h : b ≤ a
| HSub.hSub (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) = (f : (a : α) → β) (a - b)
have rw : HSub.hSub (α := β) (β := β) ((f : (a : α) → β) (a - b + b) : β) ((f : (a : α) → β) b : β)
Tactic: lhs; rw [← tsub_add_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Unbundled.Hom (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : PartialOrder β
inst_7 : AddCommSemigroup β
inst_8 : Sub β
inst_9 : OrderedSub β
inst_10 : AddLeftReflectLE β
inst_11 : FunLike F α β
inst_12 : AddHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ HSub.hSub (α := β) (β := β) ((f : (a : α) → β) a : β) ((f : (a : α) → β) b : β) = (f : (a : α) → β) (a - b)
have conv : HSub.hSub (α := β) (β := β) ((f : (a : α) → β) (a - b + b) : β) ((f : (a : α) → β) b : β) = (f : (a : α) → β) (a - b)
Tactic: conv => lhs; rw [← tsub_add_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Unbundled.Hom (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : PartialOrder β
inst_7 : AddCommSemigroup β
inst_8 : Sub β
inst_9 : OrderedSub β
inst_10 : AddLeftReflectLE β
inst_11 : FunLike F α β
inst_12 : AddHomClass F α β
f : F
a b : α
h : b ≤ a
⊢ HSub.hSub (α := β) (β := β) ((f : (a : α) → β) (a - b + b) : β) ((f : (a : α) → β) b : β) = (f : (a : α) → β) (a - b)
have rw : HSub.hSub (β := β) (HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) (a - b) : β) ((f : (a : α) → β) b : β))
    ((f : (a : α) → β) b : β) =
  (f : (a : α) → β) (a - b)
Tactic: rw [map_add, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Unbundled.Hom (goal)
Goal:
α : Type u_1
β : Type u_2
F : Type u_3
inst : PartialOrder α
inst_1 : AddCommSemigroup α
inst_2 : ExistsAddOfLE α
inst_3 : AddLeftMono α
inst_4 : Sub α
inst_5 : OrderedSub α
inst_6 : PartialOrder β
inst_7 : AddCommSemigroup β
inst_8 : Sub β
inst_9 : OrderedSub β
inst_10 : AddLeftReflectLE β
inst_11 : FunLike F α β
inst_12 : AddHomClass F α β
f : F
a b : α
h : b ≤ a
rw :
  HSub.hSub (β := β) (HAdd.hAdd (α := β) (β := β) ((f : (a : α) → β) (a - b) : β) ((f : (a : α) → β) b : β))
      ((f : (a : α) → β) b : β) =
    (f : (a : α) → β) (a - b)
⊢ HSub.hSub (α := β) (β := β) ((f : (a : α) → β) (a - b + b) : β) ((f : (a : α) → β) b : β) = (f : (a : α) → β) (a - b)
have rw₁ : Eq.{u_2 + 1} (α := β) ((f : (a : α) → β) (a - b) : β) ((f : (a : α) → β) (a - b) : β)
Tactic: rw [map_add, add_tsub_cancel_right]
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Unbundled.Hom (goal)
Goal:
M : Type u_3
N : Type u_4
inst : Preorder M
inst_1 : Add M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : PartialOrder N
inst_5 : Add N
inst_6 : Sub N
inst_7 : OrderedSub N
e : M ≃o N
h_add :
  ∀ (a b : M),
    (e : (a : M) → N) (a + b) = HAdd.hAdd (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)
a b : M
e_add : M ≃+ N :=
  { toEquiv := e.toEquiv (r := fun (x1 x2 : M) ↦ x1 ≤ x2) (s := fun (x1 x2 : N) ↦ x1 ≤ x2), map_add' := h_add }
⊢ (e : (a : M) → N) (a - b) = HSub.hSub (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)
have refine : (e : (a : M) → N) (a - b) ≤ HSub.hSub (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)
Tactic: refine le_antisymm ?_ (e_add.toAddHom.le_map_tsub e.monotone a b)
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.Unbundled.Hom (goal)
Goal:
M : Type u_3
N : Type u_4
inst : Preorder M
inst_1 : Add M
inst_2 : Sub M
inst_3 : OrderedSub M
inst_4 : PartialOrder N
inst_5 : Add N
inst_6 : Sub N
inst_7 : OrderedSub N
e : M ≃o N
h_add :
  ∀ (a b : M),
    (e : (a : M) → N) (a + b) = HAdd.hAdd (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)
a b : M
e_add : M ≃+ N :=
  { toEquiv := e.toEquiv (r := fun (x1 x2 : M) ↦ x1 ≤ x2) (s := fun (x1 x2 : N) ↦ x1 ≤ x2), map_add' := h_add }
⊢ (e : (a : M) → N) (a - b) ≤ HSub.hSub (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)
have suffices : LE.le.{u_4} (α := N)
  ((e : (a : M) → N)
      (HSub.hSub (α := M) (β := M) ((e.symm : (a : N) → M) ((e : (a : M) → N) a : N) : M)
        ((e.symm : (a : N) → M) ((e : (a : M) → N) b : N) : M)) :
    N)
  ((e : (a : M) → N)
      ((e.symm : (a : N) → M) (HSub.hSub (α := N) (β := N) ((e : (a : M) → N) a : N) ((e : (a : M) → N) b : N)) : M) :
    N)
Tactic: suffices e (e.symm (e a) - e.symm (e b)) ≤ e (e.symm (e a - e b)) by simpa
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
a : WithTop α
⊢ a - ⊤ = (↑⊥ : WithTop α)
have top : HSub.hSub (α := WithTop α) ⊤ ⊤ = (↑⊥ : WithTop α)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
a : WithTop α
top : HSub.hSub (α := WithTop α) ⊤ ⊤ = (↑⊥ : WithTop α)
⊢ a - ⊤ = (↑⊥ : WithTop α)
have coe : ∀ (a : α), (↑a : WithTop α) - ⊤ = (↑⊥ : WithTop α)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
a b : WithTop α
⊢ a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤
have top : ⊤ - b = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ b ≠ ⊤
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
a b : WithTop α
top : ⊤ - b = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ b ≠ ⊤
⊢ a - b = ⊤ ↔ a = ⊤ ∧ b ≠ ⊤
have coe : ∀ (a : α), (↑a : WithTop α) - b = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ b ≠ ⊤
Tactic: induction a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
b : WithTop α
⊢ ⊤ - b = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ b ≠ ⊤
have top : HSub.hSub (α := WithTop α) ⊤ ⊤ = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ Ne.{u_1 + 1} (α := WithTop α) ⊤ ⊤
Tactic: induction b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
b : WithTop α
top : HSub.hSub (α := WithTop α) ⊤ ⊤ = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ Ne.{u_1 + 1} (α := WithTop α) ⊤ ⊤
⊢ ⊤ - b = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ b ≠ ⊤
have top₁ : ∀ (a : α), ⊤ - (↑a : WithTop α) = ⊤ ↔ Eq.{u_1 + 1} (α := WithTop α) ⊤ ⊤ ∧ (↑a : WithTop α) ≠ ⊤
Tactic: induction b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
b : WithTop α
a : α
⊢ (↑a : WithTop α) - b = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ b ≠ ⊤
have coe : (↑a : WithTop α) - ⊤ = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ Ne.{u_1 + 1} (α := WithTop α) ⊤ ⊤
Tactic: induction b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
inst : Sub α
inst_1 : Bot α
b : WithTop α
a : α
coe : (↑a : WithTop α) - ⊤ = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ Ne.{u_1 + 1} (α := WithTop α) ⊤ ⊤
⊢ (↑a : WithTop α) - b = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ b ≠ ⊤
have coe₁ : ∀ (a_1 : α), (↑a : WithTop α) - (↑a_1 : WithTop α) = ⊤ ↔ (↑a : WithTop α) = ⊤ ∧ (↑a_1 : WithTop α) ≠ ⊤
Tactic: induction b
Cleared hypotheses: b
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
⊢ OrderedSub.{u_1} (WithTop α)
have tsub_le_iff_right : ∀ (a b c : WithTop α), a - b ≤ c ↔ a ≤ c + b
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
x y z : WithTop α
⊢ x - y ≤ z ↔ x ≤ z + y
have tsub_le_iff_right : x - ⊤ ≤ z ↔ x ≤ z + ⊤
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
x y z : WithTop α
tsub_le_iff_right : x - ⊤ ≤ z ↔ x ≤ z + ⊤
⊢ x - y ≤ z ↔ x ≤ z + y
have tsub_le_iff_right₁ : ∀ (a : α), x - (↑a : WithTop α) ≤ z ↔ x ≤ z + (↑a : WithTop α)
Tactic: cases y
Cleared hypotheses: y
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
x z : WithTop α
⊢ x - ⊤ ≤ z ↔ x ≤ z + ⊤
have tsub_le_iff_right : x - ⊤ ≤ ⊤ ↔ x ≤ HAdd.hAdd (α := WithTop α) ⊤ ⊤
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
x z : WithTop α
tsub_le_iff_right : x - ⊤ ≤ ⊤ ↔ x ≤ HAdd.hAdd (α := WithTop α) ⊤ ⊤
⊢ x - ⊤ ≤ z ↔ x ≤ z + ⊤
have tsub_le_iff_right₁ : ∀ (a : α), x - ⊤ ≤ (↑a : WithTop α) ↔ x ≤ (↑a : WithTop α) + ⊤
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
x z : WithTop α
a : α
⊢ x - (↑a : WithTop α) ≤ z ↔ x ≤ z + (↑a : WithTop α)
have tsub_le_iff_right : ⊤ - (↑a : WithTop α) ≤ z ↔ ⊤ ≤ z + (↑a : WithTop α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
x z : WithTop α
a : α
tsub_le_iff_right : ⊤ - (↑a : WithTop α) ≤ z ↔ ⊤ ≤ z + (↑a : WithTop α)
⊢ x - (↑a : WithTop α) ≤ z ↔ x ≤ z + (↑a : WithTop α)
have tsub_le_iff_right₁ : ∀ (a_1 : α), (↑a_1 : WithTop α) - (↑a : WithTop α) ≤ z ↔ (↑a_1 : WithTop α) ≤ z + (↑a : WithTop α)
Tactic: cases x
Cleared hypotheses: x
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
z : WithTop α
a a_1 : α
⊢ (↑a_1 : WithTop α) - (↑a : WithTop α) ≤ z ↔ (↑a_1 : WithTop α) ≤ z + (↑a : WithTop α)
have tsub_le_iff_right : (↑a_1 : WithTop α) - (↑a : WithTop α) ≤ ⊤ ↔ (↑a_1 : WithTop α) ≤ ⊤ + (↑a : WithTop α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
z : WithTop α
a a_1 : α
tsub_le_iff_right : (↑a_1 : WithTop α) - (↑a : WithTop α) ≤ ⊤ ↔ (↑a_1 : WithTop α) ≤ ⊤ + (↑a : WithTop α)
⊢ (↑a_1 : WithTop α) - (↑a : WithTop α) ≤ z ↔ (↑a_1 : WithTop α) ≤ z + (↑a : WithTop α)
have tsub_le_iff_right₁ : ∀ (a_2 : α),
  (↑a_1 : WithTop α) - (↑a : WithTop α) ≤ (↑a_2 : WithTop α) ↔
    (↑a_1 : WithTop α) ≤ (↑a_2 : WithTop α) + (↑a : WithTop α)
Tactic: cases z
Cleared hypotheses: z
-- Lean 4 proof step from Mathlib.Algebra.Order.Sub.WithTop (goal)
Goal:
α : Type u_1
β : Type u_2
inst : Add α
inst_1 : LE α
inst_2 : OrderBot α
inst_3 : Sub α
inst_4 : OrderedSub α
a a_1 a_2 : α
⊢ (↑a_1 : WithTop α) - (↑a : WithTop α) ≤ (↑a_2 : WithTop α) ↔
    (↑a_1 : WithTop α) ≤ (↑a_2 : WithTop α) + (↑a : WithTop α)
have tsub_le_iff_right : a_1 - a ≤ a_2 ↔ a_1 ≤ a_2 + a
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred.PartialSups (goal)
Goal:
ι : Type u_2
inst : LinearOrder ι
α : Type u_3
inst_1 : SemilatticeSup α
inst_2 : LocallyFiniteOrder ι
inst_3 : SuccOrder ι
inst_4 : OrderBot ι
f : ι → α
i : ι
⊢ (partialSups f : (a : ι) → α) (Order.succ i) = f ⊥ ⊔ (partialSups (f ∘ Order.succ) : (a : ι) → α) i
have refine : ∀ (j : ι),
  ⊥ ≤ j →
    ∀ (h : (partialSups f : (a : ι) → α) (Order.succ j) = f ⊥ ⊔ (partialSups (f ∘ Order.succ) : (a : ι) → α) j),
      (partialSups f : (a : ι) → α) (Order.succ (Order.succ j)) =
        f ⊥ ⊔ (partialSups (f ∘ Order.succ) : (a : ι) → α) (Order.succ j)
Tactic: refine Succ.rec (by simp) (fun j _ h ↦ ?_) (bot_le (a := i))
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred.PartialSups (hypothesis)
Goal:
ι : Type u_2
inst : LinearOrder ι
α : Type u_3
inst_1 : SemilatticeSup α
inst_2 : LocallyFiniteOrder ι
inst_3 : SuccOrder ι
inst_4 : OrderBot ι
f : ι → α
i j : ι
h_1 : ⊥ ≤ j
h : (partialSups f : (a : ι) → α) (Order.succ j) = f ⊥ ⊔ (partialSups (f ∘ Order.succ) : (a : ι) → α) j
⊢ (partialSups f : (a : ι) → α) (Order.succ (Order.succ j)) =
    f ⊥ ⊔ (partialSups (f ∘ Order.succ) : (a : ι) → α) (Order.succ j)
have this : Eq.{u_3 + 1} (α := α) ((partialSups (f ∘ Order.succ) : (a : ι) → α) (Order.succ j) : α)
  ((partialSups (f ∘ Order.succ) : (a : ι) → α) j ⊔ (f ∘ Order.succ) (Order.succ j) : α)
Tactic: have : (partialSups (f ∘ Order.succ)) (Order.succ j) =
      ((partialSups (f ∘ Order.succ)) j ⊔ (f ∘ Order.succ) (Order.succ j)) := by simp
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred.WithBot (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : AddMonoidWithOne α
inst_3 : SuccAddOrder α
n : ℕ
⊢ succ (↑n : WithBot α) = HAdd.hAdd (α := α) (↑n : α) 1
have rw : succ (↑(↑n : α) : WithBot α) = HAdd.hAdd (α := α) (↑n : α) 1
Tactic: rw [← WithBot.coe_natCast, succ_coe, Order.succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred.WithBot (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : AddMonoidWithOne α
inst_3 : SuccAddOrder α
n : ℕ
rw : succ (↑(↑n : α) : WithBot α) = HAdd.hAdd (α := α) (↑n : α) 1
⊢ succ (↑n : WithBot α) = HAdd.hAdd (α := α) (↑n : α) 1
have rw₁ : Order.succ (↑n : α) = HAdd.hAdd (α := α) (↑n : α) 1
Tactic: rw [← WithBot.coe_natCast, succ_coe, Order.succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred.WithBot (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : OrderBot α
inst_2 : AddMonoidWithOne α
inst_3 : SuccAddOrder α
n : ℕ
rw : succ (↑(↑n : α) : WithBot α) = HAdd.hAdd (α := α) (↑n : α) 1
rw₁ : Order.succ (↑n : α) = HAdd.hAdd (α := α) (↑n : α) 1
⊢ succ (↑n : WithBot α) = HAdd.hAdd (α := α) (↑n : α) 1
have rw₂ : HAdd.hAdd (α := α) (↑n : α) 1 = HAdd.hAdd (α := α) (↑n : α) 1
Tactic: rw [← WithBot.coe_natCast, succ_coe, Order.succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred.WithBot (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_2} (R := α) 1
inst_4 : SuccAddOrder α
a : WithBot α
⊢ 1 ≤ a ↔ 0 < a
have bot : LE.le.{u_2} (α := WithBot α) 1 ⊥ ↔ LT.lt.{u_2} (α := WithBot α) 0 ⊥
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred.WithBot (goal)
Goal:
α : Type u_2
inst : PartialOrder α
inst_1 : AddMonoidWithOne α
inst_2 : ZeroLEOneClass α
inst_3 : NeZero.{u_2} (R := α) 1
inst_4 : SuccAddOrder α
a : WithBot α
bot : LE.le.{u_2} (α := WithBot α) 1 ⊥ ↔ LT.lt.{u_2} (α := WithBot α) 0 ⊥
⊢ 1 ≤ a ↔ 0 < a
have coe : ∀ (a : α), 1 ≤ (↑a : WithBot α) ↔ 0 < (↑a : WithBot α)
Tactic: cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x y : α
inst : Preorder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
h : x < y
⊢ x + 1 ≤ y
have rw : 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 : Preorder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
hx : ¬IsMax x
⊢ x + 1 ≤ y ↔ x < y
have rw : succ x ≤ y ↔ x < y
Tactic: rw [← succ_eq_add_one, succ_le_iff_of_not_isMax hx]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x y : α
inst : Preorder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
hx : ¬IsMax x
rw : succ x ≤ y ↔ x < y
⊢ x + 1 ≤ y ↔ x < y
have rw₁ : x < y ↔ x < y
Tactic: rw [← succ_eq_add_one, succ_le_iff_of_not_isMax hx]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
x : α
⊢ x ⩿ x + 1
have rw : x ⩿ succ x
Tactic: rw [← succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Add α
inst_2 : One α
inst_3 : SuccAddOrder α
inst_4 : NoMaxOrder α
x : α
⊢ x ⋖ x + 1
have rw : x ⋖ succ x
Tactic: rw [← succ_eq_add_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x y : α
inst : Preorder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
h : 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 : Preorder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
hy : ¬IsMin y
⊢ x ≤ y - 1 ↔ x < y
have rw : x ≤ pred y ↔ x < y
Tactic: rw [← pred_eq_sub_one, le_pred_iff_of_not_isMin hy]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
x y : α
inst : Preorder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
hy : ¬IsMin y
rw : x ≤ pred y ↔ x < y
⊢ x ≤ y - 1 ↔ x < y
have rw₁ : x < y ↔ x < y
Tactic: rw [← pred_eq_sub_one, le_pred_iff_of_not_isMin hy]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
x : α
⊢ x - 1 ⩿ x
have rw : pred x ⩿ x
Tactic: rw [← pred_eq_sub_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : Sub α
inst_2 : One α
inst_3 : PredSubOrder α
inst_4 : NoMinOrder α
x : α
⊢ x - 1 ⋖ x
have rw : pred x ⋖ x
Tactic: rw [← pred_eq_sub_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
x : α
⊢ succ^[0] x = x + (↑0 : α)
have zero : x = x + (↑0 : α)
Tactic: rw [Function.iterate_zero_apply, Nat.cast_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
x : α
zero : x = x + (↑0 : α)
⊢ succ^[0] x = x + (↑0 : α)
have zero₁ : x = x + 0
Tactic: rw [Function.iterate_zero_apply, Nat.cast_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
x : α
zero : x = x + (↑0 : α)
zero₁ : x = x + 0
⊢ succ^[0] x = x + (↑0 : α)
have zero₂ : x = x
Tactic: rw [Function.iterate_zero_apply, Nat.cast_zero, add_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
x : α
n : ℕ
IH : succ^[n] x = x + (↑n : α)
⊢ succ^[n + 1] x = x + (↑(n + 1) : α)
have succ : succ (succ^[n] x) = x + (↑(n + 1) : α)
Tactic: rw [Function.iterate_succ_apply', IH, Nat.cast_add, succ_eq_add_one, Nat.cast_one, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
x : α
n : ℕ
IH : Order.succ^[n] x = x + (↑n : α)
succ : Order.succ (Order.succ^[n] x) = x + (↑(n + 1) : α)
⊢ Order.succ^[n + 1] x = x + (↑(n + 1) : α)
have succ₁ : Order.succ (x + (↑n : α)) = x + (↑(n + 1) : α)
Tactic: rw [Function.iterate_succ_apply', IH, Nat.cast_add, succ_eq_add_one, Nat.cast_one, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
x : α
n : ℕ
IH : Order.succ^[n] x = x + (↑n : α)
succ : Order.succ (Order.succ^[n] x) = x + (↑(n + 1) : α)
succ₁ : Order.succ (x + (↑n : α)) = x + (↑(n + 1) : α)
⊢ Order.succ^[n + 1] x = x + (↑(n + 1) : α)
have succ₂ : Order.succ (x + (↑n : α)) = x + HAdd.hAdd (α := α) (↑n : α) (↑1 : α)
Tactic: rw [Function.iterate_succ_apply', IH, Nat.cast_add, succ_eq_add_one, Nat.cast_one, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
x : α
n : ℕ
IH : Order.succ^[n] x = x + (↑n : α)
succ : Order.succ (Order.succ^[n] x) = x + (↑(n + 1) : α)
succ₁ : Order.succ (x + (↑n : α)) = x + (↑(n + 1) : α)
succ₂ : Order.succ (x + (↑n : α)) = x + HAdd.hAdd (α := α) (↑n : α) (↑1 : α)
⊢ Order.succ^[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, succ_eq_add_one, Nat.cast_one, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
x : α
n : ℕ
IH : Order.succ^[n] x = x + (↑n : α)
succ : Order.succ (Order.succ^[n] x) = x + (↑(n + 1) : α)
succ₁ : Order.succ (x + (↑n : α)) = x + (↑(n + 1) : α)
succ₂ : Order.succ (x + (↑n : α)) = x + HAdd.hAdd (α := α) (↑n : α) (↑1 : α)
succ₃ : x + (↑n : α) + 1 = x + HAdd.hAdd (α := α) (↑n : α) (↑1 : α)
⊢ Order.succ^[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, succ_eq_add_one, Nat.cast_one, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
x : α
n : ℕ
IH : Order.succ^[n] x = x + (↑n : α)
succ : Order.succ (Order.succ^[n] x) = x + (↑(n + 1) : α)
succ₁ : Order.succ (x + (↑n : α)) = x + (↑(n + 1) : α)
succ₂ : Order.succ (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
⊢ Order.succ^[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, succ_eq_add_one, Nat.cast_one, add_assoc]
-- Lean 4 proof step from Mathlib.Algebra.Order.SuccPred (goal)
Goal:
α : Type u_1
inst : Preorder α
inst_1 : AddMonoidWithOne α
inst_2 : SuccAddOrder α
x : α
n : ℕ
⊢ succ^[n] x = x + (↑n : α)
have zero : succ^[0] x = x + (↑0 : α)
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