-- Mathlib/Probability/Kernel/Composition/CompProd.lean
theorem ae_kernel_lt_top (a : α) (h2s : (κ ⊗ₖ η) a s ≠ ∞) :
    ∀ᵐ b ∂κ a, η (a, b) (Prod.mk b ⁻¹' s) < ∞

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
h2t : ((κ ⊗ₖ η) a) t ≠ ⊤
ht_lt_top : ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' t) < ⊤
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤

Tactic:
filter_upwards [ht_lt_top] with b hb

Result:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
h2t : ((κ ⊗ₖ η) a) t ≠ ⊤
ht_lt_top : ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' t) < ⊤
b : β
hb : (η (a, b)) (Prod.mk b ⁻¹' t) < ⊤
⊢ (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
h2t : ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ t} ∂κ a ≠ ⊤
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' t) < ⊤

Tactic:
exact ae_lt_top (Kernel.measurable_kernel_prod_mk_left' ht a) h2t

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
h2t : ((κ ⊗ₖ η) a) t ≠ ⊤
ht_lt_top : ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' t) < ⊤
b : β
hb : (η (a, b)) (Prod.mk b ⁻¹' t) < ⊤
⊢ (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤

Tactic:
exact (this b).trans_lt hb

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤

Tactic:
have ht : MeasurableSet t := measurableSet_toMeasurable _ _

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤

Tactic:
let t := toMeasurable ((κ ⊗ₖ η) a) s

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤

Tactic:
have : ∀ b : β, η (a, b) (Prod.mk b ⁻¹' s) ≤ η (a, b) (Prod.mk b ⁻¹' t) := fun b =>
  measure_mono (Set.preimage_mono (subset_toMeasurable _ _))

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
h2t : ((κ ⊗ₖ η) a) t ≠ ⊤
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤

Tactic:
have ht_lt_top : ∀ᵐ b ∂κ a, η (a, b) (Prod.mk b ⁻¹' t) < ∞ := by
  rw [Kernel.compProd_apply ht] at h2t
  exact ae_lt_top (Kernel.measurable_kernel_prod_mk_left' ht a) h2t

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
h2t : ((κ ⊗ₖ η) a) t ≠ ⊤
ht_lt_top : ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' t) < ⊤
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' s) < ⊤

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
h2t : ((κ ⊗ₖ η) a) t ≠ ⊤
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' t) < ⊤

Tactic:
rw [Kernel.compProd_apply ht] at h2t

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
h2t : ∫⁻ (b : β), (η (a, b)) {c | (b, c) ∈ t} ∂κ a ≠ ⊤
⊢ ∀ᵐ (b : β) ∂κ a, (η (a, b)) (Prod.mk b ⁻¹' t) < ⊤

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
h2s : ((κ ⊗ₖ η) a) s ≠ ⊤
t : Set (β × γ) := toMeasurable ((κ ⊗ₖ η) a) s
this : ∀ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ≤ (η (a, b)) (Prod.mk b ⁻¹' t)
ht : MeasurableSet t
⊢ ((κ ⊗ₖ η) a) t ≠ ⊤

Tactic:
rwa [measure_toMeasurable]

Result:
no goals