awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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
neg : ∀ (p_eq : ¬p = 0), Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | p ≤ f i a}) x
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | p ≤ f i a}) x

Tactic:
by_cases p_eq : p = 0
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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

Tactic:
simp [p_eq]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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
⊢ c ((rs : (a : α) → ℝ≥0) x) = p

Tactic:
simp only [coe_map, mem_preimage, Function.comp_apply, mem_singleton_iff] at hx

Premises used: MeasureTheory.SimpleFunc.coe_map, Set.mem_singleton_iff, Function.comp_apply, Set.mem_preimage
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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
neg :
  ∀ (p_eq : ¬c ((rs : (a : α) → ℝ≥0) x) = 0),
    Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | c ((rs : (a : α) → ℝ≥0) x) ≤ f i a}) x
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | p ≤ f i a}) x

Tactic:
subst hx
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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
rwa₁ rwa₂ rwa₃ rwa₄ : ¬(↑(HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0)) : ℝ≥0∞) = 0
⊢ HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0) ≠ 0

Tactic:
rwa [Ne, ← ENNReal.coe_eq_zero]

Premises used: Ne, ENNReal.coe_eq_zero
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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

Tactic:
have : r * s x ≠ 0 := by rwa [Ne, ← ENNReal.coe_eq_zero]
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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
⊢ Ne (α := ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)

Tactic:
have : s x ≠ 0 := right_ne_zero_of_mul this
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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∞)

Tactic:
lt_of_lt_of_le (ENNReal.coe_lt_coe.2 ?_) (hsf x)

Premises used: Iff.mpr, ENNReal.coe_lt_coe, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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)
refine : LT.lt (α := ℝ≥0) ((rs : (a : α) → ℝ≥0) x : ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0)
⊢ LT.lt (α := ℝ≥0∞) ((SimpleFunc.map c rs : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (⨆ (n : ℕ), f n x : ℝ≥0∞)

Tactic:
refine lt_of_lt_of_le (ENNReal.coe_lt_coe.2 ?_) (hsf x)

Premises used: Iff.mpr, ENNReal.coe_lt_coe, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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_2 : Ne (α := ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
this :
  HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0) <
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) (1 : ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0)
⊢ LT.lt (α := ℝ≥0) ((rs : (a : α) → ℝ≥0) x : ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0)

Tactic:
simpa
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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)
suffices :
  HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0) <
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) (1 : ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0)
⊢ LT.lt (α := ℝ≥0) ((rs : (a : α) → ℝ≥0) x : ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0)

Tactic:
suffices r * s x < 1 * s x by simpa
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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)
ha₁ : LT.lt (α := ℝ≥0) (0 : ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0)
⊢ HMul.hMul (β := ℝ≥0) r ((s : (a : α) → ℝ≥0) x : ℝ≥0) <
    HMul.hMul (α := ℝ≥0) (β := ℝ≥0) (1 : ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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∞)

Tactic:
have : (rs.map c) x < ⨆ n : ℕ, f n x := by
      refine lt_of_lt_of_le (ENNReal.coe_lt_coe.2 ?_) (hsf x)
      suffices r * s x < 1 * s x by simpa
      gcongr
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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_2 : Ne (α := ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
this : LT.lt (α := ℝ≥0∞) ((SimpleFunc.map c rs : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (⨆ (n : ℕ), f n x : ℝ≥0∞)
neg :
  ∀ (i : ℕ) (hi : (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) x < f i x),
    Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | c ((rs : (a : α) → ℝ≥0) x) ≤ f i a}) x
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | c ((rs : (a : α) → ℝ≥0) x) ≤ f i a}) x

Tactic:
rcases lt_iSup_iff.1 this with ⟨i, hi⟩

Premises used: Iff.mp, lt_iSup_iff
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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_2 : Ne (α := ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
this : LT.lt (α := ℝ≥0∞) ((SimpleFunc.map c rs : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (⨆ (n : ℕ), f n x : ℝ≥0∞)
i : ℕ
hi : (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) x < f i x
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | c ((rs : (a : α) → ℝ≥0) x) ≤ f i a}) x

Tactic:
mem_iUnion.2 ⟨i, le_of_lt hi⟩

Premises used: Iff.mpr, Set.mem_iUnion, le_of_lt, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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_2 : Ne (α := ℝ≥0) ((s : (a : α) → ℝ≥0) x : ℝ≥0) (0 : ℝ≥0)
this : LT.lt (α := ℝ≥0∞) ((SimpleFunc.map c rs : (a : α) → ℝ≥0∞) x : ℝ≥0∞) (⨆ (n : ℕ), f n x : ℝ≥0∞)
i : ℕ
hi : (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) x < f i x
⊢ Membership.mem (γ := Set α) (⋃ (i : ℕ), {a : α | c ((rs : (a : α) → ℝ≥0) x) ≤ f i a}) x

Tactic:
exact mem_iUnion.2 ⟨i, le_of_lt hi⟩

Premises used: Iff.mpr, Set.mem_iUnion, le_of_lt, Exists.intro
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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})

Tactic:
have eq : ∀ p, rs.map c ⁻¹' {p} = ⋃ n, rs.map c ⁻¹' {p} ∩ { a | p ≤ f n a } := by
    intro p
    rw [← inter_iUnion]; nth_rw 1 [← inter_univ (map c rs ⁻¹' {p})]
    refine Set.ext fun x => and_congr_right fun hx => (iff_of_eq (true_iff _)).2 ?_
    by_cases p_eq : p = 0
    · simp [p_eq]
    simp only [coe_map, mem_preimage, Function.comp_apply, mem_singleton_iff] at hx
    subst hx
    have : r * s x ≠ 0 := by rwa [Ne, ← ENNReal.coe_eq_zero]
    have : s x ≠ 0 := right_ne_zero_of_mul this
    have : (rs.map c) x < ⨆ n : ℕ, f n x := by
      refine lt_of_lt_of_le (ENNReal.coe_lt_coe.2 ?_) (hsf x)
      suffices r * s x < 1 * s x by simpa
      gcongr
    rcases lt_iSup_iff.1 this with ⟨i, hi⟩
    exact mem_iUnion.2 ⟨i, le_of_lt hi⟩
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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_1 : ℝ≥0
right ha_1 : (↑r_1 : ℝ≥0∞) < 1
ha : r_1 < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r_1 * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r_1 : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (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})
r : ℝ≥0∞
i j : ℕ
h : i ≤ j
refine : Subset.{u_1} (α := Set α) {a : α | r ≤ f i a} {a : α | r ≤ f j a}
⊢ LE.le.{u_1} (α := Set α)
    ((fun (n : ℕ) ↦ (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a} : Set α))
      i)
    ((fun (n : ℕ) ↦ (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a} : Set α))
      j)

Tactic:
refine inter_subset_inter_right _ ?_

Premises used: Set.inter_subset_inter_right
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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_1 : ℝ≥0
right ha_1 : (↑r_1 : ℝ≥0∞) < 1
ha : r_1 < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r_1 * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r_1 : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (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})
r : ℝ≥0∞
i j : ℕ
h : i ≤ j
x : α
hx : r ≤ f i x
⊢ r ≤ f j x

Tactic:
le_trans hx (h_mono h x)

Premises used: le_trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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_1 : ℝ≥0
right ha_1 : (↑r_1 : ℝ≥0∞) < 1
ha : r_1 < 1
rs : α →ₛ ℝ≥0 := SimpleFunc.map (fun (a : ℝ≥0) ↦ r_1 * a) s
eq_rs : SimpleFunc.map c rs = const α (↑r_1 : ℝ≥0∞) * SimpleFunc.map c s
eq :
  ∀ (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})
r : ℝ≥0∞
i j : ℕ
h : i ≤ j
x : α
hx : r ≤ f i x
⊢ r ≤ f j x

Tactic:
exact le_trans hx (h_mono h x)

Premises used: le_trans
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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
eq :
  ∀ (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})
⊢ ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}

Tactic:
have mono : ∀ r : ℝ≥0∞, Monotone fun n => rs.map c ⁻¹' {r} ∩ { a | r ≤ f n a } := by
    intro r i j h
    refine inter_subset_inter_right _ ?_
    simp_rw [subset_def, mem_setOf]
    intro x hx
    exact le_trans hx (h_mono h x)
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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
eq :
  ∀ (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})
mono :
  ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
⊢ ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}

Tactic:
have h_meas : ∀ n, MeasurableSet {a : α | map c rs a ≤ f n a} := fun n =>
    measurableSet_le (SimpleFunc.measurable _) (hf n)
-- Module: Mathlib.MeasureTheory.Integral.Lebesgue.Add
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
eq :
  ∀ (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})
mono :
  ∀ (r : ℝ≥0∞),
    Monotone.{0, u_1} (β := Set α) fun (n : ℕ) ↦
      preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r} ∩ {a : α | r ≤ f n a}
h_meas : ∀ (n : ℕ), MeasurableSet.{u_1} (α := α) {a : α | (SimpleFunc.map c rs : (a : α) → ℝ≥0∞) a ≤ f n a}
rw :
  (const α (↑r : ℝ≥0∞) * SimpleFunc.map c s).lintegral μ =
    ∑ r ∈ (SimpleFunc.map c rs).range,
      HMul.hMul (β := ℝ≥0∞) r
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞)
rw₁ :
  (const α (↑r : ℝ≥0∞) * SimpleFunc.map c s).lintegral μ =
    ∑ r_1 ∈ (const α (↑r : ℝ≥0∞) * SimpleFunc.map c s).range,
      HMul.hMul (β := ℝ≥0∞) r_1
        ((μ : (a : Set α) → ℝ≥0∞)
            (preimage (β := ℝ≥0∞) (⇑(const α (↑r : ℝ≥0∞) * SimpleFunc.map c s) : (a : α) → ℝ≥0∞) {r_1}) :
          ℝ≥0∞)
rw₂ rw₃ :
  Eq (α := ℝ≥0∞)
    (∑ x ∈ (const α (↑r : ℝ≥0∞) * SimpleFunc.map c s).range,
      HMul.hMul (β := ℝ≥0∞) x
        ((μ : (a : Set α) → ℝ≥0∞)
            (preimage (β := ℝ≥0∞) (⇑(const α (↑r : ℝ≥0∞) * SimpleFunc.map c s) : (a : α) → ℝ≥0∞) {x}) :
          ℝ≥0∞))
    (∑ r_1 ∈ (const α (↑r : ℝ≥0∞) * SimpleFunc.map c s).range,
      HMul.hMul (β := ℝ≥0∞) r_1
        ((μ : (a : Set α) → ℝ≥0∞)
            (preimage (β := ℝ≥0∞) (⇑(const α (↑r : ℝ≥0∞) * SimpleFunc.map c s) : (a : α) → ℝ≥0∞) {r_1}) :
          ℝ≥0∞))
⊢ (↑r : ℝ≥0∞) * (SimpleFunc.map c s).lintegral μ =
    ∑ r ∈ (SimpleFunc.map c rs).range,
      HMul.hMul (β := ℝ≥0∞) r
        ((μ : (a : Set α) → ℝ≥0∞) (preimage (β := ℝ≥0∞) (⇑(SimpleFunc.map c rs) : (a : α) → ℝ≥0∞) {r}) : ℝ≥0∞)

Tactic:
rw [← const_mul_lintegral, eq_rs, SimpleFunc.lintegral]

Premises used: MeasureTheory.SimpleFunc.lintegral, MeasureTheory.SimpleFunc.const_mul_lintegral