case intro
α : Type ?u.327971
β : Type ?u.327974
b c d : ℝ≥0∞
r p q a : ℝ≥0
⊢ ↑a - ↑a / 2 = ↑a / 2
α : Type ?u.327971
β : Type ?u.327974
a b c d : ℝ≥0∞
r p q : ℝ≥0
h : a ≠ ⊤
⊢ a - a / 2 = a / 2
lift a to ℝ≥0 using h
no goals
case intro
α : Type ?u.327971
β : Type ?u.327974
b c d : ℝ≥0∞
r p q a : ℝ≥0
⊢ ↑a - ↑a / 2 = ↑a / 2
exact sub_eq_of_add_eq (mul_ne_top coe_ne_top <| by simp) (ENNReal.add_halves a)
no goals
α : Type ?u.327971
β : Type ?u.327974
b c d : ℝ≥0∞
r p q a : ℝ≥0
⊢ 2⁻¹ ≠ ⊤
simp