awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.StrongLaw
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 : UniformIntegrable X p μ
⊢ UniformIntegrable.{u_1, u_2, 0} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := Ω → E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i)) p μ

Tactic:
apply uniformIntegrable_average hp

Premises used: MeasureTheory.uniformIntegrable_average
-- Module: Mathlib.Probability.StrongLaw
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 X p μ

Tactic:
MemLp.uniformIntegrable_of_identDistrib hp hp' hℒp hident

Premises used: ProbabilityTheory.MemLp.uniformIntegrable_of_identDistrib
-- Module: Mathlib.Probability.StrongLaw
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 X p μ

Tactic:
exact MemLp.uniformIntegrable_of_identDistrib hp hp' hℒp hident

Premises used: ProbabilityTheory.MemLp.uniformIntegrable_of_identDistrib
-- Module: Mathlib.Probability.StrongLaw
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 ω)) μ
h₁ :
  ∀ (n : ℕ) (ω : Ω),
    HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω) =
      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)

Tactic:
ext n ω
-- Module: Mathlib.Probability.StrongLaw
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 ω)) μ
n : ℕ
ω : Ω
⊢ HSMul.hSMul (α := ℝ) (β := E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i ω) =
    HSMul.hSMul (α := ℝ) (β := Ω → E) (↑n : ℝ)⁻¹ (∑ i ∈ range n, X i) ω

Tactic:
simp only [Pi.smul_apply, sum_apply]

Premises used: Finset.sum_apply, Pi.smul_apply
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
⊢ Eq.{u_1 + 1} (α := Measure Ω) (uniformOn ∅) 0

Tactic:
simp [uniformOn]

Premises used: ProbabilityTheory.uniformOn
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s : Set Ω
⊢ Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) ∅ : ENNReal) (0 : ENNReal)

Tactic:
simp
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s : Set Ω
hs : MeasurableSet s
⊢ Eq (α := Measure Ω) (uniformOn s) 0 ↔ s.Infinite ∨ s = ∅

Tactic:
simp [uniformOn, hs]

Premises used: ProbabilityTheory.uniformOn
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s : Set Ω
inst_1 : MeasurableSingletonClass Ω
⊢ Eq (α := Measure Ω) (uniformOn s) 0 ↔ s.Infinite ∨ s = ∅

Tactic:
simp [uniformOn]

Premises used: ProbabilityTheory.uniformOn
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s t : Set Ω
h : Ne (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (0 : ENNReal)
by_contra : ∀ (hs' : ¬s.Finite), False
⊢ s.Finite

Tactic:
by_contra hs'
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s t : Set Ω
h : Ne (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (0 : ENNReal)
hs' : ¬s.Finite
⊢ False

Tactic:
simp [uniformOn, cond, Measure.count_apply_infinite hs'] at h

Premises used: MeasureTheory.Measure.count_apply_infinite, ProbabilityTheory.cond, ProbabilityTheory.uniformOn
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : Fintype Ω
s : Set Ω
⊢ ((uniformOn Set.univ : Measure Ω) : (a : Set Ω) → ENNReal) s =
    HDiv.hDiv (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal)
      ((↑(Fintype.card Ω) : ENNReal) : ENNReal)

Tactic:
simp [uniformOn, cond_apply, ← ENNReal.div_eq_inv_mul]

Premises used: ProbabilityTheory.cond_apply, ProbabilityTheory.uniformOn, ENNReal.div_eq_inv_mul
-- Module: Mathlib.Probability.UniformOn
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)
hs : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (⊤ : ENNReal)
⊢ IsProbabilityMeasure (m0 := inst) (uniformOn s)

Tactic:
apply cond_isProbabilityMeasure_of_finite

Premises used: ProbabilityTheory.cond_isProbabilityMeasure_of_finite
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s : Set Ω
hs_fin : s.Finite
hs_nonempty : s.Nonempty
hs_meas : MeasurableSet s
hcs hcs₁ hcs₂ hcs₃ : s.Nonempty
⊢ Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (0 : ENNReal)

Tactic:
rwa [Measure.count_ne_zero_iff]

Premises used: MeasureTheory.Measure.count_ne_zero_iff
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s : Set Ω
hs_fin : s.Finite
hs_nonempty : s.Nonempty
hs_meas : MeasurableSet s
⊢ Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (⊤ : ENNReal)

Tactic:
(Measure.count_apply_lt_top' hs_meas).2 hs_fin |>.ne

Premises used: Iff.mpr, MeasureTheory.Measure.count_apply_lt_top', LT.lt.ne
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s : Set Ω
hs_fin : s.Finite
hs_nonempty : s.Nonempty
hs_meas : MeasurableSet s
⊢ Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (⊤ : ENNReal)

Tactic:
exact (Measure.count_apply_lt_top' hs_meas).2 hs_fin |>.ne

Premises used: Iff.mpr, MeasureTheory.Measure.count_apply_lt_top', LT.lt.ne
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
s : Set Ω
inst_1 : Finite Ω
inst_2 : Nonempty Ω
⊢ IsProbabilityMeasure.{u_1} (α := Ω) (m0 := inst) (uniformOn Set.univ)

Tactic:
isProbabilityMeasure_uniformOn' Set.finite_univ Set.univ_nonempty .univ

Premises used: Set.univ_nonempty, ProbabilityTheory.isProbabilityMeasure_uniformOn', Set.finite_univ, MeasurableSet.univ
-- Module: Mathlib.Probability.UniformOn
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)
rw₁ : MeasurableSet (↑(s ∩ t) : Set Ω)
⊢ ((uniformOn (↑s : Set Ω) : Measure Ω) : (a : Set Ω) → ENNReal) (↑t : Set Ω) =
    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']

Premises used: ProbabilityTheory.cond_apply, MeasureTheory.Measure.count_apply_finset', Finset.coe_inter, ProbabilityTheory.uniformOn
-- Module: Mathlib.Probability.UniformOn
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)⁻¹
rw₁ rw₂ :
  HMul.hMul (α := ENNReal) (↑(#(s ∩ t)) : ENNReal) (↑(#s) : 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)

Tactic:
rw [div_eq_mul_inv, mul_comm]

Premises used: div_eq_mul_inv, mul_comm
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_2
inst : DecidableEq Ω
x : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet (↑s : Set Ω)
ht : MeasurableSet (↑t : Set Ω)
rw : MeasurableSet ((↑s : Set Ω) ∩ (↑t : Set Ω))
⊢ MeasurableSet (↑(s ∩ t) : Set Ω)

Tactic:
rw [coe_inter]

Premises used: Finset.coe_inter
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_2
inst : DecidableEq Ω
x : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet (↑s : Set Ω)
ht : MeasurableSet (↑t : Set Ω)
⊢ MeasurableSet ((↑s : Set Ω) ∩ (↑t : Set Ω))

Tactic:
hs.inter ht

Premises used: MeasurableSet.inter
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_2
inst : DecidableEq Ω
x : MeasurableSpace Ω
s t : Finset Ω
hs : MeasurableSet (↑s : Set Ω)
ht : MeasurableSet (↑t : Set Ω)
⊢ MeasurableSet ((↑s : Set Ω) ∩ (↑t : Set Ω))

Tactic:
exact hs.inter ht

Premises used: MeasurableSet.inter
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
inst_2 : DecidableEq Ω
s t : Finset Ω
⊢ ((uniformOn (↑s : Set Ω) : Measure Ω) : (a : Set Ω) → ENNReal) (↑t : Set Ω) =
    HDiv.hDiv (α := ENNReal) (↑(#(s ∩ t)) : ENNReal) (↑(#s) : ENNReal)

Tactic:
uniformOn_apply_finset' s.measurableSet t.measurableSet

Premises used: Finset.measurableSet, ProbabilityTheory.uniformOn_apply_finset'
-- Module: Mathlib.Probability.UniformOn
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)
hs₁ : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (⊤ : ENNReal)
⊢ IsProbabilityMeasure (m0 := inst) (uniformOn s)

Tactic:
apply cond_isProbabilityMeasure_of_finite

Premises used: ProbabilityTheory.cond_isProbabilityMeasure_of_finite
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' hcs hcs₁ hcs₂ hcs₃ : s.Nonempty
⊢ Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (0 : ENNReal)

Tactic:
rwa [Measure.count_ne_zero_iff]

Premises used: MeasureTheory.Measure.count_ne_zero_iff
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (⊤ : ENNReal)

Tactic:
(Measure.count_apply_lt_top.2 hs).ne

Premises used: Iff.mpr, MeasureTheory.Measure.count_apply_lt_top, LT.lt.ne
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' : s.Nonempty
⊢ Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (⊤ : ENNReal)

Tactic:
exact (Measure.count_apply_lt_top.2 hs).ne

Premises used: Iff.mpr, MeasureTheory.Measure.count_apply_lt_top, LT.lt.ne
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst_2 : Decidable (ω ∈ t)
rw :
  Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ({ω} ∩ t) : ENNReal)
    (if ω ∈ t then 1 else 0 : ENNReal)
⊢ Eq (α := ENNReal) (((uniformOn {ω} : 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]

Premises used: ProbabilityTheory.cond_apply, inv_one, MeasurableSingletonClass.measurableSet_singleton, MeasureTheory.Measure.count_singleton, ProbabilityTheory.uniformOn, one_mul
-- Module: Mathlib.Probability.UniformOn
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)
neg :
  ω ∉ t → Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ({ω} ∩ t) : ENNReal) (0 : ENNReal)
⊢ Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ({ω} ∩ t) : ENNReal)
    (if ω ∈ t then 1 else 0 : ENNReal)

Tactic:
split_ifs
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
ω : Ω
t : Set Ω
inst_2 : Decidable (ω ∈ t)
h : ω ∈ t
⊢ {ω} ∩ t = {ω}

Tactic:
simpa
-- Module: Mathlib.Probability.UniformOn
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)
pos₁ pos₂ : Eq (α := ENNReal) 1 1
⊢ Eq (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) ({ω} ∩ t) : ENNReal) (1 : ENNReal)

Tactic:
rw [(by simpa : ({ω} : Set Ω) ∩ t = {ω}), Measure.count_singleton]

Premises used: MeasureTheory.Measure.count_singleton
-- Module: Mathlib.Probability.UniformOn
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) (0 : ENNReal)

Tactic:
simpa
-- Module: Mathlib.Probability.UniformOn
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)
rw₁ rw₂ : Eq (α := ENNReal) (Measure.count[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)

Tactic:
rw [uniformOn, cond_inter_self hs.measurableSet]

Premises used: ProbabilityTheory.cond_inter_self, Set.Finite.measurableSet, ProbabilityTheory.uniformOn
-- Module: Mathlib.Probability.UniformOn
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)
ht : Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (⊤ : ENNReal)
⊢ Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (1 : ENNReal)

Tactic:
rw [uniformOn, cond_apply hs.measurableSet, Set.inter_self, ENNReal.inv_mul_cancel]

Premises used: ProbabilityTheory.cond_apply, Set.inter_self, ENNReal.inv_mul_cancel, Set.Finite.measurableSet, ProbabilityTheory.uniformOn
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s : Set Ω
hs : s.Finite
hs' h0 h0₁ h0₂ h0₃ : s.Nonempty
⊢ Ne (α := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal) (0 : ENNReal)

Tactic:
rwa [Measure.count_ne_zero_iff]

Premises used: MeasureTheory.Measure.count_ne_zero_iff
-- Module: Mathlib.Probability.UniformOn
Goal:
Ω : Type u_1
inst : MeasurableSpace Ω
inst_1 : MeasurableSingletonClass Ω
s t : Set Ω
hs : s.Finite
hs' : s.Nonempty
ht : s ⊆ t
⊢ IsProbabilityMeasure (m0 := inst) (uniformOn s)

Tactic:
haveI := isProbabilityMeasure_uniformOn hs hs'
-- Module: Mathlib.Probability.UniformOn
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)

Tactic:
eq_of_le_of_not_lt prob_le_one ?_

Premises used: MeasureTheory.prob_le_one, eq_of_le_of_not_lt
-- Module: Mathlib.Probability.UniformOn
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)
refine : ¬LT.lt (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (1 : ENNReal)
⊢ Eq (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (1 : ENNReal)

Tactic:
refine eq_of_le_of_not_lt prob_le_one ?_

Premises used: MeasureTheory.prob_le_one, eq_of_le_of_not_lt
-- Module: Mathlib.Probability.UniformOn
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)
rw :
  LE.le (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal)
    (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)
⊢ ¬LT.lt (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (1 : ENNReal)

Tactic:
rw [not_lt, ← uniformOn_self hs hs']

Premises used: ProbabilityTheory.uniformOn_self, not_lt
-- Module: Mathlib.Probability.UniformOn
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)
⊢ LE.le (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal)
    (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)

Tactic:
measure_mono ht

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.Probability.UniformOn
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)
⊢ LE.le (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) s : ENNReal)
    (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal)

Tactic:
exact measure_mono ht

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.Probability.UniformOn
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)
rw : Ne (α := ENNReal) 1 0
⊢ Ne (α := ENNReal) (((uniformOn s : Measure Ω) : (a : Set Ω) → ENNReal) t : ENNReal) (0 : ENNReal)

Tactic:
rw [h]
-- Module: Mathlib.Probability.UniformOn
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) 1 0

Tactic:
one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Probability.UniformOn
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) 1 0

Tactic:
exact one_ne_zero

Premises used: one_ne_zero
-- Module: Mathlib.Probability.UniformOn
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.Finite

Tactic:
have hsf := finite_of_uniformOn_ne_zero (by rw [h]; exact one_ne_zero)
-- Module: Mathlib.Probability.UniformOn
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
⊢ 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

Premises used: ProbabilityTheory.cond_apply, mul_comm, Set.Finite.measurableSet, ProbabilityTheory.uniformOn
-- Module: Mathlib.Probability.UniformOn
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
h₁ :
  HMul.hMul (α := ENNReal) (β := ENNReal) (((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) (s ∩ t) : ENNReal)
      ((((Measure.count : Measure Ω) : (a : Set Ω) → ENNReal) s)⁻¹ : ENNReal) =
    1
⊢ s.Finite

Tactic:
rw [uniformOn, cond_apply hsf.measurableSet, mul_comm] at h

Premises used: ProbabilityTheory.cond_apply, mul_comm, Set.Finite.measurableSet, ProbabilityTheory.uniformOn
-- Module: Mathlib.Probability.UniformOn
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
⊢ 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
-- Module: Mathlib.Probability.UniformOn
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)
⊢ #(⋯.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

Premises used: Set.Finite.inter_of_left, Nat.cast_inj, inv_inv, MeasureTheory.Measure.count_apply_finite