awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
key : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ = ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
lhs_finite : ∫⁻ (ω : α), ENNReal.ofReal (f ω) ∂μ < ∞
rhs_finite : ∫⁻ (t : ℝ) in Ioi 0, (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} < ∞
rhs_integrand_finite : ∀ t > 0, LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Measurable (β := ℝ) fun (t : ℝ) ↦ μ.real {a : α | t < f a}
have h : Measurable (β := ℝ≥0∞) fun (t : ℝ) ↦ (μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a}
Tactic: refine Measurable.ennreal_toReal ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
⊢ Eq (α := ℝ) (∫ (ω : α), f ω ∂μ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t ≤ f a})
have rw : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    μ.real {a : α | t < f a})
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    μ.real {a : α | t ≤ f a})
Tactic: rw [Integrable.integral_eq_integral_meas_lt f_intble f_nn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t < f a})
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t ≤ f a})
have h : (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ)
  (fun (a : ℝ) ↦ μ.real {a_1 : α | a < f a_1}) fun (a : ℝ) ↦ μ.real {a_1 : α | a ≤ f a_1}
Tactic: apply integral_congr_ae
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Ioi 0))).EventuallyEq (β := ℝ)
    (fun (a : ℝ) ↦ μ.real {a_1 : α | a < f a_1}) fun (a : ℝ) ↦ μ.real {a_1 : α | a ≤ f a_1}
have h : ∀ (t : ℝ)
  (ht :
    Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞)
      ((μ : (a : Set α) → ℝ≥0∞) {a : α | t < f a} : ℝ≥0∞)),
  μ.real {a : α | t < f a} = μ.real {a : α | t ≤ f a}
Tactic: filter_upwards [meas_le_ae_eq_meas_lt μ (volume.restrict (Ioi 0)) f] with t ht
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
⊢ Eq (α := ℝ) (∫ (ω : α), f ω ∂μ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 M)) fun (t : ℝ) ↦
      μ.real {a : α | t ≤ f a})
have rw : Eq (α := ℝ)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
    μ.real {a : α | t ≤ f a})
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 M)) fun (t : ℝ) ↦
    μ.real {a : α | t ≤ f a})
Tactic: rw [f_intble.integral_eq_integral_meas_le f_nn]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioi 0)) fun (t : ℝ) ↦
      μ.real {a : α | t ≤ f a})
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace (Measure.restrict volume (Ioc 0 M)) fun (t : ℝ) ↦
      μ.real {a : α | t ≤ f a})
have rw : ∀ᵐ (x : ℝ), x ∈ Ioi 0 \ Ioc 0 M → μ.real {a : α | x ≤ f a} = 0
Tactic: rw [setIntegral_eq_of_subset_of_ae_diff_eq_zero
      nullMeasurableSet_Ioi Ioc_subset_Ioi_self ?_]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
⊢ ∀ᵐ (x : ℝ), x ∈ Ioi 0 \ Ioc 0 M → μ.real {a : α | x ≤ f a} = 0
have apply : ∀ (t : ℝ) (ht : t ∈ Ioi 0 \ Ioc 0 M), μ.real {a : α | t ≤ f a} = 0
Tactic: apply Eventually.of_forall (fun t ht ↦ ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
⊢ μ.real {a : α | t ≤ f a} = 0
have htM : M < t
Tactic: have htM : M < t := by simp_all only [mem_diff, mem_Ioi, mem_Ioc, not_and, not_le]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | M < f a} : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : ∀ᵐ (a : α) ∂μ, a ∉ {a : α | M < f a}
Tactic: rw [measure_eq_zero_iff_ae_notMem]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
⊢ ∀ᵐ (a : α) ∂μ, a ∉ {a : α | M < f a}
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ (fun (x : α) ↦ M) x) x} x →
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ a ∉ {a : α | M < f a}) x} x}
    a
Tactic: filter_upwards [f_bdd] with a ha using not_lt.mpr ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ f x ≤ (fun (x : α) ↦ M) x) x} x →
          Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ a ∉ {a : α | M < f a}) x} x}
      a
⊢ ∀ᵐ (a : α) ∂μ, a ∉ {a : α | M < f a}
have h₁ : ∀ (a : α), f a ≤ M → ¬M < f a
Tactic: filter_upwards [f_bdd] with a ha using not_lt.mpr ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (hypothesis)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
⊢ μ.real {a : α | t ≤ f a} = 0
have obs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | M < f a} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: have obs : μ {a | M < f a} = 0 := by
    rw [measure_eq_zero_iff_ae_notMem]
    filter_upwards [f_bdd] with a ha using not_lt.mpr ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Layercake (goal)
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
f : α → ℝ
M : ℝ
f_intble : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
f_bdd : f ≤ᶠ[ae μ] fun (x : α) ↦ M
t : ℝ
ht : t ∈ Ioi 0 \ Ioc 0 M
htM : M < t
obs : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | M < f a} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ μ.real {a : α | t ≤ f a} = 0
have rw : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (0 : ℝ≥0∞) ∨
  Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | t ≤ f a} : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: rw [measureReal_def, ENNReal.toReal_eq_zero_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
⊢ lintegral μ F = ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have refine : lintegral μ F ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
Tactic: refine le_antisymm ?_ (iSup_lintegral_le _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
⊢ lintegral μ F ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have rw : LE.le (α := ℝ≥0∞)
  (⨆ (φ : α →ₛ ℝ≥0),
    ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x), (SimpleFunc.map ofNNReal φ).lintegral μ)
  (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)
Tactic: rw [lintegral_eq_nnreal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
⊢ LE.le (α := ℝ≥0∞)
    (⨆ (φ : α →ₛ ℝ≥0),
      ⨆ (_ : ∀ (x : α), (↑((φ : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x), (SimpleFunc.map ofNNReal φ).lintegral μ)
    (⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ)
have refine : ∀ (s : α →ₛ ℝ≥0) (hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x),
  (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
Tactic: refine iSup_le fun s => iSup_le fun hsf => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
⊢ (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have refine : ∀ (a : ℝ≥0∞) (ha : a < 1), a * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
Tactic: refine ENNReal.le_of_forall_lt_one_mul_le fun a ha => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
a : ℝ≥0∞
ha : a < 1
⊢ a * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have rcases : ∀ (r : ℝ≥0),
  (↑r : ℝ≥0∞) < 1 →
    ∀ (ha : (↑r : ℝ≥0∞) < 1), (↑r : ℝ≥0∞) * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
Tactic: rcases ENNReal.lt_iff_exists_coe.1 ha with ⟨r, rfl, _⟩
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha : (↑r : ℝ≥0∞) < 1
⊢ (↑r : ℝ≥0∞) * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have ha₁ : r < 1
Tactic: have ha : r < 1 := ENNReal.coe_lt_coe.1 ha
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
⊢ (↑r : ℝ≥0∞) * (SimpleFunc.map ofNNReal s).lintegral μ ≤ ⨆ (n : ℕ), ∫⁻ (a : α), f n a ∂μ
have eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
Tactic: have eq_rs : rs.map c = (const α r : α →ₛ ℝ≥0∞) * map c s := rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
p : ℝ≥0∞
⊢ Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
    (⋃ (n : ℕ), preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ {a : α | p ≤ f n a})
have rw : Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
  (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ ⋃ (i : ℕ), {a : α | p ≤ f i a})
Tactic: rw [← inter_iUnion]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
p : ℝ≥0∞
⊢ Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p})
    (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ ⋃ (i : ℕ), {a : α | p ≤ f i a})
have nth_rw : Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ univ)
  (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ ⋃ (i : ℕ), {a : α | p ≤ f i a})
Tactic: nth_rw 1 [← inter_univ (map c rs ⁻¹' {p})]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
p : ℝ≥0∞
⊢ Eq (α := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ univ)
    (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p} ∩ ⋃ (i : ℕ), {a : α | p ≤ f i a})
have refine : ∀ (x : α) (hx : Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p}) x),
  Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | p ≤ f i a}) x
Tactic: refine Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff _)).2 ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
p : ℝ≥0∞
x : α
hx : Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p}) x
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | p ≤ f i a}) x
have pos : ∀ (p_eq : p = 0), Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | p ≤ f i a}) x
Tactic: by_cases p_eq : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
p : ℝ≥0∞
x : α
hx : Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p}) x
pos : ∀ (p_eq : p = 0), Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | p ≤ f i a}) x
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | p ≤ f i a}) x
have neg : ∀ (p_eq : ¬p = 0), Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | p ≤ f i a}) x
Tactic: by_cases p_eq : p = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
p : ℝ≥0∞
x : α
hx : Membership.mem (γ := Set α) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {p}) x
p_eq : ¬p = 0
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | p ≤ f i a}) x
have hx₁ : c ((rs : (a : α) → ℝ≥0) x) = p
Tactic: simp only [coe_map, mem_preimage, Function.comp_apply, mem_singleton_iff] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
p : ℝ≥0∞
x : α
p_eq : ¬p = 0
hx : c ((rs : (a : α) → ℝ≥0) x) = p
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | p ≤ f i a}) x
have neg : ∀ (p_eq : ¬c ((rs : (a : α) → ℝ≥0) x) = 0),
  Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | c ((rs : (a : α) → ℝ≥0) x) ≤ f i a}) x
Tactic: subst hx
Cleared hypotheses: p, p_eq, hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
x : α
p_eq : ¬c ((rs : (a : α) → ℝ≥0) x) = 0
⊢ HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0) ≠ 0
have rwa : ¬HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0) = 0
Tactic: rwa [Ne, ← ENNReal.coe_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
x : α
p_eq : ¬c ((rs : (a : α) → ℝ≥0) x) = 0
rwa : ¬HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0) = 0
⊢ HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0) ≠ 0
have rwa₁ : ¬(↑(HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0)) : ℝ≥0∞) = 0
Tactic: rwa [Ne, ← ENNReal.coe_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
x : α
p_eq : ¬c ((rs : (a : α) → ℝ≥0) x) = 0
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | c ((rs : (a : α) → ℝ≥0) x) ≤ f i a}) x
have this : HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0) ≠ 0
Tactic: have : r * s x ≠ 0 := by rwa [Ne, ← ENNReal.coe_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
x : α
p_eq : ¬c ((rs : (a : α) → ℝ≥0) x) = 0
this : HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0) ≠ 0
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | c ((rs : (a : α) → ℝ≥0) x) ≤ f i a}) x
have this₁ : Ne (α := ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
Tactic: have : s x ≠ 0 := right_ne_zero_of_mul this
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
x : α
p_eq : ¬c ((rs : (a : α) → ℝ≥0) x) = 0
this_1 : HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0) ≠ 0
this : Ne (α := ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
⊢ LT.lt (α := ℝ≥0∞) ((SimpleFunc.map c rs : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (⨆ (n : ℕ), f n x : ℝ≥0∞)
have refine : LT.lt (α := ℝ≥0) ((rs : (a : α) → ℝ≥0) x : ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0)
Tactic: refine lt_of_lt_of_le (ENNReal.coe_lt_coe.2 ?_) (hsf x)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Lebesgue.Add (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : ℕ → α → ℝ≥0∞
hf : ∀ (n : ℕ), Measurable (f n)
h_mono : Monotone f
c : ℝ≥0 → ℝ≥0∞ := ofNNReal
F : (a : α) → ℝ≥0∞ := fun (a : α) ↦ ⨆ (n : ℕ), f n a
s : α →ₛ ℝ≥0
hsf : ∀ (x : α), (↑((s : (a : α) → ℝ≥0) x) : ℝ≥0∞) ≤ ⨆ (n : ℕ), f n x
r : ℝ≥0
right ha_1 : (↑r : ℝ≥0∞) < 1
ha : r < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r : ℝ≥0∞) * SimpleFunc.map c s
x : α
p_eq : ¬c ((rs : (a : α) → ℝ≥0) x) = 0
this_1 : HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0) ≠ 0
this : Ne (α := ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
⊢ LT.lt (α := ℝ≥0) ((rs : (a : α) → ℝ≥0) x : ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0)
have suffices : HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0) <
  HMul.hMul (α := ℝ≥0) (β := ℝ≥0) (1 : ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0)
Tactic: suffices r * s x < 1 * s x by simpa