case top
α : Type ?u.836153
β : Type ?u.836156
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ENNReal.toNNReal ⊤⁻¹ = (ENNReal.toNNReal ⊤)⁻¹

case coe
α : Type ?u.836153
β : Type ?u.836156
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
⊢ ENNReal.toNNReal (↑a)⁻¹ = (ENNReal.toNNReal ↑a)⁻¹
α : Type ?u.836153
β : Type ?u.836156
a✝ b c d : ℝ≥0∞
r p q : ℝ≥0
a : ℝ≥0∞
⊢ ENNReal.toNNReal a⁻¹ = (ENNReal.toNNReal a)⁻¹
induction' a using recTopCoe with a
case coe.inl
α : Type ?u.836153
β : Type ?u.836156
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ENNReal.toNNReal (↑0)⁻¹ = (ENNReal.toNNReal ↑0)⁻¹

case coe.inr
α : Type ?u.836153
β : Type ?u.836156
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
ha : a ≠ 0
⊢ ENNReal.toNNReal (↑a)⁻¹ = (ENNReal.toNNReal ↑a)⁻¹
case coe
α : Type ?u.836153
β : Type ?u.836156
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
⊢ ENNReal.toNNReal (↑a)⁻¹ = (ENNReal.toNNReal ↑a)⁻¹
rcases eq_or_ne a 0 with (rfl | ha)
no goals
case coe.inr
α : Type ?u.836153
β : Type ?u.836156
a✝ b c d : ℝ≥0∞
r p q a : ℝ≥0
ha : a ≠ 0
⊢ ENNReal.toNNReal (↑a)⁻¹ = (ENNReal.toNNReal ↑a)⁻¹
rw [← coe_inv ha, toNNReal_coe, toNNReal_coe]
no goals
case top
α : Type ?u.836153
β : Type ?u.836156
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ENNReal.toNNReal ⊤⁻¹ = (ENNReal.toNNReal ⊤)⁻¹
simp
no goals
case coe.inl
α : Type ?u.836153
β : Type ?u.836156
a b c d : ℝ≥0∞
r p q : ℝ≥0
⊢ ENNReal.toNNReal (↑0)⁻¹ = (ENNReal.toNNReal ↑0)⁻¹
simp