mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.GroupTheory.PushoutI

Goal state before:
pp: case e'_8
ι : Type u_1
G : ι → Type u_2
H : Type u_3
K : Type u_4
inst✝⁴ : Monoid K
inst✝³ : (i : ι) → Group (G i)
inst✝² : Group H
φ : (i : ι) → H →* G i
d : Transversal φ
inst✝¹ : DecidableEq ι
inst✝ : (i : ι) → DecidableEq (G i)
motive : NormalWord d → Sort ?u.126
empty : motive NormalWord.empty
cons :
  (i : ι) →
    (g : G i) →
      (w : NormalWord d) →
        (hmw : w.fstIdx ≠ some i) →
          g ∈ d.set i → (hgr : g ∉ (φ i).range) → w.head = 1 → motive w → motive (NormalWord.cons g w hmw hgr)
base : (h : H) → (w : NormalWord d) → w.head = 1 → motive w → motive ((PushoutI.base φ) h • w)
head : H
i : ι
g : G i
w : Word G
h1 : w.fstIdx ≠ some i
hg1 : g ≠ 1
ih : (h3 : ∀ (i : ι) (g : G i), ⟨i, g⟩ ∈ w.toList → g ∈ d.set i) → motive { toWord := w, head := 1, normalized := h3 }
h3 : ∀ (i_1 : ι) (g_1 : G i_1), ⟨i_1, g_1⟩ ∈ (Word.cons g w h1 hg1).toList → g_1 ∈ d.set i_1
⊢ Word.cons g w h1 hg1 = (NormalWord.cons g { toWord := w, head := 1, normalized := ⋯ } h1 ?cons).toWord

Tactic:
simp only [Word.cons, NormalWord.cons, map_one, mul_one,
          (equiv_snd_eq_self_iff_mem (d.compl i) (one_mem _)).2
          (h3 _ _ List.mem_cons_self)]

Goal state after:
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
I : Finset ι
κ : ι → Kernel α β
a : α
s : Set β
⊢ ((∑ i ∈ I, κ i) a) s = ∑ i ∈ I, ((κ i) a) s

Tactic:
sum_apply,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
I : Finset ι
κ : ι → Kernel α β
a : α
s : Set β
⊢ (∑ i ∈ I, (κ i) a) s = ∑ i ∈ I, ((κ i) a) s
Module: Mathlib.Probability.Kernel.Defs

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
h : IsFiniteKernel κ
n : ℕ
⊢ IsFiniteKernel ((fun n ↦ if n = 0 then κ else 0) n)

Tactic:
by
      simp only; split_ifs
      · exact h
      · infer_instance

Goal state after:
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
s t : Set β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hs : MeasurableSet s
a : α
⊢ (κ.restrict hs) a = (Kernel.sum fun n ↦ (κ.seq n).restrict hs) a

Tactic:
sum_apply,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
s t : Set β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hs : MeasurableSet s
a : α
⊢ (κ.restrict hs) a = Measure.sum fun n ↦ ((κ.seq n).restrict hs) a
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
s t : Set β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hs : MeasurableSet s
a : α
⊢ (κ a).restrict s = (Measure.sum fun i ↦ (κ.seq i) a).restrict s

Tactic:
← sum_apply,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ✝ : Kernel α β
s t : Set β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
hs : MeasurableSet s
a : α
⊢ (κ a).restrict s = ((Kernel.sum κ.seq) a).restrict s
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ : ∀ (a : α), (κ a) (Set.range f) = 1
a : α
⊢ ((κ.comapRight hf) a) Set.univ = 1

Tactic:
comapRight_apply' κ hf a MeasurableSet.univ

Goal state after:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
mγ : MeasurableSpace γ
f : γ → β
κ : Kernel α β
hf : MeasurableEmbedding f
hκ : ∀ (a : α), (κ a) (Set.range f) = 1
a : α
⊢ (κ a) (f '' Set.univ) = 1
Module: Mathlib.Probability.Kernel.Basic

Goal state before:
pp: α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ (piecewise hs κ η) a = (Kernel.sum fun n ↦ piecewise hs (κ.seq n) (η.seq n)) a

Tactic:
sum_apply,

Goal state after:
α : Type u_1
β : Type u_2
ι : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
s : Set α
hs : MeasurableSet s
inst✝² : DecidablePred fun x ↦ x ∈ s
inst✝¹ : IsSFiniteKernel κ
inst✝ : IsSFiniteKernel η
a : α
⊢ (piecewise hs κ η) a = Measure.sum fun n ↦ (piecewise hs (κ.seq n) (η.seq n)) a
Module: Mathlib.Probability.Kernel.MeasurableLIntegral

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
t : Set (α × β)
ht : MeasurableSet t
⊢ Measurable fun a ↦ (κ a) (Prod.mk a ⁻¹' t)

Tactic:
by
  rw [← Kernel.kernel_sum_seq κ]
  have (a : _) : Kernel.sum (Kernel.seq κ) a (Prod.mk a ⁻¹' t) =
      ∑' n, Kernel.seq κ n a (Prod.mk a ⁻¹' t) :=
    Kernel.sum_apply' _ _ (measurable_prodMk_left ht)
  simp_rw [this]
  refine Measurable.tsum fun n => ?_
  exact measurable_kernel_prodMk_left_of_finite ht inferInstance

Goal state after:
Module: Mathlib.InformationTheory.Coding.KraftMcMillan

Goal state before:

Tactic:
(∑ w ∈ S, (1 / (Fintype.card α) : ℝ) ^ w.length) ^ r
    _ = ∑ w : Fin r → S, ∏ i : Fin r, (1 / D) ^ (w i).val.length := by
      simpa [(Finset.sum_coe_sort S _).symm] using
        Fintype.sum_pow (f := fun c : S => (1 / D) ^ c.val.length) r
    -- Each tuple contributes the weight `(1/D)^{|concatFn w|}`.
    _ = ∑ w, (1 / D) ^ (concatFn w).length := by
      apply Fintype.sum_congr
      intro w
      simpa [concatFn_length] using Finset.prod_pow_eq_pow_sum Finset.univ _ _
    -- Unique decodability makes `concatFn` injective, so these concatenations are distinct;
    -- we can reindex the sum by the set `T` of words.
    _ = ∑ x ∈ T, (1 / D) ^ x.length :=
      (Finset.sum_image (f := fun x => (1 / D) ^ x.length)
        (fun _ _ _ _ hEq => concatFn_injective_of_uniquelyDecodable h r hEq)).symm
    -- Group the sum over `T` by the length `s`.
    -- The admissible lengths lie in `[r, r*maxLen]` by `hlen_maps`.
    _ = ∑ s ∈ Finset.Icc r (r * maxLen), ∑ x ∈ T with x.length = s, (1 / D) ^ x.length :=
      (Finset.sum_fiberwise_of_maps_to hlen_maps _).symm

Goal state after:
case calc.step
α : Type u_1
S : Finset (List α)
inst✝¹ : Fintype α
inst✝ : Nonempty α
h : UniquelyDecodable ↑S
r : ℕ
hr : r ≥ 1
maxLen : ℕ := S.sup List.length
T : Finset (List α) := Finset.image concatFn Finset.univ
hlen_maps : ∀ x ∈ T, x.length ∈ Finset.Icc r (r * maxLen)
D : ℝ := ↑(Fintype.card α)
⊢ ∑ s ∈ Finset.Icc r (r * maxLen), ∑ x ∈ T with x.length = s, (1 / D) ^ x.length ≤ ↑r * ↑maxLen
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : ι → Kernel α β
η : Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((η ∘ₖ Kernel.sum κ) a✝) s✝ = ((Kernel.sum fun i ↦ η ∘ₖ κ i) a✝) s✝

Tactic:
sum_apply,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : ι → Kernel α β
η : Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((η ∘ₖ Kernel.sum κ) a✝) s✝ = (Measure.sum fun n ↦ (η ∘ₖ κ n) a✝) s✝
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : ι → Kernel α β
η : Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ∫⁻ (b : β), (η b) s✝ ∂(Kernel.sum κ) a✝ = ∑' (i : ι), ((η ∘ₖ κ i) a✝) s✝

Tactic:
sum_apply,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : ι → Kernel α β
η : Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ (∫⁻ (b : β), (η b) s✝ ∂Measure.sum fun n ↦ (κ n) a✝) = ∑' (i : ι), ((η ∘ₖ κ i) a✝) s✝
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : Kernel α β
η : ι → Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((Kernel.sum η ∘ₖ κ) a✝) s✝ = ((Kernel.sum fun i ↦ η i ∘ₖ κ) a✝) s✝

Tactic:
sum_apply,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : Kernel α β
η : ι → Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ((Kernel.sum η ∘ₖ κ) a✝) s✝ = (Measure.sum fun n ↦ (η n ∘ₖ κ) a✝) s✝
Module: Mathlib.Probability.Kernel.Composition.Comp

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : Kernel α β
η : ι → Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ∫⁻ (b : β), ((Kernel.sum η) b) s✝ ∂κ a✝ = (Measure.sum fun n ↦ (η n ∘ₖ κ) a✝) s✝

Tactic:
sum_apply,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝ : Countable ι
κ : Kernel α β
η : ι → Kernel β γ
a✝ : α
s✝ : Set γ
hs : MeasurableSet s✝
⊢ ∫⁻ (b : β), (Measure.sum fun n ↦ (η n) b) s✝ ∂κ a✝ = (Measure.sum fun n ↦ (η n ∘ₖ κ) a✝) s✝
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel κ
p : α × β → Prop
h : ∀ᵐ (x : α × β) ∂μ ⊗ₘ κ, p x
⊢ ∀ᵐ (a : α) ∂μ, ∀ᵐ (b : β) ∂κ a, p (a, b)

Tactic:
by
  convert! Kernel.ae_ae_of_ae_compProd h

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_5
inst✝ : Countable ι
κ : ι → Kernel α β
a✝¹ : γ × α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((Kernel.sum fun i ↦ prodMkLeft γ (κ i)) a✝¹) s✝ = ((prodMkLeft γ (Kernel.sum κ)) a✝¹) s✝

Tactic:
sum_apply,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_5
inst✝ : Countable ι
κ : ι → Kernel α β
a✝¹ : γ × α
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ (Measure.sum fun n ↦ (prodMkLeft γ (κ n)) a✝¹) s✝ = ((prodMkLeft γ (Kernel.sum κ)) a✝¹) s✝
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_5
inst✝ : Countable ι
κ : ι → Kernel α β
a✝¹ : α × γ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ ((Kernel.sum fun i ↦ prodMkRight γ (κ i)) a✝¹) s✝ = ((prodMkRight γ (Kernel.sum κ)) a✝¹) s✝

Tactic:
sum_apply,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_5
inst✝ : Countable ι
κ : ι → Kernel α β
a✝¹ : α × γ
s✝ : Set β
a✝ : MeasurableSet s✝
⊢ (Measure.sum fun n ↦ (prodMkRight γ (κ n)) a✝¹) s✝ = ((prodMkRight γ (Kernel.sum κ)) a✝¹) s✝
Module: Mathlib.Probability.Kernel.Composition.MapComap

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α (β × γ)
a : α
s : Set (γ × β)
hs : MeasurableSet s
⊢ (κ.swapRight a) s = (κ a) {p | p.swap ∈ s}

Tactic:
rw [swapRight_apply, Measure.map_apply measurable_swap hs]; rfl

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
⊢ Measurable fun x ↦
    ∫⁻ (y : β),
      ((swap γ β ∘ₖ (η ∥ₖ Kernel.id) ∘ₖ deterministic ⇑MeasurableEquiv.prodAssoc.symm ⋯ ∘ₖ (Kernel.id ∥ₖ copy β))
          (x, y))
        s ∂κ (a, a).2

Tactic:
suffices Measurable fun p : α × β ↦
      (swap γ β ∘ₖ (η ∥ₖ Kernel.id)
        ∘ₖ deterministic MeasurableEquiv.prodAssoc.symm (MeasurableEquiv.measurable _)
        ∘ₖ (Kernel.id ∥ₖ copy β)) p s by fun_prop
    exact Kernel.measurable_coe _ hs

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MeasureCompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
μ : Measure α
κ η : Kernel α β
inst✝¹ : SFinite μ
inst✝ : IsSFiniteKernel η
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
hκ : IsSFiniteKernel κ
s : Set (α × β)
hs : MeasurableSet s
hs_zero : (fun a ↦ (η a) (Prod.mk a ⁻¹' s)) =ᵐ[μ] 0
⊢ (fun a ↦ (κ a) (Prod.mk a ⁻¹' s)) =ᵐ[μ] 0

Tactic:
filter_upwards [hs_zero, hκη] with a ha_zero ha_ac using ha_ac ha_zero

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case e_f
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
s : Set (β × γ)
hs : MeasurableSet s
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
b : β
h_int : ∀ (x : γ), ∫⁻ (y : β), ((swap γ β) (x, y)) s ∂Measure.dirac b = (Prod.mk b ⁻¹' s).indicator 1 x
⊢ MeasurableSet (Prod.mk b ⁻¹' s)

Tactic:
exact measurable_prodMk_left hs

Goal state after:
Module: Mathlib.Probability.Kernel.Composition.MeasureComp

Goal state before:
pp: α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ η : Kernel α β
μ : Measure α
hκη : ∀ᵐ (a : α) ∂μ, κ a ≪ η a
s : Set β
hs : MeasurableSet s
hs_zero : (fun a ↦ (η a) s) =ᵐ[μ] 0
⊢ (fun a ↦ (κ a) s) =ᵐ[μ] 0

Tactic:
filter_upwards [hs_zero, hκη] with a ha_zero ha_ac using ha_ac ha_zero

Goal state after:
Module: Mathlib.Probability.Kernel.MeasurableIntegral

Goal state before:
pp: case pos.refine_2
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable f (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s n)
x : α
⊢ Tendsto (fun i ↦ f' i x) atTop (𝓝 (∫ (y : β), f y ∂κ x))

Tactic:
by_cases hfx : Integrable f (κ x)

Goal state after:
case pos
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable f (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s n)
x : α
hfx : Integrable f (κ x)
⊢ Tendsto (fun i ↦ f' i x) atTop (𝓝 (∫ (y : β), f y ∂κ x))

case neg
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
E : Type u_4
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : β → E
hf : StronglyMeasurable f
hE : CompleteSpace E
this✝¹ : MeasurableSpace E := borel E
this✝ : BorelSpace E
this : TopologicalSpace.SeparableSpace ↑(range f ∪ {0})
s : ℕ → SimpleFunc β E := SimpleFunc.approxOn f ⋯ (range f ∪ {0}) 0 ⋯
f' : ℕ → α → E := fun n ↦ {x | Integrable f (κ x)}.indicator fun x ↦ SimpleFunc.integral (κ x) (s n)
x : α
hfx : ¬Integrable f (κ x)
⊢ Tendsto (fun i ↦ f' i x) atTop (𝓝 (∫ (y : β), f y ∂κ x))
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : Measurable f
g : β → γ → ℝ≥0∞ := Function.curry f
⊢ ∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η) a = ∫⁻ (bc : β × γ), g bc.1 bc.2 ∂(κ ⊗ₖ η) a

Tactic:
g,

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : Measurable f
g : β → γ → ℝ≥0∞ := Function.curry f
⊢ ∫⁻ (bc : β × γ), f bc ∂(κ ⊗ₖ η) a = ∫⁻ (bc : β × γ), Function.curry f bc.1 bc.2 ∂(κ ⊗ₖ η) a
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : Measurable f
g : β → γ → ℝ≥0∞ := Function.curry f
⊢ Measurable (Function.uncurry g)

Tactic:
g,

Goal state after:
case hf
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : Measurable f
g : β → γ → ℝ≥0∞ := Function.curry f
⊢ Measurable (Function.uncurry (Function.curry f))
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : AEMeasurable f ((κ ⊗ₖ η) a)
A : ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η) a
⊢ ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a

Tactic:
have B : ∫⁻ x, ∫⁻ y, f (x, y) ∂η (a, x) ∂κ a = ∫⁻ x, ∫⁻ y, hf.mk f (x, y) ∂η (a, x) ∂κ a := by
    apply lintegral_congr_ae
    filter_upwards [ae_ae_of_ae_compProd hf.ae_eq_mk] with _ ha using lintegral_congr_ae ha

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
inst✝¹ : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝ : IsSFiniteKernel η
a : α
f : β × γ → ℝ≥0∞
hf : AEMeasurable f ((κ ⊗ₖ η) a)
A : ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫⁻ (z : β × γ), AEMeasurable.mk f hf z ∂(κ ⊗ₖ η) a
B : ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a = ∫⁻ (x : β), ∫⁻ (y : γ), AEMeasurable.mk f hf (x, y) ∂η (a, x) ∂κ a
⊢ ∫⁻ (z : β × γ), f z ∂(κ ⊗ₖ η) a = ∫⁻ (x : β), ∫⁻ (y : γ), f (x, y) ∂η (a, x) ∂κ a
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : ¬IsSFiniteKernel ξ
h_sfin : IsSFiniteKernel (ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯)
⊢ IsSFiniteKernel ξ

Tactic:
have : ξ = (ξ.comap MeasurableEquiv.prodAssoc (MeasurableEquiv.measurable _)).comap
          MeasurableEquiv.prodAssoc.symm (MeasurableEquiv.measurable _) := by
        simp [← comap_comp_right]

Goal state after:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
δ : Type u_4
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel (α × β) γ
ξ : Kernel (α × β × γ) δ
hκ : IsSFiniteKernel κ
hη : IsSFiniteKernel η
hξ : ¬IsSFiniteKernel ξ
h_sfin : IsSFiniteKernel (ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯)
this : ξ = (ξ.comap ⇑MeasurableEquiv.prodAssoc ⋯).comap ⇑MeasurableEquiv.prodAssoc.symm ⋯
⊢ IsSFiniteKernel ξ
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((Kernel.sum κ ⊗ₖ η) a) s = ((Kernel.sum fun i ↦ κ i ⊗ₖ η) a) s

Tactic:
sum_apply,

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((Kernel.sum κ ⊗ₖ η) a) s = (Measure.sum fun n ↦ (κ n ⊗ₖ η) a) s
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂(Kernel.sum κ) a = (Measure.sum fun n ↦ (κ n ⊗ₖ η) a) s

Tactic:
sum_apply,

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : ι → Kernel α β
η : Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (κ i)
hη : IsSFiniteKernel η
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ (∫⁻ (b : β), (η (a, b)) (Prod.mk b ⁻¹' s) ∂Measure.sum fun n ↦ (κ n) a) = (Measure.sum fun n ↦ (κ n ⊗ₖ η) a) s
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ ⊗ₖ Kernel.sum η) a) s = ((Kernel.sum fun i ↦ κ ⊗ₖ η i) a) s

Tactic:
sum_apply,

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ((κ ⊗ₖ Kernel.sum η) a) s = (Measure.sum fun n ↦ (κ ⊗ₖ η n) a) s
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), ((Kernel.sum η) (a, b)) (Prod.mk b ⁻¹' s) ∂κ a = ∑' (i : ι), ((κ ⊗ₖ η i) a) s

Tactic:
sum_apply,

Goal state after:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
⊢ ∫⁻ (b : β), (Measure.sum fun n ↦ (η n) (a, b)) (Prod.mk b ⁻¹' s) ∂κ a = ∑' (i : ι), ((κ ⊗ₖ η i) a) s
Module: Mathlib.Probability.Kernel.Composition.CompProd

Goal state before:
pp: case pos.e_f.hs
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
ι : Type u_4
inst✝¹ : Countable ι
κ : Kernel α β
η : ι → Kernel (α × β) γ
inst✝ : ∀ (i : ι), IsSFiniteKernel (η i)
hκ : IsSFiniteKernel κ
a : α
s : Set (β × γ)
hs : MeasurableSet s
i : β
⊢ MeasurableSet (Prod.mk i ⁻¹' s)

Tactic:
exact measurable_prodMk_left hs

Goal state after: