-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem hasFiniteIntegral_compProd_iff' ⦃f : β × γ → E⦄
    (h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)) :
    HasFiniteIntegral f ((κ ⊗ₖ η) a) ↔
      (∀ᵐ x ∂κ a, HasFiniteIntegral (fun y => f (x, y)) (η (a, x))) ∧
        HasFiniteIntegral (fun x => ∫ y, ‖f (x, y)‖ ∂η (a, x)) (κ a)

Proof state:
case h₁.h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ ∀ᵐ (x : β) ∂κ a,
    HasFiniteIntegral (fun y => AEStronglyMeasurable.mk f h1f (x, y)) (η (a, x)) ↔
      HasFiniteIntegral (fun y => f (x, y)) (η (a, x))

Tactic:
filter_upwards [ae_ae_of_ae_compProd h1f.ae_eq_mk.symm] with x hx using
  hasFiniteIntegral_congr hx

Result:
no goals

Proof state:
case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ HasFiniteIntegral (fun x => ∫ (y : γ), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂η (a, x)) (κ a) ↔
    HasFiniteIntegral (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)

Tactic:
apply hasFiniteIntegral_congr

Result:
case h₂.h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ (fun x => ∫ (y : γ), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂η (a, x)) =ᶠ[ae (κ a)] fun x =>
    ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y => AEStronglyMeasurable.mk f h1f (x, y)) (η (a, x))) ∧
      HasFiniteIntegral (fun x => ∫ (y : γ), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂η (a, x)) (κ a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y => f (x, y)) (η (a, x))) ∧
      HasFiniteIntegral (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)

Tactic:
apply and_congr

Result:
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y => AEStronglyMeasurable.mk f h1f (x, y)) (η (a, x))) ↔
    ∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y => f (x, y)) (η (a, x))

case h₂
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ HasFiniteIntegral (fun x => ∫ (y : γ), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂η (a, x)) (κ a) ↔
    HasFiniteIntegral (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ HasFiniteIntegral f ((κ ⊗ₖ η) a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y => f (x, y)) (η (a, x))) ∧
      HasFiniteIntegral (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)

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

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y => AEStronglyMeasurable.mk f h1f (x, y)) (η (a, x))) ∧
      HasFiniteIntegral (fun x => ∫ (y : γ), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂η (a, x)) (κ a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y => f (x, y)) (η (a, x))) ∧
      HasFiniteIntegral (fun x => ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)) (κ a)

Proof state:
case h₂.h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ (fun x => ∫ (y : γ), ‖AEStronglyMeasurable.mk f h1f (x, y)‖ ∂η (a, x)) =ᶠ[ae (κ a)] fun x =>
    ∫ (y : γ), ‖f (x, y)‖ ∂η (a, x)

Tactic:
filter_upwards [ae_ae_of_ae_compProd h1f.ae_eq_mk.symm] with _ hx using
  integral_congr_ae (EventuallyEq.fun_comp hx _)

Result:
no goals

Proof state:
case h₁
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y => AEStronglyMeasurable.mk f h1f (x, y)) (η (a, x))) ↔
    ∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (fun y => f (x, y)) (η (a, x))

Tactic:
apply eventually_congr

Result:
case h₁.h
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝² : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
f : β × γ → E
h1f : AEStronglyMeasurable f ((κ ⊗ₖ η) a)
⊢ ∀ᵐ (x : β) ∂κ a,
    HasFiniteIntegral (fun y => AEStronglyMeasurable.mk f h1f (x, y)) (η (a, x)) ↔
      HasFiniteIntegral (fun y => f (x, y)) (η (a, x))