case top
α : Type ?u.280595
β : Type ?u.280598
a b c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b ≠ 0 ∨ c ≠ 0
ht✝ : b ≠ ⊤ ∨ c ≠ ⊤
h0 : ⊤ ≠ 0 ∨ c ≠ 0
ht : ⊤ ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / ⊤ ↔ a * ⊤ ≤ c

case coe
α : Type ?u.280595
β : Type ?u.280598
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b✝ ≠ 0 ∨ c ≠ 0
ht✝ : b✝ ≠ ⊤ ∨ c ≠ ⊤
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c
α : Type ?u.280595
β : Type ?u.280598
a b c d : ℝ≥0∞
r p q : ℝ≥0
h0 : b ≠ 0 ∨ c ≠ 0
ht : b ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / b ↔ a * b ≤ c
induction' b using recTopCoe with b
case coe.inl
α : Type ?u.280595
β : Type ?u.280598
a b c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b ≠ 0 ∨ c ≠ 0
ht✝ : b ≠ ⊤ ∨ c ≠ ⊤
h0 : ↑0 ≠ 0 ∨ c ≠ 0
ht : ↑0 ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / ↑0 ↔ a * ↑0 ≤ c

case coe.inr
α : Type ?u.280595
β : Type ?u.280598
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b✝ ≠ 0 ∨ c ≠ 0
ht✝ : b✝ ≠ ⊤ ∨ c ≠ ⊤
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ⊤ ∨ c ≠ ⊤
hb : b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c
case coe
α : Type ?u.280595
β : Type ?u.280598
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b✝ ≠ 0 ∨ c ≠ 0
ht✝ : b✝ ≠ ⊤ ∨ c ≠ ⊤
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c
rcases eq_or_ne b 0 with (rfl | hb)
case top.intro
α : Type ?u.280595
β : Type ?u.280598
a b d : ℝ≥0∞
r p q c : ℝ≥0
h0✝ : b ≠ 0 ∨ ↑c ≠ 0
ht✝ : b ≠ ⊤ ∨ ↑c ≠ ⊤
h0 : ⊤ ≠ 0 ∨ ↑c ≠ 0
ht : ⊤ ≠ ⊤ ∨ ↑c ≠ ⊤
⊢ a ≤ ↑c / ⊤ ↔ a * ⊤ ≤ ↑c
case top
α : Type ?u.280595
β : Type ?u.280598
a b c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b ≠ 0 ∨ c ≠ 0
ht✝ : b ≠ ⊤ ∨ c ≠ ⊤
h0 : ⊤ ≠ 0 ∨ c ≠ 0
ht : ⊤ ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / ⊤ ↔ a * ⊤ ≤ c
lift c to ℝ≥0 using ht.neg_resolve_left rfl
case top.intro
α : Type ?u.280595
β : Type ?u.280598
a b d : ℝ≥0∞
r p q c : ℝ≥0
h0✝ : b ≠ 0 ∨ ↑c ≠ 0
ht✝ : b ≠ ⊤ ∨ ↑c ≠ ⊤
h0 : ⊤ ≠ 0 ∨ ↑c ≠ 0
ht : ⊤ ≠ ⊤ ∨ ↑c ≠ ⊤
⊢ a = 0 ↔ a * ⊤ ≤ ↑c
case top.intro
α : Type ?u.280595
β : Type ?u.280598
a b d : ℝ≥0∞
r p q c : ℝ≥0
h0✝ : b ≠ 0 ∨ ↑c ≠ 0
ht✝ : b ≠ ⊤ ∨ ↑c ≠ ⊤
h0 : ⊤ ≠ 0 ∨ ↑c ≠ 0
ht : ⊤ ≠ ⊤ ∨ ↑c ≠ ⊤
⊢ a ≤ ↑c / ⊤ ↔ a * ⊤ ≤ ↑c
rw [div_top, nonpos_iff_eq_zero]
no goals
case top.intro
α : Type ?u.280595
β : Type ?u.280598
a b d : ℝ≥0∞
r p q c : ℝ≥0
h0✝ : b ≠ 0 ∨ ↑c ≠ 0
ht✝ : b ≠ ⊤ ∨ ↑c ≠ ⊤
h0 : ⊤ ≠ 0 ∨ ↑c ≠ 0
ht : ⊤ ≠ ⊤ ∨ ↑c ≠ ⊤
⊢ a = 0 ↔ a * ⊤ ≤ ↑c
rcases eq_or_ne a 0 with (rfl | ha) <;> simp [*]
case coe.inl
α : Type ?u.280595
β : Type ?u.280598
a b c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b ≠ 0 ∨ c ≠ 0
ht✝ : b ≠ ⊤ ∨ c ≠ ⊤
h0 : ↑0 ≠ 0 ∨ c ≠ 0
ht : ↑0 ≠ ⊤ ∨ c ≠ ⊤
hc : c ≠ 0
⊢ a ≤ c / ↑0 ↔ a * ↑0 ≤ c
case coe.inl
α : Type ?u.280595
β : Type ?u.280598
a b c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b ≠ 0 ∨ c ≠ 0
ht✝ : b ≠ ⊤ ∨ c ≠ ⊤
h0 : ↑0 ≠ 0 ∨ c ≠ 0
ht : ↑0 ≠ ⊤ ∨ c ≠ ⊤
⊢ a ≤ c / ↑0 ↔ a * ↑0 ≤ c
have hc : c ≠ 0 := h0.neg_resolve_left rfl
no goals
case coe.inl
α : Type ?u.280595
β : Type ?u.280598
a b c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b ≠ 0 ∨ c ≠ 0
ht✝ : b ≠ ⊤ ∨ c ≠ ⊤
h0 : ↑0 ≠ 0 ∨ c ≠ 0
ht : ↑0 ≠ ⊤ ∨ c ≠ ⊤
hc : c ≠ 0
⊢ a ≤ c / ↑0 ↔ a * ↑0 ≤ c
simp [div_zero hc]
case coe.inr
α : Type ?u.280595
β : Type ?u.280598
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b✝ ≠ 0 ∨ c ≠ 0
ht✝ : b✝ ≠ ⊤ ∨ c ≠ ⊤
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ⊤ ∨ c ≠ ⊤
hb : ↑b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c
case coe.inr
α : Type ?u.280595
β : Type ?u.280598
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b✝ ≠ 0 ∨ c ≠ 0
ht✝ : b✝ ≠ ⊤ ∨ c ≠ ⊤
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ⊤ ∨ c ≠ ⊤
hb : b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c
rw [← coe_ne_zero] at hb
no goals
case coe.inr
α : Type ?u.280595
β : Type ?u.280598
a b✝ c d : ℝ≥0∞
r p q : ℝ≥0
h0✝ : b✝ ≠ 0 ∨ c ≠ 0
ht✝ : b✝ ≠ ⊤ ∨ c ≠ ⊤
b : ℝ≥0
h0 : ↑b ≠ 0 ∨ c ≠ 0
ht : ↑b ≠ ⊤ ∨ c ≠ ⊤
hb : ↑b ≠ 0
⊢ a ≤ c / ↑b ↔ a * ↑b ≤ c
rw [← ENNReal.mul_le_mul_right hb coe_ne_top, ENNReal.div_mul_cancel hb coe_ne_top]