case mp
α✝ : Type ?u.5062900
E : Type ?u.5062903
F : Type ?u.5062906
G : Type ?u.5062909
m m0 : MeasurableSpace α✝
p : ℝ≥0∞
q : ℝ
μ ν : Measure α✝
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
α : Type u_1
inst✝ : LinearOrderedSemiring α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
⊢ a ≤ b * c → a = 0 ∧ c = 0

case mpr
α✝ : Type ?u.5062900
E : Type ?u.5062903
F : Type ?u.5062906
G : Type ?u.5062909
m m0 : MeasurableSpace α✝
p : ℝ≥0∞
q : ℝ
μ ν : Measure α✝
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
α : Type u_1
inst✝ : LinearOrderedSemiring α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
⊢ a = 0 ∧ c = 0 → a ≤ b * c
α✝ : Type ?u.5062900
E : Type ?u.5062903
F : Type ?u.5062906
G : Type ?u.5062909
m m0 : MeasurableSpace α✝
p : ℝ≥0∞
q : ℝ
μ ν : Measure α✝
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
α : Type u_1
inst✝ : LinearOrderedSemiring α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
⊢ a ≤ b * c ↔ a = 0 ∧ c = 0
constructor
case mp
α✝ : Type ?u.5062900
E : Type ?u.5062903
F : Type ?u.5062906
G : Type ?u.5062909
m m0 : MeasurableSpace α✝
p : ℝ≥0∞
q : ℝ
μ ν : Measure α✝
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
α : Type u_1
inst✝ : LinearOrderedSemiring α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
h : a ≤ b * c
⊢ a = 0 ∧ c = 0
case mp
α✝ : Type ?u.5062900
E : Type ?u.5062903
F : Type ?u.5062906
G : Type ?u.5062909
m m0 : MeasurableSpace α✝
p : ℝ≥0∞
q : ℝ
μ ν : Measure α✝
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
α : Type u_1
inst✝ : LinearOrderedSemiring α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
⊢ a ≤ b * c → a = 0 ∧ c = 0
intro h
no goals
case mp
α✝ : Type ?u.5062900
E : Type ?u.5062903
F : Type ?u.5062906
G : Type ?u.5062909
m m0 : MeasurableSpace α✝
p : ℝ≥0∞
q : ℝ
μ ν : Measure α✝
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
α : Type u_1
inst✝ : LinearOrderedSemiring α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
h : a ≤ b * c
⊢ a = 0 ∧ c = 0
exact
  ⟨(h.trans (mul_nonpos_of_nonpos_of_nonneg hb.le hc)).antisymm ha,
    (nonpos_of_mul_nonneg_right (ha.trans h) hb).antisymm hc⟩
case mpr.intro
α✝ : Type ?u.5062900
E : Type ?u.5062903
F : Type ?u.5062906
G : Type ?u.5062909
m m0 : MeasurableSpace α✝
p : ℝ≥0∞
q : ℝ
μ ν : Measure α✝
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
α : Type u_1
inst✝ : LinearOrderedSemiring α
b : α
hb : b < 0
ha hc : 0 ≤ 0
⊢ 0 ≤ b * 0
case mpr
α✝ : Type ?u.5062900
E : Type ?u.5062903
F : Type ?u.5062906
G : Type ?u.5062909
m m0 : MeasurableSpace α✝
p : ℝ≥0∞
q : ℝ
μ ν : Measure α✝
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
α : Type u_1
inst✝ : LinearOrderedSemiring α
a b c : α
ha : 0 ≤ a
hb : b < 0
hc : 0 ≤ c
⊢ a = 0 ∧ c = 0 → a ≤ b * c
rintro ⟨rfl, rfl⟩
no goals
case mpr.intro
α✝ : Type ?u.5062900
E : Type ?u.5062903
F : Type ?u.5062906
G : Type ?u.5062909
m m0 : MeasurableSpace α✝
p : ℝ≥0∞
q : ℝ
μ ν : Measure α✝
inst✝³ : NormedAddCommGroup E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
α : Type u_1
inst✝ : LinearOrderedSemiring α
b : α
hb : b < 0
ha hc : 0 ≤ 0
⊢ 0 ≤ b * 0
rw [MulZeroClass.mul_zero]