awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
t : Set α
ht : MeasurableSet t
pos :
  ∀ (hμt : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞)
        ((μ.toFinite : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞)
neg :
  ∀ (hμt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)),
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞) =
      HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞)
        ((μ.toFinite : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞)
      ((μ.toFinite : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞)

Tactic:
by_cases hμt : μ (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) = 0

Premises used: MeasureTheory.Measure.sigmaFiniteSetWRT, Compl.compl, Inter.inter, DFunLike.coe
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
t : Set α
ht : MeasurableSet t
hμt : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
pos :
  HMul.hMul (α := ℝ≥0∞) ∞ 0 =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞)
      ((μ.toFinite : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞)
pos₁ pos₂ : HMul.hMul (α := ℝ≥0∞) ∞ 0 = HMul.hMul (α := ℝ≥0∞) ∞ 0
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞)
      ((μ.toFinite : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞)

Tactic:
rw [hμt, toFinite_absolutelyContinuous μ hμt]

Premises used: MeasureTheory.toFinite_absolutelyContinuous
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
t : Set α
ht : MeasurableSet t
hμt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
neg : Ne (α := ℝ≥0∞) ((μ.toFinite : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞) =
    HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (∞ : ℝ≥0∞)
      ((μ.toFinite : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞)

Tactic:
rw [ENNReal.top_mul hμt, ENNReal.top_mul]

Premises used: ENNReal.top_mul
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
t : Set α
ht : MeasurableSet t
hμt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ.toFinite : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
fun h ↦ hμt (absolutelyContinuous_toFinite μ h)

Premises used: MeasureTheory.absolutelyContinuous_toFinite, Not
-- Module: Mathlib.MeasureTheory.Measure.WithDensityFinite
Goal:
α : Type u_1
mα : MeasurableSpace α
μ : Measure α
inst : SFinite μ
t : Set α
ht : MeasurableSet t
hμt : ¬Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Ne (α := ℝ≥0∞) ((μ.toFinite : (a : Set α) → ℝ≥0∞) (t ∩ (μ.sigmaFiniteSetWRT μ)ᶜ) : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact fun h ↦ hμt (absolutelyContinuous_toFinite μ h)

Premises used: MeasureTheory.absolutelyContinuous_toFinite
-- Module: Mathlib.MeasureTheory.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MeasurableSpace α
inst_3 : MeasurableSup α
⊢ Measurable.{u_1, u_1} (α := α) oneLePart

Tactic:
measurable_sup_const _

Premises used: MeasurableSup.measurable_sup_const
-- Module: Mathlib.MeasureTheory.Order.Group.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Lattice α
inst_1 : Group α
inst_2 : MeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
inst_4 : MeasurableSup α
hf : Measurable f
⊢ Measurable.{u_2, u_1} (β := α) fun (x : β) ↦ (f x)⁺ᵐ

Tactic:
measurable_oneLePart.comp hf

Premises used: Measurable.comp, measurable_oneLePart
-- Module: Mathlib.MeasureTheory.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MeasurableSpace α
inst_3 : MeasurableInv α
inst_4 : MeasurableSup α
⊢ Measurable.{u_1, u_1} (α := α) leOnePart

Tactic:
(measurable_sup_const _).comp measurable_inv

Premises used: Measurable.comp, MeasurableInv.measurable_inv, MeasurableSup.measurable_sup_const
-- Module: Mathlib.MeasureTheory.Order.Group.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Lattice α
inst_1 : Group α
inst_2 : MeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
inst_4 : MeasurableInv α
inst_5 : MeasurableSup α
hf : Measurable f
⊢ Measurable.{u_2, u_1} (β := α) fun (x : β) ↦ (f x)⁻ᵐ

Tactic:
measurable_leOnePart.comp hf

Premises used: Measurable.comp, measurable_leOnePart
-- Module: Mathlib.MeasureTheory.Order.Group.Lattice
Goal:
α : Type u_1
inst : Lattice α
inst_1 : Group α
inst_2 : MeasurableSpace α
inst_3 : MeasurableInv α
inst_4 : MeasurableSup₂ α
⊢ Measurable.{u_1, u_1} (α := α) mabs

Tactic:
measurable_id'.sup measurable_inv

Premises used: MeasurableInv.measurable_inv, Measurable.sup, measurable_id', mabs
-- Module: Mathlib.MeasureTheory.Order.Group.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Lattice α
inst_1 : Group α
inst_2 : MeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
inst_4 : MeasurableInv α
inst_5 : MeasurableSup₂ α
hf : Measurable f
⊢ Measurable.{u_2, u_1} (β := α) fun (x : β) ↦ |f x|ₘ

Tactic:
measurable_mabs.comp hf

Premises used: Measurable.comp, measurable_mabs, mabs
-- Module: Mathlib.MeasureTheory.Order.Group.Lattice
Goal:
α : Type u_1
β : Type u_2
inst : Lattice α
inst_1 : Group α
inst_2 : MeasurableSpace α
inst_3 : MeasurableSpace β
f : β → α
inst_4 : MeasurableInv α
inst_5 : MeasurableSup₂ α
μ : MeasureTheory.Measure β
hf : AEMeasurable f μ
⊢ AEMeasurable.{u_2, u_1} (β := α) (fun (x : β) ↦ |f x|ₘ) μ

Tactic:
measurable_mabs.comp_aemeasurable hf

Premises used: Measurable.comp_aemeasurable, measurable_mabs, mabs
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
inst_1 : Min M
inst_2 : MeasurableInf M
⊢ MeasurableSup.{u_1} Mᵒᵈ

Tactic:
⟨@measurable_const_inf M _ _ _, @measurable_inf_const M _ _ _⟩

Premises used: MeasurableInf.measurable_inf_const, MeasurableSup.mk, MeasurableInf.measurable_const_inf
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
inst_1 : Max M
inst_2 : MeasurableSup M
⊢ MeasurableInf.{u_1} Mᵒᵈ

Tactic:
⟨@measurable_const_sup M _ _ _, @measurable_sup_const M _ _ _⟩

Premises used: MeasurableSup.measurable_const_sup, MeasurableInf.mk, MeasurableSup.measurable_sup_const
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
inst_1 : Min M
inst_2 : MeasurableInf₂ M
⊢ MeasurableSup₂.{u_1} Mᵒᵈ

Tactic:
⟨@measurable_inf M _ _ _⟩

Premises used: MeasurableInf₂.measurable_inf, MeasurableSup₂.mk
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
inst_1 : Max M
inst_2 : MeasurableSup₂ M
⊢ MeasurableInf₂.{u_1} Mᵒᵈ

Tactic:
⟨@measurable_sup M _ _ _⟩

Premises used: MeasurableSup₂.measurable_sup, MeasurableInf₂.mk
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
f : α → M
inst_1 : Max M
inst_2 : MeasurableSup M
hf : Measurable f
c : M
⊢ Measurable.{u_2, u_1} (β := M) fun (x : α) ↦ c ⊔ f x

Tactic:
(measurable_const_sup c).comp hf

Premises used: MeasurableSup.measurable_const_sup, Measurable.comp
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → M
inst_1 : Max M
inst_2 : MeasurableSup M
hf : AEMeasurable f μ
c : M
⊢ AEMeasurable.{u_2, u_1} (β := M) (fun (x : α) ↦ c ⊔ f x) μ

Tactic:
(MeasurableSup.measurable_const_sup c).comp_aemeasurable hf

Premises used: MeasurableSup.measurable_const_sup, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
f : α → M
inst_1 : Max M
inst_2 : MeasurableSup M
hf : Measurable f
c : M
⊢ Measurable.{u_2, u_1} (β := M) fun (x : α) ↦ f x ⊔ c

Tactic:
(measurable_sup_const c).comp hf

Premises used: Measurable.comp, MeasurableSup.measurable_sup_const
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → M
inst_1 : Max M
inst_2 : MeasurableSup M
hf : AEMeasurable f μ
c : M
⊢ AEMeasurable.{u_2, u_1} (β := M) (fun (x : α) ↦ f x ⊔ c) μ

Tactic:
(measurable_sup_const c).comp_aemeasurable hf

Premises used: MeasurableSup.measurable_sup_const, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
f g : α → M
inst_1 : Max M
inst_2 : MeasurableSup₂ M
hf : Measurable f
hg : Measurable g
⊢ Measurable (f ⊔ g)

Tactic:
measurable_sup.comp (hf.prodMk hg)

Premises used: Measurable.comp, MeasurableSup₂.measurable_sup, Measurable.prodMk
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
f g : α → M
inst_1 : Max M
inst_2 : MeasurableSup₂ M
hf : Measurable f
hg : Measurable g
⊢ Measurable.{u_2, u_1} (β := M) fun (a : α) ↦ f a ⊔ g a

Tactic:
measurable_sup.comp (hf.prodMk hg)

Premises used: Measurable.comp, MeasurableSup₂.measurable_sup, Measurable.prodMk
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f g : α → M
inst_1 : Max M
inst_2 : MeasurableSup₂ M
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable (f ⊔ g) μ

Tactic:
measurable_sup.comp_aemeasurable (hf.prodMk hg)

Premises used: MeasurableSup₂.measurable_sup, AEMeasurable.prodMk, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f g : α → M
inst_1 : Max M
inst_2 : MeasurableSup₂ M
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable.{u_2, u_1} (β := M) (fun (a : α) ↦ f a ⊔ g a) μ

Tactic:
measurable_sup.comp_aemeasurable (hf.prodMk hg)

Premises used: MeasurableSup₂.measurable_sup, AEMeasurable.prodMk, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
f : α → M
inst_1 : Min M
inst_2 : MeasurableInf M
hf : Measurable f
c : M
⊢ Measurable.{u_2, u_1} (β := M) fun (x : α) ↦ c ⊓ f x

Tactic:
(measurable_const_inf c).comp hf

Premises used: Measurable.comp, MeasurableInf.measurable_const_inf
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → M
inst_1 : Min M
inst_2 : MeasurableInf M
hf : AEMeasurable f μ
c : M
⊢ AEMeasurable.{u_2, u_1} (β := M) (fun (x : α) ↦ c ⊓ f x) μ

Tactic:
(MeasurableInf.measurable_const_inf c).comp_aemeasurable hf

Premises used: MeasurableInf.measurable_const_inf, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
f : α → M
inst_1 : Min M
inst_2 : MeasurableInf M
hf : Measurable f
c : M
⊢ Measurable.{u_2, u_1} (β := M) fun (x : α) ↦ f x ⊓ c

Tactic:
(measurable_inf_const c).comp hf

Premises used: Measurable.comp, MeasurableInf.measurable_inf_const
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f : α → M
inst_1 : Min M
inst_2 : MeasurableInf M
hf : AEMeasurable f μ
c : M
⊢ AEMeasurable.{u_2, u_1} (β := M) (fun (x : α) ↦ f x ⊓ c) μ

Tactic:
(measurable_inf_const c).comp_aemeasurable hf

Premises used: MeasurableInf.measurable_inf_const, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
f g : α → M
inst_1 : Min M
inst_2 : MeasurableInf₂ M
hf : Measurable f
hg : Measurable g
⊢ Measurable (f ⊓ g)

Tactic:
measurable_inf.comp (hf.prodMk hg)

Premises used: Measurable.comp, Measurable.prodMk, MeasurableInf₂.measurable_inf
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
f g : α → M
inst_1 : Min M
inst_2 : MeasurableInf₂ M
hf : Measurable f
hg : Measurable g
⊢ Measurable.{u_2, u_1} (β := M) fun (a : α) ↦ f a ⊓ g a

Tactic:
measurable_inf.comp (hf.prodMk hg)

Premises used: Measurable.comp, Measurable.prodMk, MeasurableInf₂.measurable_inf
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f g : α → M
inst_1 : Min M
inst_2 : MeasurableInf₂ M
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable (f ⊓ g) μ

Tactic:
measurable_inf.comp_aemeasurable (hf.prodMk hg)

Premises used: MeasurableInf₂.measurable_inf, AEMeasurable.prodMk, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
M : Type u_1
inst : MeasurableSpace M
α : Type u_2
m : MeasurableSpace α
μ : Measure α
f g : α → M
inst_1 : Min M
inst_2 : MeasurableInf₂ M
hf : AEMeasurable f μ
hg : AEMeasurable g μ
⊢ AEMeasurable.{u_2, u_1} (β := M) (fun (a : α) ↦ f a ⊓ g a) μ

Tactic:
measurable_inf.comp_aemeasurable (hf.prodMk hg)

Premises used: MeasurableInf₂.measurable_inf, AEMeasurable.prodMk, Measurable.comp_aemeasurable
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst : MeasurableSpace δ
inst_1 : SemilatticeSup α
inst_2 : MeasurableSup₂ α
ι : Type u_4
s : Finset ι
hs : s.Nonempty
f : ι → δ → α
hf : ∀ n ∈ s, Measurable (f n)
⊢ Measurable (s.sup' hs f)

Tactic:
Finset.sup'_induction hs _ (fun _f hf _g hg => hf.sup hg) fun n hn => hf n hn

Premises used: Measurable.sup, Finset.sup'_induction
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst : MeasurableSpace δ
inst_1 : SemilatticeSup α
inst_2 : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k ≤ n, Measurable (f k)
⊢ Measurable ((range (n + 1)).sup' ⋯ f)

Tactic:
Finset.measurable_sup' _ ?_

Premises used: Finset.measurable_sup'
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst : MeasurableSpace δ
inst_1 : SemilatticeSup α
inst_2 : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k ≤ n, Measurable (f k)
refine : ∀ n_1 ∈ range (n + 1), Measurable (f n_1)
⊢ Measurable ((range (n + 1)).sup' ⋯ f)

Tactic:
refine Finset.measurable_sup' _ ?_

Premises used: Finset.measurable_sup'
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst : MeasurableSpace δ
inst_1 : SemilatticeSup α
inst_2 : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k ≤ n, Measurable (f k)
⊢ ∀ n_1 ∈ range (n + 1), Measurable (f n_1)

Tactic:
simpa [Finset.mem_range]

Premises used: Finset.mem_range
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst : MeasurableSpace δ
inst_1 : SemilatticeSup α
inst_2 : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k ≤ n, Measurable (f k)
⊢ Measurable ((range (n + 1)).sup' ⋯ f)

Tactic:
Finset.measurable_range_sup' hf

Premises used: Finset.measurable_range_sup'
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst : MeasurableSpace δ
inst_1 : SemilatticeSup α
inst_2 : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k ≤ n, Measurable (f k)
h : (fun (x : δ) ↦ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k x) = (range (n + 1)).sup' ⋯ f
⊢ Measurable.{u_3, u_2} (β := α) fun (x : δ) ↦ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k x

Tactic:
convert! Finset.measurable_range_sup' hf using 1

Premises used: Finset.measurable_range_sup'
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst : MeasurableSpace δ
inst_1 : SemilatticeSup α
inst_2 : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k ≤ n, Measurable (f k)
h : ∀ (x : δ), ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k x) = (range (n + 1)).sup' ⋯ f x
⊢ (fun (x : δ) ↦ (range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k x) = (range (n + 1)).sup' ⋯ f

Tactic:
ext x
-- Module: Mathlib.MeasureTheory.Order.Lattice
Goal:
α : Type u_2
m : MeasurableSpace α
δ : Type u_3
inst : MeasurableSpace δ
inst_1 : SemilatticeSup α
inst_2 : MeasurableSup₂ α
f : ℕ → δ → α
n : ℕ
hf : ∀ k ≤ n, Measurable (f k)
x : δ
⊢ ((range (n + 1)).sup' ⋯ fun (k : ℕ) ↦ f k x) = (range (n + 1)).sup' ⋯ f x

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
h : ∀ (δ : ℝ), 0 < δ → ∃ (y : ι → ℝ), closedBall y (δ / 4) ⊆ closedBall x δ ∧ closedBall y (δ / 4) ⊆ interior s
choose :
  ∀ (f : (δ : ℝ) → 0 < δ → ι → ℝ) (hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ)
    (hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s),
    ¬Tendsto (β := ENNReal)
        (fun (r : ℝ) ↦
          HDiv.hDiv (α := ENNReal) (β := ENNReal)
            (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
            (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
        (𝓝[>] 0) (𝓝 0)
⊢ ¬Tendsto (β := ENNReal)
      (fun (r : ℝ) ↦
        HDiv.hDiv (α := ENNReal) (β := ENNReal)
          (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
          (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
      (𝓝[>] 0) (𝓝 0)

Tactic:
choose f hf₀ hf₁ using h
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 0)
obtain : ∀ (ε : ℕ → ℝ) (hε' : ∀ (n : ℕ), 0 < ε n) (hε₀ : Tendsto ε atTop (𝓝[>] 0)), False
⊢ False

Tactic:
obtain ⟨ε, -, hε', hε₀⟩ := exists_seq_strictAnti_tendsto_nhdsWithin (0 : ℝ)

Premises used: exists_seq_strictAnti_tendsto_nhdsWithin, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 0)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
⊢ False

Tactic:
not_eventually.2
    (Frequently.of_forall fun _ ↦ lt_irrefl <| ENNReal.ofReal <| 4⁻¹ ^ Fintype.card ι)
    ((Filter.Tendsto.eventually_lt (H.comp hε₀) tendsto_const_nhds ?_).mono fun n ↦
      lt_of_le_of_lt ?_)

Premises used: Iff.mpr, lt_of_le_of_lt, lt_irrefl, Filter.Frequently.of_forall, ENNReal.ofReal, tendsto_const_nhds, Fintype.card, Filter.Eventually.mono, Inv.inv, HPow.hPow, Filter.Tendsto.eventually_lt, Filter.not_eventually, Filter.Tendsto.comp, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 0)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
refine_1 : 0 < ENNReal.ofReal (HPow.hPow (α := ℝ) 4⁻¹ (Fintype.card ι))
refine_2 :
  ∀ (n : ℕ),
    ENNReal.ofReal (HPow.hPow (α := ℝ) 4⁻¹ (Fintype.card ι)) ≤
      ((fun (r : ℝ) ↦
            HDiv.hDiv (α := ENNReal) (β := ENNReal)
              (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
              (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal)) ∘
          ε)
        n
⊢ False

Tactic:
refine not_eventually.2
    (Frequently.of_forall fun _ ↦ lt_irrefl <| ENNReal.ofReal <| 4⁻¹ ^ Fintype.card ι)
    ((Filter.Tendsto.eventually_lt (H.comp hε₀) tendsto_const_nhds ?_).mono fun n ↦
      lt_of_le_of_lt ?_)

Premises used: Iff.mpr, lt_of_le_of_lt, lt_irrefl, Filter.Frequently.of_forall, ENNReal.ofReal, tendsto_const_nhds, Fintype.card, Filter.Eventually.mono, Inv.inv, HPow.hPow, Filter.Tendsto.eventually_lt, Filter.not_eventually, Filter.Tendsto.comp, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 0)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
⊢ ENNReal.ofReal (HPow.hPow (α := ℝ) 4⁻¹ (Fintype.card ι)) =
    HDiv.hDiv (α := ENNReal) (β := ENNReal)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall (f (ε n) ⋯) (ε n / 4)) : ENNReal)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x (ε n)) : ENNReal)

Tactic:
?_
-- Module: Mathlib.MeasureTheory.Order.UpperLower
Goal:
ι : Type u_1
inst : Fintype ι
s : Set (ι → ℝ)
x : ι → ℝ
f : (δ : ℝ) → 0 < δ → ι → ℝ
hf₀ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ closedBall x δ
hf₁ : ∀ (δ : ℝ) (a : 0 < δ), closedBall (f δ a) (δ / 4) ⊆ interior s
H :
  Tendsto (β := ENNReal)
    (fun (r : ℝ) ↦
      HDiv.hDiv (α := ENNReal) (β := ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x r) : ENNReal)
        (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x r) : ENNReal))
    (𝓝[>] 0) (𝓝 0)
ε : ℕ → ℝ
hε' : ∀ (n : ℕ), 0 < ε n
hε₀ : Tendsto ε atTop (𝓝[>] 0)
n : ℕ
hab : closedBall (f (ε n) ⋯) (ε n / 4) ⊆ closure s ∩ closedBall x (ε n)
⊢ HDiv.hDiv (α := ENNReal) (β := ENNReal)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall (f (ε n) ⋯) (ε n / 4)) : ENNReal)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x (ε n)) : ENNReal) ≤
    HDiv.hDiv (α := ENNReal) (β := ENNReal)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closure s ∩ closedBall x (ε n)) : ENNReal)
      (((volume : Measure (ι → ℝ)) : (a : Set (ι → ℝ)) → ENNReal) (closedBall x (ε n)) : ENNReal)

Tactic:
gcongr