case intro
α : Type ?u.160126
β : Type ?u.160129
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : ↑a ≠ 0
⊢ StrictMono fun x => ↑a * x
α : Type ?u.160126
β : Type ?u.160129
a b c d : ℝ≥0∞
r p q : ℝ≥0
h0 : a ≠ 0
hinf : a ≠ ⊤
⊢ StrictMono fun x => a * x
lift a to ℝ≥0 using hinf
case intro
α : Type ?u.160126
β : Type ?u.160129
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : a ≠ 0
⊢ StrictMono fun x => ↑a * x
case intro
α : Type ?u.160126
β : Type ?u.160129
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : ↑a ≠ 0
⊢ StrictMono fun x => ↑a * x
rw [coe_ne_zero] at h0
case intro
α : Type ?u.160126
β : Type ?u.160129
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : a ≠ 0
x y : ℝ≥0∞
h : x < y
⊢ (fun x => ↑a * x) x < (fun x => ↑a * x) y
case intro
α : Type ?u.160126
β : Type ?u.160129
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : a ≠ 0
⊢ StrictMono fun x => ↑a * x
intro x y h
case intro
α : Type ?u.160126
β : Type ?u.160129
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : a ≠ 0
x y : ℝ≥0∞
h : ↑a * y ≤ ↑a * x
⊢ y ≤ x
case intro
α : Type ?u.160126
β : Type ?u.160129
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : a ≠ 0
x y : ℝ≥0∞
h : x < y
⊢ (fun x => ↑a * x) x < (fun x => ↑a * x) y
contrapose! h
no goals
case intro
α : Type ?u.160126
β : Type ?u.160129
b c d : ℝ≥0∞
r p q a : ℝ≥0
h0 : a ≠ 0
x y : ℝ≥0∞
h : ↑a * y ≤ ↑a * x
⊢ y ≤ x
simpa only [← mul_assoc, ← coe_mul, inv_mul_cancel h0, coe_one, one_mul]
  using mul_le_mul_left' h (↑a⁻¹)