Theorem: IMOSL.Extra.Infinitesimal.FloorRing_iff_mul_right₁ (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', neg_mul, ← mul_neg]
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