awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
inst_4 : NormedSpace ℝ E
f : α × β → E
hf : AEStronglyMeasurable f (μ.prod ν)
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α | (fun (x : α) ↦ ∀ᵐ (y : β) ∂ν, f (x, y) = AEStronglyMeasurable.mk f hf (x, y)) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  Eq.{u_3 + 1} (α := E) ((fun (x : α) ↦ (∫ (y : β), f (x, y) ∂ν : E)) x)
                    ((fun (x : α) ↦ (∫ (y : β), AEStronglyMeasurable.mk f hf (x, y) ∂ν : E)) x))
                x}
            x}
      a
h₁ h₂ :
  ∀ (a : α) (hx : ∀ᵐ (y : β) ∂ν, f (a, y) = AEStronglyMeasurable.mk f hf (a, y)),
    Eq.{u_3 + 1} (α := E) (∫ (y : β), f (a, y) ∂ν) (∫ (y : β), AEStronglyMeasurable.mk f hf (a, y) ∂ν)
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) (fun (x : α) ↦ ∫ (y : β), f (x, y) ∂ν) fun (x : α) ↦
    ∫ (y : β), AEStronglyMeasurable.mk f hf (x, y) ∂ν

Tactic:
filter_upwards [ae_ae_of_ae_prod hf.ae_eq_mk] with _ hx using integral_congr_ae hx

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.Measure.ae_ae_of_ae_prod
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : SFinite ν
f : α × β → X
hf : AEStronglyMeasurable f (μ.prod ν)
h :
  ∀ (x : α) (hx : ∀ᵐ (y : β) ∂ν, f (x, y) = AEStronglyMeasurable.mk f hf (x, y)),
    AEStronglyMeasurable.{u_2, u_4} (β := X) (fun (y : β) ↦ f (x, y)) ν
⊢ ∀ᵐ (x : α) ∂μ, AEStronglyMeasurable.{u_2, u_4} (β := X) (fun (y : β) ↦ f (x, y)) ν

Tactic:
filter_upwards [ae_ae_of_ae_prod hf.ae_eq_mk] with x hx

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.Measure.ae_ae_of_ae_prod
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : SFinite ν
f : α × β → X
hf : AEStronglyMeasurable f (μ.prod ν)
x : α
hx : ∀ᵐ (y : β) ∂ν, f (x, y) = AEStronglyMeasurable.mk f hf (x, y)
⊢ AEStronglyMeasurable.{u_2, u_4} (β := X) (fun (y : β) ↦ f (x, y)) ν

Tactic:
⟨fun y ↦ hf.mk f (x, y),
    hf.stronglyMeasurable_mk.comp_measurable measurable_prodMk_left, hx⟩

Premises used: Prod.mk, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.StronglyMeasurable.comp_measurable, MeasureTheory.AEStronglyMeasurable.mk, And.intro, Exists.intro, MeasureTheory.AEStronglyMeasurable, measurable_prodMk_left
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : SFinite ν
f : α × β → X
hf : AEStronglyMeasurable f (μ.prod ν)
x : α
hx : ∀ᵐ (y : β) ∂ν, f (x, y) = AEStronglyMeasurable.mk f hf (x, y)
⊢ AEStronglyMeasurable.{u_2, u_4} (β := X) (fun (y : β) ↦ f (x, y)) ν

Tactic:
exact ⟨fun y ↦ hf.mk f (x, y),
    hf.stronglyMeasurable_mk.comp_measurable measurable_prodMk_left, hx⟩
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : SFinite μ
inst_4 : SFinite ν
f : α × β → X
hf : AEStronglyMeasurable f (μ.prod ν)
⊢ ∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.{u_1, u_4} (β := X) (fun (x : α) ↦ f (x, y)) μ

Tactic:
hf.prod_swap.prodMk_left

Premises used: MeasureTheory.AEStronglyMeasurable.prod_swap, Prod.swap, MeasureTheory.AEStronglyMeasurable.prodMk_left
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst_2 : TopologicalSpace X
f : β → X
inst_3 : SFinite ν
hf : AEStronglyMeasurable (β := X) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
hμ : μ ≠ 0
⊢ NeZero μ

Tactic:
have := NeZero.mk hμ
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst_2 : TopologicalSpace X
f : β → X
inst_3 : SFinite ν
hf : AEStronglyMeasurable (β := X) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
hμ : μ ≠ 0
this : NeZero μ
obtain :
  ∀ (y : α) (hy : AEStronglyMeasurable.{u_2, u_4} (β := X) (fun (y_1 : β) ↦ f (y, y_1).2) ν), AEStronglyMeasurable f ν
⊢ AEStronglyMeasurable f ν

Tactic:
obtain ⟨y, hy⟩ := hf.prodMk_left.exists

Premises used: Filter.Eventually.exists, MeasureTheory.AEStronglyMeasurable.prodMk_left
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst_2 : TopologicalSpace X
f : β → X
inst_3 : SFinite ν
hf : AEStronglyMeasurable (β := X) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
hμ : μ ≠ 0
this : NeZero μ
y : α
hy : AEStronglyMeasurable.{u_2, u_4} (β := X) (fun (y_1 : β) ↦ f (y, y_1).2) ν
⊢ AEStronglyMeasurable f ν

Tactic:
hy
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst_2 : TopologicalSpace X
f : β → X
inst_3 : SFinite ν
hf : AEStronglyMeasurable (β := X) (fun (x : α × β) ↦ f x.2) (μ.prod ν)
hμ : μ ≠ 0
this : NeZero μ
y : α
hy : AEStronglyMeasurable.{u_2, u_4} (β := X) (fun (y_1 : β) ↦ f (y, y_1).2) ν
⊢ AEStronglyMeasurable f ν

Tactic:
exact hy
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst_2 : TopologicalSpace X
f : α → X
inst_3 : SFinite μ
inst_4 : SFinite ν
hf : AEStronglyMeasurable (β := X) (fun (x : α × β) ↦ f x.1) (μ.prod ν)
hν : ν ≠ 0
⊢ AEStronglyMeasurable f μ

Tactic:
hf.prod_swap.of_comp_snd hν

Premises used: MeasureTheory.AEStronglyMeasurable.prod_swap, MeasureTheory.AEStronglyMeasurable.of_comp_snd
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : SFinite μ
inst_4 : SFinite ν
f : α → X
hν : ν ≠ 0
⊢ AEStronglyMeasurable (β := X) (fun (x : α × β) ↦ f x.1) (μ.prod ν) ↔ AEStronglyMeasurable f μ

Tactic:
⟨(.of_comp_fst · hν), .comp_fst⟩

Premises used: MeasureTheory.AEStronglyMeasurable.of_comp_fst, Iff.intro, MeasureTheory.AEStronglyMeasurable.comp_fst
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
X : Type u_4
inst_2 : TopologicalSpace X
inst_3 : SFinite ν
f : β → X
hμ : μ ≠ 0
⊢ AEStronglyMeasurable (β := X) (fun (x : α × β) ↦ f x.2) (μ.prod ν) ↔ AEStronglyMeasurable f ν

Tactic:
⟨(.of_comp_snd · hμ), .comp_snd⟩

Premises used: Iff.intro, MeasureTheory.AEStronglyMeasurable.comp_snd, MeasureTheory.AEStronglyMeasurable.of_comp_snd
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
inst_4 : SFinite μ
f : α × β → E
⊢ Integrable (f ∘ Prod.swap) (ν.prod μ) ↔ Integrable f (μ.prod ν)

Tactic:
measurePreserving_swap.integrable_comp_emb MeasurableEquiv.prodComm.measurableEmbedding

Premises used: MeasurableEquiv.measurableEmbedding, MeasureTheory.MeasurePreserving.integrable_comp_emb, MeasurableEquiv.prodComm, MeasureTheory.Measure.measurePreserving_swap
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
inst_4 : SFinite μ
f : α × β → E
hf : Integrable f (μ.prod ν)
⊢ Integrable (f ∘ Prod.swap) (ν.prod μ)

Tactic:
integrable_swap_iff.2 hf

Premises used: Iff.mpr, MeasureTheory.integrable_swap_iff
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
simp :
  ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) ∧ ∫⁻ (a : α), enorm (E := ℝ) (∫ (y : β), ‖f (a, y)‖ ∂ν) ∂μ < ∞
⊢ HasFiniteIntegral f (μ.prod ν) ↔
    (∀ᵐ (x : α) ∂μ, HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ f (x, y)) ν) ∧
      HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν) μ

Tactic:
simp only [hasFiniteIntegral_iff_enorm, lintegral_prod _ h1f.enorm.aemeasurable]

Premises used: Measurable.aemeasurable, MeasureTheory.StronglyMeasurable.enorm, MeasureTheory.lintegral_prod, MeasureTheory.hasFiniteIntegral_iff_enorm
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
x : α
y : β
⊢ 0 ≤ ‖f (x, y)‖

Tactic:
norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
x : α
h : ∀ (a : β), Membership.mem (γ := Set β) {x_1 : β | (fun (y : β) ↦ 0 ≤ ‖f (x, y)‖) x_1} a
h₁ h₂ : ∀ (y : β), 0 ≤ ‖f (x, y)‖
⊢ ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖

Tactic:
filter_upwards with y using norm_nonneg _

Premises used: norm_nonneg
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
⊢ ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖

Tactic:
have (x : _) : ∀ᵐ y ∂ν, 0 ≤ ‖f (x, y)‖ := by filter_upwards with y using norm_nonneg _
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
simp_rw :
  ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) ∧
      ∫⁻ (a : α), ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal ∂μ < ∞
⊢ ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) ∧ ∫⁻ (a : α), enorm (E := ℝ) (∫ (y : β), ‖f (a, y)‖ ∂ν) ∂μ < ∞

Tactic:
simp_rw [integral_eq_lintegral_of_nonneg_ae (this _)
      (h1f.norm.comp_measurable measurable_prodMk_left).aestronglyMeasurable,
    enorm_eq_ofReal toReal_nonneg, ofReal_norm]

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, ENNReal.toReal_nonneg, MeasureTheory.StronglyMeasurable.comp_measurable, MeasureTheory.integral_eq_lintegral_of_nonneg_ae, MeasureTheory.StronglyMeasurable.norm, ofReal_norm, Real.enorm_eq_ofReal, measurable_prodMk_left
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
p q r : Prop
h1 : r → p
rw : (r ↔ p ∧ q) ↔ (p ∧ r ↔ p ∧ q)
rw₁ rw₂ : (r ↔ p ∧ q) ↔ (r ↔ p ∧ q)
⊢ (r ↔ p ∧ q) ↔ p → (r ↔ q)

Tactic:
rw [← and_congr_right_iff, and_iff_right_of_imp h1]

Premises used: and_congr_right_iff, and_iff_right_of_imp
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
⊢ ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))

Tactic:
have : ∀ {p q r : Prop} (_ : r → p), (r ↔ p ∧ q) ↔ p → (r ↔ q) := fun {p q r} h1 => by
    rw [← and_congr_right_iff, and_iff_right_of_imp h1]
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this_1 : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
rw :
  (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) →
    (∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
      ∫⁻ (a : α), ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal ∂μ < ∞)
rw₁ : ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ → ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
⊢ ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) ∧
      ∫⁻ (a : α), ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal ∂μ < ∞

Tactic:
rw [this]
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this_1 : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
rw :
  (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν) fun (a : α) ↦
    ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal
⊢ ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    ∫⁻ (a : α), ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal ∂μ < ∞

Tactic:
rw [lintegral_congr_ae]

Premises used: MeasureTheory.lintegral_congr_ae
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this_1 : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
h :
  ∀ (x : α) (hx : ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞),
    ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν = ENNReal.ofReal (∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν).toReal
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν) fun (a : α) ↦
    ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal

Tactic:
filter_upwards [h2f] with x hx
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this_1 : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
x : α
hx : ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
h : ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν ≠ ∞
⊢ ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν = ENNReal.ofReal (∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν).toReal

Tactic:
rw [ofReal_toReal]

Premises used: ENNReal.ofReal_toReal
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this_1 : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
x : α
hx : ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
h : ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
⊢ ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν ≠ ∞

Tactic:
rw [← lt_top_iff_ne_top]

Premises used: lt_top_iff_ne_top
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this_1 : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
x : α
hx : ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
⊢ ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞

Tactic:
hx
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this_1 : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
x : α
hx : ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
⊢ ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞

Tactic:
exact hx
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this_1 : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞
⊢ ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞

Tactic:
ae_lt_top ?_ h2f.ne

Premises used: LT.lt.ne, MeasureTheory.ae_lt_top
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this_1 : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞
refine : Measurable (β := ℝ≥0∞) fun (x : α) ↦ ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν
⊢ ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞

Tactic:
refine ae_lt_top ?_ h2f.ne

Premises used: LT.lt.ne, MeasureTheory.ae_lt_top
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this_1 : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν

Tactic:
h1f.enorm.lintegral_prod_right'

Premises used: Measurable.lintegral_prod_right', MeasureTheory.StronglyMeasurable.enorm
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : StronglyMeasurable f
this_1 : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
this : ∀ {p q r : Prop}, (r → p) → ((r ↔ p ∧ q) ↔ p → (r ↔ q))
h2f : ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν

Tactic:
exact h1f.enorm.lintegral_prod_right'

Premises used: Measurable.lintegral_prod_right', MeasureTheory.StronglyMeasurable.enorm
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
rw :
  (∀ᵐ (x : α) ∂μ, HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ AEStronglyMeasurable.mk f h1f (x, y)) ν) ∧
      HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) μ ↔
    (∀ᵐ (x : α) ∂μ, HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ f (x, y)) ν) ∧
      HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
⊢ HasFiniteIntegral f (μ.prod ν) ↔
    (∀ᵐ (x : α) ∂μ, HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ f (x, y)) ν) ∧
      HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν) μ

Tactic:
rw [hasFiniteIntegral_congr h1f.ae_eq_mk,
    hasFiniteIntegral_prod_iff h1f.stronglyMeasurable_mk]

Premises used: MeasureTheory.hasFiniteIntegral_congr, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk, MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.hasFiniteIntegral_prod_iff
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
h₁ :
  (∀ᵐ (x : α) ∂μ, HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ AEStronglyMeasurable.mk f h1f (x, y)) ν) ↔
    ∀ᵐ (x : α) ∂μ, HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ f (x, y)) ν
h₂ :
  HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) μ ↔
    HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
⊢ (∀ᵐ (x : α) ∂μ, HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ AEStronglyMeasurable.mk f h1f (x, y)) ν) ∧
      HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) μ ↔
    (∀ᵐ (x : α) ∂μ, HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ f (x, y)) ν) ∧
      HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν) μ

Tactic:
apply and_congr

Premises used: and_congr
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
h₁ :
  ∀ᵐ (x : α) ∂μ,
    HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ AEStronglyMeasurable.mk f h1f (x, y)) ν ↔
      HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ f (x, y)) ν
⊢ (∀ᵐ (x : α) ∂μ, HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ AEStronglyMeasurable.mk f h1f (x, y)) ν) ↔
    ∀ᵐ (x : α) ∂μ, HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ f (x, y)) ν

Tactic:
apply eventually_congr

Premises used: Filter.eventually_congr
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
h :
  ∀ (a : α),
    (∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.mk f h1f (a, y) = f (a, y)) →
      (HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ AEStronglyMeasurable.mk f h1f (a, y)) ν ↔
        HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ f (a, y)) ν)
⊢ ∀ᵐ (x : α) ∂μ,
    HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ AEStronglyMeasurable.mk f h1f (x, y)) ν ↔
      HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ f (x, y)) ν

Tactic:
filter_upwards [ae_ae_of_ae_prod h1f.ae_eq_mk.symm]

Premises used: MeasureTheory.AEStronglyMeasurable.ae_eq_mk, MeasureTheory.Measure.ae_ae_of_ae_prod, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Integral.Prod
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
inst_3 : SFinite ν
f : α × β → E
h1f : AEStronglyMeasurable f (μ.prod ν)
x : α
hx : ∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.mk f h1f (x, y) = f (x, y)
⊢ HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ AEStronglyMeasurable.mk f h1f (x, y)) ν ↔
    HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ f (x, y)) ν

Tactic:
hasFiniteIntegral_congr hx

Premises used: MeasureTheory.hasFiniteIntegral_congr