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
⊢ Infinitesimal ε ↔ ∃ α, ∀ (r : R), r * ε < α
Tactic:
refine FloorRing_iff_mul_left₁.trans ⟨λ h ↦ ⟨1, h⟩, λ ⟨α, h⟩ r ↦ ?_⟩
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), r * ε < α
r α : R
h : ∀ (r : R), r * ε < α
⊢ r * ε < 1

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), r * ε < α
r α : R
h : ∀ (r : R), r * ε < α
⊢ r * ε < 1
Tactic:
have h0 : 0 < α := (zero_mul ε).symm.trans_lt (h 0)
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), r * ε < α
r α : R
h : ∀ (r : R), r * ε < α
h0 : 0 < α
⊢ r * ε < 1

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), r * ε < α
r α : R
h : ∀ (r : R), r * ε < α
h0 : 0 < α
⊢ r * ε < 1
Tactic:
specialize h (α * r)
State after:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), r * ε < α
r α : R
h0 : 0 < α
h : α * r * ε < α
⊢ r * ε < 1

State before:
R : Type u_1
inst✝¹ : LinearOrderedRing R
inst✝ : FloorRing R
ε : R
x✝ : ∃ α, ∀ (r : R), r * ε < α
r α : R
h0 : 0 < α
h : α * r * ε < α
⊢ r * ε < 1
Tactic:
rwa [mul_assoc, mul_lt_iff_lt_one_right h0] at h
State after:
no goals