case mp
α : Type u_1
E : Type u_2
F : Type ?u.414402
G : Type ?u.414405
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
⊢ f = 0 → ↑↑f =ᵐ[μ] 0

case mpr
α : Type u_1
E : Type u_2
F : Type ?u.414402
G : Type ?u.414405
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
⊢ ↑↑f =ᵐ[μ] 0 → f = 0
α : Type u_1
E : Type u_2
F : Type ?u.414402
G : Type ?u.414405
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
⊢ f = 0 ↔ ↑↑f =ᵐ[μ] 0
constructor
case mp
α : Type u_1
E : Type u_2
F : Type ?u.414402
G : Type ?u.414405
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
h : f = 0
⊢ ↑↑f =ᵐ[μ] 0
case mp
α : Type u_1
E : Type u_2
F : Type ?u.414402
G : Type ?u.414405
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
⊢ f = 0 → ↑↑f =ᵐ[μ] 0
intro h
case mp
α : Type u_1
E : Type u_2
F : Type ?u.414402
G : Type ?u.414405
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
h : f = 0
⊢ ↑↑0 =ᵐ[μ] 0
case mp
α : Type u_1
E : Type u_2
F : Type ?u.414402
G : Type ?u.414405
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
h : f = 0
⊢ ↑↑f =ᵐ[μ] 0
rw [h]
no goals
case mp
α : Type u_1
E : Type u_2
F : Type ?u.414402
G : Type ?u.414405
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
h : f = 0
⊢ ↑↑0 =ᵐ[μ] 0
exact AEEqFun.coeFn_const _ _
case mpr
α : Type u_1
E : Type u_2
F : Type ?u.414402
G : Type ?u.414405
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
h : ↑↑f =ᵐ[μ] 0
⊢ f = 0
case mpr
α : Type u_1
E : Type u_2
F : Type ?u.414402
G : Type ?u.414405
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
⊢ ↑↑f =ᵐ[μ] 0 → f = 0
intro h
case mpr.h
α : Type u_1
E : Type u_2
F : Type ?u.414402
G : Type ?u.414405
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
h : ↑↑f =ᵐ[μ] 0
⊢ ↑↑f =ᵐ[μ] ↑↑0
case mpr
α : Type u_1
E : Type u_2
F : Type ?u.414402
G : Type ?u.414405
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
h : ↑↑f =ᵐ[μ] 0
⊢ f = 0
ext1
case h
α : Type u_1
E : Type u_2
F : Type ?u.414402
G : Type ?u.414405
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
h : ↑↑f =ᵐ[μ] 0
a✝ : α
ha : ↑↑f a✝ = OfNat.ofNat 0 a✝
h'a : ↑(AEEqFun.const α 0) a✝ = Function.const α 0 a✝
⊢ ↑↑f a✝ = ↑↑0 a✝
case mpr.h
α : Type u_1
E : Type u_2
F : Type ?u.414402
G : Type ?u.414405
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
h : ↑↑f =ᵐ[μ] 0
⊢ ↑↑f =ᵐ[μ] ↑↑0
filter_upwards [h, AEEqFun.coeFn_const α (0 : E)] with _ ha h'a
case h
α : Type u_1
E : Type u_2
F : Type ?u.414402
G : Type ?u.414405
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
h : ↑↑f =ᵐ[μ] 0
a✝ : α
ha : ↑↑f a✝ = OfNat.ofNat 0 a✝
h'a : ↑(AEEqFun.const α 0) a✝ = Function.const α 0 a✝
⊢ OfNat.ofNat 0 a✝ = ↑↑0 a✝
case h
α : Type u_1
E : Type u_2
F : Type ?u.414402
G : Type ?u.414405
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
h : ↑↑f =ᵐ[μ] 0
a✝ : α
ha : ↑↑f a✝ = OfNat.ofNat 0 a✝
h'a : ↑(AEEqFun.const α 0) a✝ = Function.const α 0 a✝
⊢ ↑↑f a✝ = ↑↑0 a✝
rw [ha]
no goals
case h
α : Type u_1
E : Type u_2
F : Type ?u.414402
G : Type ?u.414405
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f : { x // x ∈ Lp E p }
h : ↑↑f =ᵐ[μ] 0
a✝ : α
ha : ↑↑f a✝ = OfNat.ofNat 0 a✝
h'a : ↑(AEEqFun.const α 0) a✝ = Function.const α 0 a✝
⊢ OfNat.ofNat 0 a✝ = ↑↑0 a✝
exact h'a.symm