awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : Measurable (Function.uncurry f)
a : α
⊢ ∫⁻ (b : β) in Set.univ, f a b ∂(κ : (a : α) → Measure β) a ≤ ∫⁻ (x : β) in Set.univ, B ∂(κ : (a : α) → Measure β) a

Tactic:
lintegral_mono (hf_B a)

Premises used: MeasureTheory.lintegral_mono
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : Measurable (Function.uncurry f)
a : α
⊢ ∫⁻ (x : β) in Set.univ, B ∂(κ : (a : α) → Measure β) a =
    HMul.hMul (β := ℝ≥0∞) B ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)

Tactic:
simp only [Measure.restrict_univ, MeasureTheory.lintegral_const]

Premises used: MeasureTheory.lintegral_const, MeasureTheory.Measure.restrict_univ
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : Measurable (Function.uncurry f)
a : α
grw grw₁ : B * κ.bound ≤ B * κ.bound
⊢ HMul.hMul (β := ℝ≥0∞) B ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
    B * κ.bound

Tactic:
grw [measure_le_bound]

Premises used: ProbabilityTheory.Kernel.measure_le_bound
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : Measurable (Function.uncurry f)
a : α
b :
  ∫⁻ (x : β) in Set.univ, B ∂(κ : (a : α) → Measure β) a =
    HMul.hMul (β := ℝ≥0∞) B ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞)
b₁ :
  HMul.hMul (β := ℝ≥0∞) B ((((κ : (a : α) → Measure β) a : Measure β) : (a : Set β) → ℝ≥0∞) Set.univ : ℝ≥0∞) ≤
    B * κ.bound
⊢ ∫⁻ (b : β) in Set.univ, f a b ∂(κ : (a : α) → Measure β) a ≤ B * κ.bound

Tactic:
calc
          ∫⁻ b in Set.univ, f a b ∂κ a ≤ ∫⁻ _ in Set.univ, B ∂κ a := lintegral_mono (hf_B a)
          _ = B * κ a Set.univ := by
            simp only [Measure.restrict_univ, MeasureTheory.lintegral_const]
          _ ≤ B * κ.bound := by grw [measure_le_bound]

Premises used: Set.univ, MeasureTheory.lintegral_mono, DFunLike.coe, ProbabilityTheory.Kernel.bound
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : Measurable (Function.uncurry f)
⊢ IsFiniteKernel (κ.withDensity f)

Tactic:
exact ⟨⟨B * κ.bound, ENNReal.mul_lt_top hB_top.lt_top κ.bound_lt_top, fun a => by
        rw [Kernel.withDensity_apply' κ hf a Set.univ]
        calc
          ∫⁻ b in Set.univ, f a b ∂κ a ≤ ∫⁻ _ in Set.univ, B ∂κ a := lintegral_mono (hf_B a)
          _ = B * κ a Set.univ := by
            simp only [Measure.restrict_univ, MeasureTheory.lintegral_const]
          _ ≤ B * κ.bound := by grw [measure_le_bound]⟩⟩
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : ¬Measurable (Function.uncurry f)
neg : IsFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
⊢ IsFiniteKernel (κ.withDensity f)

Tactic:
rw [withDensity_of_not_measurable _ hf]

Premises used: ProbabilityTheory.Kernel.withDensity_of_not_measurable
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
B : ℝ≥0∞
hB_top : B ≠ ∞
hf_B : ∀ (a : α) (b : β), f a b ≤ B
hf : ¬Measurable (Function.uncurry f)
⊢ IsFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
pos : ∀ (hf : Measurable (Function.uncurry f)), IsSFiniteKernel (κ.withDensity f)
neg : ∀ (hf : ¬Measurable (Function.uncurry f)), IsSFiniteKernel (κ.withDensity f)
⊢ IsSFiniteKernel (κ.withDensity f)

Tactic:
by_cases hf : Measurable (Function.uncurry f)

Premises used: Measurable, Function.uncurry
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : ¬Measurable (Function.uncurry f)
neg : IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0
⊢ IsSFiniteKernel (κ.withDensity f)

Tactic:
rw [withDensity_of_not_measurable _ hf]

Premises used: ProbabilityTheory.Kernel.withDensity_of_not_measurable
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : ¬Measurable (Function.uncurry f)
⊢ IsSFiniteKernel.{u_1, u_2} (α := α) (β := β) (mα := mα) (mβ := mβ) 0

Tactic:
infer_instance
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
⊢ (f a b).toReal ≤ (↑n : ℝ)

Tactic:
have : (f a b).toReal ≤ n := Nat.le_of_ceil_le hn
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
this : (f a b).toReal ≤ (↑n : ℝ)
rw : ∀ (this : f a b ≤ ENNReal.ofReal (↑n : ℝ)), f a b ≤ (↑n : ℝ≥0∞)
rw₁ : LE.le (α := ℝ) 0 (↑n : ℝ)
⊢ f a b ≤ (↑n : ℝ≥0∞)

Tactic:
rw [← ENNReal.le_ofReal_iff_toReal_le (hf_ne_top a b) _] at this

Premises used: ENNReal.le_ofReal_iff_toReal_le
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
this : f a b ≤ ENNReal.ofReal (↑n : ℝ)
⊢ f a b ≤ (↑n : ℝ≥0∞)

Tactic:
simpa
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
this : (f a b).toReal ≤ (↑n : ℝ)
⊢ LE.le (α := ℝ) 0 (↑n : ℝ)

Tactic:
n.cast_nonneg

Premises used: Nat.cast_nonneg
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
this : (f a b).toReal ≤ (↑n : ℝ)
⊢ LE.le (α := ℝ) 0 (↑n : ℝ)

Tactic:
exact n.cast_nonneg

Premises used: Nat.cast_nonneg
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
⊢ ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)

Tactic:
have h_le : ∀ a b n, ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ n := by
    intro a b n hn
    have : (f a b).toReal ≤ n := Nat.le_of_ceil_le hn
    rw [← ENNReal.le_ofReal_iff_toReal_le (hf_ne_top a b) _] at this
    · simpa
    · exact n.cast_nonneg
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
this : min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) = f a b ∧ min (f a b) (↑n : ℝ≥0∞) = f a b
simp_rw : min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞) = 0
simp_rw₁ : f a b - min (f a b) (↑n : ℝ≥0∞) = 0
simp_rw₂ : f a b - f a b = 0
⊢ fs n a b = 0

Tactic:
simp_rw [fs, this.1, this.2, tsub_self (f a b)]

Premises used: tsub_self, And.right, And.left
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
suffices : min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) = f a b ∧ min (f a b) (↑n : ℝ≥0∞) = f a b
⊢ fs n a b = 0

Tactic:
suffices min (f a b) (n + 1) = f a b ∧ min (f a b) n = f a b by
      simp_rw [fs, this.1, this.2, tsub_self (f a b)]
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
⊢ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) = f a b ∧ min (f a b) (↑n : ℝ≥0∞) = f a b

Tactic:
⟨min_eq_left ((h_le a b n hn).trans (le_add_of_nonneg_right zero_le_one)),
      min_eq_left (h_le a b n hn)⟩

Premises used: zero_le_one, le_add_of_nonneg_right, min_eq_left, And.intro, LE.le.trans
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
a : α
b : β
n : ℕ
hn : ⌈(f a b).toReal⌉₊ ≤ n
⊢ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) = f a b ∧ min (f a b) (↑n : ℝ≥0∞) = f a b

Tactic:
exact ⟨min_eq_left ((h_le a b n hn).trans (le_add_of_nonneg_right zero_le_one)),
      min_eq_left (h_le a b n hn)⟩
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
⊢ ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0

Tactic:
have h_zero : ∀ a b n, ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0 := by
    intro a b n hn
    suffices min (f a b) (n + 1) = f a b ∧ min (f a b) n = f a b by
      simp_rw [fs, this.1, this.2, tsub_self (f a b)]
    exact ⟨min_eq_left ((h_le a b n hn).trans (le_add_of_nonneg_right zero_le_one)),
      min_eq_left (h_le a b n hn)⟩
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
⊢ ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a

Tactic:
have h_sum_a : ∀ a, Summable fun n => fs n a :=
      fun _ => Pi.summable.mpr fun _ => ENNReal.summable
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
h : ∀ (a : α) (b : β), f a b = (∑' (n : ℕ), fs n) a b
⊢ f = ∑' (n : ℕ), fs n

Tactic:
ext a b : 2
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
h : f a b = Filter.liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, fs i a b) Filter.atTop
⊢ f a b = (∑' (n : ℕ), fs n) a b

Tactic:
rw [tsum_apply (Pi.summable.mpr h_sum_a), tsum_apply (h_sum_a a),
      ENNReal.tsum_eq_liminf_sum_nat]

Premises used: Iff.mpr, tsum_apply, Pi.summable, ENNReal.tsum_eq_liminf_sum_nat
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
⊢ ∑ i ∈ Finset.range 0, fs i a b = min (f a b) (↑0 : ℝ≥0∞)

Tactic:
simp
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
n : ℕ
hn : ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)
succ : min (f a b) (↑n : ℝ≥0∞) + fs n a b = min (f a b) (↑(n + 1) : ℝ≥0∞)
⊢ ∑ i ∈ Finset.range (n + 1), fs i a b = min (f a b) (↑(n + 1) : ℝ≥0∞)

Tactic:
rw [Finset.sum_range_succ, hn]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
n : ℕ
hn : ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)
⊢ min (f a b) (↑n : ℝ≥0∞) + fs n a b = min (f a b) (↑(n + 1) : ℝ≥0∞)

Tactic:
simp [fs]
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
n : ℕ
zero : ∑ i ∈ Finset.range 0, fs i a b = min (f a b) (↑0 : ℝ≥0∞)
succ :
  ∀ (n : ℕ) (hn : ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)),
    ∑ i ∈ Finset.range (n + 1), fs i a b = min (f a b) (↑(n + 1) : ℝ≥0∞)
⊢ ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)

Tactic:
induction n with
      | zero => simp
      | succ n hn =>
        rw [Finset.sum_range_succ, hn]
        simp [fs]

Premises used: Finset.sum_range_succ
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
⊢ ∀ (n : ℕ), ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)

Tactic:
have h_finsetSum : ∀ n, ∑ i ∈ Finset.range n, fs i a b = min (f a b) n := fun n ↦ by
      induction n with
      | zero => simp
      | succ n hn =>
        rw [Finset.sum_range_succ, hn]
        simp [fs]
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
h_finsetSum : ∀ (n : ℕ), ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)
h : f a b = Filter.liminf (fun (n : ℕ) ↦ min (f a b) (↑n : ℝ≥0∞)) Filter.atTop
⊢ f a b = Filter.liminf (fun (n : ℕ) ↦ ∑ i ∈ Finset.range n, fs i a b) Filter.atTop

Tactic:
simp_rw [h_finsetSum]
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
h_finsetSum : ∀ (n : ℕ), ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)
⊢ f a b = Filter.liminf (fun (n : ℕ) ↦ min (f a b) (↑n : ℝ≥0∞)) Filter.atTop

Tactic:
(Filter.Tendsto.liminf_eq ?_).symm

Premises used: Filter.Tendsto.liminf_eq, Eq.symm
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
h_finsetSum : ∀ (n : ℕ), ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)
h : Filter.Tendsto (fun (n : ℕ) ↦ min (f a b) (↑n : ℝ≥0∞)) Filter.atTop (nhds (f a b))
⊢ f a b = Filter.liminf (fun (n : ℕ) ↦ min (f a b) (↑n : ℝ≥0∞)) Filter.atTop

Tactic:
refine (Filter.Tendsto.liminf_eq ?_).symm

Premises used: Filter.Tendsto.liminf_eq, Eq.symm
-- Module: Mathlib.Probability.Kernel.WithDensity
Goal:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
f : α → β → ℝ≥0∞
κ : Kernel α β
inst : IsFiniteKernel κ
hf_ne_top : ∀ (a : α) (b : β), f a b ≠ ∞
hf : Measurable (Function.uncurry f)
fs : ℕ → α → β → ℝ≥0∞ :=
  fun (n : ℕ) (a : α) (b : β) ↦ min (f a b) (HAdd.hAdd (α := ℝ≥0∞) (↑n : ℝ≥0∞) 1) - min (f a b) (↑n : ℝ≥0∞)
h_le : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → f a b ≤ (↑n : ℝ≥0∞)
h_zero : ∀ (a : α) (b : β) (n : ℕ), ⌈(f a b).toReal⌉₊ ≤ n → fs n a b = 0
h_sum_a : ∀ (a : α), Summable.{u_2, 0} (α := β → ℝ≥0∞) fun (n : ℕ) ↦ fs n a
a : α
b : β
h_finsetSum : ∀ (n : ℕ), ∑ i ∈ Finset.range n, fs i a b = min (f a b) (↑n : ℝ≥0∞)
⊢ Filter.Tendsto (fun (n : ℕ) ↦ min (f a b) (↑n : ℝ≥0∞)) Filter.atTop (nhds (f a b))

Tactic:
Filter.Tendsto.congr' ?_ tendsto_const_nhds

Premises used: tendsto_const_nhds, Filter.Tendsto.congr'