α : Type ?u.142320
β : Type ?u.142323
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : a = ⊤ → b = ⊤
h_nnreal : a ≠ ⊤ → b ≠ ⊤ → ENNReal.toNNReal a ≤ ENNReal.toNNReal b
hlt : b < a
⊢ False
α : Type ?u.142320
β : Type ?u.142323
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : a = ⊤ → b = ⊤
h_nnreal : a ≠ ⊤ → b ≠ ⊤ → ENNReal.toNNReal a ≤ ENNReal.toNNReal b
⊢ a ≤ b
by_contra' hlt
case intro
α : Type ?u.142320
β : Type ?u.142323
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
b : ℝ≥0
h : a = ⊤ → ↑b = ⊤
h_nnreal : a ≠ ⊤ → ↑b ≠ ⊤ → ENNReal.toNNReal a ≤ ENNReal.toNNReal ↑b
hlt : ↑b < a
⊢ False
α : Type ?u.142320
β : Type ?u.142323
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a b : ℝ≥0∞
h : a = ⊤ → b = ⊤
h_nnreal : a ≠ ⊤ → b ≠ ⊤ → ENNReal.toNNReal a ≤ ENNReal.toNNReal b
hlt : b < a
⊢ False
lift b to ℝ≥0 using hlt.ne_top
case intro.intro
α : Type ?u.142320
β : Type ?u.142323
a✝ b✝ c d : ℝ≥0∞
r p q b a : ℝ≥0
h : ↑a = ⊤ → ↑b = ⊤
h_nnreal : ↑a ≠ ⊤ → ↑b ≠ ⊤ → ENNReal.toNNReal ↑a ≤ ENNReal.toNNReal ↑b
hlt : ↑b < ↑a
⊢ False
case intro
α : Type ?u.142320
β : Type ?u.142323
a✝ b✝ c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
b : ℝ≥0
h : a = ⊤ → ↑b = ⊤
h_nnreal : a ≠ ⊤ → ↑b ≠ ⊤ → ENNReal.toNNReal a ≤ ENNReal.toNNReal ↑b
hlt : ↑b < a
⊢ False
lift a to ℝ≥0 using mt h coe_ne_top
case intro.intro
α : Type ?u.142320
β : Type ?u.142323
a✝ b✝ c d : ℝ≥0∞
r p q b a : ℝ≥0
h : ↑a = ⊤ → ↑b = ⊤
h_nnreal : ↑a ≠ ⊤ → ↑b ≠ ⊤ → ENNReal.toNNReal ↑a ≤ ENNReal.toNNReal ↑b
hlt : ↑b < ↑a
⊢ ↑a ≤ ↑b
case intro.intro
α : Type ?u.142320
β : Type ?u.142323
a✝ b✝ c d : ℝ≥0∞
r p q b a : ℝ≥0
h : ↑a = ⊤ → ↑b = ⊤
h_nnreal : ↑a ≠ ⊤ → ↑b ≠ ⊤ → ENNReal.toNNReal ↑a ≤ ENNReal.toNNReal ↑b
hlt : ↑b < ↑a
⊢ False
refine hlt.not_le ?_
no goals
case intro.intro
α : Type ?u.142320
β : Type ?u.142323
a✝ b✝ c d : ℝ≥0∞
r p q b a : ℝ≥0
h : ↑a = ⊤ → ↑b = ⊤
h_nnreal : ↑a ≠ ⊤ → ↑b ≠ ⊤ → ENNReal.toNNReal ↑a ≤ ENNReal.toNNReal ↑b
hlt : ↑b < ↑a
⊢ ↑a ≤ ↑b
simpa using h_nnreal