awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegular
simp_rw : (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ ¬μ = 0
simp_rw₁ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₂ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ¬Eq (α := ℝ≥0∞) (⨆ (K : Set α), ⨆ (_ : K ⊆ univ), ⨆ (_ : IsCompact K), (μ : (a : Set α) → ℝ≥0∞) K) 0
simp_rw₃ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ¬∀ (i : Set α) (i_1 : i ⊆ univ) (i_2 : IsCompact i), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (∃ (K : Set α), IsCompact K ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ μ ≠ 0
have simp_rw₄ : (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
  ∃ (x : Set α) (_ : x ⊆ univ) (_ : IsCompact x), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [Ne, ← measure_univ_eq_zero, MeasurableSet.univ.measure_eq_iSup_isCompact,
    ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegular
simp_rw : (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ ¬μ = 0
simp_rw₁ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₂ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ¬Eq (α := ℝ≥0∞) (⨆ (K : Set α), ⨆ (_ : K ⊆ univ), ⨆ (_ : IsCompact K), (μ : (a : Set α) → ℝ≥0∞) K) 0
simp_rw₃ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ¬∀ (i : Set α) (i_1 : i ⊆ univ) (i_2 : IsCompact i), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₄ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ∃ (x : Set α) (_ : x ⊆ univ) (_ : IsCompact x), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (∃ (K : Set α), IsCompact K ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ μ ≠ 0
have simp_rw₅ : (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
  ∃ x ⊆ univ, IsCompact x ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [Ne, ← measure_univ_eq_zero, MeasurableSet.univ.measure_eq_iSup_isCompact,
    ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : μ.InnerRegular
simp_rw : (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ ¬μ = 0
simp_rw₁ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₂ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ¬Eq (α := ℝ≥0∞) (⨆ (K : Set α), ⨆ (_ : K ⊆ univ), ⨆ (_ : IsCompact K), (μ : (a : Set α) → ℝ≥0∞) K) 0
simp_rw₃ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ¬∀ (i : Set α) (i_1 : i ⊆ univ) (i_2 : IsCompact i), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) i : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₄ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ∃ (x : Set α) (_ : x ⊆ univ) (_ : IsCompact x), ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
simp_rw₅ :
  (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
    ∃ x ⊆ univ, IsCompact x ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ (∃ (K : Set α), IsCompact K ∧ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔ μ ≠ 0
have simp_rw₆ : (∃ (K : Set α), IsCompact K ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) (0 : ℝ≥0∞)) ↔
  ∃ (x : Set α), True ∧ IsCompact x ∧ ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) x : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [Ne, ← measure_univ_eq_zero, MeasurableSet.univ.measure_eq_iSup_isCompact,
    ENNReal.iSup_eq_zero, not_forall, exists_prop, subset_univ, true_and]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
f : α ≃ₜ β
⊢ InnerRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ) ↔ μ.InnerRegular
have refine : ∀ (h : InnerRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)), μ.InnerRegular
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ h.map f⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
f : α ≃ₜ β
h : InnerRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
⊢ μ.InnerRegular
have h₁ : μ = map.{u_2, u_1} (α := β) (⇑f.symm : (a : β) → α) (map (⇑f : (a : α) → β) μ)
Tactic: convert! h.map f.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ : Measure α
inst_1 : TopologicalSpace α
inst_2 : BorelSpace α
inst_3 : MeasurableSpace β
inst_4 : TopologicalSpace β
inst_5 : BorelSpace β
f : α ≃ₜ β
h : InnerRegular.{u_2} (α := β) (map (⇑f : (a : α) → β) μ)
⊢ μ = map.{u_2, u_1} (α := β) (⇑f.symm : (a : β) → α) (map (⇑f : (a : α) → β) μ)
have h₁ : μ = map (Function.comp.{u_1 + 1, u_2 + 1, u_1 + 1} (β := β) (⇑f.symm : (a : β) → α) (⇑f : (a : α) → β)) μ
Tactic: rw [map_map f.symm.continuous.measurable f.continuous.measurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
⊢ (μ + ν).InnerRegular
have innerRegular : (μ + ν).InnerRegularWRT IsCompact MeasurableSet
Tactic: constructor
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
have innerRegular : ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
Tactic: rcases eq_or_ne (μ s) 0 with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
innerRegular :
  ∀ (h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
have innerRegular₁ : ∀ (h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
Tactic: rcases eq_or_ne (μ s) 0 with h | h
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
have hr₁ : r < (ν : (a : Set α) → ℝ≥0∞) s
Tactic: simp only [h, zero_add] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
h : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hr : r < (ν : (a : Set α) → ℝ≥0∞) s
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
have innerRegular : ∀ (K : Set α) (Ks : K ⊆ s) (hK : IsCompact K) (h'K : r < (ν : (a : Set α) → ℝ≥0∞) K),
  ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
Tactic: rcases MeasurableSet.exists_lt_isCompact hs hr with ⟨K, Ks, hK, h'K⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
have innerRegular : ∀ (h' : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
Tactic: rcases eq_or_ne (ν s) 0 with h' | h'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
innerRegular :
  ∀ (h' : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
    ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
have innerRegular₁ : ∀ (h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)),
  ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
Tactic: rcases eq_or_ne (ν s) 0 with h' | h'
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (hypothesis)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
have hr₁ : r < (μ : (a : Set α) → ℝ≥0∞) s
Tactic: simp only [h', add_zero] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
hr : r < (μ : (a : Set α) → ℝ≥0∞) s
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
have innerRegular : ∀ (K : Set α) (Ks : K ⊆ s) (hK : IsCompact K) (h'K : r < (μ : (a : Set α) → ℝ≥0∞) K),
  ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
Tactic: rcases MeasurableSet.exists_lt_isCompact hs hr with ⟨K, Ks, hK, h'K⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
have innerRegular : ∀ (u : ℝ≥0∞) (hu : u < (μ : (a : Set α) → ℝ≥0∞) s) (v : ℝ≥0∞) (hv : v < (ν : (a : Set α) → ℝ≥0∞) s) (huv : r < u + v),
  ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
Tactic: rcases ENNReal.exists_lt_add_of_lt_add hr h h' with ⟨u, hu, v, hv, huv⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℝ≥0∞
hu : u < (μ : (a : Set α) → ℝ≥0∞) s
v : ℝ≥0∞
hv : v < (ν : (a : Set α) → ℝ≥0∞) s
huv : r < u + v
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
have innerRegular : ∀ (K : Set α) (Ks : K ⊆ s) (hK : IsCompact K) (h'K : u < (μ : (a : Set α) → ℝ≥0∞) K),
  ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
Tactic: rcases MeasurableSet.exists_lt_isCompact hs hu with ⟨K, Ks, hK, h'K⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℝ≥0∞
hu : u < (μ : (a : Set α) → ℝ≥0∞) s
v : ℝ≥0∞
hv : v < (ν : (a : Set α) → ℝ≥0∞) s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < (μ : (a : Set α) → ℝ≥0∞) K
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
have innerRegular : ∀ (K' : Set α) (K's : K' ⊆ s) (hK' : IsCompact K') (h'K' : v < (ν : (a : Set α) → ℝ≥0∞) K'),
  ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
Tactic: rcases MeasurableSet.exists_lt_isCompact hs hv with ⟨K', K's, hK', h'K'⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℝ≥0∞
hu : u < (μ : (a : Set α) → ℝ≥0∞) s
v : ℝ≥0∞
hv : v < (ν : (a : Set α) → ℝ≥0∞) s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < (μ : (a : Set α) → ℝ≥0∞) K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < (ν : (a : Set α) → ℝ≥0∞) K'
⊢ ∃ K ⊆ s, IsCompact K ∧ r < (μ + ν : (a : Set α) → ℝ≥0∞) K
have innerRegular : u + v ≤ (μ + ν : (a : Set α) → ℝ≥0∞) (K ∪ K')
Tactic: refine ⟨K ∪ K', union_subset Ks K's, hK.union hK', huv.trans_le ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℝ≥0∞
hu : u < (μ : (a : Set α) → ℝ≥0∞) s
v : ℝ≥0∞
hv : v < (ν : (a : Set α) → ℝ≥0∞) s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < (μ : (a : Set α) → ℝ≥0∞) K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < (ν : (a : Set α) → ℝ≥0∞) K'
⊢ u + v ≤ (μ + ν : (a : Set α) → ℝ≥0∞) (K ∪ K')
have innerRegular : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) K' : ℝ≥0∞) ≤
  (μ + ν : (a : Set α) → ℝ≥0∞) (K ∪ K')
Tactic: apply (add_le_add h'K.le h'K'.le).trans
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℝ≥0∞
hu : u < (μ : (a : Set α) → ℝ≥0∞) s
v : ℝ≥0∞
hv : v < (ν : (a : Set α) → ℝ≥0∞) s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < (μ : (a : Set α) → ℝ≥0∞) K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < (ν : (a : Set α) → ℝ≥0∞) K'
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) K' : ℝ≥0∞) ≤
    (μ + ν : (a : Set α) → ℝ≥0∞) (K ∪ K')
have innerRegular : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) K' : ℝ≥0∞) ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K ∪ K') : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (K ∪ K') : ℝ≥0∞)
Tactic: simp only [Measure.coe_add, Pi.add_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℝ≥0∞
hu : u < (μ : (a : Set α) → ℝ≥0∞) s
v : ℝ≥0∞
hv : v < (ν : (a : Set α) → ℝ≥0∞) s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < (μ : (a : Set α) → ℝ≥0∞) K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < (ν : (a : Set α) → ℝ≥0∞) K'
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) K' : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K ∪ K') : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (K ∪ K') : ℝ≥0∞)
have innerRegular : K ⊆ K ∪ K'
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
μ ν : Measure α
inst_2 : μ.InnerRegular
inst_3 : ν.InnerRegular
s : Set α
hs : MeasurableSet s
r : ℝ≥0∞
hr : r < HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
h' : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
u : ℝ≥0∞
hu : u < (μ : (a : Set α) → ℝ≥0∞) s
v : ℝ≥0∞
hv : v < (ν : (a : Set α) → ℝ≥0∞) s
huv : r < u + v
K : Set α
Ks : K ⊆ s
hK : IsCompact K
h'K : u < (μ : (a : Set α) → ℝ≥0∞) K
K' : Set α
K's : K' ⊆ s
hK' : IsCompact K'
h'K' : v < (ν : (a : Set α) → ℝ≥0∞) K'
innerRegular : K ⊆ K ∪ K'
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) K : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) K' : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (K ∪ K') : ℝ≥0∞)
      ((ν : (a : Set α) → ℝ≥0∞) (K ∪ K') : ℝ≥0∞)
have innerRegular₁ : K' ⊆ K ∪ K'
Tactic: gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
a : ι
s : Finset ι
ha : a ∉ s
ih : InnerRegular.{u_1} (α := α) (∑ i ∈ s, μ i)
⊢ InnerRegular.{u_1} (α := α) (∑ i ∈ insert a s, μ i)
have insert : (μ a + ∑ i ∈ s, μ i).InnerRegular
Tactic: simp only [ha, not_false_eq_true, Finset.sum_insert]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
a : Finset ι
⊢ InnerRegular.{u_1} (α := α) (∑ i ∈ a, μ i)
have empty : InnerRegular.{u_1} (α := α) (∑ i ∈ ∅, μ i)
Tactic: induction a using Finset.induction with
  | empty => simp only [Finset.sum_empty]; infer_instance
  | insert a s ha ih => simp only [ha, not_false_eq_true, Finset.sum_insert]; infer_instance
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
a : Finset ι
empty : InnerRegular.{u_1} (α := α) (∑ i ∈ ∅, μ i)
⊢ InnerRegular.{u_1} (α := α) (∑ i ∈ a, μ i)
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s) (ih : InnerRegular.{u_1} (α := α) (∑ i ∈ s, μ i)),
  InnerRegular.{u_1} (α := α) (∑ i ∈ insert a s, μ i)
Tactic: induction a using Finset.induction with
  | empty => simp only [Finset.sum_empty]; infer_instance
  | insert a s ha ih => simp only [ha, not_false_eq_true, Finset.sum_insert]; infer_instance
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
a : Finset ι
⊢ InnerRegular.{u_1} (α := α) (∑ i ∈ a, μ i)
have empty : InnerRegular.{u_1} (α := α) (∑ i ∈ ∅, μ i)
Tactic: classical
  induction a using Finset.induction with
  | empty => simp only [Finset.sum_empty]; infer_instance
  | insert a s ha ih => simp only [ha, not_false_eq_true, Finset.sum_insert]; infer_instance
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
a : Finset ι
empty : InnerRegular.{u_1} (α := α) (∑ i ∈ ∅, μ i)
⊢ InnerRegular.{u_1} (α := α) (∑ i ∈ a, μ i)
have insert : ∀ (a : ι) (s : Finset ι) (ha : a ∉ s) (ih : InnerRegular.{u_1} (α := α) (∑ i ∈ s, μ i)),
  InnerRegular.{u_1} (α := α) (∑ i ∈ insert a s, μ i)
Tactic: classical
  induction a using Finset.induction with
  | empty => simp only [Finset.sum_empty]; infer_instance
  | insert a s ha ih => simp only [ha, not_false_eq_true, Finset.sum_insert]; infer_instance
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.Regular (goal)
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
μ_1 : Measure α
inst_1 : TopologicalSpace α
ι : Type u_3
μ : ι → Measure α
inst_2 : ∀ (i : ι), (μ i).InnerRegular
⊢ (sum μ).InnerRegular
have innerRegular : (sum μ).InnerRegularWRT IsCompact MeasurableSet
Tactic: constructor