-- Mathlib/MeasureTheory/Function/AEEqOfIntegral.lean
theorem ae_eq_zero_of_forall_inner [NormedAddCommGroup E] [InnerProductSpace 𝕜 E]
    [SecondCountableTopology E] {f : α → E} (hf : ∀ c : E, (fun x => (inner c (f x) : 𝕜)) =ᵐ[μ] 0) :
    f =ᵐ[μ] 0

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᶠ[ae μ] 0
s : ℕ → E := denseSeq E
⊢ f =ᶠ[ae μ] 0

Tactic:
have hs : DenseRange s := denseRange_denseSeq E

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᶠ[ae μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
⊢ f =ᶠ[ae μ] 0

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᶠ[ae μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), inner (s n) (f x) = 0
x : α
hx : ∀ (n : ℕ), inner (s n) (f x) = 0
h_closed : IsClosed {c | inner c (f x) = 0}
⊢ inner (f x) (f x) = 0

Tactic:
exact @isClosed_property ℕ E _ s (fun c => inner c (f x) = (0 : 𝕜)) hs h_closed hx _

Result:
no goals

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᶠ[ae μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
⊢ f =ᶠ[ae μ] 0

Tactic:
have hf' : ∀ᵐ x ∂μ, ∀ n : ℕ, inner (s n) (f x) = (0 : 𝕜) := ae_all_iff.mpr fun n => hf (s n)

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᶠ[ae μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), inner (s n) (f x) = 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✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᶠ[ae μ] 0
⊢ f =ᶠ[ae μ] 0

Tactic:
let s := denseSeq E

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᶠ[ae μ] 0
s : ℕ → E := denseSeq E
⊢ f =ᶠ[ae μ] 0

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᶠ[ae μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), inner (s n) (f x) = 0
x : α
hx : ∀ (n : ℕ), inner (s n) (f x) = 0
⊢ inner (f x) (f x) = 0

Tactic:
have h_closed : IsClosed {c : E | inner c (f x) = (0 : 𝕜)} :=
  isClosed_eq (continuous_id.inner continuous_const) continuous_const

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᶠ[ae μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), inner (s n) (f x) = 0
x : α
hx : ∀ (n : ℕ), inner (s n) (f x) = 0
h_closed : IsClosed {c | inner c (f x) = 0}
⊢ inner (f x) (f x) = 0

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᶠ[ae μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), inner (s n) (f x) = 0
x : α
hx : ∀ (n : ℕ), inner (s n) (f x) = 0
⊢ f x = 0 x

Tactic:
rw [Pi.zero_apply, ← @inner_self_eq_zero 𝕜]

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᶠ[ae μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), inner (s n) (f x) = 0
x : α
hx : ∀ (n : ℕ), inner (s n) (f x) = 0
⊢ inner (f x) (f x) = 0

Proof state:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᶠ[ae μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), inner (s n) (f x) = 0
⊢ f =ᶠ[ae μ] 0

Tactic:
refine hf'.mono fun x hx => ?_

Result:
α : Type u_1
E : Type u_2
𝕜 : Type u_3
m : MeasurableSpace α
μ : Measure α
inst✝³ : RCLike 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : SecondCountableTopology E
f : α → E
hf : ∀ (c : E), (fun x => inner c (f x)) =ᶠ[ae μ] 0
s : ℕ → E := denseSeq E
hs : DenseRange s
hf' : ∀ᵐ (x : α) ∂μ, ∀ (n : ℕ), inner (s n) (f x) = 0
x : α
hx : ∀ (n : ℕ), inner (s n) (f x) = 0
⊢ f x = 0 x