awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : TopologicalSpace β
inst_1 : T1Space β
inst_2 : SecondCountableTopology β
inst_3 : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure
h : ∀ (b : β), Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) {b}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
inhabited_h : Inhabited β
this : Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
b : β
hb : ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∃ (a : β) (b : β),
    a ≠ b ∧
      (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
        ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
have rcases : ∀ (a : β) (hab : a ≠ b) (ha : ∀ t ∈ 𝓝[{b}ᶜ] a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)),
  ∃ (a : β) (b : β),
    a ≠ b ∧
      (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
        ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
Tactic: rcases exists_mem_forall_mem_nhdsWithin_pos_measure (h b) with ⟨a, hab : a ≠ b, ha⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_5
inst : TopologicalSpace β
inst_1 : T1Space β
inst_2 : SecondCountableTopology β
inst_3 : Nonempty β
f : α → β
m : OuterMeasure β := (OuterMeasure.map f : (a : OuterMeasure α) → OuterMeasure β) μ.toOuterMeasure
h : ∀ (b : β), Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) {b}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
inhabited_h : Inhabited β
this : Ne (α := ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
b : β
hb : ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
a : β
hab : a ≠ b
ha : ∀ t ∈ 𝓝[{b}ᶜ] a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
⊢ ∃ (a : β) (b : β),
    a ≠ b ∧
      (∀ s ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' s) : ℝ≥0∞)) ∧
        ∀ t ∈ 𝓝 b, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f ⁻¹' t) : ℝ≥0∞)
have ha₁ : ∀ t ∈ 𝓝 a, LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((m : (a : Set β) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: simp only [isOpen_compl_singleton.nhdsWithin_eq hab] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
⊢ IsFiniteMeasure ν
have measure_univ_lt_top : LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
⊢ LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
have measure_univ_lt_top : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [← h_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have this : IsFiniteMeasure ν
Tactic: haveI : IsFiniteMeasure ν := by
    constructor
    rw [← h_univ]
    apply IsFiniteMeasure.measure_univ_lt_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
this : IsFiniteMeasure ν
t : Set α
htm : MeasurableSet t
iht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)
have compl : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
  (ν : (a : Set α) → ℝ≥0∞) tᶜ
Tactic: rw [measure_compl (h t htm) (by finiteness), measure_compl (h t htm) (by finiteness), iht,
      h_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
this : IsFiniteMeasure ν
t : Set α
htm : MeasurableSet t
iht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
compl :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    (ν : (a : Set α) → ℝ≥0∞) tᶜ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)
have compl₁ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [measure_compl (h t htm) (by finiteness), measure_compl (h t htm) (by finiteness), iht,
      h_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
this : IsFiniteMeasure ν
t : Set α
htm : MeasurableSet t
iht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
compl :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    (ν : (a : Set α) → ℝ≥0∞) tᶜ
compl₁ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)
have compl₂ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [measure_compl (h t htm) (by finiteness), measure_compl (h t htm) (by finiteness), iht,
      h_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
this : IsFiniteMeasure ν
t : Set α
htm : MeasurableSet t
iht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
compl :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    (ν : (a : Set α) → ℝ≥0∞) tᶜ
compl₁ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
compl₂ :
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
    HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)
have compl₃ : HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) =
  HSub.hSub (α := ℝ≥0∞) (β := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [measure_compl (h t htm) (by finiteness), measure_compl (h t htm) (by finiteness), iht,
      h_univ]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have empty : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞)
Tactic: induction s, hs using induction_on_inter hA hC with
  | empty => simp
  | basic t ht => exact hμν t ht
  | compl t htm iht =>
    rw [measure_compl (h t htm) (by finiteness), measure_compl (h t htm) (by finiteness), iht,
      h_univ]
  | iUnion f hfd hfm ihf =>
    simp [measure_iUnion, hfd, h _ (hfm _), ihf]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
empty : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞)
basic :
  ∀ (t : Set α) (ht : t ∈ C), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have compl : ∀ (t : Set α) (htm : MeasurableSet t)
  (iht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)
Tactic: induction s, hs using induction_on_inter hA hC with
  | empty => simp
  | basic t ht => exact hμν t ht
  | compl t htm iht =>
    rw [measure_compl (h t htm) (by finiteness), measure_compl (h t htm) (by finiteness), iht,
      h_univ]
  | iUnion f hfd hfm ihf =>
    simp [measure_iUnion, hfd, h _ (hfm _), ihf]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_5
m₀ : MeasurableSpace α
μ ν : Measure α
inst : IsFiniteMeasure μ
C : Set (Set α)
hμν : ∀ s ∈ C, Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
m : MeasurableSpace α
h : m ≤ m₀
hA : m = generateFrom C
hC : IsPiSystem C
h_univ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞)
s : Set α
hs : MeasurableSet s
this : IsFiniteMeasure ν
empty : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞)
basic :
  ∀ (t : Set α) (ht : t ∈ C), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
compl :
  ∀ (t : Set α) (htm : MeasurableSet t)
    (iht : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)),
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) tᶜ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have iUnion : ∀ (f : ℕ → Set α) (hfd : Pairwise (Disjoint on f)) (hfm : ∀ (i : ℕ), MeasurableSet (f i))
  (ihf : ∀ (i : ℕ), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (f i) : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), f i) : ℝ≥0∞)
Tactic: induction s, hs using induction_on_inter hA hC with
  | empty => simp
  | basic t ht => exact hμν t ht
  | compl t htm iht =>
    rw [measure_compl (h t htm) (by finiteness), measure_compl (h t htm) (by finiteness), iht,
      h_univ]
  | iUnion f hfd hfm ihf =>
    simp [measure_iUnion, hfd, h _ (hfm _), ihf]
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : Filter α
⊢ μ.FiniteAtFilter (f ⊓ ae μ) ↔ μ.FiniteAtFilter f
have refine : μ.FiniteAtFilter (f ⊓ ae μ) → μ.FiniteAtFilter f
Tactic: refine ⟨?_, fun h => h.filter_mono inf_le_left⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f : Filter α
t : Set α
ht : t ∈ f
u : Set α
hu : u ∈ ae μ
hμ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ μ.FiniteAtFilter f
have suffices : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ u) : ℝ≥0∞)
Tactic: suffices μ t ≤ μ (t ∩ u) from ⟨t, ht, this.trans_lt hμ⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∃ U ⊇ s, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_1 : ∃ U ⊇ ∅, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine IsCompact.induction_on h ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
refine_1 : ∃ U ⊇ ∅, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ U ⊇ s, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_2 : ∀ ⦃s t : Set α⦄,
  s ⊆ t →
    (∃ U ⊇ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)) →
      ∃ U ⊇ s, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine IsCompact.induction_on h ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
refine_1 : ∃ U ⊇ ∅, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 :
  ∀ ⦃s t : Set α⦄,
    s ⊆ t →
      (∃ U ⊇ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)) →
        ∃ U ⊇ s, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ U ⊇ s, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_3 : ∀ ⦃s t : Set α⦄,
  (∃ U ⊇ s, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)) →
    (∃ U ⊇ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)) →
      ∃ U ⊇ s ∪ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine IsCompact.induction_on h ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
refine_1 : ∃ U ⊇ ∅, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 :
  ∀ ⦃s t : Set α⦄,
    s ⊆ t →
      (∃ U ⊇ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)) →
        ∃ U ⊇ s, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_3 :
  ∀ ⦃s t : Set α⦄,
    (∃ U ⊇ s, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)) →
      (∃ U ⊇ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)) →
        ∃ U ⊇ s ∪ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∃ U ⊇ s, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_4 : ∀ x ∈ s, ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine IsCompact.induction_on h ?_ ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
⊢ ∃ U ⊇ ∅, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
have h₁ : Superset.{u_1} (α := Set α) ∅ ∅ ∧ IsOpen[inst] ∅ ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: use ∅
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
s : Set α
h : IsCompact s
hμ : ∀ x ∈ s, μ.FiniteAtFilter (𝓝 x)
x : α
hx : x ∈ s
⊢ ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
have refine_4 : ∀ (U : Set α) (hU : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)) (hx : x ∈ U)
  (hUo : IsOpen[inst] U),
  ∃ t ∈ 𝓝[s] x, ∃ U ⊇ t, IsOpen[inst] U ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) U : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rcases (hμ x hx).exists_mem_basis (nhds_basis_opens _) with ⟨U, ⟨hx, hUo⟩, hU⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : CompactSpace α
⊢ IsFiniteMeasure μ ↔ IsFiniteMeasureOnCompacts μ
have mp : IsFiniteMeasure μ → IsFiniteMeasureOnCompacts μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
inst : TopologicalSpace α
inst_1 : MeasurableSpace α
μ : Measure α
inst_2 : CompactSpace α
mp : IsFiniteMeasure μ → IsFiniteMeasureOnCompacts μ
⊢ IsFiniteMeasure μ ↔ IsFiniteMeasureOnCompacts μ
have mpr : IsFiniteMeasureOnCompacts μ → IsFiniteMeasure μ
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
⊢ μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K}
have suffices : Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
Tactic: suffices H : Nonempty (μ.FiniteSpanningSetsIn { K | IsOpen K }) from H.some
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
⊢ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
have inl : IsEmpty α → Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
inl : IsEmpty α → Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
⊢ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
have inr : Nonempty α → Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
Tactic: cases isEmpty_or_nonempty α
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : Nonempty α
⊢ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
have inr : ∀ (inhabited_h : Inhabited α), Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
Tactic: inhabit α
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
⊢ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
have inr : ∀ (T : Set (Set α)) (T_count : T.Countable) (TS : T ⊆ S) (hT : ⋃₀ T = ⋃₀ S),
  Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
Tactic: obtain ⟨T, T_count, TS, hT⟩ : ∃ T : Set (Set α), T.Countable ∧ T ⊆ S ∧ ⋃₀ T = ⋃₀ S :=
    isOpen_sUnion_countable S fun s hs => hs.1
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (hypothesis)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = ⋃₀ S
⊢ Nonempty.{u_1 + 1} (μ.FiniteSpanningSetsIn {K : Set α | IsOpen[inst] K})
have hT₁ : ⋃₀ T = univ
Tactic: rw [μ.isTopologicalBasis_isOpen_lt_top.sUnion_eq] at hT
Cleared hypotheses: hT
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Typeclasses.Finite (goal)
Goal:
α : Type u_1
β : Type u_2
δ : Type u_3
ι : Type u_4
inst : TopologicalSpace α
inst_1 : SecondCountableTopology α
m : MeasurableSpace α
μ : Measure α
inst_2 : IsLocallyFiniteMeasure μ
h : Nonempty α
inhabited_h : Inhabited α
S : Set (Set α) := {s : Set α | IsOpen[inst] s ∧ LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)}
T : Set (Set α)
T_count : T.Countable
TS : T ⊆ S
hT : ⋃₀ T = univ
⊢ T.Nonempty
have by_contra : ∀ (h'T : ¬T.Nonempty), False
Tactic: by_contra h'T