case intro
α : Type ?u.827878
β : Type ?u.827881
b c d : ℝ≥0∞
r p q : ℝ≥0
hb : b ≠ ⊤
a : ℝ≥0
⊢ ENNReal.toReal ↑a = ENNReal.toReal b ↔ ↑a = b
α : Type ?u.827878
β : Type ?u.827881
a b c d : ℝ≥0∞
r p q : ℝ≥0
ha : a ≠ ⊤
hb : b ≠ ⊤
⊢ ENNReal.toReal a = ENNReal.toReal b ↔ a = b
lift a to ℝ≥0 using ha
case intro.intro
α : Type ?u.827878
β : Type ?u.827881
c d : ℝ≥0∞
r p q a b : ℝ≥0
⊢ ENNReal.toReal ↑a = ENNReal.toReal ↑b ↔ ↑a = ↑b
case intro
α : Type ?u.827878
β : Type ?u.827881
b c d : ℝ≥0∞
r p q : ℝ≥0
hb : b ≠ ⊤
a : ℝ≥0
⊢ ENNReal.toReal ↑a = ENNReal.toReal b ↔ ↑a = b
lift b to ℝ≥0 using hb
no goals
case intro.intro
α : Type ?u.827878
β : Type ?u.827881
c d : ℝ≥0∞
r p q a b : ℝ≥0
⊢ ENNReal.toReal ↑a = ENNReal.toReal ↑b ↔ ↑a = ↑b
simp only [coe_eq_coe, NNReal.coe_eq, coe_toReal]