case mk
α : Type u_1
E : Type u_2
F : Type ?u.358556
G : Type ?u.358559
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : { x // x ∈ Lp E p }
val✝ : α →ₘ[μ] E
property✝ : val✝ ∈ Lp E p
h : ↑↑{ val := val✝, property := property✝ } =ᵐ[μ] ↑↑g
⊢ { val := val✝, property := property✝ } = g
α : Type u_1
E : Type u_2
F : Type ?u.358556
G : Type ?u.358559
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
f g : { x // x ∈ Lp E p }
h : ↑↑f =ᵐ[μ] ↑↑g
⊢ f = g
cases f
case mk.mk
α : Type u_1
E : Type u_2
F : Type ?u.358556
G : Type ?u.358559
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
val✝¹ : α →ₘ[μ] E
property✝¹ : val✝¹ ∈ Lp E p
val✝ : α →ₘ[μ] E
property✝ : val✝ ∈ Lp E p
h : ↑↑{ val := val✝¹, property := property✝¹ } =ᵐ[μ] ↑↑{ val := val✝, property := property✝ }
⊢ { val := val✝¹, property := property✝¹ } = { val := val✝, property := property✝ }
case mk
α : Type u_1
E : Type u_2
F : Type ?u.358556
G : Type ?u.358559
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
g : { x // x ∈ Lp E p }
val✝ : α →ₘ[μ] E
property✝ : val✝ ∈ Lp E p
h : ↑↑{ val := val✝, property := property✝ } =ᵐ[μ] ↑↑g
⊢ { val := val✝, property := property✝ } = g
cases g
case mk.mk
α : Type u_1
E : Type u_2
F : Type ?u.358556
G : Type ?u.358559
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
val✝¹ : α →ₘ[μ] E
property✝¹ : val✝¹ ∈ Lp E p
val✝ : α →ₘ[μ] E
property✝ : val✝ ∈ Lp E p
h : ↑↑{ val := val✝¹, property := property✝¹ } =ᵐ[μ] ↑↑{ val := val✝, property := property✝ }
⊢ val✝¹ = val✝
case mk.mk
α : Type u_1
E : Type u_2
F : Type ?u.358556
G : Type ?u.358559
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
val✝¹ : α →ₘ[μ] E
property✝¹ : val✝¹ ∈ Lp E p
val✝ : α →ₘ[μ] E
property✝ : val✝ ∈ Lp E p
h : ↑↑{ val := val✝¹, property := property✝¹ } =ᵐ[μ] ↑↑{ val := val✝, property := property✝ }
⊢ { val := val✝¹, property := property✝¹ } = { val := val✝, property := property✝ }
simp only [Subtype.mk_eq_mk]
no goals
case mk.mk
α : Type u_1
E : Type u_2
F : Type ?u.358556
G : Type ?u.358559
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
val✝¹ : α →ₘ[μ] E
property✝¹ : val✝¹ ∈ Lp E p
val✝ : α →ₘ[μ] E
property✝ : val✝ ∈ Lp E p
h : ↑↑{ val := val✝¹, property := property✝¹ } =ᵐ[μ] ↑↑{ val := val✝, property := property✝ }
⊢ val✝¹ = val✝
exact AEEqFun.ext h