-- 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:
α : 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
this : c ∈ upperBounds (Set.Iio c)
⊢ ∃ b ∈ upperBounds (Set.Iio c), b < c

Tactic:
simpa [IsLUB, IsLeast, this, lowerBounds] using H

Result:
no goals

Proof state:
case h.mp.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)
x : α
h : f x < c
n : ℕ
hn : f x < u n
⊢ ∃ i, f x ≤ u i

Tactic:
exact ⟨n, hn.le⟩

Result:
no goals

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ μ {a | ¬c ≤ f a} = 0 ↔ ∀ b < c, μ {x | f x ≤ b} = 0

Tactic:
push_neg

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ μ {a | f a < c} = 0 ↔ ∀ b < c, μ {x | f x ≤ b} = 0

Proof state:
case pos.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 : ¬∀ (b : β), c ≤ b
H : ¬IsLUB (Set.Iio c) c
this : c ∈ upperBounds (Set.Iio c)
b : β
b_up : b ∈ upperBounds (Set.Iio c)
bc : b < c
⊢ μ {a | f a < c} = 0

Tactic:
exact measure_mono_null (fun x hx => b_up hx) (hc b bc)

Result:
no goals

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
⊢ μ {a | f a < c} = 0

Tactic:
by_cases H : ¬IsLUB (Set.Iio c) c

Result:
case pos
α : 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

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

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ μ {a | f a < c} = 0 ↔ ∀ b < c, μ {x | f x ≤ b} = 0

Tactic:
constructor

Result:
case mp
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ μ {a | f a < c} = 0 → ∀ b < c, μ {x | f x ≤ b} = 0

case mpr
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ (∀ b < c, μ {x | f x ≤ b} = 0) → μ {a | f a < c} = 0

Proof state:
case pos
α : 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
this : c ∈ upperBounds (Set.Iio c)
⊢ μ {a | f a < c} = 0

Tactic:
obtain ⟨b, b_up, bc⟩ : ∃ b : β, b ∈ upperBounds (Set.Iio c) ∧ b < c := by
  simpa [IsLUB, IsLeast, this, lowerBounds] using H

Result:
case pos.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 : ¬∀ (b : β), c ≤ b
H : ¬IsLUB (Set.Iio c) c
this : c ∈ upperBounds (Set.Iio c)
b : β
b_up : b ∈ upperBounds (Set.Iio c)
bc : b < c
⊢ μ {a | f a < c} = 0

Proof state:
α : 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
⊢ {a | f a < c} = ∅

Tactic:
apply Set.eq_empty_iff_forall_not_mem.2 fun x hx => ?_

Result:
α : 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
x : α
hx : x ∈ {a | f a < c}
⊢ False

Proof state:
case pos
α : 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
this : {a | f a < c} = ∅
⊢ μ {a | f a < c} = 0

Tactic:
simp [this]

Result:
no goals

Proof state:
case pos
α : 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:
have : c ∈ upperBounds (Set.Iio c) := fun y hy => le_of_lt hy

Result:
case pos
α : 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
this : c ∈ upperBounds (Set.Iio c)
⊢ μ {a | f a < c} = 0

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ (∀ᵐ (x : α) ∂μ, c ≤ f x) ↔ ∀ b < c, μ {x | f x ≤ b} = 0

Tactic:
rw [ae_iff]

Result:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝³ : LinearOrder β
inst✝² : TopologicalSpace β
inst✝¹ : OrderTopology β
inst✝ : FirstCountableTopology β
f : α → β
c : β
⊢ μ {a | ¬c ≤ f a} = 0 ↔ ∀ b < c, μ {x | f x ≤ b} = 0

Proof state:
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

Tactic:
obtain ⟨n, hn⟩ := h

Result:
case h.mpr.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)
x : α
n : ℕ
hn : f x ≤ u n
⊢ f x < c