case pos
α : Type ?u.287943
β : Type ?u.287946
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
h0 : c = 0
⊢ a / c ≤ b

case neg
α : Type ?u.287943
β : Type ?u.287946
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
h0 : ¬c = 0
⊢ a / c ≤ b
α : Type ?u.287943
β : Type ?u.287946
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
⊢ a / c ≤ b
by_cases h0 : c = 0
case pos
α : Type ?u.287943
β : Type ?u.287946
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
h0 : ¬c = 0
hinf : c = ⊤
⊢ a / c ≤ b

case neg
α : Type ?u.287943
β : Type ?u.287946
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
h0 : ¬c = 0
hinf : ¬c = ⊤
⊢ a / c ≤ b
case neg
α : Type ?u.287943
β : Type ?u.287946
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
h0 : ¬c = 0
⊢ a / c ≤ b
by_cases hinf : c = ∞
no goals
case neg
α : Type ?u.287943
β : Type ?u.287946
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
h0 : ¬c = 0
hinf : ¬c = ⊤
⊢ a / c ≤ b
exact (ENNReal.div_le_iff_le_mul (Or.inl h0) (Or.inl hinf)).2 h
case pos
α : Type ?u.287943
β : Type ?u.287946
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
h0 : c = 0
this : a = 0
⊢ a / c ≤ b
case pos
α : Type ?u.287943
β : Type ?u.287946
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
h0 : c = 0
⊢ a / c ≤ b
have : a = 0 := by simpa [h0] using h
no goals
case pos
α : Type ?u.287943
β : Type ?u.287946
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
h0 : c = 0
this : a = 0
⊢ a / c ≤ b
simp [*]
no goals
α : Type ?u.287943
β : Type ?u.287946
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
h0 : c = 0
⊢ a = 0
simpa [h0] using h
no goals
case pos
α : Type ?u.287943
β : Type ?u.287946
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≤ b * c
h0 : ¬c = 0
hinf : c = ⊤
⊢ a / c ≤ b
simp [hinf]