awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg :
  ∀ (n : ℕ),
    AEStronglyMeasurable.{u_1, u_2} (β := E)
      (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) μ
⊢ Tendsto (β := ℝ≥0∞)
    (fun (n : ℕ) ↦
      eLpNorm.{u_1, u_2} (ε := E)
        (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω) - ∫ (x : Ω), X 0 x ∂μ) p μ)
    atTop (𝓝 0)
have neg : UnifIntegrable.{u_1, u_2, 0} (β := E)
  (fun (n : ℕ) (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) p μ
Tactic: refine tendsto_Lp_finite_of_tendstoInMeasure hp hp' havg (memLp_const _) ?_
    (tendstoInMeasure_of_tendsto_ae havg (strong_law_ae _ hint hindep hident))
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg :
  ∀ (n : ℕ),
    AEStronglyMeasurable.{u_1, u_2} (β := E)
      (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) μ
⊢ UnifIntegrable.{u_1, u_2, 0} (β := E)
    (fun (n : ℕ) (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) p μ
have neg : UnifIntegrable.{u_1, u_2, 0} (β := E) (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := Ω → E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i))
  p μ
Tactic: rw [(_ : (fun (n : ℕ) ω => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i ω))
            = fun (n : ℕ) => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i))]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg :
  ∀ (n : ℕ),
    AEStronglyMeasurable.{u_1, u_2} (β := E)
      (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) μ
neg :
  UnifIntegrable.{u_1, u_2, 0} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := Ω → E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i)) p μ
⊢ UnifIntegrable.{u_1, u_2, 0} (β := E)
    (fun (n : ℕ) (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) p μ
have rw : Eq (α := (n : ℕ) → (ω : Ω) → E) (fun (n : ℕ) (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω))
  fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := Ω → E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i)
Tactic: rw [(_ : (fun (n : ℕ) ω => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i ω))
            = fun (n : ℕ) => (n : ℝ)⁻¹ • (∑ i ∈ range n, X i))]
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg :
  ∀ (n : ℕ),
    AEStronglyMeasurable.{u_1, u_2} (β := E)
      (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) μ
⊢ UnifIntegrable.{u_1, u_2, 0} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := Ω → E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i)) p μ
have neg : UniformIntegrable.{u_1, u_2, 0} (β := E)
  (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := Ω → E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i)) p μ
Tactic: apply UniformIntegrable.unifIntegrable
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg :
  ∀ (n : ℕ),
    AEStronglyMeasurable.{u_1, u_2} (β := E)
      (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) μ
⊢ UniformIntegrable.{u_1, u_2, 0} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := Ω → E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i)) p μ
have neg : UniformIntegrable X p μ
Tactic: apply uniformIntegrable_average hp
-- Lean 4 proof step from Mathlib.Probability.StrongLaw (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
μ : Measure Ω
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
inst_3 : MeasurableSpace E
inst_4 : BorelSpace E
p : ℝ≥0∞
hp : 1 ≤ p
hp' : p ≠ ∞
X : ℕ → Ω → E
hℒp : MemLp (X 0) p μ
hindep : Pairwise ((fun (x1 x2 : Ω → E) ↦ x1 ⟂ᵢ[μ] x2) on X)
hident : ∀ (i : ℕ), IdentDistrib (X i) (X 0) μ μ
h : ¬∀ᵐ (ω : Ω) ∂μ, X 0 ω = 0
this : IsProbabilityMeasure μ
hmeas : ∀ (i : ℕ), AEStronglyMeasurable (X i) μ
hint : Integrable (X 0) μ
havg :
  ∀ (n : ℕ),
    AEStronglyMeasurable.{u_1, u_2} (β := E)
      (fun (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) μ
⊢ Eq (α := (n : ℕ) → (ω : Ω) → E)
    (fun (n : ℕ) (ω : Ω) ↦ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω)) fun (n : ℕ) ↦
    HSMul.hSMul (α := ℝ) (β := Ω → E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i)
have h₁ : ∀ (n : ℕ) (ω : Ω),
  HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω) =
    HSMul.hSMul (α := ℝ) (β := Ω → E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i) ω
Tactic: ext n ω
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s t : Set Ω
h : Ne (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (0 : ENNReal)
⊢ s.Finite
have by_contra : ∀ (hs' : ¬s.Finite), False
Tactic: by_contra hs'
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s : Set Ω
hs_fin : s.Finite
hs_nonempty : s.Nonempty
hs_meas : MeasurableSet s
⊢ IsProbabilityMeasure (m0 := inst) (uniformOn s)
have hcs : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (0 : ENNReal)
Tactic: apply cond_isProbabilityMeasure_of_finite
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s : Set Ω
hs_fin : s.Finite
hs_nonempty : s.Nonempty
hs_meas : MeasurableSet s
hcs : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ IsProbabilityMeasure (m0 := inst) (uniformOn s)
have hs : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (⊤ : ENNReal)
Tactic: apply cond_isProbabilityMeasure_of_finite
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_2
inst : DecidableEq Ω
x : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet (↑s : Set Ω)
ht : MeasurableSet (↑t : Set Ω)
⊢ ((uniformOn (↑s : Set Ω) : Measure Ω) : (a : Set Ω) → ENNReal) (↑t : Set Ω) =
    HDiv.hDiv (α := ENNReal) (↑(#(s ∩ t)) : ENNReal) (↑(#s) : ENNReal)
have rw : HMul.hMul (α := ENNReal) (↑(#s) : ENNReal)⁻¹ (↑(#(s ∩ t)) : ENNReal) =
  HDiv.hDiv (α := ENNReal) (↑(#(s ∩ t)) : ENNReal) (↑(#s) : ENNReal)
Tactic: rw [uniformOn, cond_apply hs, Measure.count_apply_finset' hs, ← coe_inter,
    Measure.count_apply_finset']
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_2
inst : DecidableEq Ω
x : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet (↑s : Set Ω)
ht : MeasurableSet (↑t : Set Ω)
rw :
  HMul.hMul (α := ENNReal) (↑(#s) : ENNReal)⁻¹ (↑(#(s ∩ t)) : ENNReal) =
    HDiv.hDiv (α := ENNReal) (↑(#(s ∩ t)) : ENNReal) (↑(#s) : ENNReal)
⊢ ((uniformOn (↑s : Set Ω) : Measure Ω) : (a : Set Ω) → ENNReal) (↑t : Set Ω) =
    HDiv.hDiv (α := ENNReal) (↑(#(s ∩ t)) : ENNReal) (↑(#s) : ENNReal)
have rw₁ : MeasurableSet (↑(s ∩ t) : Set Ω)
Tactic: rw [uniformOn, cond_apply hs, Measure.count_apply_finset' hs, ← coe_inter,
    Measure.count_apply_finset']
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_2
inst : DecidableEq Ω
x : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet (↑s : Set Ω)
ht : MeasurableSet (↑t : Set Ω)
⊢ HMul.hMul (α := ENNReal) (↑(#s) : ENNReal)⁻¹ (↑(#(s ∩ t)) : ENNReal) =
    HDiv.hDiv (α := ENNReal) (↑(#(s ∩ t)) : ENNReal) (↑(#s) : ENNReal)
have rw : HMul.hMul (α := ENNReal) (↑(#s) : ENNReal)⁻¹ (↑(#(s ∩ t)) : ENNReal) =
  HMul.hMul (α := ENNReal) (↑(#(s ∩ t)) : ENNReal) (↑(#s) : ENNReal)⁻¹
Tactic: rw [div_eq_mul_inv, mul_comm]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_2
inst : DecidableEq Ω
x : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet (↑s : Set Ω)
ht : MeasurableSet (↑t : Set Ω)
rw :
  HMul.hMul (α := ENNReal) (↑(#s) : ENNReal)⁻¹ (↑(#(s ∩ t)) : ENNReal) =
    HMul.hMul (α := ENNReal) (↑(#(s ∩ t)) : ENNReal) (↑(#s) : ENNReal)⁻¹
⊢ HMul.hMul (α := ENNReal) (↑(#s) : ENNReal)⁻¹ (↑(#(s ∩ t)) : ENNReal) =
    HDiv.hDiv (α := ENNReal) (↑(#(s ∩ t)) : ENNReal) (↑(#s) : ENNReal)
have rw₁ : HMul.hMul (α := ENNReal) (↑(#(s ∩ t)) : ENNReal) (↑(#s) : ENNReal)⁻¹ =
  HMul.hMul (α := ENNReal) (↑(#(s ∩ t)) : ENNReal) (↑(#s) : ENNReal)⁻¹
Tactic: rw [div_eq_mul_inv, mul_comm]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_2
inst : DecidableEq Ω
x : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet (↑s : Set Ω)
ht : MeasurableSet (↑t : Set Ω)
⊢ MeasurableSet (↑(s ∩ t) : Set Ω)
have rw : MeasurableSet ((↑s : Set Ω) ∩ (↑t : Set Ω))
Tactic: rw [coe_inter]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ IsProbabilityMeasure (m0 := inst) (uniformOn s)
have hcs : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (0 : ENNReal)
Tactic: apply cond_isProbabilityMeasure_of_finite
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' : s.Nonempty
hcs : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ IsProbabilityMeasure (m0 := inst) (uniformOn s)
have hs₁ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (⊤ : ENNReal)
Tactic: apply cond_isProbabilityMeasure_of_finite
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst_2 : Decidable (ω ∈ t)
⊢ Eq (α := ENNReal) (((uniformOn {ω} : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
    (if ω ∈ t then 1 else 0 : ENNReal)
have rw : Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ({ω} ∩ t) : ENNReal)
  (if ω ∈ t then 1 else 0 : ENNReal)
Tactic: rw [uniformOn, cond_apply (measurableSet_singleton ω), Measure.count_singleton, inv_one,
    one_mul]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst_2 : Decidable (ω ∈ t)
⊢ Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ({ω} ∩ t) : ENNReal)
    (if ω ∈ t then 1 else 0 : ENNReal)
have pos : ω ∈ t → Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ({ω} ∩ t) : ENNReal) (1 : ENNReal)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst_2 : Decidable (ω ∈ t)
pos :
  ω ∈ t → Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ({ω} ∩ t) : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ({ω} ∩ t) : ENNReal)
    (if ω ∈ t then 1 else 0 : ENNReal)
have neg : ω ∉ t → Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ({ω} ∩ t) : ENNReal) (0 : ENNReal)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst_2 : Decidable (ω ∈ t)
h : ω ∈ t
⊢ Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ({ω} ∩ t) : ENNReal) (1 : ENNReal)
have rw : {ω} ∩ t = {ω}
Tactic: rw [(by simpa : ({ω} : Set Ω) ∩ t = {ω}), Measure.count_singleton]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst_2 : Decidable (ω ∈ t)
h : ω ∈ t
rw : {ω} ∩ t = {ω}
⊢ Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ({ω} ∩ t) : ENNReal) (1 : ENNReal)
have pos : Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) {ω} : ENNReal) (1 : ENNReal)
Tactic: rw [(by simpa : ({ω} : Set Ω) ∩ t = {ω}), Measure.count_singleton]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst_2 : Decidable (ω ∈ t)
h : ω ∈ t
rw : {ω} ∩ t = {ω}
pos : Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) {ω} : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ({ω} ∩ t) : ENNReal) (1 : ENNReal)
have pos₁ : Eq (α := ENNReal) 1 1
Tactic: rw [(by simpa : ({ω} : Set Ω) ∩ t = {ω}), Measure.count_singleton]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
⊢ Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ t) : ENNReal)
    (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
have rw : Eq (α := ENNReal) (Measure.count[s ∩ t | s] : ENNReal) (Measure.count[t | s] : ENNReal)
Tactic: rw [uniformOn, cond_inter_self hs.measurableSet]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
rw : Eq (α := ENNReal) (Measure.count[s ∩ t | s] : ENNReal) (Measure.count[t | s] : ENNReal)
⊢ Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ t) : ENNReal)
    (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
have rw₁ : Eq (α := ENNReal) (Measure.count[t | s] : ENNReal) (Measure.count[t | s] : ENNReal)
Tactic: rw [uniformOn, cond_inter_self hs.measurableSet]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (1 : ENNReal)
have h0 : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (0 : ENNReal)
Tactic: rw [uniformOn, cond_apply hs.measurableSet, Set.inter_self, ENNReal.inv_mul_cancel]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' : s.Nonempty
h0 : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (1 : ENNReal)
have ht : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (⊤ : ENNReal)
Tactic: rw [uniformOn, cond_apply hs.measurableSet, Set.inter_self, ENNReal.inv_mul_cancel]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : s ⊆ t
⊢ Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (1 : ENNReal)
have this : IsProbabilityMeasure (m0 := inst) (uniformOn s)
Tactic: haveI := isProbabilityMeasure_uniformOn hs hs'
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : s ⊆ t
this : IsProbabilityMeasure (m0 := inst) (uniformOn s)
⊢ Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (1 : ENNReal)
have refine : ¬LT.lt (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (1 : ENNReal)
Tactic: refine eq_of_le_of_not_lt prob_le_one ?_
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : s ⊆ t
this : IsProbabilityMeasure (m0 := inst) (uniformOn s)
⊢ ¬LT.lt (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (1 : ENNReal)
have rw : LE.le (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal)
  (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
Tactic: rw [not_lt, ← uniformOn_self hs hs']
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
h : Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (1 : ENNReal)
⊢ Ne (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (0 : ENNReal)
have rw : Ne (α := ENNReal) 1 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
h : Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (1 : ENNReal)
⊢ s ⊆ t
have hsf : s.Finite
Tactic: have hsf := finite_of_uniformOn_ne_zero (by rw [h]; exact one_ne_zero)
-- Lean 4 proof step from Mathlib.Probability.UniformOn (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
h : Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (1 : ENNReal)
hsf : s.Finite
⊢ s ⊆ t
have h₁ : HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ t) : ENNReal)
    ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹ : ENNReal) =
  1
Tactic: rw [uniformOn, cond_apply hsf.measurableSet, mul_comm] at h
Cleared hypotheses: h, hsf
-- Lean 4 proof step from Mathlib.Probability.UniformOn (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
h :
  HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ t) : ENNReal)
      ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹ : ENNReal) =
    1
hsf : s.Finite
⊢ s ⊆ t
have h₁ : Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ t) : ENNReal)
  ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹⁻¹ : ENNReal)
Tactic: replace h := ENNReal.eq_inv_of_mul_eq_one_left h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.UniformOn (hypothesis)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h :
  Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ t) : ENNReal)
    ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹⁻¹ : ENNReal)
⊢ s ⊆ t
have h₁ : #(sorry.toFinset (s := s ∩ t)) = #(hsf.toFinset (s := s))
Tactic: rw [inv_inv, Measure.count_apply_finite _ hsf, Measure.count_apply_finite _ (hsf.inter_of_left _),
    Nat.cast_inj] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : #(⋯.toFinset (s := s ∩ t)) = #(hsf.toFinset (s := s))
⊢ s ⊆ t
have suffices : s ∩ t = s
Tactic: suffices s ∩ t = s by exact this ▸ fun x hx => hx.2
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : #(⋯.toFinset (s := s ∩ t)) = #(hsf.toFinset (s := s))
⊢ s ∩ t = s
have rw : sorry.toFinset (s := s ∩ t) = hsf.toFinset (s := s)
Tactic: rw [← @Set.Finite.toFinset_inj _ _ _ (hsf.inter_of_left _) hsf]
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
⊢ ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ t) : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
have pos : ∀ (hst : s ∩ t = ∅),
  ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ t) : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
Tactic: by_cases hst : s ∩ t = ∅
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
pos :
  ∀ (hst : s ∩ t = ∅),
    ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
      HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ t) : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
        (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
⊢ ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ t) : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
have neg : ∀ (hst : ¬s ∩ t = ∅),
  ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ t) : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
Tactic: by_cases hst : s ∩ t = ∅
-- Lean 4 proof step from Mathlib.Probability.UniformOn (goal)
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t u : Set Ω
hs : s.Finite
hst : s ∩ t = ∅
⊢ ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
    HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn (s ∩ t) : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
      (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
have pos : ((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) (t ∩ u) =
  HMul.hMul (α := ENNReal) (β := ENNReal) (((uniformOn ∅ : Measure Ω) : (a : Set Ω) → ENNReal) u : ENNReal)
    (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
Tactic: rw [hst, uniformOn_empty_meas, Measure.coe_zero, Pi.zero_apply, zero_mul,
      uniformOn_eq_zero_iff hs, ← Set.inter_assoc, hst, Set.empty_inter]