simp only [Finset.mem_univ, integrable, forall_true_left, Subtype.forall, implies_true]
case hf
V : Type
Ω : Type u_1
inst✝⁴ : Fintype V
inst✝³ : DecidableEq V
inst✝² : MeasurableSpace Ω
μ : Measure Ω
inst✝¹ : IsProbabilityMeasure μ
G : Ω → SimpleGraph V
inst✝ : (ω : Ω) → (e : EdgeType V) → Decidable (Edge (G ω) e)
p : NNReal
n : ℕ
h : ErdosRenyi G p μ
hn : Fintype.card V = n
⊢ ∀ i ∈ Finset.univ, Integrable fun ω => ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) ω
no goals