-- Mathlib/MeasureTheory/Function/AEEqOfLIntegral.lean
theorem ae_const_le_iff_forall_lt_measure_zero {β} [LinearOrder β] [TopologicalSpace β]
    [OrderTopology β] [FirstCountableTopology β] (f : α → β) (c : β) :
    (∀ᵐ x ∂μ, c ≤ f x) ↔ ∀ b < c, μ {x | f x ≤ b} = 0

Proof state:
case neg.intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ b < c, μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (𝓝 c)
h_Union : {x | f x < c} = ⋃ n, {x | f x ≤ u n}
n : ℕ
⊢ μ {x | f x ≤ u n} = 0

Tactic:
exact hc _ (u_lt n)

Result:
no goals

Proof state:
case neg.intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ b < c, μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (𝓝 c)
h_Union : {x | f x < c} = ⋃ n, {x | f x ≤ u n}
⊢ μ {a | f a < c} = 0

Tactic:
rw [h_Union, measure_iUnion_null_iff]

Result:
case neg.intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ b < c, μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (𝓝 c)
h_Union : {x | f x < c} = ⋃ n, {x | f x ≤ u n}
⊢ ∀ (i : ℕ), μ {x | f x ≤ u i} = 0

Proof state:
case h
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ b < c, μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (𝓝 c)
x : α
⊢ f x < c ↔ ∃ i, f x ≤ u i

Tactic:
constructor <;> intro h

Result:
case h.mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ b < c, μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h✝ : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (𝓝 c)
x : α
h : f x < c
⊢ ∃ i, f x ≤ u i

case h.mpr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ b < c, μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h✝ : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (𝓝 c)
x : α
h : ∃ i, f x ≤ u i
⊢ f x < c

Proof state:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ b < c, μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
⊢ μ {a | f a < c} = 0

Tactic:
obtain ⟨u, _, u_lt, u_lim, -⟩ :
  ∃ u : ℕ → β,
    StrictMono u ∧ (∀ n : ℕ, u n < c) ∧ Tendsto u atTop (𝓝 c) ∧ ∀ n : ℕ, u n ∈ Set.Iio c :=
  H.exists_seq_strictMono_tendsto_of_not_mem (lt_irrefl c) h

Result:
case neg.intro.intro.intro.intro
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ b < c, μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
u : ℕ → β
left✝ : StrictMono u
u_lt : ∀ (n : ℕ), u n < c
u_lim : Tendsto u atTop (𝓝 c)
⊢ μ {a | f a < c} = 0

Proof state:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ b < c, μ {x | f x ≤ b} = 0
h : ¬∀ (b : β), c ≤ b
H : ¬¬IsLUB (Set.Iio c) c
⊢ μ {a | f a < c} = 0

Tactic:
push_neg at H h

Result:
case neg
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
hc : ∀ b < c, μ {x | f x ≤ b} = 0
H : IsLUB (Set.Iio c) c
h : ∃ b, b < c
⊢ μ {a | f a < c} = 0