awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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
⊢ EventuallyEq.{u_1, u_3} (β := E) (ae μ) (fun (x : α) ↦ ∫ (y : β), f (x, y) ∂ν) fun (x : α) ↦
    ∫ (y : β), AEStronglyMeasurable.mk f hf (x, y) ∂ν
have h₁ : ∀ (a : α),
  (∀ᵐ (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) ∂ν)
Tactic: filter_upwards [ae_ae_of_ae_prod hf.ae_eq_mk] with _ hx using integral_congr_ae hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 : α) ∂μ, AEStronglyMeasurable.{u_2, u_4} (β := X) (fun (y : β) ↦ f (x, y)) ν
have h : ∀ (x : α) (hx : ∀ᵐ (y : β) ∂ν, f (x, y) = AEStronglyMeasurable.mk f hf (x, y)),
  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
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
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
⊢ AEStronglyMeasurable f ν
have this : NeZero μ
Tactic: have := NeZero.mk hμ
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 μ
⊢ AEStronglyMeasurable f ν
have obtain : ∀ (y : α) (hy : AEStronglyMeasurable.{u_2, u_4} (β := X) (fun (y_1 : β) ↦ f (y, y_1).2) ν), AEStronglyMeasurable f ν
Tactic: obtain ⟨y, hy⟩ := hf.prodMk_left.exists
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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
⊢ HasFiniteIntegral f (μ.prod ν) ↔
    (∀ᵐ (x : α) ∂μ, HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ f (x, y)) ν) ∧
      HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
have simp : ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
  (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) ∧ ∫⁻ (a : α), enorm (E := ℝ) (∫ (y : β), ‖f (a, y)‖ ∂ν) ∂μ < ∞
Tactic: simp only [hasFiniteIntegral_iff_enorm, lintegral_prod _ h1f.enorm.aemeasurable]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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)‖
have h : ∀ (a : β), Membership.mem (γ := Set β) {x_1 : β | (fun (y : β) ↦ 0 ≤ ‖f (x, y)‖) x_1} a
Tactic: filter_upwards with y using norm_nonneg _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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
⊢ ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
have h₁ : ∀ (a : β), 0 ≤ ‖f (x, a)‖
Tactic: filter_upwards with y using norm_nonneg _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
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 : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) ∧ ∫⁻ (a : α), enorm (E := ℝ) (∫ (y : β), ‖f (a, y)‖ ∂ν) ∂μ < ∞
have this : ∀ (x : α), ∀ᵐ (y : β) ∂ν, 0 ≤ ‖f (x, y)‖
Tactic: have (x : _) : ∀ᵐ y ∂ν, 0 ≤ ‖f (x, y)‖ := by filter_upwards with y using norm_nonneg _
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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)‖
⊢ ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) ∧ ∫⁻ (a : α), enorm (E := ℝ) (∫ (y : β), ‖f (a, y)‖ ∂ν) ∂μ < ∞
have simp_rw : ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
  (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) ∧
    ∫⁻ (a : α), ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal ∂μ < ∞
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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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
⊢ (r ↔ p ∧ q) ↔ p → (r ↔ q)
have rw : (r ↔ p ∧ q) ↔ (p ∧ r ↔ p ∧ q)
Tactic: rw [← and_congr_right_iff, and_iff_right_of_imp h1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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)
⊢ (r ↔ p ∧ q) ↔ p → (r ↔ q)
have rw₁ : (r ↔ p ∧ q) ↔ (r ↔ p ∧ q)
Tactic: rw [← and_congr_right_iff, and_iff_right_of_imp h1]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (hypothesis)
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)‖
⊢ ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) ∧
      ∫⁻ (a : α), ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal ∂μ < ∞
have this₁ : ∀ {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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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))
⊢ ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) ∧
      ∫⁻ (a : α), ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal ∂μ < ∞
have rw : (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) →
  (∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    ∫⁻ (a : α), ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal ∂μ < ∞)
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 ∂μ < ∞)
⊢ ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    (∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞) ∧
      ∫⁻ (a : α), ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal ∂μ < ∞
have rw₁ : ∫⁻ (x : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ → ∀ᵐ (x : α) ∂μ, ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 : α), ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν ∂μ < ∞ ↔
    ∫⁻ (a : α), ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal ∂μ < ∞
have rw : (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν) fun (a : α) ↦
  ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal
Tactic: rw [lintegral_congr_ae]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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)‖ₑ ∂ν < ∞
⊢ (ae μ).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν) fun (a : α) ↦
    ENNReal.ofReal (∫⁻ (a_1 : β), ‖f (a, a_1)‖ₑ ∂ν).toReal
have h : ∀ (x : α) (hx : ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν < ∞),
  ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν = ENNReal.ofReal (∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν).toReal
Tactic: filter_upwards [h2f] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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)‖ₑ ∂ν < ∞
⊢ ∫⁻ (y : β), ‖f (x, y)‖ₑ ∂ν = ENNReal.ofReal (∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν).toReal
have h : ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν ≠ ∞
Tactic: rw [ofReal_toReal]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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)‖ₑ ∂ν < ∞
have refine : Measurable (β := ℝ≥0∞) fun (x : α) ↦ ∫⁻ (a : β), ‖f (x, a)‖ₑ ∂ν
Tactic: refine ae_lt_top ?_ h2f.ne
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 ν)
⊢ HasFiniteIntegral f (μ.prod ν) ↔
    (∀ᵐ (x : α) ∂μ, HasFiniteIntegral.{u_2, u_3} (ε := E) (fun (y : β) ↦ f (x, y)) ν) ∧
      HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
have 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)‖ ∂ν) μ
Tactic: rw [hasFiniteIntegral_congr h1f.ae_eq_mk,
    hasFiniteIntegral_prod_iff h1f.stronglyMeasurable_mk]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 : α) ∂μ, 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)‖ ∂ν) μ
have 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)) ν
Tactic: apply and_congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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)) ν
⊢ (∀ᵐ (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)‖ ∂ν) μ
have h₂ : HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) μ ↔
  HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
Tactic: apply and_congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 : α) ∂μ, 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)) ν
have 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)) ν
Tactic: apply eventually_congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 : α) ∂μ,
    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)) ν
have 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)) ν)
Tactic: filter_upwards [ae_ae_of_ae_prod h1f.ae_eq_mk.symm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 ν)
⊢ HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) μ ↔
    HasFiniteIntegral (ε := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
have h₂ : (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) fun (x : α) ↦
  ∫ (y : β), ‖f (x, y)‖ ∂ν
Tactic: apply hasFiniteIntegral_congr
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 ν)
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) fun (x : α) ↦
    ∫ (y : β), ‖f (x, y)‖ ∂ν
have h : ∀ (a : α),
  Membership.mem (γ := Set α)
    {x : α |
      Membership.mem (γ := Set α)
          {x : α | (fun (x : α) ↦ ∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.mk f h1f (x, y) = f (x, y)) x} x →
        Membership.mem (γ := Set α)
          {x : α |
            (fun (x : α) ↦
                Eq (α := ℝ) ((fun (x : α) ↦ (∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν : ℝ)) x)
                  ((fun (x : α) ↦ (∫ (y : β), ‖f (x, y)‖ ∂ν : ℝ)) x))
              x}
          x}
    a
Tactic: filter_upwards [ae_ae_of_ae_prod h1f.ae_eq_mk.symm] with _ hx using
      integral_congr_ae (EventuallyEq.fun_comp hx _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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 : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α)
            {x : α | (fun (x : α) ↦ ∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.mk f h1f (x, y) = f (x, y)) x} x →
          Membership.mem (γ := Set α)
            {x : α |
              (fun (x : α) ↦
                  Eq (α := ℝ) ((fun (x : α) ↦ (∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν : ℝ)) x)
                    ((fun (x : α) ↦ (∫ (y : β), ‖f (x, y)‖ ∂ν : ℝ)) x))
                x}
            x}
      a
⊢ (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ ∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂ν) fun (x : α) ↦
    ∫ (y : β), ‖f (x, y)‖ ∂ν
have h₁ : ∀ (a : α),
  (∀ᵐ (y : β) ∂ν, AEStronglyMeasurable.mk f h1f (a, y) = f (a, y)) →
    Eq (α := ℝ) (∫ (y : β), ‖AEStronglyMeasurable.mk f h1f (a, y)‖ ∂ν) (∫ (y : β), ‖f (a, y)‖ ∂ν)
Tactic: filter_upwards [ae_ae_of_ae_prod h1f.ae_eq_mk.symm] with _ hx using
      integral_congr_ae (EventuallyEq.fun_comp hx _)
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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
h1f : AEStronglyMeasurable f (μ.prod ν)
⊢ Integrable f (μ.prod ν) ↔
    (∀ᵐ (y : β) ∂ν, Integrable.{u_3, u_1} (ε := E) (fun (x : α) ↦ f (x, y)) μ) ∧
      Integrable (ε := ℝ) (fun (y : β) ↦ ∫ (x : α), ‖f (x, y)‖ ∂μ) ν
have h : Integrable f (μ.prod ν) ↔ Integrable (ε := E) (fun (z : β × α) ↦ f z.swap) (ν.prod μ)
Tactic: convert! integrable_prod_iff h1f.prod_swap using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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
h1f : AEStronglyMeasurable f (μ.prod ν)
⊢ Integrable f (μ.prod ν) ↔ Integrable (ε := E) (fun (z : β × α) ↦ f z.swap) (ν.prod μ)
have h : Integrable f (μ.prod ν) ↔ Integrable (ε := E) (fun (x : β × α) ↦ (f ∘ Prod.swap) x) (ν.prod μ)
Tactic: rw [funext fun _ => Function.comp_apply.symm, integrable_swap_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
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
h1f : AEStronglyMeasurable f (μ.prod ν)
h : Integrable f (μ.prod ν) ↔ Integrable (ε := E) (fun (x : β × α) ↦ (f ∘ Prod.swap) x) (ν.prod μ)
⊢ Integrable f (μ.prod ν) ↔ Integrable (ε := E) (fun (z : β × α) ↦ f z.swap) (ν.prod μ)
have h₁ : Integrable f (μ.prod ν) ↔ Integrable f (μ.prod ν)
Tactic: rw [funext fun _ => Function.comp_apply.symm, integrable_swap_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
F : Type u_4
G : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
hop_norm : ∃ (C : ℝ), ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
⊢ Integrable (ε := G) (fun (z : α × β) ↦ op (f z.1) (g z.2)) (μ.prod ν)
have right : HasFiniteIntegral (ε := G) (fun (z : α × β) ↦ op (f z.1) (g z.2)) (μ.prod ν)
Tactic: use hop.comp_aestronglyMeasurable₂ hf.1.comp_fst hg.1.comp_snd
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
F : Type u_4
G : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
hop_norm : ∃ (C : ℝ), ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
⊢ HasFiniteIntegral (ε := G) (fun (z : α × β) ↦ op (f z.1) (g z.2)) (μ.prod ν)
have right : ∀ (C : ℝ) (hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖),
  HasFiniteIntegral (ε := G) (fun (z : α × β) ↦ op (f z.1) (g z.2)) (μ.prod ν)
Tactic: rcases hop_norm with ⟨C, hC⟩
Cleared hypotheses: hop_norm
-- Lean 4 proof step from Mathlib.MeasureTheory.Integral.Prod (goal)
Goal:
α : Type u_1
β : Type u_2
E : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
μ : Measure α
ν : Measure β
inst_2 : NormedAddCommGroup E
F : Type u_4
G : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : NormedAddCommGroup G
op : E → F → G
hop : Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (uncurry op)
f : α → E
g : β → F
hf : Integrable f μ
hg : Integrable g ν
C : ℝ
hC : ∀ (x : E) (y : F), ‖op x y‖ ≤ C * ‖x‖ * ‖y‖
⊢ ∫⁻ (z : α × β), ‖op (f z.1) (g z.2)‖ₑ ∂μ.prod ν ≤ ∫⁻ (z : α × β), ENNReal.ofReal C * ‖f z.1‖ₑ * ‖g z.2‖ₑ ∂μ.prod ν
have hfg : ∀ (z : α × β), ‖op (f z.1) (g z.2)‖ₑ ≤ ENNReal.ofReal C * ‖f z.1‖ₑ * ‖g z.2‖ₑ
Tactic: gcongr with z