case hnc
α : Type ?u.3022017
E : Type ?u.3022020
F : Type ?u.3022023
G : Type ?u.3022026
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
hp : 1 ≤ p
⊢ ¬p ∈ Set.Ioo 0 1
α : Type ?u.3022017
E : Type ?u.3022020
F : Type ?u.3022023
G : Type ?u.3022026
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
hp : 1 ≤ p
⊢ LpAddConst p = 1
rw [LpAddConst, if_neg]
case hnc
α : Type ?u.3022017
E : Type ?u.3022020
F : Type ?u.3022023
G : Type ?u.3022026
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
hp : 1 ≤ p
h : p ∈ Set.Ioo 0 1
⊢ False
case hnc
α : Type ?u.3022017
E : Type ?u.3022020
F : Type ?u.3022023
G : Type ?u.3022026
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
hp : 1 ≤ p
⊢ ¬p ∈ Set.Ioo 0 1
intro h
no goals
case hnc
α : Type ?u.3022017
E : Type ?u.3022020
F : Type ?u.3022023
G : Type ?u.3022026
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedAddCommGroup G
p : ℝ≥0∞
hp : 1 ≤ p
h : p ∈ Set.Ioo 0 1
⊢ False
exact lt_irrefl _ (h.2.trans_le hp)