-- Mathlib/Probability/Kernel/Disintegration/Unique.lean
/-- Auxiliary lemma for `eq_condKernel_of_measure_eq_compProd`.
Uniqueness of the disintegration kernel on ℝ. -/
lemma eq_condKernel_of_measure_eq_compProd_real {ρ : Measure (α × ℝ)} [IsFiniteMeasure ρ]
    (κ : Kernel α ℝ) [IsFiniteKernel κ] (hκ : ρ = ρ.fst ⊗ₘ κ) :
    ∀ᵐ x ∂ρ.fst, κ x = ρ.condKernel x

Proof state:
case h_union
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst,
    ∀ (f : ℕ → Set ℝ),
      Pairwise (Function.onFun Disjoint f) →
        (∀ (i : ℕ), MeasurableSet (f i)) →
          (∀ (i : ℕ), (κ x) (f i) = (ρ.condKernel x) (f i)) → (κ x) (⋃ i, f i) = (ρ.condKernel x) (⋃ i, f i)

Tactic:
refine ae_of_all _ (fun x f hdisj hf heq ↦ ?_)

Result:
case h_union
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
x : α
f : ℕ → Set ℝ
hdisj : Pairwise (Function.onFun Disjoint f)
hf : ∀ (i : ℕ), MeasurableSet (f i)
heq : ∀ (i : ℕ), (κ x) (f i) = (ρ.condKernel x) (f i)
⊢ (κ x) (⋃ i, f i) = (ρ.condKernel x) (⋃ i, f i)

Proof state:
case h.h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
this : ∀ᵐ (x : α) ∂ρ.fst, ∀ ⦃t : Set ℝ⦄, MeasurableSet t → (κ x) t = (ρ.condKernel x) t
x : α
hx : ∀ ⦃t : Set ℝ⦄, MeasurableSet t → (κ x) t = (ρ.condKernel x) t
t : Set ℝ
ht : MeasurableSet t
⊢ (κ x) t = (ρ.condKernel x) t

Tactic:
exact hx ht

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
this : ∀ᵐ (x : α) ∂ρ.fst, ∀ ⦃t : Set ℝ⦄, MeasurableSet t → (κ x) t = (ρ.condKernel x) t
⊢ ∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x

Tactic:
filter_upwards [this] with x hx

Result:
case h
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
this : ∀ᵐ (x : α) ∂ρ.fst, ∀ ⦃t : Set ℝ⦄, MeasurableSet t → (κ x) t = (ρ.condKernel x) t
x : α
hx : ∀ ⦃t : Set ℝ⦄, MeasurableSet t → (κ x) t = (ρ.condKernel x) t
⊢ κ x = ρ.condKernel x

Proof state:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst, κ x = ρ.condKernel x

Tactic:
suffices ∀ᵐ x ∂ρ.fst, ∀ ⦃t⦄, MeasurableSet t → κ x t = ρ.condKernel x t by
  filter_upwards [this] with x hx
  ext t ht; exact hx ht

Result:
α : Type u_1
mα : MeasurableSpace α
ρ : Measure (α × ℝ)
inst✝¹ : IsFiniteMeasure ρ
κ : Kernel α ℝ
inst✝ : IsFiniteKernel κ
hκ : ρ = ρ.fst ⊗ₘ κ
huniv : ∀ᵐ (x : α) ∂ρ.fst, (κ x) univ = (ρ.condKernel x) univ
⊢ ∀ᵐ (x : α) ∂ρ.fst, ∀ ⦃t : Set ℝ⦄, MeasurableSet t → (κ x) t = (ρ.condKernel x) t