awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
inst_8 : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst_8, _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z) : (a : X) → Y) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
z : Z
hz : ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < (μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s)
w : Z
hw :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f w) : (a : X) → Y) ⁻¹' t) ∆ ((⇑(f z) : (a : X) → Y) ⁻¹' t)) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞)
hw' : (⇑(f w) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s
hw₁ :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞)
⊢ (⇑(f w) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s

Tactic:
rw [measure_congr (hw'.symmDiff (ae_eq_refl _)), symmDiff_comm] at hw

Premises used: MeasureTheory.measure_congr, symmDiff_comm, MeasureTheory.ae_eq_refl, Filter.EventuallyEq.symmDiff
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
inst_8 : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst_8, _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z) : (a : X) → Y) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
z : Z
hz : ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < (μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s)
w : Z
hw :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞)
hw' : (⇑(f w) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s
⊢ False

Tactic:
hw.false

Premises used: LT.lt.false
-- Module: Mathlib.MeasureTheory.Measure.ContinuousPreimage
Goal:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst : TopologicalSpace X
inst_1 : MeasurableSpace X
inst_2 : BorelSpace X
inst_3 : R1Space X
inst_4 : TopologicalSpace Y
inst_5 : MeasurableSpace Y
inst_6 : BorelSpace Y
inst_7 : R1Space Y
inst_8 : TopologicalSpace Z
μ : Measure X
ν : Measure Y
inst_9 : μ.InnerRegularCompactLTTop
inst_10 : IsLocallyFiniteMeasure ν
f : Z → C(X, Y)
hf : Continuous[inst_8, _] f
hfm : ∀ (z : Z), MeasurePreserving (⇑(f z) : (a : X) → Y) μ ν
s : Set X
t : Set Y
htm : NullMeasurableSet t ν
ht : Ne (α := ℝ≥0∞) ((ν : (a : Set Y) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
z : Z
hz : ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < (μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s)
w : Z
hw :
  LT.lt (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞)
    ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞)
hw' : (⇑(f w) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s
⊢ False

Tactic:
exact hw.false

Premises used: LT.lt.false
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Nonempty α
⊢ Ne.{u_1 + 1} (α := Measure α) count 0

Tactic:
simp [count]

Premises used: MeasureTheory.Measure.count
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
⊢ LE.le (α := ℝ≥0∞) (∑' (x : (↑s : Type u_1)), 1 : ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
calc
    (∑' _ : s, 1 : ℝ≥0∞) = ∑' i, indicator s 1 i := tsum_subtype s 1
    _ ≤ ∑' i, dirac i s := ENNReal.tsum_le_tsum fun _ => le_dirac_apply
    _ ≤ count s := le_sum_apply _ _

Premises used: Trans.trans, ENNReal.tsum_le_tsum, MeasureTheory.Measure.le_sum_apply, tsum_subtype, MeasureTheory.Measure.le_dirac_apply, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
hs : MeasurableSet s
⊢ ((count : Measure α) : (a : Set α) → ℝ≥0∞) s = (↑s.encard : ℝ≥0∞)

Tactic:
simp [count, hs, ← tsum_subtype]

Premises used: tsum_subtype, MeasureTheory.Measure.count
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Finset α
hs : MeasurableSet (↑s : Set α)
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞) ((↑(#s) : ℝ≥0∞) : ℝ≥0∞)

Tactic:
simp [count_apply hs]

Premises used: MeasureTheory.Measure.count_apply
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
s : Finset α
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (↑s : Set α) : ℝ≥0∞) ((↑(#s) : ℝ≥0∞) : ℝ≥0∞)

Tactic:
count_apply_finset' s.measurableSet

Premises used: Finset.measurableSet, MeasureTheory.Measure.count_apply_finset'
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
s_fin : s.Finite
s_mble : MeasurableSet s
⊢ MeasurableSet (↑(s_fin.toFinset (s := s)) : Set α)

Tactic:
simpa only [Finite.coe_toFinset] using s_mble

Premises used: Set.Finite.coe_toFinset
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
s_fin : s.Finite
s_mble : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((↑(#(s_fin.toFinset (s := s))) : ℝ≥0∞) : ℝ≥0∞)

Tactic:
simp [←
    @count_apply_finset' _ _ s_fin.toFinset (by simpa only [Finite.coe_toFinset] using s_mble)]

Premises used: MeasureTheory.Measure.count_apply_finset'
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
s : Set α
hs : s.Finite
rw :
  Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure α) : (a : Set α) → ℝ≥0∞) (↑(hs.toFinset (s := s)) : Set α) : ℝ≥0∞)
rw₁ rw₂ :
  Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((↑(#(hs.toFinset (s := s))) : ℝ≥0∞) : ℝ≥0∞)

Tactic:
rw [← count_apply_finset, Finite.coe_toFinset]

Premises used: Set.Finite.coe_toFinset, MeasureTheory.Measure.count_apply_finset
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
hs : s.Infinite
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
top_unique (le_of_tendsto' ENNReal.tendsto_nat_nhds_top fun n => ?_)

Premises used: ENNReal.tendsto_nat_nhds_top, top_unique, le_of_tendsto'
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
hs : s.Infinite
refine : ∀ (n : ℕ), LE.le (α := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
refine top_unique (le_of_tendsto' ENNReal.tendsto_nat_nhds_top fun n => ?_)

Premises used: ENNReal.tendsto_nat_nhds_top, top_unique, le_of_tendsto'
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
hs : s.Infinite
n : ℕ
rcases :
  ∀ (t : Finset α) (ht : (↑t : Set α) ⊆ s),
    LE.le (α := ℝ≥0∞) ((↑(#t) : ℝ≥0∞) : ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rcases hs.exists_subset_card_eq n with ⟨t, ht, rfl⟩

Premises used: Set.Infinite.exists_subset_card_eq, rfl
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
hs : s.Infinite
t : Finset α
ht : (↑t : Set α) ⊆ s
⊢ Eq (α := ℝ≥0∞) (↑(#t) : ℝ≥0∞) (∑ i ∈ t, 1)

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
hs : s.Infinite
t : Finset α
ht : (↑t : Set α) ⊆ s
⊢ Eq (α := ℝ≥0∞) (∑ i ∈ t, 1) (∑' (i : (↑(↑t : Set α) : Type u_1)), 1)

Tactic:
(t.tsum_subtype 1).symm

Premises used: OfNat.ofNat, Eq.symm, Finset.tsum_subtype
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
hs : s.Infinite
t : Finset α
ht : (↑t : Set α) ⊆ s
⊢ LE.le (α := ℝ≥0∞) (∑' (i : (↑(↑t : Set α) : Type u_1)), 1 : ℝ≥0∞)
    (((count : Measure α) : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞)

Tactic:
le_count_apply

Premises used: MeasureTheory.Measure.le_count_apply
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
hs : s.Infinite
t : Finset α
ht : (↑t : Set α) ⊆ s
⊢ LE.le (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (↑t : Set α) : ℝ≥0∞)
    (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
measure_mono ht

Premises used: MeasureTheory.measure_mono
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
hs : s.Infinite
t : Finset α
ht : (↑t : Set α) ⊆ s
i : Eq (α := ℝ≥0∞) (↑(#t) : ℝ≥0∞) (∑ i ∈ t, 1)
⊢ LE.le (α := ℝ≥0∞) ((↑(#t) : ℝ≥0∞) : ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
calc
    (#t : ℝ≥0∞) = ∑ i ∈ t, 1 := by simp
    _ = ∑' i : (t : Set α), 1 := (t.tsum_subtype 1).symm
    _ ≤ count (t : Set α) := le_count_apply
    _ ≤ count s := measure_mono ht

Premises used: Nat.cast, SetLike.coe, MeasureTheory.measure_mono, MeasureTheory.Measure.le_count_apply, Finset.card, MeasureTheory.Measure.count, OfNat.ofNat, Eq.symm, DFunLike.coe, Finset.tsum_subtype
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
pos : ∀ (hs : s.Finite), Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite
neg : ∀ (hs : ¬s.Finite), Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite

Tactic:
by_cases hs : s.Finite

Premises used: Set.Finite
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
hs : s.Finite
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite

Tactic:
simp [Set.Infinite, hs, count_apply_finite' hs s_mble]

Premises used: MeasureTheory.Measure.count_apply_finite', Set.Infinite
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
hs : ¬s.Finite
⊢ s.Infinite

Tactic:
change s.Infinite at hs

Premises used: Set.Infinite
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
hs : s.Infinite
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite

Tactic:
simp [hs, count_apply_infinite]

Premises used: MeasureTheory.Measure.count_apply_infinite
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
inst_1 : MeasurableSingletonClass α
pos : ∀ (hs : s.Finite), Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite
neg : ∀ (hs : ¬s.Finite), Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite

Tactic:
by_cases hs : s.Finite

Premises used: Set.Finite
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
inst_1 : MeasurableSingletonClass α
hs : s.Finite
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite

Tactic:
count_apply_eq_top' hs.measurableSet

Premises used: MeasureTheory.Measure.count_apply_eq_top', Set.Finite.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
inst_1 : MeasurableSingletonClass α
hs : s.Finite
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite

Tactic:
exact count_apply_eq_top' hs.measurableSet

Premises used: MeasureTheory.Measure.count_apply_eq_top', Set.Finite.measurableSet
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
inst_1 : MeasurableSingletonClass α
hs : ¬s.Finite
⊢ s.Infinite

Tactic:
change s.Infinite at hs

Premises used: Set.Infinite
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
inst_1 : MeasurableSingletonClass α
hs : s.Infinite
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite

Tactic:
simp [hs, count_apply_infinite]

Premises used: MeasureTheory.Measure.count_apply_infinite
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
⊢ LT.lt (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Finite

Tactic:
calc
    count s < ∞ ↔ count s ≠ ∞ := lt_top_iff_ne_top
    _ ↔ ¬s.Infinite := not_congr (count_apply_eq_top' s_mble)
    _ ↔ s.Finite := Classical.not_not

Premises used: Trans.trans, Classical.not_not, lt_top_iff_ne_top, MeasureTheory.Measure.count_apply_eq_top', not_congr
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
inst_1 : MeasurableSingletonClass α
⊢ LT.lt (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Finite

Tactic:
calc
    count s < ∞ ↔ count s ≠ ∞ := lt_top_iff_ne_top
    _ ↔ ¬s.Infinite := not_congr count_apply_eq_top
    _ ↔ s.Finite := Classical.not_not

Premises used: Trans.trans, Classical.not_not, MeasureTheory.Measure.count_apply_eq_top, lt_top_iff_ne_top, not_congr
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
h : Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
x : α
hx : x ∈ s
⊢ False

Tactic:
simpa [hx] using ((ENNReal.le_tsum x).trans <| le_sum_apply _ _).trans_eq h

Premises used: LE.le.trans_eq, MeasureTheory.Measure.le_sum_apply, ENNReal.le_tsum, LE.le.trans
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) ∅) 0

Tactic:
measure_empty

Premises used: MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) ∅) 0

Tactic:
exact measure_empty

Premises used: MeasureTheory.measure_empty
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
⊢ Ne (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞) ↔ s.Nonempty

Tactic:
count_eq_zero_iff.not.trans nonempty_iff_ne_empty.symm

Premises used: MeasureTheory.Measure.count_eq_zero_iff, Iff.not, Set.nonempty_iff_ne_empty, Iff.trans, Iff.symm
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
p : α → Prop
⊢ (∀ᵐ (x : α) ∂count, p x) ↔ ∀ (x : α), p x

Tactic:
⟨fun h x ↦ ?_, ae_of_all _⟩

Premises used: MeasureTheory.ae_of_all, Iff.intro
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
p : α → Prop
refine : ∀ (h : ∀ᵐ (x : α) ∂count, p x) (x : α), p x
⊢ (∀ᵐ (x : α) ∂count, p x) ↔ ∀ (x : α), p x

Tactic:
refine ⟨fun h x ↦ ?_, ae_of_all _⟩
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
p : α → Prop
h : ∀ᵐ (x : α) ∂count, p x
x : α
rw : ∀ (h : Eq.{u_1 + 1} (α := Set α) {a : α | ¬p a} ∅) (x : α), p x
⊢ p x

Tactic:
rw [ae_iff, count_eq_zero_iff] at h

Premises used: MeasureTheory.Measure.count_eq_zero_iff, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
p : α → Prop
h : Eq.{u_1 + 1} (α := Set α) {a : α | ¬p a} ∅
x : α
by_contra : ∀ (hx : ¬p x), False
⊢ p x

Tactic:
by_contra hx
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
p : α → Prop
h : Eq.{u_1 + 1} (α := Set α) {a : α | ¬p a} ∅
x : α
hx : ¬p x
rwa : Membership.mem (γ := Set α) ∅ x
rwa₁ rwa₂ rwa₃ rwa₄ : Membership.mem (γ := Set α) {a : α | ¬p a} x
⊢ False

Tactic:
rwa [← mem_empty_iff_false x, ← h]

Premises used: Set.mem_empty_iff_false
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
ha : MeasurableSet (α := α) {a}
rw : Eq (α := ℝ≥0∞) (↑(Finset.card (α := α) (toFinset {a})) : ℝ≥0∞) 1
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
rw [count_apply_finite' (Set.finite_singleton a) ha, Set.Finite.toFinset]

Premises used: Set.Finite.toFinset, MeasureTheory.Measure.count_apply_finite', Set.finite_singleton
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
ha : MeasurableSet (α := α) {a}
⊢ Eq (α := ℝ≥0∞) (↑(Finset.card (α := α) (toFinset {a})) : ℝ≥0∞) 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (1 : ℝ≥0∞)

Tactic:
count_singleton' (measurableSet_singleton a)

Premises used: MeasureTheory.Measure.count_singleton', MeasurableSingletonClass.measurableSet_singleton
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
ha : MeasurableSet (α := α) {a}
rw : ENNReal.toReal (((count : Measure α) : (a : Set α) → ℝ≥0∞) {a}) = 1
rw₁ : ENNReal.toReal 1 = 1
rw₂ rw₃ : Eq (α := ℝ) 1 1
⊢ Measure.real (α := α) (m := inst) count {a} = 1

Tactic:
rw [measureReal_def, count_singleton' ha, ENNReal.toReal_one]

Premises used: MeasureTheory.Measure.count_singleton', ENNReal.toReal_one, MeasureTheory.measureReal_def
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
a : α
⊢ Measure.real (α := α) (m := inst) count {a} = 1

Tactic:
count_real_singleton' (measurableSet_singleton a)

Premises used: MeasurableSingletonClass.measurableSet_singleton, MeasureTheory.count_real_singleton'
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
pos :
  ∀ (hs : s.Finite),
    Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
      (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
neg :
  ∀ (hs : ¬s.Finite),
    Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
      (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
by_cases hs : s.Finite

Premises used: Set.Finite
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : s.Finite
⊢ s.Finite

Tactic:
hs
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : s.Finite
pos :
  ∀ (s : Finset β) (s_mble : MeasurableSet (↑s : Set β)) (fs_mble : MeasurableSet (f '' (↑s : Set β))),
    Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' (↑s : Set β)) : ℝ≥0∞)
      (((count : Measure β) : (a : Set β) → ℝ≥0∞) (↑s : Set β) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
lift s to Finset β using hs

Premises used: Finset
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Finset β
s_mble : MeasurableSet (↑s : Set β)
fs_mble : MeasurableSet (f '' (↑s : Set β))
rw : MeasurableSet (↑(Finset.image f s) : Set α)
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' (↑s : Set β)) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) (↑s : Set β) : ℝ≥0∞)

Tactic:
rw [← Finset.coe_image, count_apply_finset' _, count_apply_finset' s_mble,
      s.card_image_of_injective hf]

Premises used: Finset.coe_image, Finset.card_image_of_injective, MeasureTheory.Measure.count_apply_finset'
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Finset β
s_mble : MeasurableSet (↑s : Set β)
fs_mble : MeasurableSet (f '' (↑s : Set β))
⊢ MeasurableSet (↑(Finset.image f s) : Set α)

Tactic:
simpa only [Finset.coe_image] using fs_mble

Premises used: Finset.coe_image
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬s.Finite
neg : Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
rw [count_apply_infinite hs]

Premises used: MeasureTheory.Measure.count_apply_infinite
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬s.Finite
⊢ ¬(f '' s).Finite

Tactic:
rw [← finite_image_iff hf.injOn] at hs

Premises used: Function.Injective.injOn, Set.finite_image_iff
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
hs : ¬(f '' s).Finite
neg neg₁ : Eq (α := ℝ≥0∞) ∞ ∞
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
rw [count_apply_infinite hs]

Premises used: MeasureTheory.Measure.count_apply_infinite
-- Module: Mathlib.MeasureTheory.Measure.Count
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : β → α
hf : Function.Injective f
s : Set β
s_mble : MeasurableSet s
fs_mble : MeasurableSet (f '' s)
pos :
  ∀ (hs : s.Finite),
    Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
      (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
neg neg₁ :
  ∀ (hs : ¬s.Finite),
    Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
      (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)

Tactic:
classical
  by_cases hs : s.Finite
  · lift s to Finset β using hs
    rw [← Finset.coe_image, count_apply_finset' _, count_apply_finset' s_mble,
      s.card_image_of_injective hf]
    simpa only [Finset.coe_image] using fs_mble
  · rw [count_apply_infinite hs]
    rw [← finite_image_iff hf.injOn] at hs
    rw [count_apply_infinite hs]

Premises used: Function.Injective.injOn, Finset, Set.Finite, Finset.coe_image, MeasureTheory.Measure.count_apply_finset', Set.finite_image_iff