Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑(condCount s) t = 1
hsf : Set.Finite s
⊢ s ⊆ t
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑(condCount s) t = 1
⊢ s ⊆ t
have hsf := finite_of_condCount_ne_zero (by rw [h]; exact one_ne_zero)
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑Measure.count (s ∩ t) * (↑↑Measure.count s)⁻¹ = 1
hsf : Set.Finite s
⊢ s ⊆ t
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑(condCount s) t = 1
hsf : Set.Finite s
⊢ s ⊆ t
rw [condCount, cond_apply _ hsf.measurableSet, mul_comm] at h
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : ↑↑Measure.count (s ∩ t) = (↑↑Measure.count s)⁻¹⁻¹
⊢ s ⊆ t
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑Measure.count (s ∩ t) * (↑↑Measure.count s)⁻¹ = 1
hsf : Set.Finite s
⊢ s ⊆ t
replace h := ENNReal.eq_inv_of_mul_eq_one_left h
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : Finset.card (Set.Finite.toFinset (_ : Set.Finite (s ∩ t))) = Finset.card (Set.Finite.toFinset hsf)
⊢ s ⊆ t
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : ↑↑Measure.count (s ∩ t) = (↑↑Measure.count s)⁻¹⁻¹
⊢ s ⊆ t
rw [inv_inv, Measure.count_apply_finite _ hsf, Measure.count_apply_finite _ (hsf.inter_of_left _),
  Nat.cast_inj] at h
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : Finset.card (Set.Finite.toFinset (_ : Set.Finite (s ∩ t))) = Finset.card (Set.Finite.toFinset hsf)
⊢ s ∩ t = s
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : Finset.card (Set.Finite.toFinset (_ : Set.Finite (s ∩ t))) = Finset.card (Set.Finite.toFinset hsf)
⊢ s ⊆ t
suffices s ∩ t = s by exact this ▸ fun x hx => hx.2
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : Finset.card (Set.Finite.toFinset (_ : Set.Finite (s ∩ t))) = Finset.card (Set.Finite.toFinset hsf)
⊢ Set.Finite.toFinset (_ : Set.Finite (s ∩ t)) = Set.Finite.toFinset hsf
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : Finset.card (Set.Finite.toFinset (_ : Set.Finite (s ∩ t))) = Finset.card (Set.Finite.toFinset hsf)
⊢ s ∩ t = s
rw [← @Set.Finite.toFinset_inj _ _ _ (hsf.inter_of_left _) hsf]
no goals
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : Finset.card (Set.Finite.toFinset (_ : Set.Finite (s ∩ t))) = Finset.card (Set.Finite.toFinset hsf)
⊢ Set.Finite.toFinset (_ : Set.Finite (s ∩ t)) = Set.Finite.toFinset hsf
exact Finset.eq_of_subset_of_card_le (Set.Finite.toFinset_mono <| s.inter_subset_left t) h.ge
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑(condCount s) t = 1
⊢ 1 ≠ 0
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑(condCount s) t = 1
⊢ ↑↑(condCount ?m.112707) ?m.112708 ≠ 0
rw [h]
no goals
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
h : ↑↑(condCount s) t = 1
⊢ 1 ≠ 0
exact one_ne_zero
no goals
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t u : Set Ω
hsf : Set.Finite s
h : Finset.card (Set.Finite.toFinset (_ : Set.Finite (s ∩ t))) = Finset.card (Set.Finite.toFinset hsf)
this : s ∩ t = s
⊢ s ⊆ t
exact this ▸ fun x hx => hx.2