awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (goal)
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 : Membership.mem (γ := Set Z) {z : Z | (⇑(f z) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s}ᶜ z
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞)
have h : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rwa [pos_iff_ne_zero, ne_eq, measure_symmDiff_eq_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (goal)
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 : Membership.mem (γ := Set Z) {z : Z | (⇑(f z) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s}ᶜ z
h : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞)
have h₁ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rwa [pos_iff_ne_zero, ne_eq, measure_symmDiff_eq_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (goal)
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 : Membership.mem (γ := Set Z) {z : Z | (⇑(f z) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s}ᶜ z
h : Ne (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞) (0 : ℝ≥0∞)
h₁ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s) : ℝ≥0∞)
have h₂ : ¬(⇑(f z) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s
Tactic: rwa [pos_iff_ne_zero, ne_eq, measure_symmDiff_eq_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (hypothesis)
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 : Membership.mem (γ := Set Z) {z : Z | (⇑(f z) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s}ᶜ z
⊢ {z : Z | (⇑(f z) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s}ᶜ ∈ 𝓝 z
have hz₁ : ∀ᶠ (ε : ℝ≥0∞) in 𝓝 0, ε < (μ : (a : Set X) → ℝ≥0∞) (((⇑(f z) : (a : X) → Y) ⁻¹' t) ∆ s)
Tactic: replace hz : ∀ᶠ ε : ℝ≥0∞ in 𝓝 0, ε < μ ((f z ⁻¹' t) ∆ s) := by
    apply gt_mem_nhds
    rwa [pos_iff_ne_zero, ne_eq, measure_symmDiff_eq_zero_iff]
Cleared hypotheses: hz
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (goal)
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)
⊢ {z : Z | (⇑(f z) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s}ᶜ ∈ 𝓝 z
have h : ∀ (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∞)),
  Membership.mem (γ := Set Z) {z : Z | (⇑(f z) : (a : X) → Y) ⁻¹' t =ᶠ[ae μ] s}ᶜ w
Tactic: filter_upwards [(tendsto_measure_symmDiff_preimage_nhds_zero (hf.tendsto z)
    (.of_forall hfm) (hfm z) htm ht).eventually hz] with w hw
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.ContinuousPreimage (hypothesis)
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
⊢ False
have 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∞)
Tactic: rw [measure_congr (hw'.symmDiff (ae_eq_refl _)), symmDiff_comm] at hw
Cleared hypotheses: hw, hw'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : MeasurableSingletonClass α
s : Set α
hs : s.Finite
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((↑(#(hs.toFinset (s := s))) : ℝ≥0∞) : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  (((count : Measure α) : (a : Set α) → ℝ≥0∞) (↑(hs.toFinset (s := s)) : Set α) : ℝ≥0∞)
Tactic: rw [← count_apply_finset, Finite.coe_toFinset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((↑(#(hs.toFinset (s := s))) : ℝ≥0∞) : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
  (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [← count_apply_finset, Finite.coe_toFinset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
hs : s.Infinite
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine : ∀ (n : ℕ), LE.le (α := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine top_unique (le_of_tendsto' ENNReal.tendsto_nat_nhds_top fun n => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
hs : s.Infinite
n : ℕ
⊢ LE.le (α := ℝ≥0∞) ((↑n : ℝ≥0∞) : ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rcases : ∀ (t : Finset α) (ht : (↑t : Set α) ⊆ s),
  LE.le (α := ℝ≥0∞) ((↑(#t) : ℝ≥0∞) : ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rcases hs.exists_subset_card_eq n with ⟨t, ht, rfl⟩
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
hs : s.Infinite
t : Finset α
ht : (↑t : Set α) ⊆ s
⊢ LE.le (α := ℝ≥0∞) ((↑(#t) : ℝ≥0∞) : ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have i : Eq (α := ℝ≥0∞) (↑(#t) : ℝ≥0∞) (∑ i ∈ t, 1)
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
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
s_mble : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite
have pos : ∀ (hs : s.Finite), Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite
Tactic: by_cases hs : s.Finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
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
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite
have neg : ∀ (hs : ¬s.Finite), Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite
Tactic: by_cases hs : s.Finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (hypothesis)
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
have hs₁ : s.Infinite
Tactic: change s.Infinite at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
s : Set α
inst_1 : MeasurableSingletonClass α
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite
have pos : ∀ (hs : s.Finite), Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite
Tactic: by_cases hs : s.Finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
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
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite
have neg : ∀ (hs : ¬s.Finite), Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ↔ s.Infinite
Tactic: by_cases hs : s.Finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (hypothesis)
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
have hs₁ : s.Infinite
Tactic: change s.Infinite at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : α → Prop
⊢ (∀ᵐ (x : α) ∂count, p x) ↔ ∀ (x : α), p x
have refine : ∀ (h : ∀ᵐ (x : α) ∂count, p x) (x : α), p x
Tactic: refine ⟨fun h x ↦ ?_, ae_of_all _⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : α → Prop
h : ∀ᵐ (x : α) ∂count, p x
x : α
⊢ p x
have rw : ∀ (h : Eq.{u_1 + 1} (α := Set α) {a : α | ¬p a} ∅) (x : α), p x
Tactic: rw [ae_iff, count_eq_zero_iff] at h
Cleared hypotheses: h, x
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : α → Prop
h : Eq.{u_1 + 1} (α := Set α) {a : α | ¬p a} ∅
x : α
⊢ p x
have by_contra : ∀ (hx : ¬p x), False
Tactic: by_contra hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
p : α → Prop
h : Eq.{u_1 + 1} (α := Set α) {a : α | ¬p a} ∅
x : α
hx : ¬p x
⊢ False
have rwa : Membership.mem (γ := Set α) ∅ x
Tactic: rwa [← mem_empty_iff_false x, ← h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
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
⊢ False
have rwa₁ : Membership.mem (γ := Set α) {a : α | ¬p a} x
Tactic: rwa [← mem_empty_iff_false x, ← h]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
ha : MeasurableSet (α := α) {a}
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) {a} : ℝ≥0∞) (1 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) (↑(Finset.card (α := α) (toFinset {a})) : ℝ≥0∞) 1
Tactic: rw [count_apply_finite' (Set.finite_singleton a) ha, Set.Finite.toFinset]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
ha : MeasurableSet (α := α) {a}
⊢ Measure.real (α := α) (m := inst) count {a} = 1
have rw : ENNReal.toReal (((count : Measure α) : (a : Set α) → ℝ≥0∞) {a}) = 1
Tactic: rw [measureReal_def, count_singleton' ha, ENNReal.toReal_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
a : α
ha : MeasurableSet (α := α) {a}
rw : ENNReal.toReal (((count : Measure α) : (a : Set α) → ℝ≥0∞) {a}) = 1
⊢ Measure.real (α := α) (m := inst) count {a} = 1
have rw₁ : ENNReal.toReal 1 = 1
Tactic: rw [measureReal_def, count_singleton' ha, ENNReal.toReal_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
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
⊢ Measure.real (α := α) (m := inst) count {a} = 1
have rw₂ : Eq (α := ℝ) 1 1
Tactic: rw [measureReal_def, count_singleton' ha, ENNReal.toReal_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
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)
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have pos : ∀ (hs : s.Finite),
  Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: by_cases hs : s.Finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have neg : ∀ (hs : ¬s.Finite),
  Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: by_cases hs : s.Finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
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
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have 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∞)
Tactic: lift s to Finset β using hs
Cleared hypotheses: s, s_mble, fs_mble, hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
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 β))
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' (↑s : Set β)) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) (↑s : Set β) : ℝ≥0∞)
have rw : MeasurableSet (↑(Finset.image f s) : Set α)
Tactic: rw [← Finset.coe_image, count_apply_finset' _, count_apply_finset' s_mble,
      s.card_image_of_injective hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
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
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have neg : Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [count_apply_infinite hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (hypothesis)
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
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have hs₁ : ¬(f '' s).Finite
Tactic: rw [← finite_image_iff hf.injOn] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
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
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg : Eq (α := ℝ≥0∞) ∞ ∞
Tactic: rw [count_apply_infinite hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
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)
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have pos : ∀ (hs : s.Finite),
  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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
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∞)
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have neg : ∀ (hs : ¬s.Finite),
  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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have pos : ∀ (hs : s.Finite),
  Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: by_cases hs : s.Finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
pos :
  ∀ (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∞)
have neg : ∀ (hs : ¬s.Finite),
  Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: by_cases hs : s.Finite
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬s.Finite
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞)
    (((count : Measure β) : (a : Set β) → ℝ≥0∞) s : ℝ≥0∞)
have neg : Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [count_apply_infinite hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬s.Finite
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have hs₁ : ¬(f '' s).Finite
Tactic: rw [← finite_image_iff hf.injOn] at hs
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
inst_2 : MeasurableSingletonClass α
inst_3 : MeasurableSingletonClass β
f : β → α
hf : Function.Injective f
s : Set β
hs : ¬(f '' s).Finite
⊢ Eq (α := ℝ≥0∞) (((count : Measure α) : (a : Set α) → ℝ≥0∞) (f '' s) : ℝ≥0∞) (∞ : ℝ≥0∞)
have neg : Eq (α := ℝ≥0∞) ∞ ∞
Tactic: rw [count_apply_infinite hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Count (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
inst_1 : Subsingleton α
i : α
⊢ Eq (α := Measure α) (restrict count univ) (restrict count {i})
have e_s : Eq (α := Set α) univ {i}
Tactic: congr