-- Mathlib/Probability/UniformOn.lean
theorem pred_true_of_uniformOn_eq_one (h : uniformOn s t = 1) : s ⊆ t

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
h : (uniformOn s) t = 1
hsf : s.Finite
⊢ s ⊆ t

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

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
h : Measure.count (s ∩ t) * (Measure.count s)⁻¹ = 1
hsf : s.Finite
⊢ s ⊆ t

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : ⋯.toFinset.card = hsf.toFinset.card
⊢ s ∩ t = s

Tactic:
rw [← @Set.Finite.toFinset_inj _ _ _ (hsf.inter_of_left _) hsf]

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : ⋯.toFinset.card = hsf.toFinset.card
⊢ ⋯.toFinset = hsf.toFinset

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
h : (uniformOn s) t = 1
⊢ (uniformOn ?m.15105) ?m.15106 ≠ 0

Tactic:
rw [h]

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
h : (uniformOn s) t = 1
⊢ 1 ≠ 0

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : ⋯.toFinset.card = hsf.toFinset.card
⊢ ⋯.toFinset = hsf.toFinset

Tactic:
exact Finset.eq_of_subset_of_card_le (Set.Finite.toFinset_mono s.inter_subset_left) h.ge

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : Measure.count (s ∩ t) = (Measure.count s)⁻¹⁻¹
⊢ s ⊆ t

Tactic:
rw [inv_inv, Measure.count_apply_finite _ hsf, Measure.count_apply_finite _ (hsf.inter_of_left _),
  Nat.cast_inj] at h

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : ⋯.toFinset.card = hsf.toFinset.card
⊢ s ⊆ t

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
h : (uniformOn s) t = 1
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
h : Measure.count (s ∩ t) * (Measure.count s)⁻¹ = 1
hsf : s.Finite
⊢ s ⊆ t

Tactic:
replace h := ENNReal.eq_inv_of_mul_eq_one_left h

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : Measure.count (s ∩ t) = (Measure.count s)⁻¹⁻¹
⊢ s ⊆ t

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : ⋯.toFinset.card = hsf.toFinset.card
this : s ∩ t = s
⊢ s ⊆ t

Tactic:
exact this ▸ fun x hx => hx.2

Result:
no goals

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : ⋯.toFinset.card = hsf.toFinset.card
⊢ s ⊆ t

Tactic:
suffices s ∩ t = s by exact this ▸ fun x hx => hx.2

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
hsf : s.Finite
h : ⋯.toFinset.card = hsf.toFinset.card
⊢ s ∩ t = s

Proof state:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
h : (uniformOn s) t = 1
⊢ s ⊆ t

Tactic:
have hsf := finite_of_uniformOn_ne_zero (by rw [h]; exact one_ne_zero)

Result:
Ω : Type u_1
inst✝¹ : MeasurableSpace Ω
inst✝ : MeasurableSingletonClass Ω
s t : Set Ω
h : (uniformOn s) t = 1
hsf : s.Finite
⊢ s ⊆ t