-- Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
theorem congr' (h_left : ∀ᶠ i in l, f i =ᵐ[μ] f' i) (h_right : g =ᵐ[μ] g')
    (h_tendsto : TendstoInMeasure μ f l g) : TendstoInMeasure μ f' l g'

Proof state:
case h
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ {x | ε ≤ dist (f' i x) (g' x)} x ↔ {x | ε ≤ dist (f i x) (g x)} x

Tactic:
change ε ≤ dist (f' i x) (g' x) ↔ ε ≤ dist (f i x) (g x)

Result:
case h
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ ε ≤ dist (f' i x) (g' x) ↔ ε ≤ dist (f i x) (g x)

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
⊢ (fun i => μ {x | ε ≤ dist (f' i x) (g' x)}) =ᶠ[l] fun i => μ {x | ε ≤ dist (f i x) (g x)}

Tactic:
filter_upwards [h_left] with i h_ae_eq

Result:
case h
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
⊢ μ {x | ε ≤ dist (f' i x) (g' x)} = μ {x | ε ≤ dist (f i x) (g x)}

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
this : (fun i => μ {x | ε ≤ dist (f' i x) (g' x)}) =ᶠ[l] fun i => μ {x | ε ≤ dist (f i x) (g x)}
⊢ Tendsto (fun i => μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)

Tactic:
exact h_tendsto ε hε

Result:
no goals

Proof state:
case h
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ {x | ε ≤ dist (f' i x) (g' x)} x = {x | ε ≤ dist (f i x) (g x)} x

Tactic:
rw [eq_iff_iff]

Result:
case h
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ {x | ε ≤ dist (f' i x) (g' x)} x ↔ {x | ε ≤ dist (f i x) (g x)} x

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun i => μ {x | ε ≤ dist (f' i x) (g' x)}) l (𝓝 0)

Tactic:
suffices
  (fun i => μ { x | ε ≤ dist (f' i x) (g' x) }) =ᶠ[l] fun i => μ { x | ε ≤ dist (f i x) (g x) } by
  rw [tendsto_congr' this]
  exact h_tendsto ε hε

Result:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
⊢ (fun i => μ {x | ε ≤ dist (f' i x) (g' x)}) =ᶠ[l] fun i => μ {x | ε ≤ dist (f i x) (g x)}

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
this : (fun i => μ {x | ε ≤ dist (f' i x) (g' x)}) =ᶠ[l] fun i => μ {x | ε ≤ dist (f i x) (g x)}
⊢ Tendsto (fun i => μ {x | ε ≤ dist (f' i x) (g' x)}) l (𝓝 0)

Tactic:
rw [tendsto_congr' this]

Result:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
this : (fun i => μ {x | ε ≤ dist (f' i x) (g' x)}) =ᶠ[l] fun i => μ {x | ε ≤ dist (f i x) (g x)}
⊢ Tendsto (fun i => μ {x | ε ≤ dist (f i x) (g x)}) l (𝓝 0)

Proof state:
case h
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ ε ≤ dist (f' i x) (g' x) ↔ ε ≤ dist (f i x) (g x)

Tactic:
rw [hxg, hxf]

Result:
no goals

Proof state:
case h
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
⊢ {x | ε ≤ dist (f' i x) (g' x)} =ᶠ[ae μ] {x | ε ≤ dist (f i x) (g x)}

Tactic:
filter_upwards [h_ae_eq, h_right] with x hxf hxg

Result:
case h
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
x : α
hxf : f i x = f' i x
hxg : g x = g' x
⊢ {x | ε ≤ dist (f' i x) (g' x)} x = {x | ε ≤ dist (f i x) (g x)} x

Proof state:
case h
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
⊢ μ {x | ε ≤ dist (f' i x) (g' x)} = μ {x | ε ≤ dist (f i x) (g x)}

Tactic:
refine measure_congr ?_

Result:
case h
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
i : ι
h_ae_eq : f i =ᶠ[ae μ] f' i
⊢ {x | ε ≤ dist (f' i x) (g' x)} =ᶠ[ae μ] {x | ε ≤ dist (f i x) (g x)}

Proof state:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
⊢ TendstoInMeasure μ f' l g'

Tactic:
intro ε hε

Result:
α : Type u_1
ι : Type u_2
E : Type u_4
m : MeasurableSpace α
μ : Measure α
inst✝ : Dist E
l : Filter ι
f f' : ι → α → E
g g' : α → E
h_left : ∀ᶠ (i : ι) in l, f i =ᶠ[ae μ] f' i
h_right : g =ᶠ[ae μ] g'
h_tendsto : TendstoInMeasure μ f l g
ε : ℝ
hε : 0 < ε
⊢ Tendsto (fun i => μ {x | ε ≤ dist (f' i x) (g' x)}) l (𝓝 0)