awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a : R
inl : ∀ (ha : a ≤ 0), ⌊a⌋₊ ≤ ⌈a⌉₊
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊
have inr : ∀ (ha : 0 ≤ a), ⌊a⌋₊ ≤ ⌈a⌉₊
Tactic: obtain ha | ha := le_total a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a : R
ha : a ≤ 0
⊢ ⌊a⌋₊ ≤ ⌈a⌉₊
have inl : 0 ≤ ⌈a⌉₊
Tactic: rw [floor_of_nonpos ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
⊢ ⌊a⌋₊ < ⌈b⌉₊
have inl : ∀ (ha : 0 ≤ a), ⌊a⌋₊ < ⌈b⌉₊
Tactic: rcases le_or_gt 0 a with (ha | ha)
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
inl : ∀ (ha : 0 ≤ a), ⌊a⌋₊ < ⌈b⌉₊
⊢ ⌊a⌋₊ < ⌈b⌉₊
have inr : ∀ (ha : a < 0), ⌊a⌋₊ < ⌈b⌉₊
Tactic: rcases le_or_gt 0 a with (ha | ha)
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : 0 ≤ a
⊢ ⌊a⌋₊ < ⌈b⌉₊
have inl : a < (↑⌈b⌉₊ : R)
Tactic: rw [floor_lt ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : a < 0
⊢ ⌊a⌋₊ < ⌈b⌉₊
have inr : 0 < ⌈b⌉₊
Tactic: rwa [floor_of_nonpos ha.le, lt_ceil, Nat.cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a b : R
h : a < b
h' : 0 < b
ha : a < 0
inr : 0 < ⌈b⌉₊
⊢ ⌊a⌋₊ < ⌈b⌉₊
have inr₁ : (↑0 : R) < b
Tactic: rwa [floor_of_nonpos ha.le, lt_ceil, Nat.cast_zero]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a b : R
ha : 0 ≤ a
⊢ Nat.cast ⁻¹' Ioo a b = Ioo ⌊a⌋₊ ⌈b⌉₊
have h : ∀ (x : ℕ), x ∈ Nat.cast ⁻¹' Ioo a b ↔ x ∈ Ioo ⌊a⌋₊ ⌈b⌉₊
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a b : R
⊢ Nat.cast ⁻¹' Ico a b = Ico ⌈a⌉₊ ⌈b⌉₊
have h : ∀ (x : ℕ), x ∈ Nat.cast ⁻¹' Ico a b ↔ x ∈ Ico ⌈a⌉₊ ⌈b⌉₊
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a b : R
ha : 0 ≤ a
hb : 0 ≤ b
⊢ Nat.cast ⁻¹' Ioc a b = Ioc ⌊a⌋₊ ⌊b⌋₊
have h : ∀ (x : ℕ), x ∈ Nat.cast ⁻¹' Ioc a b ↔ x ∈ Ioc ⌊a⌋₊ ⌊b⌋₊
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a b : R
hb : 0 ≤ b
⊢ Nat.cast ⁻¹' Icc a b = Icc ⌈a⌉₊ ⌊b⌋₊
have h : ∀ (x : ℕ), x ∈ Nat.cast ⁻¹' Icc a b ↔ x ∈ Icc ⌈a⌉₊ ⌊b⌋₊
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ Nat.cast ⁻¹' Ioi a = Ioi ⌊a⌋₊
have h : ∀ (x : ℕ), x ∈ Nat.cast ⁻¹' Ioi a ↔ x ∈ Ioi ⌊a⌋₊
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
⊢ Nat.cast ⁻¹' Ici a = Ici ⌈a⌉₊
have h : ∀ (x : ℕ), x ∈ Nat.cast ⁻¹' Ici a ↔ x ∈ Ici ⌈a⌉₊
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
⊢ Nat.cast ⁻¹' Iio a = Iio ⌈a⌉₊
have h : ∀ (x : ℕ), x ∈ Nat.cast ⁻¹' Iio a ↔ x ∈ Iio ⌈a⌉₊
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
ha : 0 ≤ a
⊢ Nat.cast ⁻¹' Iic a = Iic ⌊a⌋₊
have h : ∀ (x : ℕ), x ∈ Nat.cast ⁻¹' Iic a ↔ x ∈ Iic ⌊a⌋₊
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
⊢ b ≤ ⌊a + (↑n : R)⌋₊ ↔ b ≤ ⌊a⌋₊ + n
have rw : (↑b : R) ≤ a + (↑n : R) ↔ b ≤ ⌊a⌋₊ + n
Tactic: rw [le_floor_iff (add_nonneg ha n.cast_nonneg)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
⊢ (↑b : R) ≤ a + (↑n : R) ↔ b ≤ ⌊a⌋₊ + n
have inl : ∀ (hb : n ≤ b), (↑b : R) ≤ a + (↑n : R) ↔ b ≤ ⌊a⌋₊ + n
Tactic: obtain hb | hb := le_total n b
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
inl : ∀ (hb : n ≤ b), (↑b : R) ≤ a + (↑n : R) ↔ b ≤ ⌊a⌋₊ + n
⊢ (↑b : R) ≤ a + (↑n : R) ↔ b ≤ ⌊a⌋₊ + n
have inr : ∀ (hb : b ≤ n), (↑b : R) ≤ a + (↑n : R) ↔ b ≤ ⌊a⌋₊ + n
Tactic: obtain hb | hb := le_total n b
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : n ≤ b
⊢ (↑b : R) ≤ a + (↑n : R) ↔ b ≤ ⌊a⌋₊ + n
have inl : ∀ (d : ℕ) (hb : n ≤ n + d), (↑(n + d) : R) ≤ a + (↑n : R) ↔ n + d ≤ ⌊a⌋₊ + n
Tactic: obtain ⟨d, rfl⟩ := exists_add_of_le hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ (↑(n + d) : R) ≤ a + (↑n : R) ↔ n + d ≤ ⌊a⌋₊ + n
have inl : HAdd.hAdd (α := R) (↑n : R) (↑d : R) ≤ a + (↑n : R) ↔ n + d ≤ ⌊a⌋₊ + n
Tactic: rw [Nat.cast_add, add_comm n, add_comm (n : R), add_le_add_iff_right, add_le_add_iff_right,
        le_floor_iff ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
inl : HAdd.hAdd (α := R) (↑n : R) (↑d : R) ≤ a + (↑n : R) ↔ n + d ≤ ⌊a⌋₊ + n
⊢ (↑(n + d) : R) ≤ a + (↑n : R) ↔ n + d ≤ ⌊a⌋₊ + n
have inl₁ : HAdd.hAdd (α := R) (↑n : R) (↑d : R) ≤ a + (↑n : R) ↔ d + n ≤ ⌊a⌋₊ + n
Tactic: rw [Nat.cast_add, add_comm n, add_comm (n : R), add_le_add_iff_right, add_le_add_iff_right,
        le_floor_iff ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
inl : HAdd.hAdd (α := R) (↑n : R) (↑d : R) ≤ a + (↑n : R) ↔ n + d ≤ ⌊a⌋₊ + n
inl₁ : HAdd.hAdd (α := R) (↑n : R) (↑d : R) ≤ a + (↑n : R) ↔ d + n ≤ ⌊a⌋₊ + n
⊢ (↑(n + d) : R) ≤ a + (↑n : R) ↔ n + d ≤ ⌊a⌋₊ + n
have inl₂ : HAdd.hAdd (α := R) (↑d : R) (↑n : R) ≤ a + (↑n : R) ↔ d + n ≤ ⌊a⌋₊ + n
Tactic: rw [Nat.cast_add, add_comm n, add_comm (n : R), add_le_add_iff_right, add_le_add_iff_right,
        le_floor_iff ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
inl : HAdd.hAdd (α := R) (↑n : R) (↑d : R) ≤ a + (↑n : R) ↔ n + d ≤ ⌊a⌋₊ + n
inl₁ : HAdd.hAdd (α := R) (↑n : R) (↑d : R) ≤ a + (↑n : R) ↔ d + n ≤ ⌊a⌋₊ + n
inl₂ : HAdd.hAdd (α := R) (↑d : R) (↑n : R) ≤ a + (↑n : R) ↔ d + n ≤ ⌊a⌋₊ + n
⊢ (↑(n + d) : R) ≤ a + (↑n : R) ↔ n + d ≤ ⌊a⌋₊ + n
have inl₃ : (↑d : R) ≤ a ↔ d + n ≤ ⌊a⌋₊ + n
Tactic: rw [Nat.cast_add, add_comm n, add_comm (n : R), add_le_add_iff_right, add_le_add_iff_right,
        le_floor_iff ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
inl : HAdd.hAdd (α := R) (↑n : R) (↑d : R) ≤ a + (↑n : R) ↔ n + d ≤ ⌊a⌋₊ + n
inl₁ : HAdd.hAdd (α := R) (↑n : R) (↑d : R) ≤ a + (↑n : R) ↔ d + n ≤ ⌊a⌋₊ + n
inl₂ : HAdd.hAdd (α := R) (↑d : R) (↑n : R) ≤ a + (↑n : R) ↔ d + n ≤ ⌊a⌋₊ + n
inl₃ : (↑d : R) ≤ a ↔ d + n ≤ ⌊a⌋₊ + n
⊢ (↑(n + d) : R) ≤ a + (↑n : R) ↔ n + d ≤ ⌊a⌋₊ + n
have inl₄ : (↑d : R) ≤ a ↔ d ≤ ⌊a⌋₊
Tactic: rw [Nat.cast_add, add_comm n, add_comm (n : R), add_le_add_iff_right, add_le_add_iff_right,
        le_floor_iff ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
inl : HAdd.hAdd (α := R) (↑n : R) (↑d : R) ≤ a + (↑n : R) ↔ n + d ≤ ⌊a⌋₊ + n
inl₁ : HAdd.hAdd (α := R) (↑n : R) (↑d : R) ≤ a + (↑n : R) ↔ d + n ≤ ⌊a⌋₊ + n
inl₂ : HAdd.hAdd (α := R) (↑d : R) (↑n : R) ≤ a + (↑n : R) ↔ d + n ≤ ⌊a⌋₊ + n
inl₃ : (↑d : R) ≤ a ↔ d + n ≤ ⌊a⌋₊ + n
inl₄ : (↑d : R) ≤ a ↔ d ≤ ⌊a⌋₊
⊢ (↑(n + d) : R) ≤ a + (↑n : R) ↔ n + d ≤ ⌊a⌋₊ + n
have inl₅ : (↑d : R) ≤ a ↔ (↑d : R) ≤ a
Tactic: rw [Nat.cast_add, add_comm n, add_comm (n : R), add_le_add_iff_right, add_le_add_iff_right,
        le_floor_iff ha]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : b ≤ n
⊢ (↑b : R) ≤ a + (↑n : R) ↔ b ≤ ⌊a⌋₊ + n
have inr : ∀ (d : ℕ) (hb : b ≤ b + d), (↑b : R) ≤ a + (↑(b + d) : R) ↔ b ≤ ⌊a⌋₊ + (b + d)
Tactic: obtain ⟨d, rfl⟩ := exists_add_of_le hb
Cleared hypotheses: n, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ (↑b : R) ≤ a + (↑(b + d) : R) ↔ b ≤ ⌊a⌋₊ + (b + d)
have inr : (↑b : R) ≤ (↑b : R) + (a + (↑d : R)) ↔ b ≤ b + (⌊a⌋₊ + d)
Tactic: rw [Nat.cast_add, add_left_comm _ b, add_left_comm _ (b : R)]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
b d : ℕ
hb : b ≤ b + d
⊢ (↑b : R) ≤ (↑b : R) + (a + (↑d : R)) ↔ b ≤ b + (⌊a⌋₊ + d)
have inr : (↑b : R) ≤ (↑b : R) + (a + (↑d : R))
Tactic: refine iff_of_true ?_ le_self_add
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
⊢ ⌊a + 1⌋₊ = ⌊a⌋₊ + 1
have rw : ⌊a + (↑1 : R)⌋₊ = ⌊a⌋₊ + 1
Tactic: rw [← cast_one, floor_add_natCast ha 1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
rw : ⌊a + (↑1 : R)⌋₊ = ⌊a⌋₊ + 1
⊢ ⌊a + 1⌋₊ = ⌊a⌋₊ + 1
have rw₁ : ⌊a⌋₊ + 1 = ⌊a⌋₊ + 1
Tactic: rw [← cast_one, floor_add_natCast ha 1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
⊢ ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
have inl : ∀ (ha : a ≤ 0), ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
Tactic: obtain ha | ha := le_total a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
inl : ∀ (ha : a ≤ 0), ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
⊢ ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
have inr : ∀ (ha : 0 ≤ a), ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
Tactic: obtain ha | ha := le_total a 0
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
ha : a ≤ 0
⊢ ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
have inl : ⌊a - (↑n : R)⌋₊ = 0 - n
Tactic: rw [floor_of_nonpos ha, floor_of_nonpos (tsub_nonpos_of_le (ha.trans n.cast_nonneg)), zero_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
ha : a ≤ 0
inl : ⌊a - (↑n : R)⌋₊ = 0 - n
⊢ ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
have inl₁ : 0 = 0 - n
Tactic: rw [floor_of_nonpos ha, floor_of_nonpos (tsub_nonpos_of_le (ha.trans n.cast_nonneg)), zero_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
ha : a ≤ 0
inl : ⌊a - (↑n : R)⌋₊ = 0 - n
inl₁ : 0 = 0 - n
⊢ ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
have inl₂ : Eq (α := ℕ) 0 0
Tactic: rw [floor_of_nonpos ha, floor_of_nonpos (tsub_nonpos_of_le (ha.trans n.cast_nonneg)), zero_tsub]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
⊢ ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
have inr : ∀ (h : a ≤ (↑n : R)), ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
Tactic: rcases le_total a n with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
inr : ∀ (h : a ≤ (↑n : R)), ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
⊢ ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
have inr₁ : ∀ (h : (↑n : R) ≤ a), ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
Tactic: rcases le_total a n with h | h
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : a ≤ (↑n : R)
⊢ ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
have inr : ⌊a⌋₊ ≤ n
Tactic: rw [floor_of_nonpos (tsub_nonpos_of_le h), eq_comm, tsub_eq_zero_iff_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
ha : 0 ≤ a
h : (↑n : R) ≤ a
⊢ ⌊a - (↑n : R)⌋₊ = ⌊a⌋₊ - n
have rw : 0 ≤ a - (↑n : R)
Tactic: rw [eq_tsub_iff_add_eq_of_le (le_floor h), ← floor_add_natCast _, tsub_add_cancel_of_le h]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
⊢ ⌈a + (↑n : R)⌉₊ ≤ b ↔ ⌈a⌉₊ + n ≤ b
have contrapose! : b < ⌈a + (↑n : R)⌉₊ ↔ b < ⌈a⌉₊ + n
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
⊢ b < ⌈a + (↑n : R)⌉₊ ↔ b < ⌈a⌉₊ + n
have rw : (↑b : R) < a + (↑n : R) ↔ b < ⌈a⌉₊ + n
Tactic: rw [lt_ceil]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
⊢ (↑b : R) < a + (↑n : R) ↔ b < ⌈a⌉₊ + n
have inl : ∀ (hb : n ≤ b), (↑b : R) < a + (↑n : R) ↔ b < ⌈a⌉₊ + n
Tactic: obtain hb | hb := le_or_gt n b
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
inl : ∀ (hb : n ≤ b), (↑b : R) < a + (↑n : R) ↔ b < ⌈a⌉₊ + n
⊢ (↑b : R) < a + (↑n : R) ↔ b < ⌈a⌉₊ + n
have inr : ∀ (hb : b < n), (↑b : R) < a + (↑n : R) ↔ b < ⌈a⌉₊ + n
Tactic: obtain hb | hb := le_or_gt n b
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n b : ℕ
hb : n ≤ b
⊢ (↑b : R) < a + (↑n : R) ↔ b < ⌈a⌉₊ + n
have inl : ∀ (d : ℕ) (hb : n ≤ n + d), (↑(n + d) : R) < a + (↑n : R) ↔ n + d < ⌈a⌉₊ + n
Tactic: obtain ⟨d, rfl⟩ := exists_add_of_le hb
Cleared hypotheses: b, hb
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
⊢ (↑(n + d) : R) < a + (↑n : R) ↔ n + d < ⌈a⌉₊ + n
have inl : HAdd.hAdd (α := R) (↑n : R) (↑d : R) < a + (↑n : R) ↔ n + d < ⌈a⌉₊ + n
Tactic: rw [Nat.cast_add, add_comm n, add_comm (n : R), add_lt_add_iff_right, add_lt_add_iff_right,
        lt_ceil]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
inl : HAdd.hAdd (α := R) (↑n : R) (↑d : R) < a + (↑n : R) ↔ n + d < ⌈a⌉₊ + n
⊢ (↑(n + d) : R) < a + (↑n : R) ↔ n + d < ⌈a⌉₊ + n
have inl₁ : HAdd.hAdd (α := R) (↑n : R) (↑d : R) < a + (↑n : R) ↔ d + n < ⌈a⌉₊ + n
Tactic: rw [Nat.cast_add, add_comm n, add_comm (n : R), add_lt_add_iff_right, add_lt_add_iff_right,
        lt_ceil]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
inl : HAdd.hAdd (α := R) (↑n : R) (↑d : R) < a + (↑n : R) ↔ n + d < ⌈a⌉₊ + n
inl₁ : HAdd.hAdd (α := R) (↑n : R) (↑d : R) < a + (↑n : R) ↔ d + n < ⌈a⌉₊ + n
⊢ (↑(n + d) : R) < a + (↑n : R) ↔ n + d < ⌈a⌉₊ + n
have inl₂ : HAdd.hAdd (α := R) (↑d : R) (↑n : R) < a + (↑n : R) ↔ d + n < ⌈a⌉₊ + n
Tactic: rw [Nat.cast_add, add_comm n, add_comm (n : R), add_lt_add_iff_right, add_lt_add_iff_right,
        lt_ceil]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
inl : HAdd.hAdd (α := R) (↑n : R) (↑d : R) < a + (↑n : R) ↔ n + d < ⌈a⌉₊ + n
inl₁ : HAdd.hAdd (α := R) (↑n : R) (↑d : R) < a + (↑n : R) ↔ d + n < ⌈a⌉₊ + n
inl₂ : HAdd.hAdd (α := R) (↑d : R) (↑n : R) < a + (↑n : R) ↔ d + n < ⌈a⌉₊ + n
⊢ (↑(n + d) : R) < a + (↑n : R) ↔ n + d < ⌈a⌉₊ + n
have inl₃ : (↑d : R) < a ↔ d + n < ⌈a⌉₊ + n
Tactic: rw [Nat.cast_add, add_comm n, add_comm (n : R), add_lt_add_iff_right, add_lt_add_iff_right,
        lt_ceil]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
inl : HAdd.hAdd (α := R) (↑n : R) (↑d : R) < a + (↑n : R) ↔ n + d < ⌈a⌉₊ + n
inl₁ : HAdd.hAdd (α := R) (↑n : R) (↑d : R) < a + (↑n : R) ↔ d + n < ⌈a⌉₊ + n
inl₂ : HAdd.hAdd (α := R) (↑d : R) (↑n : R) < a + (↑n : R) ↔ d + n < ⌈a⌉₊ + n
inl₃ : (↑d : R) < a ↔ d + n < ⌈a⌉₊ + n
⊢ (↑(n + d) : R) < a + (↑n : R) ↔ n + d < ⌈a⌉₊ + n
have inl₄ : (↑d : R) < a ↔ d < ⌈a⌉₊
Tactic: rw [Nat.cast_add, add_comm n, add_comm (n : R), add_lt_add_iff_right, add_lt_add_iff_right,
        lt_ceil]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
n d : ℕ
hb : n ≤ n + d
inl : HAdd.hAdd (α := R) (↑n : R) (↑d : R) < a + (↑n : R) ↔ n + d < ⌈a⌉₊ + n
inl₁ : HAdd.hAdd (α := R) (↑n : R) (↑d : R) < a + (↑n : R) ↔ d + n < ⌈a⌉₊ + n
inl₂ : HAdd.hAdd (α := R) (↑d : R) (↑n : R) < a + (↑n : R) ↔ d + n < ⌈a⌉₊ + n
inl₃ : (↑d : R) < a ↔ d + n < ⌈a⌉₊ + n
inl₄ : (↑d : R) < a ↔ d < ⌈a⌉₊
⊢ (↑(n + d) : R) < a + (↑n : R) ↔ n + d < ⌈a⌉₊ + n
have inl₅ : (↑d : R) < a ↔ (↑d : R) < a
Tactic: rw [Nat.cast_add, add_comm n, add_comm (n : R), add_lt_add_iff_right, add_lt_add_iff_right,
        lt_ceil]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
⊢ ⌈a + 1⌉₊ = ⌈a⌉₊ + 1
have rw : ⌈a + (↑1 : R)⌉₊ = ⌈a⌉₊ + 1
Tactic: rw [cast_one.symm, ceil_add_natCast ha 1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
a : R
inst_3 : IsStrictOrderedRing R
ha : 0 ≤ a
rw : ⌈a + (↑1 : R)⌉₊ = ⌈a⌉₊ + 1
⊢ ⌈a + 1⌉₊ = ⌈a⌉₊ + 1
have rw₁ : ⌈a⌉₊ + 1 = ⌈a⌉₊ + 1
Tactic: rw [cast_one.symm, ceil_add_natCast ha 1]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a b : R
⊢ ⌈a + b⌉₊ ≤ ⌈a⌉₊ + ⌈b⌉₊
have rw : a + b ≤ HAdd.hAdd (α := R) (↑⌈a⌉₊ : R) (↑⌈b⌉₊ : R)
Tactic: rw [ceil_le, Nat.cast_add]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a b : R
⊢ a + b ≤ HAdd.hAdd (α := R) (↑⌈a⌉₊ : R) (↑⌈b⌉₊ : R)
have h₁ : a ≤ (↑⌈a⌉₊ : R)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
a b : R
h₁ : a ≤ (↑⌈a⌉₊ : R)
⊢ a + b ≤ HAdd.hAdd (α := R) (↑⌈a⌉₊ : R) (↑⌈b⌉₊ : R)
have h₂ : b ≤ (↑⌈b⌉₊ : R)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
⊢ ⌈a - (↑n : R)⌉₊ = ⌈a⌉₊ - n
have inl : ∀ (han : a ≤ (↑n : R)), ⌈a - (↑n : R)⌉₊ = ⌈a⌉₊ - n
Tactic: obtain han | hna := le_total a n
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
inl : ∀ (han : a ≤ (↑n : R)), ⌈a - (↑n : R)⌉₊ = ⌈a⌉₊ - n
⊢ ⌈a - (↑n : R)⌉₊ = ⌈a⌉₊ - n
have inr : ∀ (hna : (↑n : R) ≤ a), ⌈a - (↑n : R)⌉₊ = ⌈a⌉₊ - n
Tactic: obtain han | hna := le_total a n
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
han : a ≤ (↑n : R)
⊢ ⌈a - (↑n : R)⌉₊ = ⌈a⌉₊ - n
have inl : 0 = ⌈a⌉₊ - n
Tactic: rwa [ceil_eq_zero.2 (tsub_nonpos_of_le han), eq_comm, tsub_eq_zero_iff_le, Nat.ceil_le]
-- Lean 4 proof step from Mathlib.Algebra.Order.Floor.Semiring (goal)
Goal:
R : Type u_1
inst : Semiring R
inst_1 : LinearOrder R
inst_2 : FloorSemiring R
inst_3 : IsStrictOrderedRing R
inst_4 : Sub R
inst_5 : OrderedSub R
inst_6 : ExistsAddOfLE R
a : R
n : ℕ
han : a ≤ (↑n : R)
inl : 0 = ⌈a⌉₊ - n
⊢ ⌈a - (↑n : R)⌉₊ = ⌈a⌉₊ - n
have inl₁ : ⌈a⌉₊ - n = 0
Tactic: rwa [ceil_eq_zero.2 (tsub_nonpos_of_le han), eq_comm, tsub_eq_zero_iff_le, Nat.ceil_le]