x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ a ≤ y
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
⊢ a ≤ y
have hx : x ≠ 0 := pos_iff_ne_zero.1 (lt_of_le_of_lt (zero_le _) ha)
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ a ≤ y
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ a ≤ y
have hx' : x⁻¹ ≠ 0 := by rwa [Ne.def, inv_eq_zero]
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this : a * x⁻¹ < 1
⊢ a ≤ y
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ a ≤ y
have : a * x⁻¹ < 1 := by rwa [← lt_inv_iff_mul_lt hx', inv_inv]
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this✝ : a * x⁻¹ < 1
this : a * x⁻¹ * x ≤ y
⊢ a ≤ y
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this : a * x⁻¹ < 1
⊢ a ≤ y
have : a * x⁻¹ * x ≤ y := h _ this
no goals
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
this✝ : a * x⁻¹ < 1
this : a * x⁻¹ * x ≤ y
⊢ a ≤ y
rwa [mul_assoc, inv_mul_cancel hx, mul_one] at this
no goals
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
⊢ x⁻¹ ≠ 0
rwa [Ne.def, inv_eq_zero]
no goals
x y : ℝ≥0
h : ∀ (a : ℝ≥0), a < 1 → a * x ≤ y
a : ℝ≥0
ha : a < x
hx : x ≠ 0
hx' : x⁻¹ ≠ 0
⊢ a * x⁻¹ < 1
rwa [← lt_inv_iff_mul_lt hx', inv_inv]