rw [integral_finset_sum]
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
⊢ ∫ (ω : Ω), ∑ c : EdgeType V, ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) c) = x})) ω ∂μ =
    ↑(Nat.choose n 2) * ↑p
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 : EdgeType V, ∫ (a : Ω), ↑(EdgeInd G (_ : ∀ (x : ℝ), MeasurableSet {ω | ↑(EdgeInd' (G ω) i) = x})) a ∂μ =
    ↑(Nat.choose n 2) * ↑p

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})) ω