-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem integral_comp : ∀ {f : γ → E} (_ : Integrable f ((η ∘ₖ κ) a)),
    ∫ z, f z ∂(η ∘ₖ κ) a = ∫ x, ∫ y, f y ∂η x ∂κ a

Proof state:
case pos.h_ind.e_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 α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : ((η ∘ₖ κ) a) s < ⊤
⊢ (((η ∘ₖ κ) a) s).toReal = ∫ (x : β), ((η x) s).toReal ∂κ a

Tactic:
rw [integral_toReal, Kernel.comp_apply' _ _ _ hs]

Result:
case pos.h_ind.e_a.hfm
α : 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 β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : ((η ∘ₖ κ) a) s < ⊤
⊢ AEMeasurable (fun x => (η x) s) (κ a)

case pos.h_ind.e_a.hf
α : 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 β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : ((η ∘ₖ κ) a) s < ⊤
⊢ ∀ᵐ (x : β) ∂κ a, (η x) s < ⊤

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 β γ
inst✝ : NormedSpace ℝ E
⊢ ∀ {f : γ → E}, Integrable f ((η ∘ₖ κ) a) → ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a

Tactic:
by_cases hE : CompleteSpace E

Result:
case pos
α : 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 β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
⊢ Integrable f✝ ((η ∘ₖ κ) a) → ∫ (z : γ), f✝ z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f✝ y ∂η x ∂κ a

case neg
α : 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 β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : ¬CompleteSpace E
⊢ Integrable f✝ ((η ∘ₖ κ) a) → ∫ (z : γ), f✝ z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f✝ y ∂η x ∂κ a

Proof state:
case pos.h_ae
α : 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 β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᶠ[ae ((η ∘ₖ κ) a)] g
hf : ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
⊢ ∫ (z : γ), g z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a

Tactic:
convert hf using 1

Result:
case h.e'_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 β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᶠ[ae ((η ∘ₖ κ) a)] g
hf : ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
⊢ ∫ (z : γ), g z ∂(η ∘ₖ κ) a = ∫ (z : γ), f z ∂(η ∘ₖ κ) a

case h.e'_3
α : 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 β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᶠ[ae ((η ∘ₖ κ) a)] g
hf : ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
⊢ ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a

Proof state:
case h.e'_3
α : 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 β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᶠ[ae ((η ∘ₖ κ) a)] g
hf : ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
⊢ ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a

Tactic:
apply integral_congr_ae

Result:
case h.e'_3.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 α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
f g : γ → E
hfg : f =ᶠ[ae ((η ∘ₖ κ) a)] g
hf : ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
⊢ (fun a => ∫ (y : γ), g y ∂η a) =ᶠ[ae (κ a)] fun a => ∫ (y : γ), f y ∂η a

Proof state:
case pos.h_ind
α : 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 β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : ((η ∘ₖ κ) a) s < ⊤
⊢ (((η ∘ₖ κ) a) s).toReal • c = (∫ (x : β), ((η x) s).toReal ∂κ a) • c

Tactic:
congr

Result:
case pos.h_ind.e_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 α β
η : Kernel β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : ((η ∘ₖ κ) a) s < ⊤
⊢ (((η ∘ₖ κ) a) s).toReal = ∫ (x : β), ((η x) s).toReal ∂κ a

Proof state:
case pos.h_ind
α : 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 β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : ((η ∘ₖ κ) a) s < ⊤
⊢ ∫ (z : γ), s.indicator (fun x => c) z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), s.indicator (fun x => c) y ∂η x ∂κ a

Tactic:
simp_rw [integral_indicator hs, MeasureTheory.setIntegral_const, integral_smul_const]

Result:
case pos.h_ind
α : 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 β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
c : E
s : Set γ
hs : MeasurableSet s
ms : ((η ∘ₖ κ) a) s < ⊤
⊢ (((η ∘ₖ κ) a) s).toReal • c = (∫ (x : β), ((η x) s).toReal ∂κ a) • c

Proof state:
case pos.h_add
α : 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 β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
⊢ ∀ ⦃f g : γ → E⦄,
    Disjoint (support f) (support g) →
      Integrable f ((η ∘ₖ κ) a) →
        Integrable g ((η ∘ₖ κ) a) →
          ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a →
            ∫ (z : γ), g z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a →
              ∫ (z : γ), (f + g) z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), (f + g) y ∂η x ∂κ a

Tactic:
rintro f g - i_f i_g hf hg

Result:
case pos.h_add
α : 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 β γ
inst✝ : NormedSpace ℝ E
f✝ : γ → E
hE : CompleteSpace E
f g : γ → E
i_f : Integrable f ((η ∘ₖ κ) a)
i_g : Integrable g ((η ∘ₖ κ) a)
hf : ∫ (z : γ), f z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a
hg : ∫ (z : γ), g z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a
⊢ ∫ (z : γ), (f + g) z ∂(η ∘ₖ κ) a = ∫ (x : β), ∫ (y : γ), (f + g) y ∂η x ∂κ a