-- Mathlib/Probability/Kernel/Disintegration/CDFToKernel.lean
lemma IsRatCondKernelCDFAux.tendsto_atBot_zero (hf : IsRatCondKernelCDFAux f κ ν) [IsFiniteKernel ν]
    (a : α) :
    ∀ᵐ t ∂(ν a), Tendsto (f (a, t)) atBot (𝓝 0)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun n => f (a, t) (-↑n)) atTop (𝓝 0)
t : β
ht : Tendsto (fun n => f (a, t) (-↑n)) atTop (𝓝 0)
h_mono : Monotone (f (a, t))
⊢ Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)

Tactic:
have h_anti : Antitone (fun q ↦ f (a, t) (-q)) := h_mono.comp_antitone monotone_id.neg

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun n => f (a, t) (-↑n)) atTop (𝓝 0)
t : β
ht : Tendsto (fun n => f (a, t) (-↑n)) atTop (𝓝 0)
h_mono : Monotone (f (a, t))
h_anti : Antitone fun q => f (a, t) (-q)
⊢ Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
t : β
ht : Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
h_eq_neg : f (a, t) = fun q => f (a, t) (- -q)
⊢ Tendsto (fun q => f (a, t) (- -q)) atBot (𝓝 0)

Tactic:
convert ht.comp tendsto_neg_atBot_atTop

Result:
case h.e'_3.h.h.e'_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
t : β
ht : Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
h_eq_neg : f (a, t) = fun q => f (a, t) (- -q)
x✝ : ℚ
⊢ - -x✝ = x✝

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
⊢ ∀ᵐ (t : β) ∂ν a, Tendsto (f (a, t)) atBot (𝓝 0)

Tactic:
suffices ∀ᵐ t ∂(ν a), Tendsto (fun q : ℚ ↦ f (a, t) (-q)) atTop (𝓝 0) by
  filter_upwards [this] with t ht
  have h_eq_neg : f (a, t) = fun q : ℚ ↦ f (a, t) (- -q) := by
    simp_rw [neg_neg]
  rw [h_eq_neg]
  convert ht.comp tendsto_neg_atBot_atTop
  simp

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
⊢ ∀ᵐ (t : β) ∂ν a, Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
⊢ ∀ᵐ (t : β) ∂ν a, Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)

Tactic:
suffices ∀ᵐ t ∂(ν a), Tendsto (fun (n : ℕ) ↦ f (a, t) (-n)) atTop (𝓝 0) by
  filter_upwards [this, hf.mono a] with t ht h_mono
  have h_anti : Antitone (fun q ↦ f (a, t) (-q)) := h_mono.comp_antitone monotone_id.neg
  exact (tendsto_iff_tendsto_subseq_of_antitone h_anti tendsto_natCast_atTop_atTop).mpr ht

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
⊢ ∀ᵐ (t : β) ∂ν a, Tendsto (fun n => f (a, t) (-↑n)) atTop (𝓝 0)

Proof state:
case h.e'_3.h.h.e'_1
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
t : β
ht : Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
h_eq_neg : f (a, t) = fun q => f (a, t) (- -q)
x✝ : ℚ
⊢ - -x✝ = x✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun n => f (a, t) (-↑n)) atTop (𝓝 0)
⊢ ∀ᵐ (t : β) ∂ν a, Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)

Tactic:
filter_upwards [this, hf.mono a] with t ht h_mono

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun n => f (a, t) (-↑n)) atTop (𝓝 0)
t : β
ht : Tendsto (fun n => f (a, t) (-↑n)) atTop (𝓝 0)
h_mono : Monotone (f (a, t))
⊢ Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
⊢ ∀ᵐ (t : β) ∂ν a, Tendsto (fun n => f (a, t) (-↑n)) atTop (𝓝 0)

Tactic:
exact hf.tendsto_zero_of_antitone _ _ Nat.mono_cast.neg
  (tendsto_neg_atBot_iff.mpr tendsto_natCast_atTop_atTop)

Result:
no goals

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
t : β
ht : Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
⊢ Tendsto (f (a, t)) atBot (𝓝 0)

Tactic:
have h_eq_neg : f (a, t) = fun q : ℚ ↦ f (a, t) (- -q) := by
  simp_rw [neg_neg]

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
t : β
ht : Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
h_eq_neg : f (a, t) = fun q => f (a, t) (- -q)
⊢ Tendsto (f (a, t)) atBot (𝓝 0)

Proof state:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun n => f (a, t) (-↑n)) atTop (𝓝 0)
t : β
ht : Tendsto (fun n => f (a, t) (-↑n)) atTop (𝓝 0)
h_mono : Monotone (f (a, t))
h_anti : Antitone fun q => f (a, t) (-q)
⊢ Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)

Tactic:
exact (tendsto_iff_tendsto_subseq_of_antitone h_anti tendsto_natCast_atTop_atTop).mpr ht

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
⊢ ∀ᵐ (t : β) ∂ν a, Tendsto (f (a, t)) atBot (𝓝 0)

Tactic:
filter_upwards [this] with t ht

Result:
case h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
t : β
ht : Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
⊢ Tendsto (f (a, t)) atBot (𝓝 0)

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α (β × ℝ)
ν : Kernel α β
f : α × β → ℚ → ℝ
hf : IsRatCondKernelCDFAux f κ ν
inst✝ : IsFiniteKernel ν
a : α
this : ∀ᵐ (t : β) ∂ν a, Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
t : β
ht : Tendsto (fun q => f (a, t) (-q)) atTop (𝓝 0)
⊢ f (a, t) = fun q => f (a, t) (- -q)

Tactic:
simp_rw [neg_neg]

Result:
no goals