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

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
⊢ k • |ε| < 1
Tactic:
rcases le_total 0 ε with h0 | h0
State after:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
h0 : 0 ≤ ε
⊢ k • |ε| < 1

case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
h0 : ε ≤ 0
⊢ k • |ε| < 1

State before:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
h0 : 0 ≤ ε
⊢ k • |ε| < 1
Tactic:
rw [abs_eq_self.mpr h0, nsmul_eq_mul]
State after:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
h0 : 0 ≤ ε
⊢ ↑k * ε < 1

State before:
case inl
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
h0 : 0 ≤ ε
⊢ ↑k * ε < 1
Tactic:
exact h _
State after:
no goals

State before:
case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
h0 : ε ≤ 0
⊢ k • |ε| < 1
Tactic:
rw [abs_eq_neg_self.mpr h0, nsmul_eq_mul, mul_neg, ← neg_mul]
State after:
case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
h0 : ε ≤ 0
⊢ -↑k * ε < 1

State before:
case inr
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
h : ∀ (r : R), r * ε < 1
k : ℕ
h0 : ε ≤ 0
⊢ -↑k * ε < 1
Tactic:
exact h _
State after:
no goals