α : Type ?u.833800
β : Type ?u.833803
γ : Type ?u.833806
δ : Type ?u.833809
inst✝ : MeasurableSpace α
K : Type ?u.833815
q : ℚ
⊢ ENNReal.ofReal ↑(Option.getD (Option.some q) 0) = ↑(Real.toNNReal ↑q)
α : Type ?u.833800
β : Type ?u.833803
γ : Type ?u.833806
δ : Type ?u.833809
inst✝ : MeasurableSpace α
K : Type ?u.833815
q : ℚ
⊢ ennrealRatEmbed (Encodable.encode q) = ↑(Real.toNNReal ↑q)
rw [ennrealRatEmbed, Encodable.encodek]
no goals
α : Type ?u.833800
β : Type ?u.833803
γ : Type ?u.833806
δ : Type ?u.833809
inst✝ : MeasurableSpace α
K : Type ?u.833815
q : ℚ
⊢ ENNReal.ofReal ↑(Option.getD (Option.some q) 0) = ↑(Real.toNNReal ↑q)
rfl