-- Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
theorem ae_eq_zero_of_forall_dual_of_isSeparable [NormedAddCommGroup E] [NormedSpace 𝕜 E]
    {t : Set E} (ht : TopologicalSpace.IsSeparable t) {f : α → E}
    (hf : ∀ c : Dual 𝕜 E, (fun x => ⟪f x, c⟫) =ᵐ[μ] 0) (h't : ∀ᵐ x ∂μ, f x ∈ t) : f =ᵐ[μ] 0

Proof state:
case intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure d
this : Encodable ↑d
s : ↑d → E →L[𝕜] 𝕜
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
A : ∀ a ∈ t, (∀ (x : ↑d), (s x) a = 0) → a = 0
⊢ f =ᶠ[ae μ] 0

Tactic:
have hfs : ∀ y : d, ∀ᵐ x ∂μ, ⟪f x, s y⟫ = (0 : 𝕜) := fun y => hf (s y)

Result:
case intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure d
this : Encodable ↑d
s : ↑d → E →L[𝕜] 𝕜
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
A : ∀ a ∈ t, (∀ (x : ↑d), (s x) a = 0) → a = 0
hfs : ∀ (y : ↑d), ∀ᵐ (x : α) ∂μ, (s y) (f x) = 0
⊢ f =ᶠ[ae μ] 0

Proof state:
case h
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure d
this : Encodable ↑d
s : ↑d → E →L[𝕜] 𝕜
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure d
x : ↑d
hx : dist a ↑x < ‖a‖ / 2
I : ‖a‖ / 2 < ‖↑x‖
h : (s x) a = 0
⊢ ‖(s x) ↑x‖ < ‖(s x) ↑x‖

Tactic:
calc
  ‖s x x‖ = ‖s x (x - a)‖ := by simp only [h, sub_zero, ContinuousLinearMap.map_sub]
  _ ≤ 1 * ‖(x : E) - a‖ := ContinuousLinearMap.le_of_opNorm_le _ (hs x).1 _
  _ < ‖a‖ / 2 := by rw [one_mul]; rwa [dist_eq_norm'] at hx
  _ < ‖(x : E)‖ := I
  _ = ‖s x x‖ := by rw [(hs x).2, RCLike.norm_coe_norm]

Result:
no goals

Proof state:
case h
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure d
this : Encodable ↑d
s : ↑d → E →L[𝕜] 𝕜
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
A : ∀ a ∈ t, (∀ (x : ↑d), (s x) a = 0) → a = 0
hfs : ∀ (y : ↑d), ∀ᵐ (x : α) ∂μ, (s y) (f x) = 0
hf' : ∀ᵐ (x : α) ∂μ, ∀ (y : ↑d), (s y) (f x) = 0
x : α
hx : ∀ (y : ↑d), (s y) (f x) = 0
h'x : f x ∈ t
⊢ f x = 0 x

Tactic:
exact A (f x) h'x hx

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure d
this : Encodable ↑d
s : ↑d → E →L[𝕜] 𝕜
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
⊢ f =ᶠ[ae μ] 0

Tactic:
have A : ∀ a : E, a ∈ t → (∀ x, ⟪a, s x⟫ = (0 : 𝕜)) → a = 0 := by
  intro a hat ha
  contrapose! ha
  have a_pos : 0 < ‖a‖ := by simp only [ha, norm_pos_iff, Ne, not_false_iff]
  have a_mem : a ∈ closure d := hd hat
  obtain ⟨x, hx⟩ : ∃ x : d, dist a x < ‖a‖ / 2 := by
    rcases Metric.mem_closure_iff.1 a_mem (‖a‖ / 2) (half_pos a_pos) with ⟨x, h'x, hx⟩
    exact ⟨⟨x, h'x⟩, hx⟩
  use x
  have I : ‖a‖ / 2 < ‖(x : E)‖ := by
    have : ‖a‖ ≤ ‖(x : E)‖ + ‖a - x‖ := norm_le_insert' _ _
    have : ‖a - x‖ < ‖a‖ / 2 := by rwa [dist_eq_norm] at hx
    linarith
  intro h
  apply lt_irrefl ‖s x x‖
  calc
    ‖s x x‖ = ‖s x (x - a)‖ := by simp only [h, sub_zero, ContinuousLinearMap.map_sub]
    _ ≤ 1 * ‖(x : E) - a‖ := ContinuousLinearMap.le_of_opNorm_le _ (hs x).1 _
    _ < ‖a‖ / 2 := by rw [one_mul]; rwa [dist_eq_norm'] at hx
    _ < ‖(x : E)‖ := I
    _ = ‖s x x‖ := by rw [(hs x).2, RCLike.norm_coe_norm]

Result:
case intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure d
this : Encodable ↑d
s : ↑d → E →L[𝕜] 𝕜
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
A : ∀ a ∈ t, (∀ (x : ↑d), (s x) a = 0) → a = 0
⊢ f =ᶠ[ae μ] 0

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure d
this : Encodable ↑d
s : ↑d → E →L[𝕜] 𝕜
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
⊢ ∃ x, (s x) a ≠ 0

Tactic:
have a_mem : a ∈ closure d := hd hat

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure d
this : Encodable ↑d
s : ↑d → E →L[𝕜] 𝕜
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
a : E
hat : a ∈ t
ha : a ≠ 0
a_pos : 0 < ‖a‖
a_mem : a ∈ closure d
⊢ ∃ x, (s x) a ≠ 0

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure d
this : Encodable ↑d
s : ↑d → E →L[𝕜] 𝕜
hs : ∀ (x : ↑d), ‖s x‖ ≤ 1 ∧ (s x) ↑x = ↑‖↑x‖
A : ∀ a ∈ t, (∀ (x : ↑d), (s x) a = 0) → a = 0
hfs : ∀ (y : ↑d), ∀ᵐ (x : α) ∂μ, (s y) (f x) = 0
⊢ ∀ᵐ (x : α) ∂μ, ∀ (y : ↑d), (s y) (f x) = 0

Tactic:
rwa [ae_all_iff]

Result:
no goals

Proof state:
case intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure d
this : Encodable ↑d
⊢ f =ᶠ[ae μ] 0

Tactic:
have : ∀ x : d, ∃ g : E →L[𝕜] 𝕜, ‖g‖ ≤ 1 ∧ g x = ‖(x : E)‖ :=
  fun x => exists_dual_vector'' 𝕜 (x : E)

Result:
case intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure d
this✝ : Encodable ↑d
this : ∀ (x : ↑d), ∃ g, ‖g‖ ≤ 1 ∧ g ↑x = ↑‖↑x‖
⊢ f =ᶠ[ae μ] 0

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
ht : IsSeparable t
f : α → E
hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
⊢ f =ᶠ[ae μ] 0

Tactic:
rcases ht with ⟨d, d_count, hd⟩

Result:
case intro.intro
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
t : Set E
f : α → E
hf : ∀ (c : Dual 𝕜 E), (fun x => c (f x)) =ᶠ[ae μ] 0
h't : ∀ᵐ (x : α) ∂μ, f x ∈ t
d : Set E
d_count : d.Countable
hd : t ⊆ closure d
⊢ f =ᶠ[ae μ] 0