-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem ae_eq_of_ae_le_of_lintegral_le {f g : α → ℝ≥0∞} (hfg : f ≤ᵐ[μ] g) (hf : ∫⁻ x, f x ∂μ ≠ ∞)
    (hg : AEMeasurable g μ) (hgf : ∫⁻ x, g x ∂μ ≤ ∫⁻ x, f x ∂μ) : f =ᵐ[μ] g

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹

Tactic:
simp only [ae_iff, not_lt]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
⊢ μ {a | f a + (↑n)⁻¹ ≤ g a} = 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
⊢ f =ᶠ[ae μ] g

Tactic:
refine hfg.mp ((ae_all_iff.2 this).mono fun x hlt hle => hle.antisymm ?_)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] 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

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
⊢ f =ᶠ[ae μ] g

Tactic:
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.natCast_ne_top _))

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹
⊢ f =ᶠ[ae μ] g

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] 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

Tactic:
exact this.resolve_left (ENNReal.inv_ne_zero.2 (ENNReal.natCast_ne_top _))

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] 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

Tactic:
rw [(ENNReal.cancel_of_ne hf).add_le_iff_nonpos_right, nonpos_iff_eq_zero, mul_eq_zero] at this

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] 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

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] 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))

Tactic:
simpa only [inv_top, add_zero] using
  tendsto_const_nhds.add (ENNReal.tendsto_inv_iff.2 ENNReal.tendsto_nat_nhds_top)

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
⊢ μ {a | f a + (↑n)⁻¹ ≤ g a} = 0

Tactic:
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

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] 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

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] 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

Tactic:
suffices Tendsto (fun n : ℕ => f x + (n : ℝ≥0∞)⁻¹) atTop (𝓝 (f x)) from
  ge_of_tendsto' this fun i => (hlt i).le

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] 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))

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
⊢ ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹

Tactic:
intro n

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
hfg : f ≤ᶠ[ae μ] g
hf : ∫⁻ (x : α), f x ∂μ ≠ ⊤
hg : AEMeasurable g μ
hgf : ∫⁻ (x : α), g x ∂μ ≤ ∫⁻ (x : α), f x ∂μ
n : ℕ
⊢ ∀ᵐ (x : α) ∂μ, g x < f x + (↑n)⁻¹