Theorem: IMOSL.Extra.Infinitesimal.FloorRing_mul_left (IMOSLLean4/Extra/Infinitesimal/FloorRing.lean)

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • |r * ε| < 1
Tactic:
apply (hε (k * ⌈|r|⌉.natAbs)).trans_le'
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • |r * ε| ≤ (k * ⌈|r|⌉.natAbs) • |ε|

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • |r * ε| ≤ (k * ⌈|r|⌉.natAbs) • |ε|
Tactic:
rw [abs_mul, mul_nsmul', nsmul_eq_mul ⌈|r|⌉.natAbs]
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • (|r| * |ε|) ≤ k • (↑⌈|r|⌉.natAbs * |ε|)

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ k • (|r| * |ε|) ≤ k • (↑⌈|r|⌉.natAbs * |ε|)
Tactic:
refine nsmul_le_nsmul_right (mul_le_mul_of_nonneg_right ?_ (abs_nonneg ε)) k
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ |r| ≤ ↑⌈|r|⌉.natAbs

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ |r| ≤ ↑⌈|r|⌉.natAbs
Tactic:
rw [← Int.cast_natCast ⌈|r|⌉.natAbs, ← Int.ceil_le]
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ ⌈|r|⌉ ≤ ↑⌈|r|⌉.natAbs

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
hε : Infinitesimal ε
r : R
k : ℕ
⊢ ⌈|r|⌉ ≤ ↑⌈|r|⌉.natAbs
Tactic:
exact Int.le_natAbs
State after:
no goals