awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
this : HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'
h₁ :
  ∀ (x : ℕ) (x_1 : Ω),
    (√(↑x : ℝ))⁻¹ * (∑ k ∈ Finset.range x, X k x_1 - HMul.hMul (α := ℝ) (↑x : ℝ) (∫ (x : Ω), X 0 x ∂P)) =
      ((fun (x : ℝ) ↦ √Var[X 0; P] * x) ∘ fun (ω : Ω) ↦
          (√((↑x : ℝ) * Var[X 0; P]))⁻¹ *
            (∑ k ∈ Finset.range x, X k ω - HMul.hMul (α := ℝ) (↑x : ℝ) (∫ (x : Ω), X 0 x ∂P)))
        x_1
⊢ TendstoInDistribution (Ω := fun (n : ℕ) ↦ Ω) (m := fun (i : ℕ) ↦ mΩ) (mE := Real.measurableSpace)
    (fun (n : ℕ) (ω : Ω) ↦
      (√(↑n : ℝ))⁻¹ * (∑ k ∈ Finset.range n, X k ω - HMul.hMul (α := ℝ) (↑n : ℝ) (∫ (x : Ω), X 0 x ∂P)))
    atTop Y (fun (x : ℕ) ↦ P) P'
have h₂ : Y = (fun (x : ℝ) ↦ √Var[X 0; P] * x) ∘ fun (ω : Ω') ↦ Y ω / √Var[X 0; P]
Tactic: convert!
    (tendstoInDistribution_inv_sqrt_mul_var_mul_sum_sub this h hindep hident).continuous_comp (g :=
      (√Var[X 0; P] * ·)) (by fun_prop)
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
this : HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'
x : ℕ
x_1 : Ω
⊢ (√(↑x : ℝ))⁻¹ * (∑ k ∈ Finset.range x, X k x_1 - HMul.hMul (α := ℝ) (↑x : ℝ) (∫ (x : Ω), X 0 x ∂P)) =
    ((fun (x : ℝ) ↦ √Var[X 0; P] * x) ∘ fun (ω : Ω) ↦
        (√((↑x : ℝ) * Var[X 0; P]))⁻¹ *
          (∑ k ∈ Finset.range x, X k ω - HMul.hMul (α := ℝ) (↑x : ℝ) (∫ (x : Ω), X 0 x ∂P)))
      x_1
have h₁ : (∑ k ∈ Finset.range x, X k x_1 - HMul.hMul (α := ℝ) (↑x : ℝ) (∫ (x : Ω), X 0 x ∂P)) / √(↑x : ℝ) =
  (∑ k ∈ Finset.range x, X k x_1 - HMul.hMul (α := ℝ) (↑x : ℝ) (∫ (x : Ω), X 0 x ∂P)) * √Var[X 0; P] /
    (√(↑x : ℝ) * √Var[X 0; P])
Tactic: simp [field]
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
this : HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'
⊢ Y = (fun (x : ℝ) ↦ √Var[X 0; P] * x) ∘ fun (ω : Ω') ↦ Y ω / √Var[X 0; P]
have h₁ : ∀ (x : Ω'), Y x = ((fun (x : ℝ) ↦ √Var[X 0; P] * x) ∘ fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.CentralLimitTheorem (goal)
Goal:
Ω : Type u_1
Ω' : Type u_2
mΩ : MeasurableSpace Ω
mΩ' : MeasurableSpace Ω'
P : Measure Ω
P' : Measure Ω'
X : ℕ → Ω → ℝ
Y : Ω' → ℝ
inst : IsProbabilityMeasure P
inst_1 : IsProbabilityMeasure P'
hY : HasLaw Y (gaussianReal 0 Var[X 0; P].toNNReal) P'
hX : MemLp (X 0) 2 P
hindep : iIndepFun (β := fun (x : ℕ) ↦ ℝ) X P
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) P P
h : Var[X 0; P] ≠ 0
this : HasLaw (fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) (gaussianReal 0 1) P'
x : Ω'
⊢ Y x = ((fun (x : ℝ) ↦ √Var[X 0; P] * x) ∘ fun (ω : Ω') ↦ Y ω / √Var[X 0; P]) x
have h₁ : Y x = Y x * √Var[X 0; P] / √Var[X 0; P]
Tactic: simp [field]
-- Lean 4 proof step from Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs (goal)
Goal:
V : Type u_1
p : (↑I : Type)
inst : Countable V
S : Set (SimpleGraph V)
⊢ Eq (α := ENNReal) ((G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) S : ENNReal)
    (((setBer(Sym2.diagSetᶜ, p) : Measure (Set (Sym2 V))) : (a : Set (Set (Sym2 V))) → ENNReal) (edgeSet '' S) :
      ENNReal)
have rw : Eq (α := ENNReal)
  (((comap edgeSet setBer(Sym2.diagSetᶜ, p) : Measure (SimpleGraph V)) : (a : Set (SimpleGraph V)) → ENNReal) S :
    ENNReal)
  (((setBer(Sym2.diagSetᶜ, p) : Measure (Set (Sym2 V))) : (a : Set (Set (Sym2 V))) → ENNReal) (edgeSet '' S) : ENNReal)
Tactic: rw [binomialRandom, measurableEmbedding_edgeSet.comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs (goal)
Goal:
V : Type u_1
p : (↑I : Type)
inst : Countable V
S : Set (SimpleGraph V)
rw :
  Eq (α := ENNReal)
    (((comap edgeSet setBer(Sym2.diagSetᶜ, p) : Measure (SimpleGraph V)) : (a : Set (SimpleGraph V)) → ENNReal) S :
      ENNReal)
    (((setBer(Sym2.diagSetᶜ, p) : Measure (Set (Sym2 V))) : (a : Set (Set (Sym2 V))) → ENNReal) (edgeSet '' S) :
      ENNReal)
⊢ Eq (α := ENNReal) ((G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) S : ENNReal)
    (((setBer(Sym2.diagSetᶜ, p) : Measure (Set (Sym2 V))) : (a : Set (Set (Sym2 V))) → ENNReal) (edgeSet '' S) :
      ENNReal)
have rw₁ : Eq (α := ENNReal)
  (((setBer(Sym2.diagSetᶜ, p) : Measure (Set (Sym2 V))) : (a : Set (Set (Sym2 V))) → ENNReal) (edgeSet '' S) : ENNReal)
  (((setBer(Sym2.diagSetᶜ, p) : Measure (Set (Sym2 V))) : (a : Set (Set (Sym2 V))) → ENNReal) (edgeSet '' S) : ENNReal)
Tactic: rw [binomialRandom, measurableEmbedding_edgeSet.comap_apply]
-- Lean 4 proof step from Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs (goal)
Goal:
V : Type u_1
p : (↑I : Type)
inst : Countable V
⊢ IsProbabilityMeasure G(V, p)
have refine : ∀ᵐ (a : Set (Sym2 V)) ∂setBer(Sym2.diagSetᶜ, p), Membership.mem (γ := Set (Set (Sym2 V))) (Set.range edgeSet) a
Tactic: refine measurableEmbedding_edgeSet.isProbabilityMeasure_comap ?_
-- Lean 4 proof step from Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs (goal)
Goal:
V : Type u_1
p : (↑I : Type)
inst : Countable V
⊢ ∀ᵐ (a : Set (Sym2 V)) ∂setBer(Sym2.diagSetᶜ, p), Membership.mem (γ := Set (Set (Sym2 V))) (Set.range edgeSet) a
have h : ∀ (s : Set (Sym2 V)) (hs : s ⊆ Sym2.diagSetᶜ), Membership.mem (γ := Set (Set (Sym2 V))) (Set.range edgeSet) s
Tactic: filter_upwards [setBernoulli_ae_subset] with s hs
-- Lean 4 proof step from Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs (goal)
Goal:
V : Type u_1
p : (↑I : Type)
inst : Countable V
s : Set (Sym2 V)
hs : s ⊆ Sym2.diagSetᶜ
⊢ Membership.mem (γ := Set (Set (Sym2 V))) (Set.range edgeSet) s
have h : (fromEdgeSet s).edgeSet = s
Tactic: refine ⟨.fromEdgeSet s, ?_⟩
-- Lean 4 proof step from Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs (goal)
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
⊢ (G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) {G} =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
have intro : ∀ (val : Fintype V),
  (G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) {G} =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
Tactic: cases nonempty_fintype V
-- Lean 4 proof step from Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs (goal)
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
val : Fintype V
⊢ (G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) {G} =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
have intro : (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard * (↑(toNNReal (σ p)) : ENNReal) ^ (Sym2.diagSetᶜ \ G.edgeSet).ncard =
  (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
    (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
Tactic: simp only [binomialRandom, measurableEmbedding_edgeSet.comap_apply, Set.image_singleton,
    edgeSet_subset_compl_diagSet, setBernoulli_singleton, Set.toFinite]
-- Lean 4 proof step from Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs (goal)
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
val : Fintype V
⊢ (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard * (↑(toNNReal (σ p)) : ENNReal) ^ (Sym2.diagSetᶜ \ G.edgeSet).ncard =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
have intro : (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
    (↑(toNNReal (σ p)) : ENNReal) ^ (Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ - G.edgeSet.ncard) =
  (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
    (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
Tactic: rw [Set.ncard_diff (by simp)]
-- Lean 4 proof step from Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs (goal)
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
val : Fintype V
⊢ (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ (Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ - G.edgeSet.ncard) =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
have intro : Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = (Nat.card V).choose 2
Tactic: congr!
-- Lean 4 proof step from Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs (goal)
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
val : Fintype V
⊢ Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = (Nat.card V).choose 2
have intro : Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = (Fintype.card V).choose 2
Tactic: rw [Nat.card_eq_fintype_card, ← Sym2.card_diagSet_compl, Fintype.card_eq_nat_card,
    ← Nat.card_coe_set_eq]
-- Lean 4 proof step from Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs (goal)
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
val : Fintype V
intro : Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = (Fintype.card V).choose 2
⊢ Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = (Nat.card V).choose 2
have intro₁ : Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = Fintype.card.{u_1} (↑Sym2.diagSetᶜ : Type u_1)
Tactic: rw [Nat.card_eq_fintype_card, ← Sym2.card_diagSet_compl, Fintype.card_eq_nat_card,
    ← Nat.card_coe_set_eq]
-- Lean 4 proof step from Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs (goal)
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
val : Fintype V
intro : Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = (Fintype.card V).choose 2
intro₁ : Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = Fintype.card.{u_1} (↑Sym2.diagSetᶜ : Type u_1)
⊢ Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = (Nat.card V).choose 2
have intro₂ : Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = Nat.card.{u_1} (↑Sym2.diagSetᶜ : Type u_1)
Tactic: rw [Nat.card_eq_fintype_card, ← Sym2.card_diagSet_compl, Fintype.card_eq_nat_card,
    ← Nat.card_coe_set_eq]
-- Lean 4 proof step from Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs (goal)
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
val : Fintype V
intro : Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = (Fintype.card V).choose 2
intro₁ : Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = Fintype.card.{u_1} (↑Sym2.diagSetᶜ : Type u_1)
intro₂ : Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = Nat.card.{u_1} (↑Sym2.diagSetᶜ : Type u_1)
⊢ Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = (Nat.card V).choose 2
have intro₃ : Nat.card.{u_1} (↑Sym2.diagSetᶜ : Type u_1) = Nat.card.{u_1} (↑Sym2.diagSetᶜ : Type u_1)
Tactic: rw [Nat.card_eq_fintype_card, ← Sym2.card_diagSet_compl, Fintype.card_eq_nat_card,
    ← Nat.card_coe_set_eq]
-- Lean 4 proof step from Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs (goal)
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
⊢ (G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) {G} =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
have intro : ∀ (val : Fintype V),
  (G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) {G} =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
Tactic: classical
  cases nonempty_fintype V
  simp only [binomialRandom, measurableEmbedding_edgeSet.comap_apply, Set.image_singleton,
    edgeSet_subset_compl_diagSet, setBernoulli_singleton, Set.toFinite]
  rw [Set.ncard_diff (by simp)]
  congr!
  rw [Nat.card_eq_fintype_card, ← Sym2.card_diagSet_compl, Fintype.card_eq_nat_card,
    ← Nat.card_coe_set_eq]
-- Lean 4 proof step from Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs (goal)
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
intro :
  ∀ (val : Fintype V),
    (G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) {G} =
      (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
        (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
⊢ (G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) {G} =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
have intro₁ : ∀ (val : Fintype V),
  (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard * (↑(toNNReal (σ p)) : ENNReal) ^ (Sym2.diagSetᶜ \ G.edgeSet).ncard =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
Tactic: classical
  cases nonempty_fintype V
  simp only [binomialRandom, measurableEmbedding_edgeSet.comap_apply, Set.image_singleton,
    edgeSet_subset_compl_diagSet, setBernoulli_singleton, Set.toFinite]
  rw [Set.ncard_diff (by simp)]
  congr!
  rw [Nat.card_eq_fintype_card, ← Sym2.card_diagSet_compl, Fintype.card_eq_nat_card,
    ← Nat.card_coe_set_eq]
-- Lean 4 proof step from Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs (goal)
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
intro :
  ∀ (val : Fintype V),
    (G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) {G} =
      (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
        (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
intro₁ :
  ∀ (val : Fintype V),
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard * (↑(toNNReal (σ p)) : ENNReal) ^ (Sym2.diagSetᶜ \ G.edgeSet).ncard =
      (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
        (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
⊢ (G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) {G} =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
have intro₂ : ∀ (val : Fintype V),
  (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ (Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ - G.edgeSet.ncard) =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
Tactic: classical
  cases nonempty_fintype V
  simp only [binomialRandom, measurableEmbedding_edgeSet.comap_apply, Set.image_singleton,
    edgeSet_subset_compl_diagSet, setBernoulli_singleton, Set.toFinite]
  rw [Set.ncard_diff (by simp)]
  congr!
  rw [Nat.card_eq_fintype_card, ← Sym2.card_diagSet_compl, Fintype.card_eq_nat_card,
    ← Nat.card_coe_set_eq]
-- Lean 4 proof step from Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs (goal)
Goal:
V : Type u_1
p : (↑I : Type)
inst : Finite V
G : SimpleGraph V
intro :
  ∀ (val : Fintype V),
    (G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) {G} =
      (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
        (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
intro₁ :
  ∀ (val : Fintype V),
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard * (↑(toNNReal (σ p)) : ENNReal) ^ (Sym2.diagSetᶜ \ G.edgeSet).ncard =
      (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
        (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
intro₂ :
  ∀ (val : Fintype V),
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
        (↑(toNNReal (σ p)) : ENNReal) ^ (Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ - G.edgeSet.ncard) =
      (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
        (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
⊢ (G(V, p) : (a : Set (SimpleGraph V)) → ENNReal) {G} =
    (↑(toNNReal p) : ENNReal) ^ G.edgeSet.ncard *
      (↑(toNNReal (σ p)) : ENNReal) ^ ((Nat.card V).choose 2 - G.edgeSet.ncard)
have intro₃ : ∀ (val : Fintype V), Set.ncard.{u_1} (α := Sym2 V) Sym2.diagSetᶜ = (Nat.card V).choose 2
Tactic: classical
  cases nonempty_fintype V
  simp only [binomialRandom, measurableEmbedding_edgeSet.comap_apply, Set.image_singleton,
    edgeSet_subset_compl_diagSet, setBernoulli_singleton, Set.toFinite]
  rw [Set.ncard_diff (by simp)]
  congr!
  rw [Nat.card_eq_fintype_card, ← Sym2.card_diagSet_compl, Fintype.card_eq_nat_card,
    ← Nat.card_coe_set_eq]
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : ¬m ≤ m₀
⊢ Var[X; μ | m] = 0
have rw : μ[HPow.hPow (β := ℕ) (X - μ[X | m]) 2 | m] = 0
Tactic: rw [condVar, condExp_of_not_le hm]
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : ¬m ≤ m₀
rw : μ[HPow.hPow (β := ℕ) (X - μ[X | m]) 2 | m] = 0
⊢ Var[X; μ | m] = 0
have rw₁ : Eq.{u_1 + 1} (α := Ω → ℝ) 0 0
Tactic: rw [condVar, condExp_of_not_le hm]
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
hm : m ≤ m₀
X : Ω → ℝ
μ : Measure Ω
hμm : ¬SigmaFinite (μ.trim hm)
⊢ Var[X; μ | m] = 0
have rw : μ[HPow.hPow (β := ℕ) (X - μ[X | m]) 2 | m] = 0
Tactic: rw [condVar, condExp_of_not_sigmaFinite hm hμm]
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
hm : m ≤ m₀
X : Ω → ℝ
μ : Measure Ω
hμm : ¬SigmaFinite (μ.trim hm)
rw : μ[HPow.hPow (β := ℕ) (X - μ[X | m]) 2 | m] = 0
⊢ Var[X; μ | m] = 0
have rw₁ : Eq.{u_1 + 1} (α := Ω → ℝ) 0 0
Tactic: rw [condVar, condExp_of_not_sigmaFinite hm hμm]
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
⊢ Var[fun (x : Ω) ↦ c; μ | m] = 0
have inl : Var[fun (x : Ω) ↦ 0; μ | m] = 0
Tactic: obtain rfl | hc := eq_or_ne c 0
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
inl : Var[fun (x : Ω) ↦ 0; μ | m] = 0
⊢ Var[fun (x : Ω) ↦ c; μ | m] = 0
have inr : ∀ (hc : c ≠ 0), Var[fun (x : Ω) ↦ c; μ | m] = 0
Tactic: obtain rfl | hc := eq_or_ne c 0
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
⊢ Var[fun (x : Ω) ↦ c; μ | m] = 0
have pos : ∀ (hμm : IsFiniteMeasure μ), Var[fun (x : Ω) ↦ c; μ | m] = 0
Tactic: by_cases hμm : IsFiniteMeasure μ
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
μ : Measure Ω
hm : m ≤ m₀
c : ℝ
hc : c ≠ 0
pos : ∀ (hμm : IsFiniteMeasure μ), Var[fun (x : Ω) ↦ c; μ | m] = 0
⊢ Var[fun (x : Ω) ↦ c; μ | m] = 0
have neg : ∀ (hμm : ¬IsFiniteMeasure μ), Var[fun (x : Ω) ↦ c; μ | m] = 0
Tactic: by_cases hμm : IsFiniteMeasure μ
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
⊢ HPow.hPow (β := ℕ) (X - μ[X | m]) 2 =ᶠ[ae μ] HPow.hPow (β := ℕ) (Y - μ[Y | m]) 2
have h₁ : ∀ (ω : Ω) (hω : X ω = Y ω) (hω' : μ[X | m] ω = μ[Y | m] ω),
  HPow.hPow (β := ℕ) (X - μ[X | m]) 2 ω = HPow.hPow (β := ℕ) (Y - μ[Y | m]) 2 ω
Tactic: filter_upwards [h, condExp_congr_ae h] with ω hω hω'
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
ω : Ω
hω : X ω = Y ω
hω' : μ[X | m] ω = μ[Y | m] ω
⊢ HPow.hPow (β := ℕ) (X ω - μ[X | m] ω) 2 = HPow.hPow (β := ℕ) (Y ω - μ[Y | m] ω) 2
have h₁ : HPow.hPow (β := ℕ) (Y ω - μ[X | m] ω) 2 = HPow.hPow (β := ℕ) (Y ω - μ[Y | m] ω) 2
Tactic: rw [hω, hω']
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X Y : Ω → ℝ
μ : Measure Ω
h : X =ᶠ[ae μ] Y
ω : Ω
hω : X ω = Y ω
hω' : μ[X | m] ω = μ[Y | m] ω
h₁ : HPow.hPow (β := ℕ) (Y ω - μ[X | m] ω) 2 = HPow.hPow (β := ℕ) (Y ω - μ[Y | m] ω) 2
⊢ HPow.hPow (β := ℕ) (X ω - μ[X | m] ω) 2 = HPow.hPow (β := ℕ) (Y ω - μ[Y | m] ω) 2
have h₂ : HPow.hPow (β := ℕ) (Y ω - μ[Y | m] ω) 2 = HPow.hPow (β := ℕ) (Y ω - μ[Y | m] ω) 2
Tactic: rw [hω, hω']
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ Var[X; μ | m] = μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m]
have rw : μ[HPow.hPow (β := ℕ) (X - μ[X | m]) 2 | m] =
  μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m]
Tactic: rw [condVar, sub_sq]
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
rw :
  μ[HPow.hPow (β := ℕ) (X - μ[X | m]) 2 | m] =
    μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m]
⊢ Var[X; μ | m] = μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m]
have rw₁ : μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] =
  μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m]
Tactic: rw [condVar, sub_sq]
-- Lean 4 proof step from Mathlib.Probability.CondVar (hypothesis)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
⊢ μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] =ᶠ[ae μ]
    μ[HPow.hPow (β := ℕ) X 2 | m] - 2 * HPow.hPow (β := ℕ) μ[X | m] 2 + HPow.hPow (β := ℕ) μ[X | m] 2
have aux₀ : Integrable (HPow.hPow (β := ℕ) X 2) μ
Tactic: have aux₀ : Integrable (X ^ 2) μ := hX.integrable_sq
-- Lean 4 proof step from Mathlib.Probability.CondVar (goal)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (HPow.hPow (β := ℕ) X 2) μ
⊢ Integrable (2 * X * μ[X | m]) μ
have rw : Integrable (2 * (X * μ[X | m])) μ
Tactic: rw [mul_assoc]
-- Lean 4 proof step from Mathlib.Probability.CondVar (hypothesis)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (HPow.hPow (β := ℕ) X 2) μ
⊢ μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] =ᶠ[ae μ]
    μ[HPow.hPow (β := ℕ) X 2 | m] - 2 * HPow.hPow (β := ℕ) μ[X | m] 2 + HPow.hPow (β := ℕ) μ[X | m] 2
have aux₁ : Integrable (2 * X * μ[X | m]) μ
Tactic: have aux₁ : Integrable (2 * X * μ[X | m]) μ := by
        rw [mul_assoc]
        exact (memLp_one_iff_integrable.1 <| hX.condExp.mul hX).const_mul _
-- Lean 4 proof step from Mathlib.Probability.CondVar (hypothesis)
Goal:
Ω : Type u_1
m₀ m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
hm : m ≤ m₀
inst : IsFiniteMeasure μ
hX : MemLp X 2 μ
aux₀ : Integrable (HPow.hPow (β := ℕ) X 2) μ
aux₁ : Integrable (2 * X * μ[X | m]) μ
⊢ μ[HPow.hPow (β := ℕ) X 2 - 2 * X * μ[X | m] + HPow.hPow (β := ℕ) μ[X | m] 2 | m] =ᶠ[ae μ]
    μ[HPow.hPow (β := ℕ) X 2 | m] - 2 * HPow.hPow (β := ℕ) μ[X | m] 2 + HPow.hPow (β := ℕ) μ[X | m] 2
have aux₂ : Integrable (HPow.hPow (β := ℕ) μ[X | m] 2) μ
Tactic: have aux₂ : Integrable (μ[X | m] ^ 2) μ := hX.condExp.integrable_sq