case intro
α : Type ?u.80550
β : Type ?u.80553
a b c d : ℝ≥0∞
r p q : ℝ≥0
r₂ : ℝ≥0∞
h₂ : r₂ ≠ ⊤
r₁ : ℝ≥0
⊢ ENNReal.toNNReal (↑r₁ + r₂) = ENNReal.toNNReal ↑r₁ + ENNReal.toNNReal r₂
α : Type ?u.80550
β : Type ?u.80553
a b c d : ℝ≥0∞
r p q : ℝ≥0
r₁ r₂ : ℝ≥0∞
h₁ : r₁ ≠ ⊤
h₂ : r₂ ≠ ⊤
⊢ ENNReal.toNNReal (r₁ + r₂) = ENNReal.toNNReal r₁ + ENNReal.toNNReal r₂
lift r₁ to ℝ≥0 using h₁
case intro.intro
α : Type ?u.80550
β : Type ?u.80553
a b c d : ℝ≥0∞
r p q r₁ r₂ : ℝ≥0
⊢ ENNReal.toNNReal (↑r₁ + ↑r₂) = ENNReal.toNNReal ↑r₁ + ENNReal.toNNReal ↑r₂
case intro
α : Type ?u.80550
β : Type ?u.80553
a b c d : ℝ≥0∞
r p q : ℝ≥0
r₂ : ℝ≥0∞
h₂ : r₂ ≠ ⊤
r₁ : ℝ≥0
⊢ ENNReal.toNNReal (↑r₁ + r₂) = ENNReal.toNNReal ↑r₁ + ENNReal.toNNReal r₂
lift r₂ to ℝ≥0 using h₂
no goals
case intro.intro
α : Type ?u.80550
β : Type ?u.80553
a b c d : ℝ≥0∞
r p q r₁ r₂ : ℝ≥0
⊢ ENNReal.toNNReal (↑r₁ + ↑r₂) = ENNReal.toNNReal ↑r₁ + ENNReal.toNNReal ↑r₂
rfl