awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Div (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → FloorDiv.{u_2, u_4} α (π i)
a : α
ha : a ≤ 0
f : (i : ι) → π i
⊢ Eq (α := (i : ι) → π i) (fun (i : ι) ↦ @FloorDiv.floorDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (f i) a)
    0
have h : ∀ (i : ι), @FloorDiv.floorDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (f i) a = 0 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Div (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → FloorDiv.{u_2, u_4} α (π i)
a : α
⊢ Eq (α := (i : ι) → π i) (fun (i : ι) ↦ @FloorDiv.floorDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (0 i) a)
    0
have h : ∀ (i : ι), Eq.{u_4 + 1} (α := π i) (@FloorDiv.floorDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (0 i) a) (0 i)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Div (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → CeilDiv.{u_2, u_4} α (π i)
a : α
ha : a ≤ 0
f : (i : ι) → π i
⊢ Eq (α := (i : ι) → π i) (fun (i : ι) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (f i) a) 0
have h : ∀ (i : ι), @CeilDiv.ceilDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (f i) a = 0 i
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Div (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : (i : ι) → AddCommMonoid (π i)
inst_3 : (i : ι) → PartialOrder (π i)
inst_4 : (i : ι) → SMulZeroClass.{u_2, u_4} α (π i)
inst_5 : (i : ι) → CeilDiv.{u_2, u_4} α (π i)
a : α
⊢ Eq (α := (i : ι) → π i) (fun (i : ι) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 (inst_2 i) (inst_3 i) (inst_4 i) _ (0 i) a) 0
have h : ∀ (x : ι), Eq.{u_4 + 1} (α := π x) (@CeilDiv.ceilDiv _ _ inst inst_1 (inst_2 x) (inst_3 x) (inst_4 x) _ (0 x) a) (0 x)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Div (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : FloorDiv α β
f_1 : ι →₀ β
a_1 a : α
ha : a ≤ 0
f : ι →₀ β
⊢ Eq (α := ι →₀ β) (mapRange (fun (x : β) ↦ @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ f) 0
have h : ∀ (i : ι),
  Eq.{u_3 + 1} (α := β)
    ((mapRange (fun (x : β) ↦ @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) sorry f : (a : ι) → β) i : β)
    ((0 : (a : ι) → β) i : β)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Div (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : FloorDiv α β
f : ι →₀ β
a_1 a : α
⊢ Eq (α := ι →₀ β) (mapRange (fun (x : β) ↦ @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ 0) 0
have h : ∀ (a_2 : ι),
  Eq.{u_3 + 1} (α := β)
    ((mapRange (fun (x : β) ↦ @FloorDiv.floorDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) sorry 0 : (a : ι) → β) a_2 : β)
    ((0 : (a : ι) → β) a_2 : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Div (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
f_1 : ι →₀ β
a_1 a : α
ha : a ≤ 0
f : ι →₀ β
⊢ Eq (α := ι →₀ β) (mapRange (fun (x : β) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ f) 0
have h : ∀ (i : ι),
  Eq.{u_3 + 1} (α := β)
    ((mapRange (fun (x : β) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) sorry f : (a : ι) → β) i : β)
    ((0 : (a : ι) → β) i : β)
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Div (goal)
Goal:
ι : Type u_1
α : Type u_2
β : Type u_3
inst : AddCommMonoid α
inst_1 : PartialOrder α
inst_2 : AddCommMonoid β
inst_3 : PartialOrder β
inst_4 : SMulZeroClass α β
inst_5 : CeilDiv α β
f : ι →₀ β
a_1 a : α
⊢ Eq (α := ι →₀ β) (mapRange (fun (x : β) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) ⋯ 0) 0
have h : ∀ (a_2 : ι),
  Eq.{u_3 + 1} (α := β)
    ((mapRange (fun (x : β) ↦ @CeilDiv.ceilDiv _ _ inst inst_1 inst_2 inst_3 inst_4 _ x a) sorry 0 : (a : ι) → β) a_2 : β)
    ((0 : (a : ι) → β) a_2 : β)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0∞
⊢ ⌊r⌋ₑ = ⊤ ↔ r = ∞
have top : ⌊∞⌋ₑ = ⊤ ↔ Eq (α := ℝ≥0∞) ∞ ∞
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0∞
top : ⌊∞⌋ₑ = ⊤ ↔ Eq (α := ℝ≥0∞) ∞ ∞
⊢ ⌊r⌋ₑ = ⊤ ↔ r = ∞
have coe : ∀ (x : ℝ≥0), ⌊(↑x : ℝ≥0∞)⌋ₑ = ⊤ ↔ (↑x : ℝ≥0∞) = ∞
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0∞
⊢ ⌈r⌉ₑ = ⊤ ↔ r = ∞
have top : ⌈∞⌉ₑ = ⊤ ↔ Eq (α := ℝ≥0∞) ∞ ∞
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0∞
top : ⌈∞⌉ₑ = ⊤ ↔ Eq (α := ℝ≥0∞) ∞ ∞
⊢ ⌈r⌉ₑ = ⊤ ↔ r = ∞
have coe : ∀ (x : ℝ≥0), ⌈(↑x : ℝ≥0∞)⌉ₑ = ⊤ ↔ (↑x : ℝ≥0∞) = ∞
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0∞
⊢ ⌊r⌋ₑ < ⊤ ↔ r < ∞
have top : ⌊∞⌋ₑ < ⊤ ↔ LT.lt (α := ℝ≥0∞) ∞ ∞
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0∞
top : ⌊∞⌋ₑ < ⊤ ↔ LT.lt (α := ℝ≥0∞) ∞ ∞
⊢ ⌊r⌋ₑ < ⊤ ↔ r < ∞
have coe : ∀ (x : ℝ≥0), ⌊(↑x : ℝ≥0∞)⌋ₑ < ⊤ ↔ (↑x : ℝ≥0∞) < ∞
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0∞
⊢ ⌈r⌉ₑ < ⊤ ↔ r < ∞
have top : ⌈∞⌉ₑ < ⊤ ↔ LT.lt (α := ℝ≥0∞) ∞ ∞
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0∞
top : ⌈∞⌉ₑ < ⊤ ↔ LT.lt (α := ℝ≥0∞) ∞ ∞
⊢ ⌈r⌉ₑ < ⊤ ↔ r < ∞
have coe : ∀ (x : ℝ≥0), ⌈(↑x : ℝ≥0∞)⌉ₑ < ⊤ ↔ (↑x : ℝ≥0∞) < ∞
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0∞
n : ℕ∞
⊢ n ≤ ⌊r⌋ₑ ↔ (↑n : ℝ≥0∞) ≤ r
have top : n ≤ ⌊∞⌋ₑ ↔ (↑n : ℝ≥0∞) ≤ ∞
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0∞
n : ℕ∞
top : n ≤ ⌊∞⌋ₑ ↔ (↑n : ℝ≥0∞) ≤ ∞
⊢ n ≤ ⌊r⌋ₑ ↔ (↑n : ℝ≥0∞) ≤ r
have coe : ∀ (x : ℝ≥0), n ≤ ⌊(↑x : ℝ≥0∞)⌋ₑ ↔ (↑n : ℝ≥0∞) ≤ (↑x : ℝ≥0∞)
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
n : ℕ∞
⊢ n ≤ ⌊∞⌋ₑ ↔ (↑n : ℝ≥0∞) ≤ ∞
have top : ⊤ ≤ ⌊∞⌋ₑ ↔ (↑⊤ : ℝ≥0∞) ≤ ∞
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
n : ℕ∞
top : ⊤ ≤ ⌊∞⌋ₑ ↔ (↑⊤ : ℝ≥0∞) ≤ ∞
⊢ n ≤ ⌊∞⌋ₑ ↔ (↑n : ℝ≥0∞) ≤ ∞
have top₁ : ∀ (a : ℕ), (↑a : ℕ∞) ≤ ⌊∞⌋ₑ ↔ (↑(↑a : ℕ∞) : ℝ≥0∞) ≤ ∞
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
n : ℕ∞
x : ℝ≥0
⊢ n ≤ ⌊(↑x : ℝ≥0∞)⌋ₑ ↔ (↑n : ℝ≥0∞) ≤ (↑x : ℝ≥0∞)
have coe : ⊤ ≤ ⌊(↑x : ℝ≥0∞)⌋ₑ ↔ (↑⊤ : ℝ≥0∞) ≤ (↑x : ℝ≥0∞)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
n : ℕ∞
x : ℝ≥0
coe : ⊤ ≤ ⌊(↑x : ℝ≥0∞)⌋ₑ ↔ (↑⊤ : ℝ≥0∞) ≤ (↑x : ℝ≥0∞)
⊢ n ≤ ⌊(↑x : ℝ≥0∞)⌋ₑ ↔ (↑n : ℝ≥0∞) ≤ (↑x : ℝ≥0∞)
have coe₁ : ∀ (a : ℕ), (↑a : ℕ∞) ≤ ⌊(↑x : ℝ≥0∞)⌋ₑ ↔ (↑(↑a : ℕ∞) : ℝ≥0∞) ≤ (↑x : ℝ≥0∞)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0∞
n : ℕ∞
⊢ ⌈r⌉ₑ ≤ n ↔ r ≤ (↑n : ℝ≥0∞)
have top : ⌈∞⌉ₑ ≤ n ↔ ∞ ≤ (↑n : ℝ≥0∞)
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0∞
n : ℕ∞
top : ⌈∞⌉ₑ ≤ n ↔ ∞ ≤ (↑n : ℝ≥0∞)
⊢ ⌈r⌉ₑ ≤ n ↔ r ≤ (↑n : ℝ≥0∞)
have coe : ∀ (x : ℝ≥0), ⌈(↑x : ℝ≥0∞)⌉ₑ ≤ n ↔ (↑x : ℝ≥0∞) ≤ (↑n : ℝ≥0∞)
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
n : ℕ∞
⊢ ⌈∞⌉ₑ ≤ n ↔ ∞ ≤ (↑n : ℝ≥0∞)
have top : ⌈∞⌉ₑ ≤ ⊤ ↔ ∞ ≤ (↑⊤ : ℝ≥0∞)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
n : ℕ∞
top : ⌈∞⌉ₑ ≤ ⊤ ↔ ∞ ≤ (↑⊤ : ℝ≥0∞)
⊢ ⌈∞⌉ₑ ≤ n ↔ ∞ ≤ (↑n : ℝ≥0∞)
have top₁ : ∀ (a : ℕ), ⌈∞⌉ₑ ≤ (↑a : ℕ∞) ↔ ∞ ≤ (↑(↑a : ℕ∞) : ℝ≥0∞)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
n : ℕ∞
x : ℝ≥0
⊢ ⌈(↑x : ℝ≥0∞)⌉ₑ ≤ n ↔ (↑x : ℝ≥0∞) ≤ (↑n : ℝ≥0∞)
have coe : ⌈(↑x : ℝ≥0∞)⌉ₑ ≤ ⊤ ↔ (↑x : ℝ≥0∞) ≤ (↑⊤ : ℝ≥0∞)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
n : ℕ∞
x : ℝ≥0
coe : ⌈(↑x : ℝ≥0∞)⌉ₑ ≤ ⊤ ↔ (↑x : ℝ≥0∞) ≤ (↑⊤ : ℝ≥0∞)
⊢ ⌈(↑x : ℝ≥0∞)⌉ₑ ≤ n ↔ (↑x : ℝ≥0∞) ≤ (↑n : ℝ≥0∞)
have coe₁ : ∀ (a : ℕ), ⌈(↑x : ℝ≥0∞)⌉ₑ ≤ (↑a : ℕ∞) ↔ (↑x : ℝ≥0∞) ≤ (↑(↑a : ℕ∞) : ℝ≥0∞)
Tactic: cases n
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0∞
n : ℕ∞
hn₀ : n ≠ 0
hn : n ≠ ⊤
⊢ n ≤ ⌈r⌉ₑ ↔ (↑n : ℝ≥0∞) - 1 < r
have lift : ∀ (n : ℕ) (hn₀ : Ne (α := ℕ∞) (↑n : ℕ∞) 0), (↑n : ℕ∞) ≤ ⌈r⌉ₑ ↔ (↑(↑n : ℕ∞) : ℝ≥0∞) - 1 < r
Tactic: lift n to ℕ using hn
Cleared hypotheses: n, hn₀, hn
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0∞
n : ℕ
hn₀ : Ne (α := ℕ∞) (↑n : ℕ∞) 0
⊢ (↑n : ℕ∞) ≤ ⌈r⌉ₑ ↔ (↑(↑n : ℕ∞) : ℝ≥0∞) - 1 < r
have top : (↑n : ℕ∞) ≤ ⌈∞⌉ₑ ↔ (↑(↑n : ℕ∞) : ℝ≥0∞) - 1 < ∞
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0∞
n : ℕ
hn₀ : Ne (α := ℕ∞) (↑n : ℕ∞) 0
top : (↑n : ℕ∞) ≤ ⌈∞⌉ₑ ↔ (↑(↑n : ℕ∞) : ℝ≥0∞) - 1 < ∞
⊢ (↑n : ℕ∞) ≤ ⌈r⌉ₑ ↔ (↑(↑n : ℕ∞) : ℝ≥0∞) - 1 < r
have coe : ∀ (x : ℝ≥0), (↑n : ℕ∞) ≤ ⌈(↑x : ℝ≥0∞)⌉ₑ ↔ (↑(↑n : ℕ∞) : ℝ≥0∞) - 1 < (↑x : ℝ≥0∞)
Tactic: cases r
Cleared hypotheses: r
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
n : ℕ
hn₀ : Ne (α := ℕ∞) (↑n : ℕ∞) 0
⊢ (↑n : ℕ∞) ≤ ⌈∞⌉ₑ ↔ (↑(↑n : ℕ∞) : ℝ≥0∞) - 1 < ∞
have top : HSub.hSub (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1 < ∞
Tactic: simp only [ceil_top, le_top, toENNReal_coe, true_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
n : ℕ
hn₀ : Ne (α := ℕ∞) (↑n : ℕ∞) 0
⊢ HSub.hSub (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1 < ∞
have top : LT.lt (α := ℝ≥0∞) (↑(n - 1) : ℝ≥0∞) ∞
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
n : ℕ
hn₀ : Ne (α := ℕ∞) (↑n : ℕ∞) 0
x : ℝ≥0
⊢ (↑n : ℕ∞) ≤ ⌈(↑x : ℝ≥0∞)⌉ₑ ↔ (↑(↑n : ℕ∞) : ℝ≥0∞) - 1 < (↑x : ℝ≥0∞)
have coe : ∀ (hn₀ : ¬n = 0), n ≤ ⌈x⌉₊ ↔ HSub.hSub (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1 < (↑x : ℝ≥0∞)
Tactic: simp only [ne_eq, Nat.cast_eq_zero, ceil_coe, Nat.cast_le, toENNReal_coe] at hn₀ ⊢
Cleared hypotheses: hn₀
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
n : ℕ
x : ℝ≥0
hn₀ : ¬n = 0
⊢ n ≤ ⌈x⌉₊ ↔ HSub.hSub (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1 < (↑x : ℝ≥0∞)
have coe : n ≤ ⌈x⌉₊ ↔ (↑(n - 1) : ℝ≥0) < x
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
n : ℕ
x : ℝ≥0
hn₀ : ¬n = 0
⊢ n ≤ ⌈x⌉₊ ↔ (↑(n - 1) : ℝ≥0) < x
have coe : 1 ≤ n
Tactic: rw [← Nat.add_one_le_ceil_iff, Nat.sub_add_cancel]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0
n : ℕ
⊢ ⌊(↑(r + (↑n : ℝ≥0)) : ℝ≥0∞)⌋ₑ = (↑(⌊r⌋₊ + n) : ℕ∞)
have norm_cast : ⌊r + (↑n : ℝ≥0)⌋₊ = ⌊r⌋₊ + n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0
n : ℕ
⊢ ⌈(↑(r + (↑n : ℝ≥0)) : ℝ≥0∞)⌉ₑ = (↑(⌈r⌉₊ + n) : ℕ∞)
have norm_cast : ⌈r + (↑n : ℝ≥0)⌉₊ = ⌈r⌉₊ + n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0
n : ℕ
⊢ ⌊(↑(r - (↑n : ℝ≥0)) : ℝ≥0∞)⌋ₑ = (↑(⌊r⌋₊ - n) : ℕ∞)
have norm_cast : ⌊r - (↑n : ℝ≥0)⌋₊ = ⌊r⌋₊ - n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0
n : ℕ
⊢ ⌈(↑(r - (↑n : ℝ≥0)) : ℝ≥0∞)⌉ₑ = (↑(⌈r⌉₊ - n) : ℕ∞)
have norm_cast : ⌈r - (↑n : ℝ≥0)⌉₊ = ⌈r⌉₊ - n
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
r : ℝ≥0∞
hr : r ≠ ∞
⊢ (↑⌈r⌉ₑ : ℝ≥0∞) < r + 1
have lift : ∀ (r : ℝ≥0), (↑⌈(↑r : ℝ≥0∞)⌉ₑ : ℝ≥0∞) < (↑r : ℝ≥0∞) + 1
Tactic: lift r to ℝ≥0 using hr
Cleared hypotheses: r, hr
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
a : ℝ≥0∞
⊢ toENNReal ⁻¹' Ioi a = Ioi ⌊a⌋ₑ
have h : ∀ (x : ℕ∞), x ∈ toENNReal ⁻¹' Ioi a ↔ x ∈ Ioi ⌊a⌋ₑ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
a : ℝ≥0∞
⊢ toENNReal ⁻¹' Iio a = Iio ⌈a⌉ₑ
have h : ∀ (x : ℕ∞), x ∈ toENNReal ⁻¹' Iio a ↔ x ∈ Iio ⌈a⌉ₑ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
a : ℝ≥0∞
⊢ toENNReal ⁻¹' Iic a = Iic ⌊a⌋ₑ
have h : ∀ (x : ℕ∞), x ∈ toENNReal ⁻¹' Iic a ↔ x ∈ Iic ⌊a⌋ₑ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
a : ℝ≥0∞
⊢ toENNReal ⁻¹' Ici a = Ici ⌈a⌉ₑ
have h : ∀ (x : ℕ∞), x ∈ toENNReal ⁻¹' Ici a ↔ x ∈ Ici ⌈a⌉ₑ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
a b : ℝ≥0∞
⊢ toENNReal ⁻¹' Icc a b = Icc ⌈a⌉ₑ ⌊b⌋ₑ
have h : ∀ (x : ℕ∞), x ∈ toENNReal ⁻¹' Icc a b ↔ x ∈ Icc ⌈a⌉ₑ ⌊b⌋ₑ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
a b : ℝ≥0∞
⊢ toENNReal ⁻¹' Ico a b = Ico ⌈a⌉ₑ ⌈b⌉ₑ
have h : ∀ (x : ℕ∞), x ∈ toENNReal ⁻¹' Ico a b ↔ x ∈ Ico ⌈a⌉ₑ ⌈b⌉ₑ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
a b : ℝ≥0∞
⊢ toENNReal ⁻¹' Ioc a b = Ioc ⌊a⌋ₑ ⌊b⌋ₑ
have h : ∀ (x : ℕ∞), x ∈ toENNReal ⁻¹' Ioc a b ↔ x ∈ Ioc ⌊a⌋ₑ ⌊b⌋ₑ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Extended (goal)
Goal:
a b : ℝ≥0∞
⊢ toENNReal ⁻¹' Ioo a b = Ioo ⌊a⌋ₑ ⌈b⌉ₑ
have h : ∀ (x : ℕ∞), x ∈ toENNReal ⁻¹' Ioo a b ↔ x ∈ Ioo ⌊a⌋ₑ ⌈b⌉ₑ
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
⊢ ⌊a⌋ ≤ z ↔ a < HAdd.hAdd (α := R) (↑z : R) 1
have rw : a < (↑(z + 1) : R) ↔ a < HAdd.hAdd (α := R) (↑z : R) 1
Tactic: rw [← lt_add_one_iff, floor_lt]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
⊢ a < (↑(z + 1) : R) ↔ a < HAdd.hAdd (α := R) (↑z : R) 1
have norm_cast : a < (↑(z + 1) : R) ↔ a < (↑(z + 1) : R)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
⊢ z < ⌊a⌋ ↔ HAdd.hAdd (α := R) (↑z : R) 1 ≤ a
have rw : (↑(z + 1) : R) ≤ a ↔ HAdd.hAdd (α := R) (↑z : R) 1 ≤ a
Tactic: rw [← add_one_le_iff, le_floor]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
⊢ (↑(z + 1) : R) ≤ a ↔ HAdd.hAdd (α := R) (↑z : R) 1 ≤ a
have norm_cast : (↑(z + 1) : R) ≤ a ↔ (↑(z + 1) : R) ≤ a
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
⊢ ⌊a⌋ ≤ z - 1 ↔ a < (↑z : R)
have rw : ⌊a⌋ ≤ z - 1 ↔ ⌊a⌋ < z
Tactic: rw [← floor_lt, le_sub_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : ⌊a⌋ ≤ z - 1 ↔ ⌊a⌋ < z
⊢ ⌊a⌋ ≤ z - 1 ↔ a < (↑z : R)
have rw₁ : ⌊a⌋ < z ↔ ⌊a⌋ < z
Tactic: rw [← floor_lt, le_sub_one_iff]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
⊢ 0 < ⌊a⌋ ↔ 1 ≤ a
have rw : HAdd.hAdd (α := ℤ) 0 1 ≤ ⌊a⌋ ↔ 1 ≤ a
Tactic: rw [Int.lt_iff_add_one_le, zero_add, le_floor, cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
rw : HAdd.hAdd (α := ℤ) 0 1 ≤ ⌊a⌋ ↔ 1 ≤ a
⊢ 0 < ⌊a⌋ ↔ 1 ≤ a
have rw₁ : 1 ≤ ⌊a⌋ ↔ 1 ≤ a
Tactic: rw [Int.lt_iff_add_one_le, zero_add, le_floor, cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
rw : HAdd.hAdd (α := ℤ) 0 1 ≤ ⌊a⌋ ↔ 1 ≤ a
rw₁ : 1 ≤ ⌊a⌋ ↔ 1 ≤ a
⊢ 0 < ⌊a⌋ ↔ 1 ≤ a
have rw₂ : (↑1 : R) ≤ a ↔ 1 ≤ a
Tactic: rw [Int.lt_iff_add_one_le, zero_add, le_floor, cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
a : R
rw : HAdd.hAdd (α := ℤ) 0 1 ≤ ⌊a⌋ ↔ 1 ≤ a
rw₁ : 1 ≤ ⌊a⌋ ↔ 1 ≤ a
rw₂ : (↑1 : R) ≤ a ↔ 1 ≤ a
⊢ 0 < ⌊a⌋ ↔ 1 ≤ a
have rw₃ : 1 ≤ a ↔ 1 ≤ a
Tactic: rw [Int.lt_iff_add_one_le, zero_add, le_floor, cast_one]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
⊢ ⌊a⌋ = z ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
have rw : ⌊a⌋ ≤ z ∧ z ≤ ⌊a⌋ ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
Tactic: rw [le_antisymm_iff, le_floor, ← Int.lt_add_one_iff, floor_lt, Int.cast_add, Int.cast_one,
    and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : ⌊a⌋ ≤ z ∧ z ≤ ⌊a⌋ ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
⊢ ⌊a⌋ = z ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
have rw₁ : ⌊a⌋ ≤ z ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
Tactic: rw [le_antisymm_iff, le_floor, ← Int.lt_add_one_iff, floor_lt, Int.cast_add, Int.cast_one,
    and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : ⌊a⌋ ≤ z ∧ z ≤ ⌊a⌋ ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₁ : ⌊a⌋ ≤ z ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
⊢ ⌊a⌋ = z ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
have rw₂ : ⌊a⌋ < z + 1 ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
Tactic: rw [le_antisymm_iff, le_floor, ← Int.lt_add_one_iff, floor_lt, Int.cast_add, Int.cast_one,
    and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : ⌊a⌋ ≤ z ∧ z ≤ ⌊a⌋ ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₁ : ⌊a⌋ ≤ z ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₂ : ⌊a⌋ < z + 1 ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
⊢ ⌊a⌋ = z ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
have rw₃ : a < (↑(z + 1) : R) ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
Tactic: rw [le_antisymm_iff, le_floor, ← Int.lt_add_one_iff, floor_lt, Int.cast_add, Int.cast_one,
    and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : ⌊a⌋ ≤ z ∧ z ≤ ⌊a⌋ ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₁ : ⌊a⌋ ≤ z ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₂ : ⌊a⌋ < z + 1 ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₃ : a < (↑(z + 1) : R) ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
⊢ ⌊a⌋ = z ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
have rw₄ : a < HAdd.hAdd (α := R) (↑z : R) (↑1 : R) ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
Tactic: rw [le_antisymm_iff, le_floor, ← Int.lt_add_one_iff, floor_lt, Int.cast_add, Int.cast_one,
    and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : ⌊a⌋ ≤ z ∧ z ≤ ⌊a⌋ ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₁ : ⌊a⌋ ≤ z ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₂ : ⌊a⌋ < z + 1 ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₃ : a < (↑(z + 1) : R) ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₄ : a < HAdd.hAdd (α := R) (↑z : R) (↑1 : R) ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
⊢ ⌊a⌋ = z ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
have rw₅ : a < HAdd.hAdd (α := R) (↑z : R) 1 ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
Tactic: rw [le_antisymm_iff, le_floor, ← Int.lt_add_one_iff, floor_lt, Int.cast_add, Int.cast_one,
    and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
z : ℤ
a : R
rw : ⌊a⌋ ≤ z ∧ z ≤ ⌊a⌋ ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₁ : ⌊a⌋ ≤ z ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₂ : ⌊a⌋ < z + 1 ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₃ : a < (↑(z + 1) : R) ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₄ : a < HAdd.hAdd (α := R) (↑z : R) (↑1 : R) ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
rw₅ : a < HAdd.hAdd (α := R) (↑z : R) 1 ∧ (↑z : R) ≤ a ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
⊢ ⌊a⌋ = z ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
have rw₆ : (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1 ↔ (↑z : R) ≤ a ∧ a < HAdd.hAdd (α := R) (↑z : R) 1
Tactic: rw [le_antisymm_iff, le_floor, ← Int.lt_add_one_iff, floor_lt, Int.cast_add, Int.cast_one,
    and_comm]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
z a : ℤ
⊢ a ≤ floor.{u_2} (α := R) (↑z : R) ↔ a ≤ z
have rw : LE.le.{u_2} (α := R) (↑a : R) (↑z : R) ↔ a ≤ z
Tactic: rw [le_floor, Int.cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
z a : ℤ
rw : LE.le.{u_2} (α := R) (↑a : R) (↑z : R) ↔ a ≤ z
⊢ a ≤ floor.{u_2} (α := R) (↑z : R) ↔ a ≤ z
have rw₁ : a ≤ z ↔ a ≤ z
Tactic: rw [le_floor, Int.cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
n : ℕ
a : ℤ
⊢ a ≤ floor.{u_2} (α := R) (↑n : R) ↔ a ≤ (↑n : ℤ)
have rw : LE.le.{u_2} (α := R) (↑a : R) (↑n : R) ↔ a ≤ (↑n : ℤ)
Tactic: rw [le_floor, ← cast_natCast, cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
n : ℕ
a : ℤ
rw : LE.le.{u_2} (α := R) (↑a : R) (↑n : R) ↔ a ≤ (↑n : ℤ)
⊢ a ≤ floor.{u_2} (α := R) (↑n : R) ↔ a ≤ (↑n : ℤ)
have rw₁ : LE.le.{u_2} (α := R) (↑a : R) (↑(↑n : ℤ) : R) ↔ a ≤ (↑n : ℤ)
Tactic: rw [le_floor, ← cast_natCast, cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
n : ℕ
a : ℤ
rw : LE.le.{u_2} (α := R) (↑a : R) (↑n : R) ↔ a ≤ (↑n : ℤ)
rw₁ : LE.le.{u_2} (α := R) (↑a : R) (↑(↑n : ℤ) : R) ↔ a ≤ (↑n : ℤ)
⊢ a ≤ floor.{u_2} (α := R) (↑n : R) ↔ a ≤ (↑n : ℤ)
have rw₂ : a ≤ (↑n : ℤ) ↔ a ≤ (↑n : ℤ)
Tactic: rw [le_floor, ← cast_natCast, cast_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Ring (goal)
Goal:
R : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : FloorRing R
inst_3 : IsOrderedRing R
⊢ floor.{u_2} (α := R) 0 = 0
have rw : floor.{u_2} (α := R) (↑0 : R) = 0
Tactic: rw [← cast_zero, floor_intCast]