α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
⊢ f =ᵐ[μ] g
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
⊢ f =ᵐ[μ] g
have : ∀ n : ℕ, ∀ᵐ x ∂μ, g x < f x + (n : ℝ≥0∞)⁻¹ := by
  intro n
  simp only [ae_iff, not_lt]
  have : (∫⁻ x, f x ∂μ) + (↑n)⁻¹ * μ { x : α | f x + (n : ℝ≥0∞)⁻¹ ≤ g x } ≤ ∫⁻ x, f x ∂μ :=
    (lintegral_add_mul_meas_add_le_le_lintegral hfg hg n⁻¹).trans hgf
  rw [(ENNReal.cancel_of_ne hf).add_le_iff_nonpos_right, nonpos_iff_eq_zero, mul_eq_zero] at this
  exact this.resolve_left (ENNReal.inv_ne_zero.2 (ENNReal.nat_ne_top _))
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
x : α
hlt : ∀ (i : ℕ), g x < f x + (↑i)⁻¹
hle : f x ≤ g x
⊢ g x ≤ f x
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
⊢ f =ᵐ[μ] g
refine' hfg.mp ((ae_all_iff.2 this).mono fun x hlt hle => hle.antisymm _)
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
this✝ : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
x : α
hlt : ∀ (i : ℕ), g x < f x + (↑i)⁻¹
hle : f x ≤ g x
this : Tendsto (fun n => f x + (↑n)⁻¹) atTop (𝓝 (f x))
⊢ g x ≤ f x

case this
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
x : α
hlt : ∀ (i : ℕ), g x < f x + (↑i)⁻¹
hle : f x ≤ g x
⊢ Tendsto (fun n => f x + (↑n)⁻¹) atTop (𝓝 (f x))
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
x : α
hlt : ∀ (i : ℕ), g x < f x + (↑i)⁻¹
hle : f x ≤ g x
⊢ g x ≤ f x
suffices : Tendsto (fun n : ℕ => f x + (n : ℝ≥0∞)⁻¹) atTop (𝓝 (f x))
case this
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
x : α
hlt : ∀ (i : ℕ), g x < f x + (↑i)⁻¹
hle : f x ≤ g x
⊢ Tendsto (fun n => f x + (↑n)⁻¹) atTop (𝓝 (f x))
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
this✝ : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
x : α
hlt : ∀ (i : ℕ), g x < f x + (↑i)⁻¹
hle : f x ≤ g x
this : Tendsto (fun n => f x + (↑n)⁻¹) atTop (𝓝 (f x))
⊢ g x ≤ f x

case this
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
x : α
hlt : ∀ (i : ℕ), g x < f x + (↑i)⁻¹
hle : f x ≤ g x
⊢ Tendsto (fun n => f x + (↑n)⁻¹) atTop (𝓝 (f x))
exact ge_of_tendsto' this fun i => (hlt i).le
no goals
case this
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
x : α
hlt : ∀ (i : ℕ), g x < f x + (↑i)⁻¹
hle : f x ≤ g x
⊢ Tendsto (fun n => f x + (↑n)⁻¹) atTop (𝓝 (f x))
simpa only [inv_top, add_zero] using
  tendsto_const_nhds.add (ENNReal.tendsto_inv_iff.2 ENNReal.tendsto_nat_nhds_top)
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
⊢ ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
intro n
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
⊢ ↑↑μ {a | f a + (↑n)⁻¹ ≤ g a} = 0
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
simp only [ae_iff, not_lt]
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
this : (∫⁻ (x : α), f x ∂μ) + (↑n)⁻¹ * ↑↑μ {x | f x + (↑n)⁻¹ ≤ g x} ≤ ∫⁻ (x : α), f x ∂μ
⊢ ↑↑μ {a | f a + (↑n)⁻¹ ≤ g a} = 0
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
⊢ ↑↑μ {a | f a + (↑n)⁻¹ ≤ g a} = 0
have : (∫⁻ x, f x ∂μ) + (↑n)⁻¹ * μ { x : α | f x + (n : ℝ≥0∞)⁻¹ ≤ g x } ≤ ∫⁻ x, f x ∂μ :=
  (lintegral_add_mul_meas_add_le_le_lintegral hfg hg n⁻¹).trans hgf
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
this : (↑n)⁻¹ = 0 ∨ ↑↑μ {x | f x + (↑n)⁻¹ ≤ g x} = 0
⊢ ↑↑μ {a | f a + (↑n)⁻¹ ≤ g a} = 0
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
this : (∫⁻ (x : α), f x ∂μ) + (↑n)⁻¹ * ↑↑μ {x | f x + (↑n)⁻¹ ≤ g x} ≤ ∫⁻ (x : α), f x ∂μ
⊢ ↑↑μ {a | f a + (↑n)⁻¹ ≤ g a} = 0
rw [(ENNReal.cancel_of_ne hf).add_le_iff_nonpos_right, nonpos_iff_eq_zero, mul_eq_zero] at this
no goals
α : Type u_1
β : Type ?u.967242
γ : Type ?u.967245
δ : Type ?u.967248
m : MeasurableSpace α
μ ν : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᵐ[μ] g
hf : (∫⁻ (x : α), f x ∂μ) ≠ ⊤
hg : AEMeasurable g
hgf : (∫⁻ (x : α), g x ∂μ) ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
this : (↑n)⁻¹ = 0 ∨ ↑↑μ {x | f x + (↑n)⁻¹ ≤ g x} = 0
⊢ ↑↑μ {a | f a + (↑n)⁻¹ ≤ g a} = 0
exact this.resolve_left (ENNReal.inv_ne_zero.2 (ENNReal.nat_ne_top _))