awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
have : ∀ (h_ss : aeSeqSet hf p ⊆ {x : α | p x fun (n : ι) ↦ f n x}), p x fun (n : ι) ↦ f n x
⊢ p x fun (n : ι) ↦ f n x

Tactic:
have h_ss : aeSeqSet hf p ⊆ { x | p x fun n => f n x } := by
    rw [← compl_compl { x | p x fun n => f n x }, aeSeqSet, Set.compl_subset_compl]
    refine Set.Subset.trans (Set.compl_subset_compl.mpr ?_) (subset_toMeasurable _ _)
    exact fun x hx => hx.2
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
h_ss : aeSeqSet hf p ⊆ {x : α | p x fun (n : ι) ↦ f n x}
⊢ Membership.mem (γ := Set α) {x : α | p x fun (n : ι) ↦ f n x} x

Tactic:
have hx' := Set.mem_of_subset_of_mem h_ss hx
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
h_ss : aeSeqSet hf p ⊆ {x : α | p x fun (n : ι) ↦ f n x}
hx' : Membership.mem (γ := Set α) {x : α | p x fun (n : ι) ↦ f n x} x
⊢ p x fun (n : ι) ↦ f n x

Tactic:
hx'

Premises used: Set.Mem, setOf
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
h_ss : aeSeqSet hf p ⊆ {x : α | p x fun (n : ι) ↦ f n x}
hx' : Membership.mem (γ := Set α) {x : α | p x fun (n : ι) ↦ f n x} x
⊢ p x fun (n : ι) ↦ f n x

Tactic:
exact hx'
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
have : ∀ (h_eq : Eq (α := (n : ι) → β) (fun (n : ι) ↦ f n x) fun (n : ι) ↦ aeSeq hf p n x), p x fun (n : ι) ↦ f n x
⊢ p x fun (n : ι) ↦ f n x

Tactic:
have h_eq : (fun n => f n x) = fun n => aeSeq hf p n x :=
    funext fun n => (aeSeq_eq_fun_of_mem_aeSeqSet hf hx n).symm
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
h_eq : Eq (α := (n : ι) → β) (fun (n : ι) ↦ f n x) fun (n : ι) ↦ aeSeq hf p n x
rw : p x fun (n : ι) ↦ aeSeq hf p n x
⊢ p x fun (n : ι) ↦ f n x

Tactic:
rw [h_eq]
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
h_eq : Eq (α := (n : ι) → β) (fun (n : ι) ↦ f n x) fun (n : ι) ↦ aeSeq hf p n x
⊢ p x fun (n : ι) ↦ aeSeq hf p n x

Tactic:
prop_of_mem_aeSeqSet hf hx

Premises used: aeSeq.prop_of_mem_aeSeqSet
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
x : α
hx : x ∈ aeSeqSet hf p
h_eq : Eq (α := (n : ι) → β) (fun (n : ι) ↦ f n x) fun (n : ι) ↦ aeSeq hf p n x
⊢ p x fun (n : ι) ↦ aeSeq hf p n x

Tactic:
exact prop_of_mem_aeSeqSet hf hx

Premises used: aeSeq.prop_of_mem_aeSeqSet
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
hf : ∀ (i : ι), AEMeasurable (f i) μ
⊢ MeasurableSet (aeSeqSet hf p)

Tactic:
(measurableSet_toMeasurable _ _).compl

Premises used: MeasurableSet.compl, MeasureTheory.measurableSet_toMeasurable, aeSeqSet
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
hf : ∀ (i : ι), AEMeasurable (f i) μ
p : α → (ι → β) → Prop
i : ι
⊢ Measurable (aeSeq hf p i)

Tactic:
Measurable.ite aeSeqSet_measurableSet (hf i).measurable_mk <| measurable_const' fun _ _ => rfl

Premises used: aeSeq, Measurable.ite, measurable_const', aeSeq.aeSeqSet_measurableSet, rfl, AEMeasurable.measurable_mk
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
rw :
  Eq (α := ENNReal)
    ((μ : (a : Set α) → ENNReal) {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun (n : ι) ↦ f n x}ᶜ :
      ENNReal)
    (0 : ENNReal)
⊢ Eq (α := ENNReal) ((μ : (a : Set α) → ENNReal) (aeSeqSet hf p)ᶜ : ENNReal) (0 : ENNReal)

Tactic:
rw [aeSeqSet, compl_compl, measure_toMeasurable]

Premises used: compl_compl, MeasureTheory.measure_toMeasurable, aeSeqSet
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
⊢ ∀ (i : ι), f i =ᶠ[ae μ] AEMeasurable.mk (f i) ⋯

Tactic:
have hf_eq := fun i => (hf i).ae_eq_mk
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
hf_eq : ∀ (i : ι), f i =ᶠ[ae μ] AEMeasurable.mk (f i) ⋯
⊢ ∀ᵐ (a : α) ∂μ, ∀ (i : ι), f i a = AEMeasurable.mk (f i) ⋯ a

Tactic:
simp_rw [Filter.EventuallyEq, ← ae_all_iff] at hf_eq

Premises used: Filter.EventuallyEq, MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
hf_eq : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), f i a = AEMeasurable.mk (f i) ⋯ a
⊢ Eq (α := ENNReal)
    ((μ : (a : Set α) → ENNReal) {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun (n : ι) ↦ f n x}ᶜ :
      ENNReal)
    (0 : ENNReal)

Tactic:
Filter.Eventually.and hf_eq hp

Premises used: Set.Mem, Filter.Eventually, setOf, Filter.Eventually.and
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
hf_eq : ∀ᵐ (a : α) ∂μ, ∀ (i : ι), f i a = AEMeasurable.mk (f i) ⋯ a
⊢ Eq (α := ENNReal)
    ((μ : (a : Set α) → ENNReal) {x : α | (∀ (i : ι), f i x = AEMeasurable.mk (f i) ⋯ x) ∧ p x fun (n : ι) ↦ f n x}ᶜ :
      ENNReal)
    (0 : ENNReal)

Tactic:
exact Filter.Eventually.and hf_eq hp

Premises used: Filter.Eventually.and
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
x : α
hx : x ∈ aeSeqSet hf p
i : ι
⊢ aeSeq hf p i x = AEMeasurable.mk (f i) ⋯ x

Tactic:
simp only [aeSeq, hx, if_true]

Premises used: if_true, aeSeq
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
⊢ ∀ᵐ (a : α) ∂μ, ∀ (i : ι), aeSeq hf p i a = f i a

Tactic:
haveI h_ss : { a : α | ¬∀ i : ι, aeSeq hf p i a = f i a } ⊆ (aeSeqSet hf p)ᶜ := fun _ =>
    mt fun hx i => aeSeq_eq_fun_of_mem_aeSeqSet hf hx i
  measure_mono_null h_ss (measure_compl_aeSeqSet_eq_zero hf hp)

Premises used: Set.Mem, Filter.Eventually, setOf, mt, MeasureTheory.measure_mono_null, aeSeq.measure_compl_aeSeqSet_eq_zero, aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
n : ι
⊢ aeSeq hf p n =ᶠ[ae μ] f n

Tactic:
ae_all_iff.mp (aeSeq_eq_fun_ae hf hp) n

Premises used: Filter.EventuallyEq, aeSeq.aeSeq_eq_fun_ae, Iff.mp, MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : SupSet β
inst_3 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
simp_rw :
  Eq (α := ENNReal)
    ((μ : (a : Set α) → ENNReal) {a : α | ¬Eq.{u_3 + 1} (α := β) (⨆ (i : ι), aeSeq hf p i a) (⨆ (i : ι), f i a)} :
      ENNReal)
    (0 : ENNReal)
⊢ Filter.EventuallyEq.{u_2, u_3} (β := β) (ae μ) (⨆ (n : ι), aeSeq hf p n) (⨆ (n : ι), f n)

Tactic:
simp_rw [Filter.EventuallyEq, ae_iff, iSup_apply]

Premises used: Filter.EventuallyEq, MeasureTheory.ae_iff, iSup_apply
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : SupSet β
inst_3 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
x : α
hx : x ∈ aeSeqSet hf p
e_s : Eq (α := ι → β) (fun (i : ι) ↦ aeSeq hf p i x) fun (i : ι) ↦ f i x
⊢ Membership.mem (γ := Set α) {a : α | Eq.{u_3 + 1} (α := β) (⨆ (i : ι), aeSeq hf p i a) (⨆ (i : ι), f i a)} x

Tactic:
congr
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : SupSet β
inst_3 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
x : α
hx : x ∈ aeSeqSet hf p
⊢ Eq (α := ι → β) (fun (i : ι) ↦ aeSeq hf p i x) fun (i : ι) ↦ f i x

Tactic:
funext fun i => aeSeq_eq_fun_of_mem_aeSeqSet hf hx i

Premises used: funext, aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : SupSet β
inst_3 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
x : α
hx : x ∈ aeSeqSet hf p
⊢ Eq (α := ι → β) (fun (i : ι) ↦ aeSeq hf p i x) fun (i : ι) ↦ f i x

Tactic:
exact funext fun i => aeSeq_eq_fun_of_mem_aeSeqSet hf hx i

Premises used: funext, aeSeq.aeSeq_eq_fun_of_mem_aeSeqSet
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : SupSet β
inst_3 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
⊢ aeSeqSet hf p ⊆ {a : α | Eq.{u_3 + 1} (α := β) (⨆ (i : ι), aeSeq hf p i a) (⨆ (i : ι), f i a)}

Tactic:
have h_ss : aeSeqSet hf p ⊆ { a : α | ⨆ i : ι, aeSeq hf p i a = ⨆ i : ι, f i a } := by
    intro x hx
    congr
    exact funext fun i => aeSeq_eq_fun_of_mem_aeSeqSet hf hx i
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : SupSet β
inst_3 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
h_ss : aeSeqSet hf p ⊆ {a : α | Eq.{u_3 + 1} (α := β) (⨆ (i : ι), aeSeq hf p i a) (⨆ (i : ι), f i a)}
⊢ Eq (α := ENNReal)
    ((μ : (a : Set α) → ENNReal) {a : α | ¬Eq.{u_3 + 1} (α := β) (⨆ (i : ι), aeSeq hf p i a) (⨆ (i : ι), f i a)} :
      ENNReal)
    (0 : ENNReal)

Tactic:
measure_mono_null (Set.compl_subset_compl.mpr h_ss) (measure_compl_aeSeqSet_eq_zero hf hp)

Premises used: Iff.mpr, MeasureTheory.measure_mono_null, Set.compl_subset_compl, aeSeq.measure_compl_aeSeqSet_eq_zero
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : SupSet β
inst_3 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
h_ss : aeSeqSet hf p ⊆ {a : α | Eq.{u_3 + 1} (α := β) (⨆ (i : ι), aeSeq hf p i a) (⨆ (i : ι), f i a)}
⊢ Eq (α := ENNReal)
    ((μ : (a : Set α) → ENNReal) {a : α | ¬Eq.{u_3 + 1} (α := β) (⨆ (i : ι), aeSeq hf p i a) (⨆ (i : ι), f i a)} :
      ENNReal)
    (0 : ENNReal)

Tactic:
exact measure_mono_null (Set.compl_subset_compl.mpr h_ss) (measure_compl_aeSeqSet_eq_zero hf hp)

Premises used: Iff.mpr, MeasureTheory.measure_mono_null, Set.compl_subset_compl, aeSeq.measure_compl_aeSeqSet_eq_zero
-- Module: Mathlib.MeasureTheory.Function.AEMeasurableSequence
Goal:
ι : Sort u_1
α : Type u_2
β : Type u_3
inst : MeasurableSpace α
inst_1 : MeasurableSpace β
f : ι → α → β
μ : Measure α
p : α → (ι → β) → Prop
inst_2 : InfSet β
inst_3 : Countable ι
hf : ∀ (i : ι), AEMeasurable (f i) μ
hp : ∀ᵐ (x : α) ∂μ, p x fun (n : ι) ↦ f n x
⊢ Filter.EventuallyEq.{u_2, u_3} (β := β) (ae μ) (⨅ (n : ι), aeSeq hf p n) (⨅ (n : ι), f n)

Tactic:
iSup (β := βᵒᵈ) hf hp

Premises used: iInf, aeSeq.iSup, OrderDual
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
⊢ HasBasis.{u_1, 1} (α := ℕ × (ℕ → X × X))
    (comap (β := ℝ) (fun (E : ℕ × (ℕ → X × X)) ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) (𝓝 0))
    (fun (ε : ℝ) ↦ 0 < ε) fun (i : ℝ) ↦
    (fun (E : ℕ × (ℕ → X × X)) ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) ⁻¹' Ioo (0 - i) (0 + i)

Tactic:
Filter.HasBasis.comap (α := ℝ) _ (nhds_basis_Ioo_pos _)

Premises used: nhds_basis_Ioo_pos, Filter.HasBasis.comap
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
h :
  Eq.{u_1 + 1} (α := ℝ → Set (ℕ × (ℕ → X × X)))
    (fun (ε : ℝ) ↦ {E : ℕ × (ℕ → X × X) | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε}) fun (i : ℝ) ↦
    (fun (E : ℕ × (ℕ → X × X)) ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) ⁻¹' Ioo (0 - i) (0 + i)
⊢ HasBasis.{u_1, 1} (α := ℕ × (ℕ → X × X)) totalLengthFilter (fun (ε : ℝ) ↦ 0 < ε) fun (ε : ℝ) ↦
    {E : ℕ × (ℕ → X × X) | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε}

Tactic:
convert! Filter.HasBasis.comap (α := ℝ) _ (nhds_basis_Ioo_pos _) using 1

Premises used: nhds_basis_Ioo_pos, Filter.HasBasis.comap
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
h :
  ∀ (ε : ℝ) (E : ℕ × (ℕ → X × X)),
    Membership.mem (γ := Set (ℕ × (ℕ → X × X)))
        {E : ℕ × (ℕ → X × X) | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε} E ↔
      Membership.mem (γ := Set (ℕ × (ℕ → X × X)))
        ((fun (E : ℕ × (ℕ → X × X)) ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) ⁻¹' Ioo (0 - ε) (0 + ε)) E
⊢ Eq.{u_1 + 1} (α := ℝ → Set (ℕ × (ℕ → X × X)))
    (fun (ε : ℝ) ↦ {E : ℕ × (ℕ → X × X) | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε}) fun (i : ℝ) ↦
    (fun (E : ℕ × (ℕ → X × X)) ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) ⁻¹' Ioo (0 - i) (0 + i)

Tactic:
ext ε E
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
ε : ℝ
E : ℕ × (ℕ → X × X)
h : ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε → -ε < ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2
⊢ Membership.mem (γ := Set (ℕ × (ℕ → X × X)))
      {E : ℕ × (ℕ → X × X) | ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε} E ↔
    Membership.mem (γ := Set (ℕ × (ℕ → X × X)))
      ((fun (E : ℕ × (ℕ → X × X)) ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) ⁻¹' Ioo (0 - ε) (0 + ε)) E

Tactic:
simp only [mem_setOf_eq, zero_sub, zero_add, mem_preimage, mem_Ioo, iff_and_self]

Premises used: Set.mem_Ioo, Set.mem_setOf_eq, zero_add, iff_and_self, Set.mem_preimage, zero_sub
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
ε : ℝ
E : ℕ × (ℕ → X × X)
this : LE.le (α := ℝ) 0 (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)
⊢ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε → -ε < ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
ε : ℝ
E : ℕ × (ℕ → X × X)
h : LE.le (α := ℝ) 0 (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)
⊢ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 < ε → -ε < ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2

Tactic:
suffices 0 ≤ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2 by grind
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
ε : ℝ
E : ℕ × (ℕ → X × X)
⊢ LE.le (α := ℝ) 0 (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)

Tactic:
Finset.sum_nonneg (fun _ _ ↦ dist_nonneg)

Premises used: dist_nonneg, Finset.sum_nonneg
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
X : Type u_1
inst : PseudoMetricSpace X
ε : ℝ
E : ℕ × (ℕ → X × X)
⊢ LE.le (α := ℝ) 0 (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)

Tactic:
exact Finset.sum_nonneg (fun _ _ ↦ dist_nonneg)

Premises used: dist_nonneg, Finset.sum_nonneg
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
rw :
  {E : ℕ × (ℕ → ℝ × ℝ) |
      (∀ i ∈ Finset.range E.1, (E.2 i).1 ∈ uIcc a b ∧ (E.2 i).2 ∈ uIcc a b) ∧
        (↑(Finset.range E.1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (E.2 i).1 (E.2 i).2} =
    disjWithin b a
rw₁ :
  Eq (α := Set (ℕ × (ℕ → ℝ × ℝ)))
    {E : ℕ × (ℕ → ℝ × ℝ) |
      (∀ i ∈ Finset.range E.1, (E.2 i).1 ∈ uIcc a b ∧ (E.2 i).2 ∈ uIcc a b) ∧
        (↑(Finset.range E.1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (E.2 i).1 (E.2 i).2}
    {E : ℕ × (ℕ → ℝ × ℝ) |
      (∀ i ∈ Finset.range E.1, (E.2 i).1 ∈ uIcc b a ∧ (E.2 i).2 ∈ uIcc b a) ∧
        (↑(Finset.range E.1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (E.2 i).1 (E.2 i).2}
rw₂ rw₃ :
  Eq (α := Set (ℕ × (ℕ → ℝ × ℝ)))
    {E : ℕ × (ℕ → ℝ × ℝ) |
      (∀ i ∈ Finset.range E.1, (E.2 i).1 ∈ uIcc b a ∧ (E.2 i).2 ∈ uIcc b a) ∧
        (↑(Finset.range E.1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (E.2 i).1 (E.2 i).2}
    {E : ℕ × (ℕ → ℝ × ℝ) |
      (∀ i ∈ Finset.range E.1, (E.2 i).1 ∈ uIcc b a ∧ (E.2 i).2 ∈ uIcc b a) ∧
        (↑(Finset.range E.1) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (E.2 i).1 (E.2 i).2}
⊢ disjWithin a b = disjWithin b a

Tactic:
rw [disjWithin, disjWithin, uIcc_comm]

Premises used: Set.uIcc_comm, AbsolutelyContinuousOnInterval.disjWithin
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b c d : ℝ
habcd : uIcc c d ⊆ uIcc a b
⊢ disjWithin c d ⊆ disjWithin a b

Tactic:
grind [disjWithin]

Premises used: AbsolutelyContinuousOnInterval.disjWithin
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
i : ℕ
hi : i < n
⊢ (∀ i < n, (min a b ≤ (I i).1 ∧ (I i).1 ≤ max a b) ∧ min a b ≤ (I i).2 ∧ (I i).2 ≤ max a b) ∧
    (↑(Finset.range n) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (I i).1 (I i).2

Tactic:
simp only [disjWithin, Finset.mem_range, mem_setOf_eq, uIcc, mem_Icc] at hnI

Premises used: Set.mem_setOf_eq, Finset.mem_range, AbsolutelyContinuousOnInterval.disjWithin, Set.mem_Icc, Set.uIcc
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
n : ℕ
I : ℕ → ℝ × ℝ
i : ℕ
hi : i < n
hnI :
  (∀ i < n, (min a b ≤ (I i).1 ∧ (I i).1 ≤ max a b) ∧ min a b ≤ (I i).2 ∧ (I i).2 ≤ max a b) ∧
    (↑(Finset.range n) : Set ℕ).PairwiseDisjoint (α := Set ℝ) fun (i : ℕ) ↦ uIoc (I i).1 (I i).2
⊢ uIoc (I i).1 (I i).2 ⊆ uIoc a b

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
simp : ∀ (i : ℕ) (i_1 : i < n), uIoc (I i).1 (I i).2 ⊆ uIoc a b
⊢ ⋃ i ∈ Finset.range n, uIoc (I i).1 (I i).2 ⊆ uIoc a b

Tactic:
simp only [iUnion_subset_iff, Finset.mem_range]

Premises used: Set.iUnion_subset_iff, Finset.mem_range
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
⊢ ∀ (i : ℕ) (i_1 : i < n), uIoc (I i).1 (I i).2 ⊆ uIoc a b

Tactic:
fun i hi ↦ uIoc_subset_of_mem_disjWithin hnI hi

Premises used: AbsolutelyContinuousOnInterval.uIoc_subset_of_mem_disjWithin
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
a b : ℝ
n : ℕ
I : ℕ → ℝ × ℝ
hnI : (n, I) ∈ disjWithin a b
⊢ ∀ (i : ℕ) (i_1 : i < n), uIoc (I i).1 (I i).2 ⊆ uIoc a b

Tactic:
exact fun i hi ↦ uIoc_subset_of_mem_disjWithin hnI hi

Premises used: AbsolutelyContinuousOnInterval.uIoc_subset_of_mem_disjWithin
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
hh :
  Tendsto (β := ENNReal) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2))
    totalLengthFilter (𝓝 0)
hgf :
  LE.le (α := ℕ × (ℕ → ℝ × ℝ) → ENNReal) (fun (x : ℕ × (ℕ → ℝ × ℝ)) ↦ 0) fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦
    (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2)
hfh :
  LE.le (α := ℕ × (ℕ → ℝ × ℝ) → ENNReal)
    (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
    fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2)
⊢ Tendsto (β := ENNReal)
    (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ (volume : (a : Set ℝ) → ENNReal) (⋃ i ∈ Finset.range E.1, uIoc (E.2 i).1 (E.2 i).2))
    totalLengthFilter (𝓝 0)

Tactic:
apply tendsto_of_tendsto_of_tendsto_of_le_of_le tendsto_const_nhds
    (h := fun E ↦ ENNReal.ofReal (∑ i ∈ Finset.range E.1, (dist (E.2 i).1 (E.2 i).2)))

Premises used: tendsto_of_tendsto_of_tendsto_of_le_of_le, tendsto_const_nhds
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
⊢ Tendsto (fun (a : ℕ × (ℕ → ℝ × ℝ)) ↦ ENNReal.ofReal (∑ i ∈ Finset.range a.1, dist (a.2 i).1 (a.2 i).2))
    (comap (β := ℝ) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2) (𝓝 0))
    (𝓝 (ENNReal.ofReal 0))

Tactic:
ENNReal.tendsto_ofReal (Filter.tendsto_comap)

Premises used: Filter.tendsto_comap, ENNReal.tendsto_ofReal
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
h : 0 = ENNReal.ofReal 0
⊢ Tendsto (β := ENNReal) (fun (E : ℕ × (ℕ → ℝ × ℝ)) ↦ ENNReal.ofReal (∑ i ∈ Finset.range E.1, dist (E.2 i).1 (E.2 i).2))
    totalLengthFilter (𝓝 0)

Tactic:
convert! ENNReal.tendsto_ofReal (Filter.tendsto_comap)

Premises used: Filter.tendsto_comap, ENNReal.tendsto_ofReal
-- Module: Mathlib.MeasureTheory.Function.AbsolutelyContinuous
Goal:
⊢ 0 = ENNReal.ofReal 0

Tactic:
simp