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
⊢ Infinitesimal ε ↔ ∃ α, ∀ (r : R), ε * r < α
Tactic:
refine FloorRing_iff_mul_right₁.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 < α := (mul_zero ε).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_left h0] at h
State after:
no goals