awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : ∀ᵐ (a : α) ∂μ, a ∈ t
⊢ s ≤ᶠ[ae μ] t ∩ s
have h₁ : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ a ∈ t) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ s x ≤ (t ∩ s) x) x} x}
    a
Tactic: filter_upwards [h] with x hx h'x using ⟨hx, h'x⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : ∀ᵐ (a : α) ∂μ, a ∈ t
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ a ∈ t) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ s x ≤ (t ∩ s) x) x} x}
      a
⊢ s ≤ᶠ[ae μ] t ∩ s
have h₂ : ∀ a ∈ t, s a ≤ (t ∩ s) a
Tactic: filter_upwards [h] with x hx h'x using ⟨hx, h'x⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
h : ∀ᵐ (a : α) ∂μ, a ∈ t
h₁ :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ a ∈ t) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ s x ≤ (t ∩ s) x) x} x}
      a
h₂ : ∀ a ∈ t, s a ≤ (t ∩ s) a
⊢ s ≤ᶠ[ae μ] t ∩ s
have h₃ : ∀ (x : α) (hx : x ∈ t) (h'x : s x), (t ∩ s) x
Tactic: filter_upwards [h] with x hx h'x using ⟨hx, h'x⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ms : MeasurableSpace α
h : ms ≤ OuterMeasure.caratheodory 0
⊢ OuterMeasure.toMeasure 0 h = 0
have h₁ : ∀ (s : Set α) (hs : MeasurableSet s),
  Eq (α := ℝ≥0∞) ((OuterMeasure.toMeasure 0 h : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s hs
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ms : MeasurableSpace α
μ : OuterMeasure α
h : ms ≤ μ.caratheodory
hμ : μ.toMeasure h = 0
⊢ μ = 0
have h₁ : ∀ (s : Set α), Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (((0 : OuterMeasure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
inst : IsEmpty α
x : MeasurableSpace α
μ : Measure α
s : Set α
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [eq_empty_of_isEmpty s, measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
inst : IsEmpty α
x : MeasurableSpace α
μ : Measure α
s : Set α
rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) ∅ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [eq_empty_of_isEmpty s, measure_empty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ_1 μ₁ μ₂ μ₃ ν_1 ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst_1 : IsEmpty α
m : MeasurableSpace α
μ ν : Measure α
⊢ μ = ν
have h : ∀ (s : Set α), MeasurableSet s → Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext1 s _
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ_1 μ₁ μ₂ μ₃ ν_1 ν' ν₁ ν₂ : Measure α
s_1 s' t : Set α
inst_1 : IsEmpty α
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h : MeasurableSet s
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h : Eq (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ_1 μ₁ μ₂ μ₃ ν_1 ν' ν₁ ν₂ : Measure α
s_1 s' t : Set α
inst_1 : IsEmpty α
m : MeasurableSpace α
μ ν : Measure α
s : Set α
h_1 : MeasurableSet s
h : Eq (α := ℝ≥0∞) (0 : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have h₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [apply_eq_zero_of_isEmpty, apply_eq_zero_of_isEmpty]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
⊢ Eq.{u_1 + 1} (α := Measure α) (ofMeasurable (fun (x : Set α) (x_1 : MeasurableSet x) ↦ 0) ⋯ ⋯) 0
have h : ∀ (s : Set α),
  MeasurableSet s →
    Eq (α := ℝ≥0∞)
      (((ofMeasurable (fun (x : Set α) (x_1 : MeasurableSet x) ↦ 0) sorry sorry : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
      (((0 : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: ext s
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁_1 μ₂_1 μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s' t : Set α
x : MeasurableSpace α
μ₁ μ₂ : Measure α
s : ℕ → Set α
hs : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
      ((μ₂ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) =
    ∑' (i : ℕ),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
        ((μ₂ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
    ((μ₂ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (∑' (a : ℕ), (μ₁ : (a : Set α) → ℝ≥0∞) (s a)) (∑' (a : ℕ), (μ₂ : (a : Set α) → ℝ≥0∞) (s a))
Tactic: rw [ENNReal.tsum_add, measure_iUnion hd hs, measure_iUnion hd hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁_1 μ₂_1 μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s' t : Set α
x : MeasurableSpace α
μ₁ μ₂ : Measure α
s : ℕ → Set α
hs : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
      ((μ₂ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (∑' (a : ℕ), (μ₁ : (a : Set α) → ℝ≥0∞) (s a)) (∑' (a : ℕ), (μ₂ : (a : Set α) → ℝ≥0∞) (s a))
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
      ((μ₂ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) =
    ∑' (i : ℕ),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
        ((μ₂ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw₁ : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (∑' (i : ℕ), (μ₁ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
    ((μ₂ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) =
  HAdd.hAdd (α := ℝ≥0∞) (∑' (a : ℕ), (μ₁ : (a : Set α) → ℝ≥0∞) (s a)) (∑' (a : ℕ), (μ₂ : (a : Set α) → ℝ≥0∞) (s a))
Tactic: rw [ENNReal.tsum_add, measure_iUnion hd hs, measure_iUnion hd hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁_1 μ₂_1 μ₃ ν ν' ν₁ ν₂ : Measure α
s_1 s' t : Set α
x : MeasurableSpace α
μ₁ μ₂ : Measure α
s : ℕ → Set α
hs : ∀ (i : ℕ), MeasurableSet (s i)
hd : Pairwise (Disjoint on s)
rw :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
      ((μ₂ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (∑' (a : ℕ), (μ₁ : (a : Set α) → ℝ≥0∞) (s a)) (∑' (a : ℕ), (μ₂ : (a : Set α) → ℝ≥0∞) (s a))
rw₁ :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) (∑' (i : ℕ), (μ₁ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
      ((μ₂ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) =
    HAdd.hAdd (α := ℝ≥0∞) (∑' (a : ℕ), (μ₁ : (a : Set α) → ℝ≥0∞) (s a)) (∑' (a : ℕ), (μ₂ : (a : Set α) → ℝ≥0∞) (s a))
⊢ HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞)
      ((μ₂ : (a : Set α) → ℝ≥0∞) (⋃ (i : ℕ), s i) : ℝ≥0∞) =
    ∑' (i : ℕ),
      HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ₁ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
        ((μ₂ : (a : Set α) → ℝ≥0∞) (s i) : ℝ≥0∞)
have rw₂ : HAdd.hAdd (α := ℝ≥0∞) (∑' (i : ℕ), (μ₁ : (a : Set α) → ℝ≥0∞) (s i)) (∑' (i : ℕ), (μ₂ : (a : Set α) → ℝ≥0∞) (s i)) =
  HAdd.hAdd (α := ℝ≥0∞) (∑' (a : ℕ), (μ₁ : (a : Set α) → ℝ≥0∞) (s a)) (∑' (a : ℕ), (μ₂ : (a : Set α) → ℝ≥0∞) (s a))
Tactic: rw [ENNReal.tsum_add, measure_iUnion hd hs, measure_iUnion hd hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁_1 μ₂_1 μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
x : MeasurableSpace α
μ₁ μ₂ : Measure α
⊢ (μ₁.toOuterMeasure + μ₂.toOuterMeasure).trim ≤ μ₁.toOuterMeasure + μ₂.toOuterMeasure
have rw : μ₁.trim + μ₂.trim ≤ μ₁.toOuterMeasure + μ₂.toOuterMeasure
Tactic: rw [OuterMeasure.trim_add, μ₁.trimmed, μ₂.trimmed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁_1 μ₂_1 μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
x : MeasurableSpace α
μ₁ μ₂ : Measure α
rw : μ₁.trim + μ₂.trim ≤ μ₁.toOuterMeasure + μ₂.toOuterMeasure
⊢ (μ₁.toOuterMeasure + μ₂.toOuterMeasure).trim ≤ μ₁.toOuterMeasure + μ₂.toOuterMeasure
have rw₁ : μ₁.toOuterMeasure + μ₂.trim ≤ μ₁.toOuterMeasure + μ₂.toOuterMeasure
Tactic: rw [OuterMeasure.trim_add, μ₁.trimmed, μ₂.trimmed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ μ₁_1 μ₂_1 μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
x : MeasurableSpace α
μ₁ μ₂ : Measure α
rw : μ₁.trim + μ₂.trim ≤ μ₁.toOuterMeasure + μ₂.toOuterMeasure
rw₁ : μ₁.toOuterMeasure + μ₂.trim ≤ μ₁.toOuterMeasure + μ₂.toOuterMeasure
⊢ (μ₁.toOuterMeasure + μ₂.toOuterMeasure).trim ≤ μ₁.toOuterMeasure + μ₂.toOuterMeasure
have rw₂ : μ₁.toOuterMeasure + μ₂.toOuterMeasure ≤ μ₁.toOuterMeasure + μ₂.toOuterMeasure
Tactic: rw [OuterMeasure.trim_add, μ₁.trimmed, μ₂.trimmed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ_1 μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_3 : SMul R' ℝ≥0∞
inst_4 : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
x : MeasurableSpace α
c : R
μ : Measure α
⊢ (c • μ.toOuterMeasure).trim ≤ c • μ.toOuterMeasure
have rw : c • μ.trim ≤ c • μ.toOuterMeasure
Tactic: rw [OuterMeasure.trim_smul, μ.trimmed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
β : Type u_2
γ : Type u_3
δ : Type u_4
ι : Type u_5
R : Type u_6
R' : Type u_7
m0 : MeasurableSpace α
mβ : MeasurableSpace β
inst : MeasurableSpace γ
μ_1 μ₁ μ₂ μ₃ ν ν' ν₁ ν₂ : Measure α
s s' t : Set α
inst_1 : SMul R ℝ≥0∞
inst_2 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_3 : SMul R' ℝ≥0∞
inst_4 : IsScalarTower R' ℝ≥0∞ ℝ≥0∞
x : MeasurableSpace α
c : R
μ : Measure α
rw : c • μ.trim ≤ c • μ.toOuterMeasure
⊢ (c • μ.toOuterMeasure).trim ≤ c • μ.toOuterMeasure
have rw₁ : c • μ.toOuterMeasure ≤ c • μ.toOuterMeasure
Tactic: rw [OuterMeasure.trim_smul, μ.trimmed]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
I : Finset ι
μ : ι → Measure α
s : Set α
⊢ Eq (α := ℝ≥0∞) (((∑ i ∈ I, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (∑ i ∈ I, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw : Eq (α := ℝ≥0∞) ((∑ i ∈ I, (⇑(μ i) : (a : Set α) → ℝ≥0∞)) s) (∑ i ∈ I, (μ i : (a : Set α) → ℝ≥0∞) s)
Tactic: rw [coe_finsetSum, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
ι : Type u_5
m : MeasurableSpace α
I : Finset ι
μ : ι → Measure α
s : Set α
rw : Eq (α := ℝ≥0∞) ((∑ i ∈ I, (⇑(μ i) : (a : Set α) → ℝ≥0∞)) s) (∑ i ∈ I, (μ i : (a : Set α) → ℝ≥0∞) s)
⊢ Eq (α := ℝ≥0∞) (((∑ i ∈ I, μ i : Measure α) : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
    (∑ i ∈ I, (μ i : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have rw₁ : Eq (α := ℝ≥0∞) (∑ c ∈ I, (μ c : (a : Set α) → ℝ≥0∞) s) (∑ i ∈ I, (μ i : (a : Set α) → ℝ≥0∞) s)
Tactic: rw [coe_finsetSum, Finset.sum_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
R : Type u_6
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, p x
c : R
⊢ Eq (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) {a : α | ¬p a} : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬p a} : ℝ≥0∞) = 0
Tactic: rw [smul_apply, ae_iff.1 h, ← smul_one_smul ℝ≥0∞, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
R : Type u_6
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, p x
c : R
rw : HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬p a} : ℝ≥0∞) = 0
⊢ Eq (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) {a : α | ¬p a} : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₁ : HSMul.hSMul (β := ℝ≥0∞) c 0 = 0
Tactic: rw [smul_apply, ae_iff.1 h, ← smul_one_smul ℝ≥0∞, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
R : Type u_6
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, p x
c : R
rw : HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬p a} : ℝ≥0∞) = 0
rw₁ : HSMul.hSMul (β := ℝ≥0∞) c 0 = 0
⊢ Eq (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) {a : α | ¬p a} : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₂ : HSMul.hSMul (β := ℝ≥0∞) (HSMul.hSMul (β := ℝ≥0∞) c 1) 0 = 0
Tactic: rw [smul_apply, ae_iff.1 h, ← smul_one_smul ℝ≥0∞, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
R : Type u_6
m0 : MeasurableSpace α
μ : Measure α
p : α → Prop
inst : SMul R ℝ≥0∞
inst_1 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
h : ∀ᵐ (x : α) ∂μ, p x
c : R
rw : HSMul.hSMul (β := ℝ≥0∞) c ((μ : (a : Set α) → ℝ≥0∞) {a : α | ¬p a} : ℝ≥0∞) = 0
rw₁ : HSMul.hSMul (β := ℝ≥0∞) c 0 = 0
rw₂ : HSMul.hSMul (β := ℝ≥0∞) (HSMul.hSMul (β := ℝ≥0∞) c 1) 0 = 0
⊢ Eq (α := ℝ≥0∞) ((c • μ : (a : Set α) → ℝ≥0∞) {a : α | ¬p a} : ℝ≥0∞) (0 : ℝ≥0∞)
have rw₃ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [smul_apply, ae_iff.1 h, ← smul_one_smul ℝ≥0∞, smul_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
R : Type u_8
inst : Semiring R
inst_1 : IsDomain R
inst_2 : Module R ℝ≥0∞
inst_3 : IsScalarTower R ℝ≥0∞ ℝ≥0∞
inst_4 : Module.IsTorsionFree R ℝ≥0∞
c : R
hc : c ≠ 0
μ : Measure α
⊢ ae (c • μ) = ae μ
have h : ∀ (s : Set α), s ∈ ae (c • μ) ↔ s ∈ ae μ
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
c : ℝ≥0∞
hc : c ≠ 0
μ : Measure α
⊢ ae (c • μ) = ae μ
have h : ∀ (s : Set α), s ∈ ae (c • μ) ↔ s ∈ ae μ
Tactic: ext
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : s ⊆ t
h'' : Eq (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
Tactic: refine le_antisymm (measure_mono h') ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : s ⊆ t
h'' : Eq (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have this : HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: have : μ t + ν t ≤ μ s + ν t :=
    calc
      μ t + ν t = μ s + ν s := h''.symm
      _ ≤ μ s + ν t := by gcongr
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : s ⊆ t
h'' : Eq (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
this :
  HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ≤
    HAdd.hAdd (α := ℝ≥0∞) (β := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞)
have apply : Ne (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: apply ENNReal.le_of_add_le_add_right _ this
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : s ⊆ t
h'' : Eq (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h₁ : Ne (α := ℝ≥0∞) ((ν + μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [add_comm] at h'' h
Cleared hypotheses: h, h', h''
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
h : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h' : s ⊆ t
h'' : Eq (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
h₁ : Ne (α := ℝ≥0∞) ((ν + μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h'₁ : s ⊆ t
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
have h''₁ : Eq (α := ℝ≥0∞) ((ν + μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((ν + μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [add_comm] at h'' h
Cleared hypotheses: h, h', h''
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (μ + ν) t ∩ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have refine_1 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (μ + ν) t) : ℝ≥0∞)
Tactic: refine (measure_inter_eq_of_measure_eq hs ?_ (subset_toMeasurable _ _) ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (μ + ν) t) : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (μ + ν) t ∩ s) : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have refine_2 : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine (measure_inter_eq_of_measure_eq hs ?_ (subset_toMeasurable _ _) ?_).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (toMeasurable (μ + ν) t) : ℝ≥0∞)
have refine_1 : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) (toMeasurable (μ + ν) t) : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: refine
      measure_eq_left_of_subset_of_measure_add_eq ?_ (subset_toMeasurable _ _)
        (measure_toMeasurable t).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
have ht₁ : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
  ¬Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: simp only [not_or, ENNReal.add_eq_top, Pi.add_apply, Ne, coe_add] at ht
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ ν : Measure α
s t : Set α
hs : MeasurableSet s
ht : Ne (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (toMeasurable (μ + ν) t ∩ s) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
have rw : ∀ (ht : Ne (α := ℝ≥0∞) ((ν + μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)),
  Eq (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) (toMeasurable (ν + μ) t ∩ s) : ℝ≥0∞)
    ((ν : (a : Set α) → ℝ≥0∞) (t ∩ s) : ℝ≥0∞)
Tactic: rw [add_comm] at ht ⊢
Cleared hypotheses: ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
have rw : MeasurableSet s
Tactic: rw [OuterMeasure.sInf_eq_boundedBy_sInfGen]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
⊢ MeasurableSet s
have refine : ∀ (t : Set α),
  OuterMeasure.sInfGen (toOuterMeasure '' m) (t ∩ s) + OuterMeasure.sInfGen (toOuterMeasure '' m) (t \ s) ≤
    OuterMeasure.sInfGen (toOuterMeasure '' m) t
Tactic: refine OuterMeasure.boundedBy_caratheodory fun t => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s : Set α
hs : MeasurableSet s
t : Set α
⊢ OuterMeasure.sInfGen (toOuterMeasure '' m) (t ∩ s) + OuterMeasure.sInfGen (toOuterMeasure '' m) (t \ s) ≤
    OuterMeasure.sInfGen (toOuterMeasure '' m) t
have simp : ∀ ⦃x : Measure α⦄,
  x ∈ m →
    ∀ (i : Set α) (i_1 : t ⊆ i) (i_2 : MeasurableSet i),
      HAdd.hAdd (α := ℝ≥0∞) (⨅ μ ∈ toOuterMeasure '' m, (μ : (a : Set α) → ℝ≥0∞) (t ∩ s))
          (⨅ μ ∈ toOuterMeasure '' m, (μ : (a : Set α) → ℝ≥0∞) (t \ s)) ≤
        (x : (a : Set α) → ℝ≥0∞) i
Tactic: simp only [OuterMeasure.sInfGen, le_iInf_iff, forall_mem_image, measure_eq_iInf t,
    coe_toOuterMeasure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Measure.MeasureSpace (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
m : Set (Measure α)
s_1 : Set α
hs : MeasurableSet s_1
t_1 : Set α
μ : Measure α
hμ : μ ∈ m
u : Set α
htu : t_1 ⊆ u
_hu : MeasurableSet u
s t : Set α
hst : s ⊆ t
⊢ OuterMeasure.sInfGen (toOuterMeasure '' m) s ≤ (μ : (a : Set α) → ℝ≥0∞) t
have rw : LE.le (α := ℝ≥0∞) (⨅ b ∈ m, (b.toOuterMeasure : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞)
Tactic: rw [OuterMeasure.sInfGen_def, iInf_image]