-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem Kernel.continuous_integral_integral :
    -- Continuous fun f : α × β →₁[(κ ⊗ₖ η) a] E => ∫ 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 η
inst✝ : NormedSpace ℝ E
⊢ ∀ (x : ↥(Lp E 1 ((κ ⊗ₖ η) a))), ContinuousAt (fun f => ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂η (a, x) ∂κ a) x

Tactic:
intro g

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 η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ ContinuousAt (fun f => ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂η (a, x) ∂κ a) g

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 η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ ContinuousAt (fun f => ∫ (x : β), ∫ (y : γ), ↑↑f (x, y) ∂η (a, x) ∂κ a) g

Tactic:
refine
  tendsto_integral_of_L1 _ (L1.integrable_coeFn g).integral_compProd
    (Eventually.of_forall fun h => (L1.integrable_coeFn h).integral_compProd) ?_

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 η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ Tendsto (fun i => ∫⁻ (x : β), ‖∫ (y : γ), ↑↑i (x, y) ∂η (a, x) - ∫ (y : γ), ↑↑g (x, y) ∂η (a, x)‖ₑ ∂κ a) (𝓝 g) (𝓝 0)

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 η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ Tendsto (fun i => ∫⁻ (x : β), ∫⁻ (y : γ), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂η (a, x) ∂κ a) (𝓝 g) (𝓝 0)

α : 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 η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ (fun i => ∫⁻ (x : β), ‖∫ (y : γ), ↑↑i (x, y) - ↑↑g (x, y) ∂η (a, x)‖ₑ ∂κ a) ≤ fun i =>
    ∫⁻ (x : β), ∫⁻ (y : γ), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂η (a, x) ∂κ a

Tactic:
swap

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 η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ (fun i => ∫⁻ (x : β), ‖∫ (y : γ), ↑↑i (x, y) - ↑↑g (x, y) ∂η (a, x)‖ₑ ∂κ a) ≤ fun i =>
    ∫⁻ (x : β), ∫⁻ (y : γ), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂η (a, x) ∂κ a

α : 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 η
inst✝ : NormedSpace ℝ E
g : ↥(Lp E 1 ((κ ⊗ₖ η) a))
⊢ Tendsto (fun i => ∫⁻ (x : β), ∫⁻ (y : γ), ‖↑↑i (x, y) - ↑↑g (x, y)‖ₑ ∂η (a, x) ∂κ a) (𝓝 g) (𝓝 0)