awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε = ∞
h1 : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)}) l (𝓝 0)
n : ι
pos :
  LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ∞ ≤ edist (f n x) (g x)} : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)} : ℝ≥0∞)
⊢ LE.le (α := (fun (a : ι) ↦ ℝ≥0∞) n)
    ((fun (i : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞)) n)
    ((fun (n : ι) ↦ ((μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)} : ℝ≥0∞)) n)

Tactic:
simp only [hε_top]
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε = ∞
h1 : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)}) l (𝓝 0)
n : ι
pos : ∀ (a : α), LE.le (α := ℝ≥0∞) 1 ∞
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ∞ ≤ edist (f n x) (g x)} : ℝ≥0∞)
    ((μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)} : ℝ≥0∞)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε = ∞
h1 : Tendsto (β := ℝ≥0∞) (fun (n : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {ω : α | 1 ≤ edist (f n ω) (g ω)}) l (𝓝 0)
n : ι
a : α
⊢ LE.le (α := ℝ≥0∞) 1 ∞

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ¬ε = ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
h ε hε hε_top
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ¬ε = ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
exact h ε hε hε_top
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddCommGroup E
l : Filter ι
f : ι → α → E
g : α → E
simp_rw :
  TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ≥0∞),
      0 < ε →
        ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ≥0∞),
      0 < ε → ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)

Tactic:
simp_rw [← edist_eq_enorm_sub]

Premises used: edist_eq_enorm_sub
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddCommGroup E
l : Filter ι
f : ι → α → E
g : α → E
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ≥0∞),
      0 < ε →
        ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
⟨fun h ε hε hε_top ↦ h ε hε, tendstoInMeasure_of_ne_top⟩

Premises used: MeasureTheory.tendstoInMeasure_of_ne_top, Iff.intro
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddCommGroup E
l : Filter ι
f : ι → α → E
g : α → E
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ≥0∞),
      0 < ε →
        ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
exact ⟨fun h ε hε hε_top ↦ h ε hε, tendstoInMeasure_of_ne_top⟩
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
l : Filter ι
f : ι → α → E
g : α → E
rw :
  (∀ (ε : ℝ≥0∞),
      0 < ε →
        ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)) ↔
    ∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)

Tactic:
rw [tendstoInMeasure_iff_enorm]

Premises used: MeasureTheory.tendstoInMeasure_iff_enorm
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
l : Filter ι
f : ι → α → E
g : α → E
a :
  ∀ (ε : ℝ≥0∞) (hε : 0 < ε) (hε_top : ε ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0) ↔
      Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)
⊢ (∀ (ε : ℝ≥0∞),
      0 < ε →
        ε ≠ ∞ → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)) ↔
    ∀ (ε : ℝ≥0∞), 0 < ε → ε ≠ ∞ → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ ‖f i x - g x‖ₑ}) l (𝓝 0)

Tactic:
congr! with ε hε hε_top
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ),
      0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)

Tactic:
⟨fun h ε hε ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
refine_1 :
  ∀ (h : TendstoInMeasure μ f l g) (ε : ℝ) (hε : 0 < ε),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
refine_2 :
  ∀
    (h :
      ∀ (ε : ℝ),
        0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)),
    TendstoInMeasure μ f l g
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ),
      0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)

Tactic:
refine ⟨fun h ε hε ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ENNReal.ofReal ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
h (ENNReal.ofReal ε) (ENNReal.ofReal_pos.mpr hε)

Premises used: Iff.mpr, ENNReal.ofReal, ENNReal.ofReal_pos
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
h₁ : ∀ (i : ι) (a : α), ε ≤ dist (f i a) (g a) ↔ ENNReal.ofReal ε ≤ edist (f i a) (g a)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)

Tactic:
convert! h (ENNReal.ofReal ε) (ENNReal.ofReal_pos.mpr hε) with i a

Premises used: Iff.mpr, ENNReal.ofReal, ENNReal.ofReal_pos
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
a : α
⊢ 0 ≤ dist (f i a) (g a)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
a : α
h₁ : ε ≤ dist (f i a) (g a) ↔ ENNReal.ofReal ε ≤ ENNReal.ofReal (dist (f i a) (g a))
h₂ h₃ : ε ≤ dist (f i a) (g a) ↔ ε ≤ dist (f i a) (g a)
⊢ ε ≤ dist (f i a) (g a) ↔ ENNReal.ofReal ε ≤ edist (f i a) (g a)

Tactic:
rw [edist_dist, ENNReal.ofReal_le_ofReal_iff (by positivity)]

Premises used: ENNReal.ofReal_le_ofReal_iff, edist_dist
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ),
    0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
tendstoInMeasure_of_ne_top fun ε hε hε_top ↦ ?_

Premises used: MeasureTheory.tendstoInMeasure_of_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ),
    0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
refine_2 :
  ∀ (ε : ℝ≥0∞) (hε : 0 < ε) (hε_top : ε ≠ ∞),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
⊢ TendstoInMeasure μ f l g

Tactic:
refine tendstoInMeasure_of_ne_top fun ε hε hε_top ↦ ?_

Premises used: MeasureTheory.tendstoInMeasure_of_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ),
    0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε.toReal ≤ dist (f i x) (g x)}) l (𝓝 0)

Tactic:
h ε.toReal (ENNReal.toReal_pos hε.ne' hε_top)

Premises used: ENNReal.toReal_pos, LT.lt.ne', ENNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ),
    0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
h₁ : ∀ (i : ι) (a : α), ε ≤ edist (f i a) (g a) ↔ ε.toReal ≤ dist (f i a) (g a)
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
convert! h ε.toReal (ENNReal.toReal_pos hε.ne' hε_top) with i a

Premises used: ENNReal.toReal_pos, LT.lt.ne', ENNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ),
    0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
i : ι
a : α
⊢ 0 ≤ dist (f i a) (g a)

Tactic:
positivity
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
f : ι → α → E
l : Filter ι
g : α → E
h :
  ∀ (ε : ℝ),
    0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
hε_top : ε ≠ ∞
i : ι
a : α
h₁ : ε ≤ ENNReal.ofReal (dist (f i a) (g a)) ↔ ε.toReal ≤ dist (f i a) (g a)
h₂ h₃ : ε.toReal ≤ dist (f i a) (g a) ↔ ε.toReal ≤ dist (f i a) (g a)
⊢ ε ≤ edist (f i a) (g a) ↔ ε.toReal ≤ dist (f i a) (g a)

Tactic:
rw [edist_dist, ENNReal.le_ofReal_iff_toReal_le hε_top (by positivity)]

Premises used: edist_dist, ENNReal.le_ofReal_iff_toReal_le
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
rw :
  (∀ (ε : ℝ),
      0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)) ↔
    ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)

Tactic:
rw [tendstoInMeasure_iff_dist]

Premises used: MeasureTheory.tendstoInMeasure_iff_dist
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : PseudoMetricSpace E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
a :
  ∀ (ε : ℝ) (hε : 0 < ε),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0) ↔
      Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)
⊢ (∀ (ε : ℝ),
      0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)) ↔
    ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)

Tactic:
congr! with ε hε hε_top
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddCommGroup E
l : Filter ι
f : ι → α → E
g : α → E
simp_rw :
  (∀ (ε : ℝ),
      0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ dist (f i x) (g x)}) l (𝓝 0)) ↔
    ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0)
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0)

Tactic:
simp_rw [tendstoInMeasure_iff_dist, dist_eq_norm_sub]

Premises used: dist_eq_norm_sub, MeasureTheory.tendstoInMeasure_iff_dist
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
l : Filter ι
f : ι → α → E
g : α → E
rw :
  (∀ (ε : ℝ),
      0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0)) ↔
    ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0)
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0)

Tactic:
rw [tendstoInMeasure_iff_norm]

Premises used: MeasureTheory.tendstoInMeasure_iff_norm
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : SeminormedAddCommGroup E
inst_1 : IsFiniteMeasure μ
l : Filter ι
f : ι → α → E
g : α → E
a :
  ∀ (ε : ℝ) (hε : 0 < ε),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0) ↔
      Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0)
⊢ (∀ (ε : ℝ),
      0 < ε → Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0)) ↔
    ∀ (ε : ℝ), 0 < ε → Tendsto (β := ℝ) (fun (i : ι) ↦ μ.real {x : α | ε ≤ ‖f i x - g x‖}) l (𝓝 0)

Tactic:
congr! with ε hε hε_top
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
⊢ ∀ (ε : ℝ≥0∞) (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞) (∞ : ℝ≥0∞)

Tactic:
have hfin ε i : μ { x | ε ≤ edist (f i x) (g x) } ≠ ⊤ :=
    measure_ne_top μ {x | ε ≤ edist (f i x) (g x)}
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin :
  ∀ (ε : ℝ≥0∞) (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ≥0∞),
      0 < ε →
        Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
          l (𝓝 0)

Tactic:
⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin :
  ∀ (ε : ℝ≥0∞) (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_1 :
  ∀ (h : TendstoInMeasure μ f l g) (ε : ℝ≥0∞) (hε : 0 < ε),
    Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)})) l
      (𝓝 0)
refine_2 :
  ∀
    (h :
      ∀ (ε : ℝ≥0∞),
        0 < ε →
          Tendsto (β := ℝ≥0)
            (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)})) l (𝓝 0))
    (ε : ℝ≥0∞) (hε : 0 < ε),
    Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)
⊢ TendstoInMeasure μ f l g ↔
    ∀ (ε : ℝ≥0∞),
      0 < ε →
        Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
          l (𝓝 0)

Tactic:
refine ⟨fun h ε hε ↦ ?_, fun h ε hε ↦ ?_⟩
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin :
  ∀ (ε : ℝ≥0∞) (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
⊢ Eq.{u_2 + 1} (α := (i : ι) → ℝ≥0)
    (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
    (ENNReal.toNNReal ∘ fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)})

Tactic:
have hf : (fun i => (μ { x | ε ≤ edist (f i x) (g x) }).toNNReal) =
        ENNReal.toNNReal ∘ (fun i ↦ (μ { x | ε ≤ edist (f i x) (g x) })) := rfl
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin :
  ∀ (ε : ℝ≥0∞) (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
hf :
  Eq.{u_2 + 1} (α := (i : ι) → ℝ≥0)
    (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
    (ENNReal.toNNReal ∘ fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)})
refine_1 : Tendsto (fun (x : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)}) l (𝓝 (↑0 : ℝ≥0∞))
⊢ Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)})) l
    (𝓝 0)

Tactic:
rw [hf, ENNReal.tendsto_toNNReal_iff' (hfin ε)]

Premises used: ENNReal.tendsto_toNNReal_iff'
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin :
  ∀ (ε : ℝ≥0∞) (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
hf :
  Eq.{u_2 + 1} (α := (i : ι) → ℝ≥0)
    (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
    (ENNReal.toNNReal ∘ fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)})
⊢ Tendsto (fun (x : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)}) l (𝓝 (↑0 : ℝ≥0∞))

Tactic:
h ε hε
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin :
  ∀ (ε : ℝ≥0∞) (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞) (∞ : ℝ≥0∞)
h : TendstoInMeasure μ f l g
ε : ℝ≥0∞
hε : 0 < ε
hf :
  Eq.{u_2 + 1} (α := (i : ι) → ℝ≥0)
    (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}))
    (ENNReal.toNNReal ∘ fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)})
⊢ Tendsto (fun (x : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)}) l (𝓝 (↑0 : ℝ≥0∞))

Tactic:
exact h ε hε
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin :
  ∀ (ε : ℝ≥0∞) (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)})) l
        (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
refine_2 :
  Tendsto (ENNReal.toNNReal ∘ fun (x : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)}) l
    (𝓝 (ENNReal.toNNReal 0))
⊢ Tendsto (β := ℝ≥0∞) (fun (i : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)}) l (𝓝 0)

Tactic:
rw [← ENNReal.tendsto_toNNReal_iff ENNReal.zero_ne_top (hfin ε)]

Premises used: ENNReal.zero_ne_top, ENNReal.tendsto_toNNReal_iff
-- Module: Mathlib.MeasureTheory.Function.ConvergenceInMeasure
Goal:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst : EDist E
inst_1 : IsFiniteMeasure μ
f : ι → α → E
l : Filter ι
g : α → E
hfin :
  ∀ (ε : ℝ≥0∞) (i : ι), Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)} : ℝ≥0∞) (∞ : ℝ≥0∞)
h :
  ∀ (ε : ℝ≥0∞),
    0 < ε →
      Tendsto (β := ℝ≥0) (fun (i : ι) ↦ ENNReal.toNNReal ((μ : (a : Set α) → ℝ≥0∞) {x : α | ε ≤ edist (f i x) (g x)})) l
        (𝓝 0)
ε : ℝ≥0∞
hε : 0 < ε
⊢ Tendsto (ENNReal.toNNReal ∘ fun (x : ι) ↦ (μ : (a : Set α) → ℝ≥0∞) {x_1 : α | ε ≤ edist (f x x_1) (g x_1)}) l
    (𝓝 (ENNReal.toNNReal 0))

Tactic:
h ε hε

Premises used: ENNReal.toNNReal, WithTop.untopD, WithTop.recTopCoe