-- Mathlib/Probability/Kernel/Disintegration/Density.lean
lemma tendsto_densityProcess_fst_atTop_univ_of_monotone (κ : Kernel α (γ × β)) (n : ℕ) (a : α)
    (x : γ) (seq : ℕ → Set β) (hseq : Monotone seq) (hseq_iUnion : ⋃ i, seq i = univ) :
    Tendsto (fun m ↦ densityProcess κ (fst κ) n a x (seq m)) atTop
      (𝓝 (densityProcess κ (fst κ) n a x univ))

Proof state:
case refine_1.left
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x✝ : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h : (κ a) (countablePartitionSet n x✝ ×ˢ univ) ≠ 0
h0 : (κ a) {p | p.1 ∈ countablePartitionSet n x✝} = 0
x : γ × β
⊢ x.1 ∈ countablePartitionSet n x✝ → x.2 ∈ univ → x.1 ∈ countablePartitionSet n x✝

Tactic:
exact fun h _ ↦ h

Result:
no goals

Proof state:
case h.e'_2.h.e'_6.h
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x✝ : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : (κ a) {p | p.1 ∈ countablePartitionSet n x✝} = 0
this : ∀ (m : ℕ), (κ a) (countablePartitionSet n x✝ ×ˢ seq m) = 0
x : γ × β
⊢ x ∈ countablePartitionSet n x✝ ×ˢ univ ↔ x ∈ {p | p.1 ∈ countablePartitionSet n x✝}

Tactic:
simp only [mem_prod, mem_univ, and_true, mem_setOf_eq]

Result:
no goals

Proof state:
case refine_1.right
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
⊢ (κ a) (countablePartitionSet n x ×ˢ univ) = ⊤ → (κ a) {p | p.1 ∈ countablePartitionSet n x} = ⊤

Tactic:
refine fun h_top ↦ eq_top_mono (measure_mono (fun x ↦ ?_)) h_top

Result:
case refine_1.right
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x✝ : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h_top : (κ a) (countablePartitionSet n x✝ ×ˢ univ) = ⊤
x : γ × β
⊢ x ∈ countablePartitionSet n x✝ ×ˢ univ → x ∈ {p | p.1 ∈ countablePartitionSet n x✝}

Proof state:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : (κ a) {p | p.1 ∈ countablePartitionSet n x} = 0
⊢ Tendsto (fun m => (κ a) (countablePartitionSet n x ×ˢ seq m) / (κ a) {p | p.1 ∈ countablePartitionSet n x}) atTop
    (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ a) {p | p.1 ∈ countablePartitionSet n x}))

Tactic:
suffices ∀ m, κ a (countablePartitionSet n x ×ˢ seq m) = 0 by
  simp only [this, h0, ENNReal.zero_div, tendsto_const_nhds_iff]
  suffices κ a (countablePartitionSet n x ×ˢ univ) = 0 by
    simp only [this, ENNReal.zero_div]
  convert h0
  ext x
  simp only [mem_prod, mem_univ, and_true, mem_setOf_eq]

Result:
case pos
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : (κ a) {p | p.1 ∈ countablePartitionSet n x} = 0
⊢ ∀ (m : ℕ), (κ a) (countablePartitionSet n x ×ˢ seq m) = 0

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : (κ a) {p | p.1 ∈ countablePartitionSet n x} = 0
this : ∀ (m : ℕ), (κ a) (countablePartitionSet n x ×ˢ seq m) = 0
⊢ Tendsto (fun m => (κ a) (countablePartitionSet n x ×ˢ seq m) / (κ a) {p | p.1 ∈ countablePartitionSet n x}) atTop
    (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ a) {p | p.1 ∈ countablePartitionSet n x}))

Tactic:
simp only [this, h0, ENNReal.zero_div, tendsto_const_nhds_iff]

Result:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : (κ a) {p | p.1 ∈ countablePartitionSet n x} = 0
this : ∀ (m : ℕ), (κ a) (countablePartitionSet n x ×ˢ seq m) = 0
⊢ 0 = (κ a) (countablePartitionSet n x ×ˢ univ) / 0

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
⊢ Tendsto (fun m => ((κ a) (countablePartitionSet n x ×ˢ seq m) / (κ.fst a) (countablePartitionSet n x)).toReal) atTop
    (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ.fst a) (countablePartitionSet n x)).toReal)

Tactic:
refine (ENNReal.tendsto_toReal ?_).comp ?_

Result:
case refine_1
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
⊢ (κ a) (countablePartitionSet n x ×ˢ univ) / (κ.fst a) (countablePartitionSet n x) ≠ ⊤

case refine_2
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
⊢ Tendsto (fun m => (κ a) (countablePartitionSet n x ×ˢ seq m) / (κ.fst a) (countablePartitionSet n x)) atTop
    (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ) / (κ.fst a) (countablePartitionSet n x)))

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : (κ a) {p | p.1 ∈ countablePartitionSet n x} = 0
this : ∀ (m : ℕ), (κ a) (countablePartitionSet n x ×ˢ seq m) = 0
⊢ (κ a) (countablePartitionSet n x ×ˢ univ) = 0

Tactic:
convert h0

Result:
case h.e'_2.h.e'_6
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h0 : (κ a) {p | p.1 ∈ countablePartitionSet n x} = 0
this : ∀ (m : ℕ), (κ a) (countablePartitionSet n x ×ˢ seq m) = 0
⊢ countablePartitionSet n x ×ˢ univ = {p | p.1 ∈ countablePartitionSet n x}

Proof state:
case refine_1.left
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
⊢ (κ a) (countablePartitionSet n x ×ˢ univ) ≠ 0 → (κ a) {p | p.1 ∈ countablePartitionSet n x} ≠ 0

Tactic:
refine fun h h0 ↦ h (measure_mono_null (fun x ↦ ?_) h0)

Result:
case refine_1.left
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝ : CountablyGenerated γ
κ : Kernel α (γ × β)
n : ℕ
a : α
x✝ : γ
seq : ℕ → Set β
hseq : Monotone seq
hseq_iUnion : ⋃ i, seq i = univ
h : (κ a) (countablePartitionSet n x✝ ×ˢ univ) ≠ 0
h0 : (κ a) {p | p.1 ∈ countablePartitionSet n x✝} = 0
x : γ × β
⊢ x ∈ countablePartitionSet n x✝ ×ˢ univ → x ∈ {p | p.1 ∈ countablePartitionSet n x✝}