awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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)
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)
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ m (∑ i ∈ s, μ i) fun (a : α) ↦ f a) (∑ i ∈ s, ∫ (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)

Premises used: Finset.sum_cons, Finset.forall_mem_cons
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 ν
rw : (↑(nnnorm.{u_5} (E := G) (∫ (x : α), f x ∂ν)) : ℝ≥0∞) ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂ν
⊢ (↑(nndist.{u_5} (α := G) (∫ (x : α), f x ∂μ) (∫ (x : α), f x ∂(μ + ν))) : ℝ≥0∞) ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂ν

Tactic:
rw [integral_add_measure h₁ h₂, nndist_comm, nndist_eq_nnnorm, add_sub_cancel_left]

Premises used: MeasureTheory.integral_add_measure, add_sub_cancel_left, nndist_comm, nndist_eq_nnnorm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 ν
⊢ (↑(nnnorm.{u_5} (E := G) (∫ (x : α), f x ∂ν)) : ℝ≥0∞) ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂ν

Tactic:
enorm_integral_le_lintegral_enorm _

Premises used: MeasureTheory.enorm_integral_le_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 ν
⊢ (↑(nnnorm.{u_5} (E := G) (∫ (x : α), f x ∂ν)) : ℝ≥0∞) ≤ ∫⁻ (x : α), ‖f x‖ₑ ∂ν

Tactic:
exact enorm_integral_le_lintegral_enorm _

Premises used: MeasureTheory.enorm_integral_le_lintegral_enorm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 ∂μ)
inr : ∀ (hc : c ≠ ∞), ∫ (x : α), f x ∂c • μ = HSMul.hSMul (β := G) c.toReal (∫ (x : α), f x ∂μ)
⊢ ∫ (x : α), f x ∂c • μ = HSMul.hSMul (β := G) c.toReal (∫ (x : α), f x ∂μ)

Tactic:
rcases eq_or_ne c ∞ with (rfl | hc)

Premises used: eq_or_ne, Top.top, rfl
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
inl₃ inl₄ : Eq.{u_5 + 1} (α := G) 0 0
⊢ ∫ (x : α), f x ∂HSMul.hSMul (α := ℝ≥0∞) ∞ μ = HSMul.hSMul (β := G) (ENNReal.toReal ∞) (∫ (x : α), f x ∂μ)

Tactic:
rw [ENNReal.toReal_top, zero_smul, integral_eq_setToFun, setToFun_top_smul_measure]

Premises used: MeasureTheory.setToFun_top_smul_measure, zero_smul, MeasureTheory.integral_eq_setToFun, ENNReal.toReal_top
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hc : c ≠ ∞
inr :
  setToFun (c • μ) (weightedSMul (c • μ)) ⋯ f =
    setToFun μ fun (s : Set α) ↦ HSMul.hSMul (β := G →L[ℝ] G) c.toReal (weightedSMul μ s) (C := ‖c.toReal‖ * 1) ⋯ f
⊢ ∫ (x : α), f x ∂c • μ = HSMul.hSMul (β := G) c.toReal (∫ (x : α), f x ∂μ)

Tactic:
simp_rw [integral_eq_setToFun, ← setToFun_smul_left]

Premises used: MeasureTheory.setToFun_smul_left, MeasureTheory.integral_eq_setToFun
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
f : α → G
c : ℝ≥0∞
hc : c ≠ ∞
⊢ 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
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
⊢ DominatedFinMeasAdditive.{u_1, u_5} (β := G →L[ℝ] G) (c • μ) (weightedSMul (c • μ)) 1

Tactic:
have hdfma_smul := dominatedFinMeasAdditive_weightedSMul (F := G) (c • μ)
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
inr :
  setToFun μ (weightedSMul (c • μ)) hdfma f =
    setToFun μ fun (s : Set α) ↦ HSMul.hSMul (β := G →L[ℝ] G) c.toReal (weightedSMul μ s) (C := ‖c.toReal‖ * 1) ⋯ f
⊢ setToFun (c • μ) (weightedSMul (c • μ)) ⋯ f =
    setToFun μ fun (s : Set α) ↦ HSMul.hSMul (β := G →L[ℝ] G) c.toReal (weightedSMul μ s) (C := ‖c.toReal‖ * 1) ⋯ f

Tactic:
rw [← setToFun_congr_smul_measure c hc hdfma hdfma_smul f]

Premises used: MeasureTheory.setToFun_congr_smul_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 μ (weightedSMul (c • μ)) hdfma f =
    setToFun μ fun (s : Set α) ↦ HSMul.hSMul (β := G →L[ℝ] G) c.toReal (weightedSMul μ s) (C := ‖c.toReal‖ * 1) ⋯ f

Tactic:
setToFun_congr_left' _ _ (fun s _ _ => weightedSMul_smul_measure μ c) f

Premises used: MeasureTheory.setToFun_congr_left', MeasureTheory.weightedSMul_smul_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 μ (weightedSMul (c • μ)) hdfma f =
    setToFun μ fun (s : Set α) ↦ HSMul.hSMul (β := G →L[ℝ] G) c.toReal (weightedSMul μ s) (C := ‖c.toReal‖ * 1) ⋯ f

Tactic:
exact setToFun_congr_left' _ _ (fun s _ _ => weightedSMul_smul_measure μ c) f

Premises used: MeasureTheory.setToFun_congr_left', MeasureTheory.weightedSMul_smul_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 (∫ (x : α), f x ∂μ)

Tactic:
integral_smul_measure f (c : ℝ≥0∞)

Premises used: ENNReal.ofNNReal, ENNReal.toNNReal, ENNReal.toReal, WithTop.untopD, WithTop.recTopCoe, MeasureTheory.integral_smul_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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) ∂μ)
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) ∂μ)
⊢ 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 φ μ)

Premises used: MeasureTheory.Integrable, MeasureTheory.Measure.map
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 φ μ)
neg : ¬Integrable.{u_5, u_1} (ε := G) (fun (x : α) ↦ f (φ x)) μ
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ inst_2 (Measure.map φ μ) fun (y : β) ↦ f y) (∫ (x : α), f (φ x) ∂μ)

Tactic:
rw [integral_undef hfi, integral_undef]

Premises used: MeasureTheory.integral_undef
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 φ μ)
⊢ ¬Integrable.{u_5, u_1} (ε := G) (fun (x : α) ↦ f (φ x)) μ

Tactic:
fun hfφ => hfi ((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).2 hfφ)

Premises used: Iff.mpr, Measurable.aemeasurable, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.integrable_map_measure, Not
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 φ μ)
⊢ ¬Integrable.{u_5, u_1} (ε := G) (fun (x : α) ↦ f (φ x)) μ

Tactic:
exact fun hfφ => hfi ((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).2 hfφ)

Premises used: Iff.mpr, Measurable.aemeasurable, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.integrable_map_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 φ μ)
pos :
  setToFun (m := inst_2) (Measure.map φ μ) (@weightedSMul _ _ _ _ inst_2 (Measure.map φ μ)) ⋯ f =
    setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ f (φ a)
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ inst_2 (Measure.map φ μ) fun (y : β) ↦ f y) (∫ (x : α), f (φ x) ∂μ)

Tactic:
simp only [integral_eq_setToFun]

Premises used: MeasureTheory.integral_eq_setToFun
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 φ μ)
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)
⊢ setToFun (m := inst_2) (Measure.map φ μ) (@weightedSMul _ _ _ _ inst_2 (Measure.map φ μ)) ⋯ f =
    setToFun μ (weightedSMul μ) ⋯ fun (a : α) ↦ f (φ a)

Tactic:
apply setToFun_of_le_map_of_stronglyMeasurable _ _
    ((integrable_map_measure hfm.aestronglyMeasurable hφ.aemeasurable).1 hfi) hfm hφ le_rfl

Premises used: le_rfl, Measurable.aemeasurable, MeasureTheory.StronglyMeasurable.aestronglyMeasurable, MeasureTheory.setToFun_of_le_map_of_stronglyMeasurable, Iff.mp, MeasureTheory.integrable_map_measure
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 φ μ)
s : Set β
x : G
hs : MeasurableSet s
⊢ Eq (α := G) ((@weightedSMul _ _ _ _ inst_2 (Measure.map φ μ) s : (a : G) → G) x : G)
    ((weightedSMul μ (φ ⁻¹' s) : (a : G) → G) x : G)

Tactic:
simp [weightedSMul_apply, map_measureReal_apply, hs, hφ]

Premises used: MeasureTheory.weightedSMul_apply, MeasureTheory.map_measureReal_apply
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
e_μ : Eq (α := Measure β) (Measure.map φ μ) (Measure.map (AEMeasurable.mk φ hφ) μ)
⊢ 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)

Tactic:
congr 1
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 (α := Measure β) (Measure.map φ μ) (Measure.map (AEMeasurable.mk φ hφ) μ)

Tactic:
Measure.map_congr hφ.ae_eq_mk

Premises used: MeasureTheory.Measure.map_congr, AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 (α := Measure β) (Measure.map φ μ) (Measure.map (AEMeasurable.mk φ hφ) μ)

Tactic:
exact Measure.map_congr hφ.ae_eq_mk

Premises used: MeasureTheory.Measure.map_congr, AEMeasurable.ae_eq_mk
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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) ∂μ)
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) ∂μ)
⊢ 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 μ)

Premises used: MeasureTheory.Measure.map, MeasureTheory.AEStronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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) ∂μ)

Tactic:
MeasureTheory.integral_map hf.measurable.aemeasurable hgm

Premises used: Measurable.aemeasurable, MeasureTheory.integral_map, MeasurableEmbedding.measurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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) ∂μ)

Tactic:
exact MeasureTheory.integral_map hf.measurable.aemeasurable hgm

Premises used: Measurable.aemeasurable, MeasureTheory.integral_map, MeasurableEmbedding.measurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 μ)
neg : ¬AEStronglyMeasurable.{u_1, u_5} (β := G) (fun (x : α) ↦ g (f x)) μ
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ x (Measure.map f μ) fun (y : β) ↦ g y) (∫ (x : α), g (f x) ∂μ)

Tactic:
rw [integral_non_aestronglyMeasurable hgm, integral_non_aestronglyMeasurable]

Premises used: MeasureTheory.integral_non_aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 μ)
⊢ ¬AEStronglyMeasurable.{u_1, u_5} (β := G) (fun (x : α) ↦ g (f x)) μ

Tactic:
fun hgf => hgm (hf.aestronglyMeasurable_map_iff.2 hgf)

Premises used: Iff.mpr, MeasurableEmbedding.aestronglyMeasurable_map_iff, Not
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 μ)
⊢ ¬AEStronglyMeasurable.{u_1, u_5} (β := G) (fun (x : α) ↦ g (f x)) μ

Tactic:
exact fun hgf => hgm (hf.aestronglyMeasurable_map_iff.2 hgf)

Premises used: Iff.mpr, MeasurableEmbedding.aestronglyMeasurable_map_iff
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst_2 : TopologicalSpace α
inst_3 : BorelSpace α
inst_4 : TopologicalSpace β
inst_5 : MeasurableSpace β
inst_6 : BorelSpace β
φ : α → β
hφ : IsClosedEmbedding φ
f : β → G
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ inst_5 (Measure.map φ μ) fun (y : β) ↦ f y) (∫ (x : α), f (φ x) ∂μ)

Tactic:
hφ.measurableEmbedding.integral_map _

Premises used: MeasurableEmbedding.integral_map, Topology.IsClosedEmbedding.measurableEmbedding
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst_2 : MeasurableSpace β
e : α ≃ᵐ β
f : β → G
⊢ Eq.{u_5 + 1} (α := G) (@integral _ _ _ _ inst_2 (Measure.map (⇑e : (a : α) → β) μ) fun (y : β) ↦ f y)
    (∫ (x : α), f ((e : (a : α) → β) x) ∂μ)

Tactic:
e.measurableEmbedding.integral_map f

Premises used: MeasurableEquiv.measurableEmbedding, MeasurableEmbedding.integral_map
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
G : Type u_6
A : Type u_7
inst_2 : Group G
inst_3 : AddCommGroup A
inst_4 : DistribMulAction G A
inst_5 : MeasurableSpace A
inst_6 : MeasurableConstSMul G A
μ : Measure A
g : Gᵈᵐᵃ
f : A → E
⊢ Eq.{u_2 + 1} (α := E) (∫ (x : A), f x ∂g • μ)
    (∫ (x : A), f (HSMul.hSMul (α := G) (((Equiv.symm DomMulAct.mk : (a : Gᵈᵐᵃ) → G) g)⁻¹ : G) x) ∂μ)

Tactic:
integral_map_equiv (MeasurableEquiv.smul ((DomMulAct.mk.symm g : G)⁻¹)) f

Premises used: MeasureTheory.integral_map_equiv, DomMulAct.mk, Inv.inv, MulOpposite.unop, Equiv.symm, DFunLike.coe, MeasurableEquiv.smul
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
x : MeasurableSpace β
f : α → β
ν : Measure β
h₁ : MeasurePreserving f μ ν
h₂ : MeasurableEmbedding f
g : β → G
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : α), g (f x) ∂μ) (∫ (y : β), g y ∂ν)

Tactic:
h₁.map_eq ▸ (h₂.integral_map g).symm

Premises used: MeasurableEmbedding.integral_map, Eq.rec, MeasureTheory.MeasurePreserving.map_eq, Eq.symm
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
Goal:
α : Type u_1
G : Type u_5
inst : NormedAddCommGroup G
inst_1 : NormedSpace ℝ G
m : MeasurableSpace α
μ : Measure α
β : Type u_6
inst_2 : MeasurableSpace β
ν : Measure β
f : α ≃ᵐ β
h : MeasurePreserving (⇑f : (a : α) → β) μ ν
g : β → G
⊢ Eq.{u_5 + 1} (α := G) (∫ (x : α), g ((f : (a : α) → β) x) ∂μ) (∫ (y : β), g y ∂ν)

Tactic:
MeasurePreserving.integral_comp h f.measurableEmbedding _

Premises used: MeasurableEquiv.measurableEmbedding, MeasureTheory.MeasurePreserving.integral_comp
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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
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)
⊢ 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 ∂μ)

Tactic:
rw [← map_comap_subtype_coe hs]

Premises used: map_comap_subtype_coe
-- Module: Mathlib.MeasureTheory.Integral.Bochner.Basic
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 : α))
    (@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:
((MeasurableEmbedding.subtype_coe hs).integral_map _).symm

Premises used: MeasurableEmbedding.integral_map, Eq.symm, MeasurableEmbedding.subtype_coe