-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem hasFiniteIntegral_comp_iff' ⦃f : γ → E⦄ (hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)) :
    HasFiniteIntegral f ((η ∘ₖ κ) a) ↔
    (∀ᵐ x ∂κ a, HasFiniteIntegral f (η x)) ∧ HasFiniteIntegral (fun x ↦ ∫ y, ‖f y‖ ∂η 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 α β
η : Kernel β γ
f : γ → E
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ HasFiniteIntegral f ((η ∘ₖ κ) a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral f (η x)) ∧ HasFiniteIntegral (fun x => ∫ (y : γ), ‖f y‖ ∂η x) (κ a)

Tactic:
rw [hasFiniteIntegral_congr hf.ae_eq_mk, hasFiniteIntegral_comp_iff hf.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 α β
η : Kernel β γ
f : γ → E
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (AEStronglyMeasurable.mk f hf) (η x)) ∧
      HasFiniteIntegral (fun x => ∫ (y : γ), ‖AEStronglyMeasurable.mk f hf y‖ ∂η x) (κ a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral f (η x)) ∧ HasFiniteIntegral (fun x => ∫ (y : γ), ‖f y‖ ∂η x) (κ a)

Proof state:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
f : γ → E
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ ∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (AEStronglyMeasurable.mk f hf) (η x) ↔ HasFiniteIntegral f (η x)

Tactic:
filter_upwards [ae_ae_of_ae_comp hf.ae_eq_mk.symm] with _ hx using
  hasFiniteIntegral_congr hx

Result:
no goals

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

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

Result:
no goals

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 α β
η : Kernel β γ
f : γ → E
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (AEStronglyMeasurable.mk f hf) (η x)) ∧
      HasFiniteIntegral (fun x => ∫ (y : γ), ‖AEStronglyMeasurable.mk f hf y‖ ∂η x) (κ a) ↔
    (∀ᵐ (x : β) ∂κ a, HasFiniteIntegral f (η x)) ∧ HasFiniteIntegral (fun x => ∫ (y : γ), ‖f y‖ ∂η x) (κ a)

Tactic:
refine and_congr (eventually_congr ?_) (hasFiniteIntegral_congr ?_)

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
f : γ → E
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ ∀ᵐ (x : β) ∂κ a, HasFiniteIntegral (AEStronglyMeasurable.mk f hf) (η x) ↔ HasFiniteIntegral f (η x)

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : NormedAddCommGroup E
a : α
κ : Kernel α β
η : Kernel β γ
f : γ → E
hf : AEStronglyMeasurable f ((η ∘ₖ κ) a)
⊢ (fun x => ∫ (y : γ), ‖AEStronglyMeasurable.mk f hf y‖ ∂η x) =ᶠ[ae (κ a)] fun x => ∫ (y : γ), ‖f y‖ ∂η x