awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
inst_2 : IsFiniteMeasure μ
f : α → G
C : ℝ
h : ∀ᵐ (x : α) ∂μ, ‖f x‖ ≤ C
rw : μ.real univ • C = C * μ.real univ
rw₁ : μ.real univ * C = C * μ.real univ
⊢ ∫ (x : α), C ∂μ = C * μ.real univ
have rw₂ : C * μ.real univ = C * μ.real univ
Tactic: rw [integral_const, smul_eq_mul, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
hμ : Integrable f μ
hν : Integrable f ν
⊢ ∫ (x : α), f x ∂(μ + ν) = HAdd.hAdd (α := G) (∫ (x : α), f x ∂μ) (∫ (x : α), f x ∂ν)
have simp : setToFun (μ + ν) (weightedSMul (μ + ν)) sorry f = setToFun μ (weightedSMul μ) sorry f + setToFun ν (weightedSMul ν) sorry f
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
hμ : Integrable f μ
hν : Integrable f ν
⊢ setToFun (μ + ν) (weightedSMul (μ + ν)) ⋯ f = setToFun μ (weightedSMul μ) ⋯ f + setToFun ν (weightedSMul ν) ⋯ f
have apply : ∀ (s : Set α) (hs : MeasurableSet s) (h's : LT.lt (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)),
  weightedSMul (μ + ν) s = HAdd.hAdd (α := G →L[ℝ] G) (weightedSMul μ s) (weightedSMul ν s)
Tactic: apply setToFun_add_left'' (fun s hs h's ↦ ?_) hμ hν le_rfl zero_le_one zero_le_one zero_le_one
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
hμ : Integrable f μ
hν : Integrable f ν
s : Set α
hs : MeasurableSet s
h's : LT.lt (α := ℝ≥0∞) ((μ + ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ weightedSMul (μ + ν) s = HAdd.hAdd (α := G →L[ℝ] G) (weightedSMul μ s) (weightedSMul ν s)
have h's₁ : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) ∧
  LT.lt (α := ℝ≥0∞) ((ν : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
Tactic: simp only [Measure.coe_add, Pi.add_apply, add_lt_top] at h's
Cleared hypotheses: h's
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
f : α → G
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m 0 fun (x : α) ↦ f x) 0
have simp : setToFun (m := m) 0 (@weightedSMul _ _ _ _ m 0) sorry f = 0
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
ι : Type u_6
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a : ι
s : Finset ι
h : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, Integrable f (μ i)),
    Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m (∑ i ∈ s, μ i) fun (a : α) ↦ f a) (∑ i ∈ s, ∫ (a : α), f a ∂μ i)
hf : ∀ i ∈ Finset.cons a s h, Integrable f (μ i)
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m (∑ i ∈ Finset.cons a s h, μ i) fun (a : α) ↦ f a)
    (∑ i ∈ Finset.cons a s h, ∫ (a : α), f a ∂μ i)
have hf₁ : Integrable f (μ a) ∧ ∀ x ∈ s, Integrable f (μ x)
Tactic: rw [Finset.forall_mem_cons] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
ι : Type u_6
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
a : ι
s : Finset ι
h : a ∉ s
ih :
  ∀ (hf : ∀ i ∈ s, Integrable f (μ i)),
    Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m (∑ i ∈ s, μ i) fun (a : α) ↦ f a) (∑ i ∈ s, ∫ (a : α), f a ∂μ i)
hf : Integrable f (μ a) ∧ ∀ x ∈ s, Integrable f (μ x)
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m (∑ i ∈ Finset.cons a s h, μ i) fun (a : α) ↦ f a)
    (∑ i ∈ Finset.cons a s h, ∫ (a : α), f a ∂μ i)
have cons : ∫ (a : α), f a ∂(μ a + ∑ x ∈ s, μ x) =
  HAdd.hAdd (α := G) (∫ (a : α), f a ∂μ a) (@integral _ _ _ _ m (∑ i ∈ s, μ i) fun (a : α) ↦ f a)
Tactic: rw [Finset.sum_cons, Finset.sum_cons, ← ih hf.2]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
ι : Type u_6
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
s : Finset ι
hf : ∀ i ∈ s, Integrable f (μ i)
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m (∑ i ∈ s, μ i) fun (a : α) ↦ f a) (∑ i ∈ s, ∫ (a : α), f a ∂μ i)
have empty : ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable f (μ i)),
  Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m (∑ i ∈ ∅, μ i) fun (a : α) ↦ f a) (∑ i ∈ ∅, ∫ (a : α), f a ∂μ i)
Tactic: induction s using Finset.cons_induction_on with
  | empty => simp
  | cons _ _ h ih =>
    rw [Finset.forall_mem_cons] at hf
    rw [Finset.sum_cons, Finset.sum_cons, ← ih hf.2]
    exact integral_add_measure hf.1 (integrable_finsetSum_measure.2 hf.2)
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
ι : Type u_6
m : MeasurableSpace α
f : α → G
μ : ι → Measure α
s : Finset ι
hf : ∀ i ∈ s, Integrable f (μ i)
empty :
  ∀ (hf : ∀ (i : ι), Membership.mem (γ := Finset ι) ∅ i → Integrable f (μ i)),
    Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m (∑ i ∈ ∅, μ i) fun (a : α) ↦ f a) (∑ i ∈ ∅, ∫ (a : α), f a ∂μ i)
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m (∑ i ∈ s, μ i) fun (a : α) ↦ f a) (∑ i ∈ s, ∫ (a : α), f a ∂μ i)
have cons : ∀ (a : ι) (s : Finset ι) (h : a ∉ s)
  (ih :
    ∀ (hf : ∀ i ∈ s, Integrable f (μ i)),
      Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m (∑ i ∈ s, μ i) fun (a : α) ↦ f a) (∑ i ∈ s, ∫ (a : α), f a ∂μ i))
  (hf : ∀ i ∈ Finset.cons a s h, Integrable f (μ i)),
  Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m (∑ i ∈ Finset.cons a s h, μ i) fun (a : α) ↦ f a)
    (∑ i ∈ Finset.cons a s h, ∫ (a : α), f a ∂μ i)
Tactic: induction s using Finset.cons_induction_on with
  | empty => simp
  | cons _ _ h ih =>
    rw [Finset.forall_mem_cons] at hf
    rw [Finset.sum_cons, Finset.sum_cons, ← ih hf.2]
    exact integral_add_measure hf.1 (integrable_finsetSum_measure.2 hf.2)
Cleared hypotheses: s, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ ν : Measure α
f : α → G
h₁ : Integrable f μ
h₂ : Integrable f ν
⊢ (↑(nndist.{u_5} (α := G) (∫ (x : α), f x ∂μ) (∫ (x : α), f x ∂(μ + ν))) : ℝ≥0∞) ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂ν
have rw : (↑(nnnorm.{u_5} (E := G) (∫ (x : α), f x ∂ν)) : ℝ≥0∞) ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂ν
Tactic: rw [integral_add_measure h₁ h₂, nndist_comm, nndist_eq_nnnorm, add_sub_cancel_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
⊢ ∫ (x : α), f x ∂c • μ = HSMul.hSMul (β := G) c.toReal (∫ (x : α), f x ∂μ)
have inl : ∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) ∞ μ = HSMul.hSMul (β := G) (ENNReal.toReal ∞) (∫ (x : α), f x ∂μ)
Tactic: rcases eq_or_ne c ∞ with (rfl | hc)
Cleared hypotheses: c
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
inl : ∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) ∞ μ = HSMul.hSMul (β := G) (ENNReal.toReal ∞) (∫ (x : α), f x ∂μ)
⊢ ∫ (x : α), f x ∂c • μ = HSMul.hSMul (β := G) c.toReal (∫ (x : α), f x ∂μ)
have inr : ∀ (hc : c ≠ ∞), ∫ (x : α), f x ∂c • μ = HSMul.hSMul (β := G) c.toReal (∫ (x : α), f x ∂μ)
Tactic: rcases eq_or_ne c ∞ with (rfl | hc)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
⊢ ∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) ∞ μ = HSMul.hSMul (β := G) (ENNReal.toReal ∞) (∫ (x : α), f x ∂μ)
have inl : ∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) ∞ μ = HSMul.hSMul (α := ℝ) (β := G) 0 (∫ (x : α), f x ∂μ)
Tactic: rw [ENNReal.toReal_top, zero_smul, integral_eq_setToFun, setToFun_top_smul_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
inl : ∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) ∞ μ = HSMul.hSMul (α := ℝ) (β := G) 0 (∫ (x : α), f x ∂μ)
⊢ ∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) ∞ μ = HSMul.hSMul (β := G) (ENNReal.toReal ∞) (∫ (x : α), f x ∂μ)
have inl₁ : Eq.{u_5 + 1} (α := G) (∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) ∞ μ) 0
Tactic: rw [ENNReal.toReal_top, zero_smul, integral_eq_setToFun, setToFun_top_smul_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
inl : ∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) ∞ μ = HSMul.hSMul (α := ℝ) (β := G) 0 (∫ (x : α), f x ∂μ)
inl₁ : Eq.{u_5 + 1} (α := G) (∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) ∞ μ) 0
⊢ ∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) ∞ μ = HSMul.hSMul (β := G) (ENNReal.toReal ∞) (∫ (x : α), f x ∂μ)
have inl₂ : setToFun (HSMul.hSMul (α := ℝ≥0∞) ∞ μ) (weightedSMul (HSMul.hSMul (α := ℝ≥0∞) ∞ μ)) sorry f = 0
Tactic: rw [ENNReal.toReal_top, zero_smul, integral_eq_setToFun, setToFun_top_smul_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
inl : ∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) ∞ μ = HSMul.hSMul (α := ℝ) (β := G) 0 (∫ (x : α), f x ∂μ)
inl₁ : Eq.{u_5 + 1} (α := G) (∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) ∞ μ) 0
inl₂ : setToFun (HSMul.hSMul (α := ℝ≥0∞) ∞ μ) (weightedSMul (HSMul.hSMul (α := ℝ≥0∞) ∞ μ)) ⋯ f = 0
⊢ ∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) ∞ μ = HSMul.hSMul (β := G) (ENNReal.toReal ∞) (∫ (x : α), f x ∂μ)
have inl₃ : Eq.{u_5 + 1} (α := G) 0 0
Tactic: rw [ENNReal.toReal_top, zero_smul, integral_eq_setToFun, setToFun_top_smul_measure]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hc : c ≠ ∞
⊢ ∫ (x : α), f x ∂c • μ = HSMul.hSMul (β := G) c.toReal (∫ (x : α), f x ∂μ)
have inr : setToFun (c • μ) (weightedSMul (c • μ)) sorry f =
  setToFun μ fun (s : Set α) ↦ HSMul.hSMul (β := G →L[ℝ] G) c.toReal (weightedSMul μ s) (C := ‖c.toReal‖ * 1) sorry f
Tactic: simp_rw [integral_eq_setToFun, ← setToFun_smul_left]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hc : c ≠ ∞
⊢ setToFun (c • μ) (weightedSMul (c • μ)) ⋯ f =
    setToFun μ fun (s : Set α) ↦ HSMul.hSMul (β := G →L[ℝ] G) c.toReal (weightedSMul μ s) (C := ‖c.toReal‖ * 1) ⋯ f
have hdfma : DominatedFinMeasAdditive.{u_1, u_5} (β := G →L[ℝ] G) μ (weightedSMul (c • μ)) c.toReal
Tactic: have hdfma : DominatedFinMeasAdditive μ (weightedSMul (c • μ) : Set α → G →L[ℝ] G) c.toReal :=
    mul_one c.toReal ▸ (dominatedFinMeasAdditive_weightedSMul (c • μ)).of_smul_measure hc
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hc : c ≠ ∞
hdfma : DominatedFinMeasAdditive.{u_1, u_5} (β := G →L[ℝ] G) μ (weightedSMul (c • μ)) c.toReal
⊢ setToFun (c • μ) (weightedSMul (c • μ)) ⋯ f =
    setToFun μ fun (s : Set α) ↦ HSMul.hSMul (β := G →L[ℝ] G) c.toReal (weightedSMul μ s) (C := ‖c.toReal‖ * 1) ⋯ f
have hdfma_smul : DominatedFinMeasAdditive.{u_1, u_5} (β := G →L[ℝ] G) (c • μ) (weightedSMul (c • μ)) 1
Tactic: have hdfma_smul := dominatedFinMeasAdditive_weightedSMul (F := G) (c • μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hc : c ≠ ∞
hdfma : DominatedFinMeasAdditive.{u_1, u_5} (β := G →L[ℝ] G) μ (weightedSMul (c • μ)) c.toReal
hdfma_smul : DominatedFinMeasAdditive.{u_1, u_5} (β := G →L[ℝ] G) (c • μ) (weightedSMul (c • μ)) 1
⊢ setToFun (c • μ) (weightedSMul (c • μ)) ⋯ f =
    setToFun μ fun (s : Set α) ↦ HSMul.hSMul (β := G →L[ℝ] G) c.toReal (weightedSMul μ s) (C := ‖c.toReal‖ * 1) ⋯ f
have inr : setToFun μ (weightedSMul (c • μ)) hdfma f =
  setToFun μ fun (s : Set α) ↦ HSMul.hSMul (β := G →L[ℝ] G) c.toReal (weightedSMul μ s) (C := ‖c.toReal‖ * 1) sorry f
Tactic: rw [← setToFun_congr_smul_measure c hc hdfma hdfma_smul f]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst_2 : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ inst_2 (Measure.map φ μ) fun (y : β) ↦ f y) (∫ (x : α), f (φ x) ∂μ)
have pos : ∀ (hfi : @Integrable _ _ _ _ inst_2 f (Measure.map φ μ)),
  Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ inst_2 (Measure.map φ μ) fun (y : β) ↦ f y) (∫ (x : α), f (φ x) ∂μ)
Tactic: by_cases hfi : Integrable f (Measure.map φ μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst_2 : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
pos :
  ∀ (hfi : @Integrable _ _ _ _ inst_2 f (Measure.map φ μ)),
    Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ inst_2 (Measure.map φ μ) fun (y : β) ↦ f y) (∫ (x : α), f (φ x) ∂μ)
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ inst_2 (Measure.map φ μ) fun (y : β) ↦ f y) (∫ (x : α), f (φ x) ∂μ)
have neg : ∀ (hfi : ¬@Integrable _ _ _ _ inst_2 f (Measure.map φ μ)),
  Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ inst_2 (Measure.map φ μ) fun (y : β) ↦ f y) (∫ (x : α), f (φ x) ∂μ)
Tactic: by_cases hfi : Integrable f (Measure.map φ μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst_2 : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hfi : ¬@Integrable _ _ _ _ inst_2 f (Measure.map φ μ)
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ inst_2 (Measure.map φ μ) fun (y : β) ↦ f y) (∫ (x : α), f (φ x) ∂μ)
have neg : ¬Integrable.{u_5, u_1} (ε := G) (fun (x : α) ↦ f (φ x)) μ
Tactic: rw [integral_undef hfi, integral_undef]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst_2 : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hfi : @Integrable _ _ _ _ inst_2 f (Measure.map φ μ)
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ inst_2 (Measure.map φ μ) fun (y : β) ↦ f y) (∫ (x : α), f (φ x) ∂μ)
have pos : setToFun (m := inst_2) (Measure.map φ μ) (@weightedSMul _ _ _ _ inst_2 (Measure.map φ μ)) sorry f =
  setToFun μ (weightedSMul μ) sorry fun (a : α) ↦ f (φ a)
Tactic: simp only [integral_eq_setToFun]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst_2 : MeasurableSpace β
φ : α → β
hφ : Measurable φ
f : β → G
hfm : StronglyMeasurable f
hfi : @Integrable _ _ _ _ inst_2 f (Measure.map φ μ)
⊢ setToFun (m := inst_2) (Measure.map φ μ) (@weightedSMul _ _ _ _ inst_2 (Measure.map φ μ)) ⋯ f =
    setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ f (φ a)
have pos : ∀ (s : Set β) (x : G),
  MeasurableSet s →
    Eq (α := G) ((@weightedSMul _ _ _ _ inst_2 (Measure.map φ μ) s : (a : G) → G) x : G)
      ((weightedSMul μ (φ ⁻¹' s) : (a : G) → G) x : G)
Tactic: apply setToFun_of_le_map_of_stronglyMeasurable _ _
    ((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).1 hfi) hfm hφ le_rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst_2 : MeasurableSpace β
φ : α → β
hφ : AEMeasurable φ μ
f : β → G
hfm : AEStronglyMeasurable (m₀ := inst_2) f (Measure.map φ μ)
g : β → G := AEStronglyMeasurable.mk f hfm
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ inst_2 (Measure.map φ μ) fun (y : β) ↦ g y)
    (@integral _ _ _ _ inst_2 (Measure.map (AEMeasurable.mk φ hφ) μ) fun (y : β) ↦ g y)
have e_μ : Eq (α := Measure β) (Measure.map φ μ) (Measure.map (AEMeasurable.mk φ hφ) μ)
Tactic: congr 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → G
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ x (Measure.map f μ) fun (y : β) ↦ g y) (∫ (x : α), g (f x) ∂μ)
have pos : ∀ (hgm : AEStronglyMeasurable (m₀ := x) g (Measure.map f μ)),
  Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ x (Measure.map f μ) fun (y : β) ↦ g y) (∫ (x : α), g (f x) ∂μ)
Tactic: by_cases hgm : AEStronglyMeasurable g (Measure.map f μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → G
pos :
  ∀ (hgm : AEStronglyMeasurable (m₀ := x) g (Measure.map f μ)),
    Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ x (Measure.map f μ) fun (y : β) ↦ g y) (∫ (x : α), g (f x) ∂μ)
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ x (Measure.map f μ) fun (y : β) ↦ g y) (∫ (x : α), g (f x) ∂μ)
have neg : ∀ (hgm : ¬AEStronglyMeasurable (m₀ := x) g (Measure.map f μ)),
  Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ x (Measure.map f μ) fun (y : β) ↦ g y) (∫ (x : α), g (f x) ∂μ)
Tactic: by_cases hgm : AEStronglyMeasurable g (Measure.map f μ)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x : MeasurableSpace β
f : α → β
hf : MeasurableEmbedding f
g : β → G
hgm : ¬AEStronglyMeasurable (m₀ := x) g (Measure.map f μ)
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ x (Measure.map f μ) fun (y : β) ↦ g y) (∫ (x : α), g (f x) ∂μ)
have neg : ¬AEStronglyMeasurable.{u_1, u_5} (β := G) (fun (x : α) ↦ g (f x)) μ
Tactic: rw [integral_non_aestronglyMeasurable hgm, integral_non_aestronglyMeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (goal)
Goal:
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
α : Type u_6
inst_2 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → G
⊢ Eq.{u_5 + 1} (α := G)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : α) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ) fun (x : (↑s : Type u_6)) ↦ f (↑x : α))
    (∫ (x : α) in s, f x ∂μ)
have rw : Eq.{u_5 + 1} (α := G)
  (@integral _ _ _ _ (Subtype.instMeasurableSpace (p := fun (x : α) ↦ x ∈ s))
    (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ) fun (x : (↑s : Type u_6)) ↦ f (↑x : α))
  (@integral _ _ _ _ inst_2
    (Measure.map (α := { x : α // x ∈ s }) (Subtype.val (p := fun (x : α) ↦ x ∈ s))
      (Measure.comap (Subtype.val (p := fun (x : α) ↦ x ∈ s)) μ))
    fun (x : α) ↦ f x)
Tactic: rw [← map_comap_subtype_coe hs]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Bochner.Basic (hypothesis)
Goal:
α : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hE : CompleteSpace E
inst_2 : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
⊢ (@integral _ _ _ _ inst_2 (Measure.dirac a) fun (x : α) ↦ f x) = f a
have this : let this := borel E;
BorelSpace E
Tactic: borelize E
-- 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
hE : CompleteSpace E
inst_2 : MeasurableSpace α
f : α → E
a : α
hfm : StronglyMeasurable f
this : MeasurableSpace E := borel E
this_1 : BorelSpace E
⊢ (@integral _ _ _ _ inst_2 (Measure.dirac a) fun (x : α) ↦ f x) = f a
have f₁ : (@integral _ _ _ _ inst_2 (Measure.dirac a) fun (x : α) ↦ f a) = f a
Tactic: calc
    ∫ x, f x ∂Measure.dirac a = ∫ _, f a ∂Measure.dirac a :=
      integral_congr_ae <| ae_eq_dirac' hfm.measurable
    _ = f a := by simp
-- 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
hE : CompleteSpace E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst_2 : Decidable (a ∈ s)
⊢ (@integral _ _ _ _ mα (Measure.restrict (Measure.dirac a) s) fun (x : α) ↦ f x) = if a ∈ s then f a else 0
have rw : (@integral _ _ _ _ mα (if a ∈ s then Measure.dirac a else 0) fun (x : α) ↦ f x) = if a ∈ s then f a else 0
Tactic: rw [restrict_dirac' hs]
-- 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
hE : CompleteSpace E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst_2 : Decidable (a ∈ s)
⊢ (@integral _ _ _ _ mα (if a ∈ s then Measure.dirac a else 0) fun (x : α) ↦ f x) = if a ∈ s then f a else 0
have pos : a ∈ s → (@integral _ _ _ _ mα (Measure.dirac a) fun (x : α) ↦ f x) = f a
Tactic: split_ifs
-- 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
hE : CompleteSpace E
mα : MeasurableSpace α
f : α → E
hf : StronglyMeasurable f
a : α
s : Set α
hs : MeasurableSet s
inst_2 : Decidable (a ∈ s)
pos : a ∈ s → (@integral _ _ _ _ mα (Measure.dirac a) fun (x : α) ↦ f x) = f a
⊢ (@integral _ _ _ _ mα (if a ∈ s then Measure.dirac a else 0) fun (x : α) ↦ f x) = if a ∈ s then f a else 0
have neg : a ∉ s → Eq.{u_2 + 1} (α := E) (@integral _ _ _ _ mα 0 fun (x : α) ↦ f x) 0
Tactic: split_ifs
-- 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
hE : CompleteSpace E
inst_2 : MeasurableSpace α
inst_3 : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst_4 : Decidable (a ∈ s)
⊢ (@integral _ _ _ _ inst_2 (Measure.restrict (Measure.dirac a) s) fun (x : α) ↦ f x) = if a ∈ s then f a else 0
have rw : (@integral _ _ _ _ inst_2 (if a ∈ s then Measure.dirac a else 0) fun (x : α) ↦ f x) = if a ∈ s then f a else 0
Tactic: rw [restrict_dirac]
-- 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
hE : CompleteSpace E
inst_2 : MeasurableSpace α
inst_3 : MeasurableSingletonClass α
f : α → E
a : α
s : Set α
inst_4 : Decidable (a ∈ s)
⊢ (@integral _ _ _ _ inst_2 (if a ∈ s then Measure.dirac a else 0) fun (x : α) ↦ f x) = if a ∈ s then f a else 0
have pos : a ∈ s → (@integral _ _ _ _ inst_2 (Measure.dirac a) fun (x : α) ↦ f x) = f a
Tactic: split_ifs