-- 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_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)))

Tactic:
by_cases h0 : fst κ a (countablePartitionSet n x) = 0

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 : (κ.fst a) (countablePartitionSet n x) = 0
⊢ 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)))

case neg
α : 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 : ¬(κ.fst a) (countablePartitionSet n x) = 0
⊢ 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:
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✝}

Tactic:
simp only [mem_prod, mem_setOf_eq, and_imp]

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.1 ∈ countablePartitionSet n x✝ → x.2 ∈ univ → x.1 ∈ countablePartitionSet n x✝

Proof state:
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) ≠ 0 → (κ a) {p | p.1 ∈ countablePartitionSet n x} ≠ 0) ∧
    ((κ a) (countablePartitionSet n x ×ˢ univ) = ⊤ → (κ a) {p | p.1 ∈ countablePartitionSet n x} = ⊤)

Tactic:
constructor

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
⊢ (κ a) (countablePartitionSet n x ×ˢ univ) ≠ 0 → (κ a) {p | p.1 ∈ countablePartitionSet n x} ≠ 0

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} = ⊤

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 => κ.densityProcess κ.fst n a x (seq m)) atTop (𝓝 (κ.densityProcess κ.fst n a x univ))

Tactic:
simp_rw [densityProcess]

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
⊢ 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)

Proof state:
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) ≠ 0 → (κ.fst a) (countablePartitionSet n x) ≠ 0) ∧
    ((κ a) (countablePartitionSet n x ×ˢ univ) = ⊤ → (κ.fst a) (countablePartitionSet n x) = ⊤)

Tactic:
simp_rw [fst_apply' _ _ (measurableSet_countablePartitionSet _ _)]

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) ≠ 0 → (κ a) {p | p.1 ∈ countablePartitionSet n x} ≠ 0) ∧
    ((κ a) (countablePartitionSet n x ×ˢ univ) = ⊤ → (κ a) {p | p.1 ∈ countablePartitionSet n x} = ⊤)

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
h_top : (κ a) (countablePartitionSet n x✝ ×ˢ univ) = ⊤
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 neg
α : 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 : ¬(κ.fst a) (countablePartitionSet n x) = 0
⊢ 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)))

Tactic:
refine ENNReal.Tendsto.div_const ?_ ?_

Result:
case neg.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
h0 : ¬(κ.fst a) (countablePartitionSet n x) = 0
⊢ Tendsto (fun m => (κ a) (countablePartitionSet n x ×ˢ seq m)) atTop (𝓝 ((κ a) (countablePartitionSet n x ×ˢ univ)))

case neg.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
h0 : ¬(κ.fst a) (countablePartitionSet n x) = 0
⊢ (κ a) (countablePartitionSet n x ×ˢ univ) ≠ 0 ∨ (κ.fst a) (countablePartitionSet n x) ≠ 0