awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
refine : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x (p • a + q • b)) μ
refine₁ : Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ p • f x a + q • f x b) μ
⊢ LE.le.{u_2} (α := E) (∫ (x : α), f x (p • a + q • b) ∂μ) (∫ (x : α), p • f x a + q • f x b ∂μ)
have refine₂ : EventuallyLE.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ f x (p • a + q • b)) fun (x : α) ↦ p • f x a + q • f x b
Tactic: refine integral_mono_ae ?lhs ?rhs ?ae_le
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x (p • a + q • b)) μ
have refine : p • a + q • b ∈ s
Tactic: refine hf_int _ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ p • a + q • b ∈ s
have rw : ∀ (hs : ∀ ⦃x : β⦄, x ∈ s → ∀ ⦃y : β⦄, y ∈ s → ∀ ⦃a b : ℝ⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s)
  (hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x))
  (hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ) ⦃a : β⦄ (ha : a ∈ s) ⦃b : β⦄ (hb : b ∈ s)
  ⦃p q : ℝ⦄ (hp : 0 ≤ p) (hq : 0 ≤ q) (hpq : p + q = 1), p • a + q • b ∈ s
Tactic: rw [convex_iff_add_mem] at hs
Cleared hypotheses: hs, hf_conv, hf_int, a, ha, b, hb, p, q, hp, hq, hpq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ EventuallyLE.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ f x (p • a + q • b)) fun (x : α) ↦ p • f x a + q • f x b
have h : ∀ (x : α) (hx : ConvexOn ℝ s (f x)), f x (p • a + q • b) ≤ p • f x a + q • f x b
Tactic: filter_upwards [hf_conv] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ EventuallyLE.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ f x (p • a + q • b)) fun (x : α) ↦ p • f x a + q • f x b
have h : ∀ (a_1 : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ConvexOn ℝ s (f x)) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            (fun (x : α) ↦
                LE.le.{u_2} (α := E) ((fun (x : α) ↦ f x (p • a + q • b)) x) ((fun (x : α) ↦ p • f x a + q • f x b) x))
              x}
          x}
    a_1
Tactic: case ae_le =>
                    filter_upwards [hf_conv] with x hx
                    exact hx.2 ha hb hp hq hpq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
h :
  ∀ (a_1 : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (x : α) ↦ ConvexOn ℝ s (f x)) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  LE.le.{u_2} (α := E) ((fun (x : α) ↦ f x (p • a + q • b)) x)
                    ((fun (x : α) ↦ p • f x a + q • f x b) x))
                x}
            x}
      a_1
⊢ EventuallyLE.{u_1, u_2} (β := E) (ae μ) (fun (x : α) ↦ f x (p • a + q • b)) fun (x : α) ↦ p • f x a + q • f x b
have h₁ : ∀ (a_1 : α), ConvexOn ℝ s (f a_1) → f a_1 (p • a + q • b) ≤ p • f a_1 a + q • f a_1 b
Tactic: case ae_le =>
                    filter_upwards [hf_conv] with x hx
                    exact hx.2 ha hb hp hq hpq
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ ∫ (x : α), p • f x a + q • f x b ∂μ = HAdd.hAdd (α := E) (∫ (x : α), p • f x a ∂μ) (∫ (x : α), q • f x b ∂μ)
have hf : Integrable.{u_2, u_1} (ε := E) (fun (a_1 : α) ↦ p • f a_1 a) μ
Tactic: apply integral_add
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
hf : Integrable.{u_2, u_1} (ε := E) (fun (a_1 : α) ↦ p • f a_1 a) μ
⊢ ∫ (x : α), p • f x a + q • f x b ∂μ = HAdd.hAdd (α := E) (∫ (x : α), p • f x a ∂μ) (∫ (x : α), q • f x b ∂μ)
have hg : Integrable.{u_2, u_1} (ε := E) (fun (a : α) ↦ q • f a b) μ
Tactic: apply integral_add
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
⊢ (fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) (p • a + q • b) ≤
    HSMul.hSMul (β := E) p ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) a) +
      HSMul.hSMul (β := E) q ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) b)
have calc : LE.le.{u_2} (α := E) (∫ (x : α), f x (p • a + q • b) ∂μ) (∫ (x : α), p • f x a + q • f x b ∂μ)
Tactic: calc ∫ x, f x (p • a + q • b) ∂μ ≤ ∫ x, p • f x a + q • f x b ∂μ := by
                  refine integral_mono_ae ?lhs ?rhs ?ae_le
                  case lhs =>
                    refine hf_int _ ?_
                    rw [convex_iff_add_mem] at hs
                    exact hs ha hb hp hq hpq
                  case rhs => fun_prop (disch := aesop)
                  case ae_le =>
                    filter_upwards [hf_conv] with x hx
                    exact hx.2 ha hb hp hq hpq
            _ = ∫ x, p • f x a ∂μ + ∫ x, q • f x b ∂μ := by
                  apply integral_add
                  all_goals fun_prop (disch := aesop)
            _ = p • ∫ x, f x a ∂μ + q • ∫ x, f x b ∂μ := by simp [integral_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
calc : LE.le.{u_2} (α := E) (∫ (x : α), f x (p • a + q • b) ∂μ) (∫ (x : α), p • f x a + q • f x b ∂μ)
⊢ (fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) (p • a + q • b) ≤
    HSMul.hSMul (β := E) p ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) a) +
      HSMul.hSMul (β := E) q ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) b)
have calc₁ : ∫ (x : α), p • f x a + q • f x b ∂μ = HAdd.hAdd (α := E) (∫ (x : α), p • f x a ∂μ) (∫ (x : α), q • f x b ∂μ)
Tactic: calc ∫ x, f x (p • a + q • b) ∂μ ≤ ∫ x, p • f x a + q • f x b ∂μ := by
                  refine integral_mono_ae ?lhs ?rhs ?ae_le
                  case lhs =>
                    refine hf_int _ ?_
                    rw [convex_iff_add_mem] at hs
                    exact hs ha hb hp hq hpq
                  case rhs => fun_prop (disch := aesop)
                  case ae_le =>
                    filter_upwards [hf_conv] with x hx
                    exact hx.2 ha hb hp hq hpq
            _ = ∫ x, p • f x a ∂μ + ∫ x, q • f x b ∂μ := by
                  apply integral_add
                  all_goals fun_prop (disch := aesop)
            _ = p • ∫ x, f x a ∂μ + q • ∫ x, f x b ∂μ := by simp [integral_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conv : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
a : β
ha : a ∈ s
b : β
hb : b ∈ s
p q : ℝ
hp : 0 ≤ p
hq : 0 ≤ q
hpq : p + q = 1
calc : LE.le.{u_2} (α := E) (∫ (x : α), f x (p • a + q • b) ∂μ) (∫ (x : α), p • f x a + q • f x b ∂μ)
calc₁ : ∫ (x : α), p • f x a + q • f x b ∂μ = HAdd.hAdd (α := E) (∫ (x : α), p • f x a ∂μ) (∫ (x : α), q • f x b ∂μ)
⊢ (fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) (p • a + q • b) ≤
    HSMul.hSMul (β := E) p ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) a) +
      HSMul.hSMul (β := E) q ((fun (b : β) ↦ (∫ (x : α), f x b ∂μ : E)) b)
have calc₂ : HAdd.hAdd (α := E) (∫ (x : α), p • f x a ∂μ) (∫ (x : α), q • f x b ∂μ) =
  HSMul.hSMul (β := E) p (∫ (x : α), f x a ∂μ) + HSMul.hSMul (β := E) q (∫ (x : α), f x b ∂μ)
Tactic: calc ∫ x, f x (p • a + q • b) ∂μ ≤ ∫ x, p • f x a + q • f x b ∂μ := by
                  refine integral_mono_ae ?lhs ?rhs ?ae_le
                  case lhs =>
                    refine hf_int _ ?_
                    rw [convex_iff_add_mem] at hs
                    exact hs ha hb hp hq hpq
                  case rhs => fun_prop (disch := aesop)
                  case ae_le =>
                    filter_upwards [hf_conv] with x hx
                    exact hx.2 ha hb hp hq hpq
            _ = ∫ x, p • f x a ∂μ + ∫ x, q • f x b ∂μ := by
                  apply integral_add
                  all_goals fun_prop (disch := aesop)
            _ = p • ∫ x, f x a ∂μ + q • ∫ x, f x b ∂μ := by simp [integral_smul]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
m : MeasurableSpace α
μ : Measure α
inst_2 : PartialOrder E
inst_3 : IsOrderedAddMonoid E
inst_4 : IsOrderedModule ℝ E
inst_5 : ClosedIciTopology E
β : Type u_6
inst_6 : AddCommMonoid β
inst_7 : Module ℝ β
f : α → β → E
s : Set β
hs : Convex ℝ s
hf_conc : ∀ᵐ (x : α) ∂μ, ConcaveOn ℝ s (f x)
hf_int : ∀ a ∈ s, Integrable.{u_2, u_1} (ε := E) (fun (x : α) ↦ f x a) μ
⊢ ConcaveOn.{0, u_6, u_2} ℝ (β := E) s fun (b : β) ↦ ∫ (x : α), f x b ∂μ
have simp_rw : ∀ (hf_conc : ∀ᵐ (x : α) ∂μ, ConvexOn ℝ s (-f x)),
  ConvexOn.{0, u_6, u_2} ℝ (β := E) s (-fun (b : β) ↦ ∫ (x : α), f x b ∂μ)
Tactic: simp_rw [← neg_convexOn_iff] at hf_conc ⊢
Cleared hypotheses: hf_conc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
⊢ ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫ (a : α), (↑(f a) : ℝ) ∂μ)
have simp_rw : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal
Tactic: simp_rw [integral_eq_lintegral_of_nonneg_ae (Eventually.of_forall fun x => (f x).coe_nonneg)
      hfi.aestronglyMeasurable, ← ENNReal.coe_nnreal_eq]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
⊢ ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ = ENNReal.ofReal (∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ).toReal
have rw : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≠ ∞
Tactic: rw [ENNReal.ofReal_toReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
⊢ ENNReal.ofReal (∫ (x : α), f x ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
have this : f =ᶠ[ae μ] fun (x : α) ↦ ‖f x‖
Tactic: have : f =ᵐ[μ] (‖f ·‖) := f_nn.mono fun _x hx ↦ (abs_of_nonneg hx).symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hfi : Integrable f μ
f_nn : 0 ≤ᶠ[ae μ] f
this : f =ᶠ[ae μ] fun (x : α) ↦ ‖f x‖
⊢ ENNReal.ofReal (∫ (x : α), f x ∂μ) = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
have simp_rw : ∫⁻ (x : α), ENNReal.ofReal ‖f x‖ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
Tactic: simp_rw [integral_congr_ae this, ofReal_integral_norm_eq_lintegral_enorm hfi,
    ← ofReal_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hfm : AEMeasurable f μ
hf : ∀ᵐ (x : α) ∂μ, f x < ∞
⊢ ∫ (a : α), (f a).toReal ∂μ = (∫⁻ (a : α), f a ∂μ).toReal
have rw : (ae μ).EventuallyLE (β := ℝ) 0 fun (x : α) ↦ (f x).toReal
Tactic: rw [integral_eq_lintegral_of_nonneg_ae _ hfm.ennreal_toReal.aestronglyMeasurable,
    lintegral_congr_ae (ofReal_toReal_ae_eq hf)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
b : ℝ≥0
⊢ ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≤ (↑b : ℝ≥0∞) ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
have rw : ENNReal.ofReal (∫ (a : α), (↑(f a) : ℝ) ∂μ) ≤ (↑b : ℝ≥0∞) ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
Tactic: rw [lintegral_coe_eq_integral f hfi, ENNReal.ofReal, ENNReal.coe_le_coe,
    Real.toNNReal_le_iff_le_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
b : ℝ≥0
rw : ENNReal.ofReal (∫ (a : α), (↑(f a) : ℝ) ∂μ) ≤ (↑b : ℝ≥0∞) ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
⊢ ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≤ (↑b : ℝ≥0∞) ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
have rw₁ : (↑(Real.toNNReal (∫ (a : α), (↑(f a) : ℝ) ∂μ)) : ℝ≥0∞) ≤ (↑b : ℝ≥0∞) ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
Tactic: rw [lintegral_coe_eq_integral f hfi, ENNReal.ofReal, ENNReal.coe_le_coe,
    Real.toNNReal_le_iff_le_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
b : ℝ≥0
rw : ENNReal.ofReal (∫ (a : α), (↑(f a) : ℝ) ∂μ) ≤ (↑b : ℝ≥0∞) ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
rw₁ : (↑(Real.toNNReal (∫ (a : α), (↑(f a) : ℝ) ∂μ)) : ℝ≥0∞) ≤ (↑b : ℝ≥0∞) ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
⊢ ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≤ (↑b : ℝ≥0∞) ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
have rw₂ : Real.toNNReal (∫ (a : α), (↑(f a) : ℝ) ∂μ) ≤ b ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
Tactic: rw [lintegral_coe_eq_integral f hfi, ENNReal.ofReal, ENNReal.coe_le_coe,
    Real.toNNReal_le_iff_le_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
hfi : Integrable (ε := ℝ) (fun (x : α) ↦ (↑(f x) : ℝ)) μ
b : ℝ≥0
rw : ENNReal.ofReal (∫ (a : α), (↑(f a) : ℝ) ∂μ) ≤ (↑b : ℝ≥0∞) ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
rw₁ : (↑(Real.toNNReal (∫ (a : α), (↑(f a) : ℝ) ∂μ)) : ℝ≥0∞) ≤ (↑b : ℝ≥0∞) ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
rw₂ : Real.toNNReal (∫ (a : α), (↑(f a) : ℝ) ∂μ) ≤ b ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
⊢ ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≤ (↑b : ℝ≥0∞) ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
have rw₃ : ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ) ↔ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
Tactic: rw [lintegral_coe_eq_integral f hfi, ENNReal.ofReal, ENNReal.coe_le_coe,
    Real.toNNReal_le_iff_le_coe]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≤ (↑b : ℝ≥0∞)
⊢ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
have pos : ∀ (hf : Integrable (ε := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) μ), ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
Tactic: by_cases hf : Integrable (fun a => (f a : ℝ)) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≤ (↑b : ℝ≥0∞)
pos : ∀ (hf : Integrable (ε := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) μ), ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
⊢ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
have neg : ∀ (hf : ¬Integrable (ε := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) μ), ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
Tactic: by_cases hf : Integrable (fun a => (f a : ℝ)) μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0
b : ℝ≥0
h : ∫⁻ (a : α), (↑(f a) : ℝ≥0∞) ∂μ ≤ (↑b : ℝ≥0∞)
hf : ¬Integrable (ε := ℝ) (fun (a : α) ↦ (↑(f a) : ℝ)) μ
⊢ ∫ (a : α), (↑(f a) : ℝ) ∂μ ≤ (↑b : ℝ)
have neg : 0 ≤ (↑b : ℝ)
Tactic: rw [integral_undef hf]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ Eq (α := ℝ) (∫ (x : α), f x ∂μ) 0 ↔ f =ᶠ[ae μ] 0
have simp_rw : ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = 0 ↔ f =ᶠ[ae μ] 0
Tactic: simp_rw [integral_eq_lintegral_of_nonneg_ae hf hfi.1, ENNReal.toReal_eq_zero_iff,
    ← ENNReal.not_lt_top, ← hasFiniteIntegral_iff_ofReal hf, hfi.2, not_true_eq_false, or_false]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = 0 ↔ f =ᶠ[ae μ] 0
have rw : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f a)) 0 ↔ f =ᶠ[ae μ] 0
Tactic: rw [lintegral_eq_zero_iff']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
rw : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f a)) 0 ↔ f =ᶠ[ae μ] 0
⊢ ∫⁻ (a : α), ENNReal.ofReal (f a) ∂μ = 0 ↔ f =ᶠ[ae μ] 0
have rw₁ : AEMeasurable (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f a)) μ
Tactic: rw [lintegral_eq_zero_iff']
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (a : α) ↦ ENNReal.ofReal (f a)) 0 ↔ f =ᶠ[ae μ] 0
have rw : (∀ᵐ (x : α) ∂μ, ENNReal.ofReal (f x) = 0 x) ↔ ∀ᵐ (x : α) ∂μ, f x ≤ 0 x
Tactic: rw [← hf.ge_iff_eq', Filter.EventuallyEq, Filter.EventuallyLE]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
⊢ Eq (α := ℝ) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ) ↔ f =ᶠ[ae μ] g
have refine : ∀ (h_le : Eq (α := ℝ) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)), g =ᶠ[ae μ] f
Tactic: refine ⟨fun h_le ↦ EventuallyEq.symm ?_, fun h ↦ integral_congr_ae h⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ
hf : Integrable f μ
hg : Integrable g μ
hfg : f ≤ᶠ[ae μ] g
h_le : Eq (α := ℝ) (∫ (a : α), f a ∂μ) (∫ (a : α), g a ∂μ)
⊢ g =ᶠ[ae μ] f
have rw : Eq (α := ℝ) (∫ (x : α), (g - f) x ∂μ) 0
Tactic: rw [← sub_ae_eq_zero,
    ← integral_eq_zero_iff_of_nonneg_ae ((sub_nonneg_ae _ _).mpr hfg) (hg.sub hf)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
⊢ LT.lt (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)
have simp_rw : Ne (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)
Tactic: simp_rw [(integral_nonneg_of_ae hf).lt_iff_ne, pos_iff_ne_zero, Ne, @eq_comm ℝ 0,
    integral_eq_zero_iff_of_nonneg_ae hf hfi, Filter.EventuallyEq, ae_iff, Pi.zero_apply,
    Function.support]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : 0 ≤ᶠ[ae μ] f
hfi : Integrable f μ
simp_rw :
  Ne (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)
⊢ LT.lt (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔
    LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞)
have simp_rw₁ : Ne (α := ℝ) 0 (∫ (x : α), f x ∂μ) ↔ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (Function.support f) : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [(integral_nonneg_of_ae hf).lt_iff_ne, pos_iff_ne_zero, Ne, @eq_comm ℝ 0,
    integral_eq_zero_iff_of_nonneg_ae hf hfi, Filter.EventuallyEq, ae_iff, Pi.zero_apply,
    Function.support]