Theorem: norm_eq_duals_supr' (Ray/Hartogs/Duals.lean)

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖
Tactic:
by_cases k0 : k = 0
State after:
case pos
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : k = 0
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖

case neg
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖

State before:
case neg
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖
Tactic:
have kp : 0 < (k : ℝ) := by simp only [NNReal.coe_pos]; exact Ne.bot_lt k0
State after:
case neg
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖

State before:
case neg
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖
Tactic:
apply le_antisymm
State after:
case neg.a
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
⊢ g ‖x‖ ≤ ⨆ n, g ‖(duals n) x‖

case neg.a
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
⊢ ⨆ n, g ‖(duals n) x‖ ≤ g ‖x‖

State before:
case pos
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : k = 0
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖
Tactic:
rw [k0] at gk
State after:
case pos
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith 0 g
x : E
k0 : k = 0
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖

State before:
case pos
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith 0 g
x : E
k0 : k = 0
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖
Tactic:
have g0 := gk.is_const 0
State after:
case pos
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith 0 g
x : E
k0 : k = 0
g0 : ∀ (y : ℝ), g 0 = g y
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖

State before:
case pos
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith 0 g
x : E
k0 : k = 0
g0 : ∀ (y : ℝ), g 0 = g y
⊢ g ‖x‖ = ⨆ n, g ‖(duals n) x‖
Tactic:
simp only [← g0 _, ciSup_const]
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
⊢ 0 < ↑k
Tactic:
simp only [NNReal.coe_pos]
State after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
⊢ 0 < k

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
⊢ 0 < k
Tactic:
exact Ne.bot_lt k0
State after:
no goals

State before:
case neg.a
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
⊢ g ‖x‖ ≤ ⨆ n, g ‖(duals n) x‖
Tactic:
apply le_of_forall_pos_le_add
State after:
case neg.a.h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
⊢ ∀ (ε : ℝ), 0 < ε → g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + ε

State before:
case neg.a.h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
⊢ ∀ (ε : ℝ), 0 < ε → g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + ε
Tactic:
intro e ep
State after:
case neg.a.h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e

State before:
case neg.a.h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
Tactic:
rcases Metric.denseRange_iff.mp (TopologicalSpace.denseRange_denseSeq E)
  x (e / 2 / k) (by bound) with ⟨n, nx⟩
State after:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
nx : dist x (TopologicalSpace.denseSeq E n) < e / 2 / ↑k
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e

State before:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
nx : dist x (TopologicalSpace.denseSeq E n) < e / 2 / ↑k
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
Tactic:
generalize hy : TopologicalSpace.denseSeq E n = y
State after:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
nx : dist x (TopologicalSpace.denseSeq E n) < e / 2 / ↑k
y : E
hy : TopologicalSpace.denseSeq E n = y
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e

State before:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
nx : dist x (TopologicalSpace.denseSeq E n) < e / 2 / ↑k
y : E
hy : TopologicalSpace.denseSeq E n = y
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
Tactic:
rw [hy] at nx
State after:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
hy : TopologicalSpace.denseSeq E n = y
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e

State before:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
hy : TopologicalSpace.denseSeq E n = y
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
Tactic:
have hn : duals n = dualVector y := by rw [← hy, duals]
State after:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
hy : TopologicalSpace.denseSeq E n = y
hn : duals n = dualVector y
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e

State before:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
hy : TopologicalSpace.denseSeq E n = y
hn : duals n = dualVector y
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
Tactic:
have h := le_ciSup (duals_bddAbove gm x) n
State after:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
hy : TopologicalSpace.denseSeq E n = y
hn : duals n = dualVector y
h : g ‖(duals n) x‖ ≤ ⨆ n, g ‖(duals n) x‖
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e

State before:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
hy : TopologicalSpace.denseSeq E n = y
hn : duals n = dualVector y
h : g ‖(duals n) x‖ ≤ ⨆ n, g ‖(duals n) x‖
⊢ g ‖x‖ ≤ (⨆ n, g ‖(duals n) x‖) + e
Tactic:
generalize hs : ⨆ n, g ‖duals n x‖ = s
State after:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
hy : TopologicalSpace.denseSeq E n = y
hn : duals n = dualVector y
h : g ‖(duals n) x‖ ≤ ⨆ n, g ‖(duals n) x‖
s : ℝ
hs : ⨆ n, g ‖(duals n) x‖ = s
⊢ g ‖x‖ ≤ s + e

State before:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
hy : TopologicalSpace.denseSeq E n = y
hn : duals n = dualVector y
h : g ‖(duals n) x‖ ≤ ⨆ n, g ‖(duals n) x‖
s : ℝ
hs : ⨆ n, g ‖(duals n) x‖ = s
⊢ g ‖x‖ ≤ s + e
Tactic:
simp_rw [hs, hn] at h
State after:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
hy : TopologicalSpace.denseSeq E n = y
hn : duals n = dualVector y
s : ℝ
hs : ⨆ n, g ‖(duals n) x‖ = s
h : g ‖(dualVector y) x‖ ≤ s
⊢ g ‖x‖ ≤ s + e

State before:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
hy : TopologicalSpace.denseSeq E n = y
hn : duals n = dualVector y
s : ℝ
hs : ⨆ n, g ‖(duals n) x‖ = s
h : g ‖(dualVector y) x‖ ≤ s
⊢ g ‖x‖ ≤ s + e
Tactic:
clear hs hn hy
State after:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g ‖(dualVector y) x‖ ≤ s
⊢ g ‖x‖ ≤ s + e

State before:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g ‖(dualVector y) x‖ ≤ s
⊢ g ‖x‖ ≤ s + e
Tactic:
simp only [Complex.norm_eq_abs] at h
State after:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
⊢ g ‖x‖ ≤ s + e

State before:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
⊢ g ‖x‖ ≤ s + e
Tactic:
have gk' : LipschitzWith k fun x ↦ g (abs (dualVector y x)) := by
  have k11 : (k : ℝ≥0) = k * 1 * 1 := by norm_num
  rw [k11]
  simp_rw [←Complex.norm_eq_abs]; apply (gk.comp lipschitzWith_one_norm).comp
  exact (dualVector y).lipschitz.weaken (dualVector_nnnorm y)
State after:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ g ‖x‖ ≤ s + e

State before:
case neg.a.h.intro
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ g ‖x‖ ≤ s + e
Tactic:
calc g ‖x‖
  _ ≤ g ‖y‖ + k * 1 * dist x y := (gk.comp lipschitzWith_one_norm).le x y
  _ ≤ g ‖y‖ + k * 1 * (e / 2 / k) := by bound
  _ = g ‖y‖ + k / k * e / 2 := by ring
  _ ≤ g ‖y‖ + 1 * e / 2 := by bound
  _ = g ‖y‖ + e / 2 := by simp only [one_mul]
  _ = g (abs (dualVector y y)) + e / 2 := by
    simp only [dualVector_apply, Complex.abs_ofReal, abs_norm]
  _ ≤ g (abs (dualVector y x)) + k * dist y x + e / 2 := by bound [gk'.le]
  _ ≤ s + k * dist y x + e / 2 := by linarith
  _ = s + k * dist x y + e / 2 := by rw [dist_comm]
  _ ≤ s + k * (e / 2 / k) + e / 2 := by bound
  _ = s + k / k * e / 2 + e / 2 := by ring_nf
  _ ≤ s + 1 * e / 2 + e / 2 := by bound
  _ = s + e := by ring_nf
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
⊢ e / 2 / ↑k > 0
Tactic:
bound
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
hy : TopologicalSpace.denseSeq E n = y
⊢ duals n = dualVector y
Tactic:
rw [← hy, duals]
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
⊢ LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
Tactic:
have k11 : (k : ℝ≥0) = k * 1 * 1 := by norm_num
State after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
k11 : k = k * 1 * 1
⊢ LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
k11 : k = k * 1 * 1
⊢ LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
Tactic:
rw [k11]
State after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
k11 : k = k * 1 * 1
⊢ LipschitzWith (k * 1 * 1) fun x => g (Complex.abs ((dualVector y) x))

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
k11 : k = k * 1 * 1
⊢ LipschitzWith (k * 1 * 1) fun x => g (Complex.abs ((dualVector y) x))
Tactic:
simp_rw [←Complex.norm_eq_abs]
State after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
k11 : k = k * 1 * 1
⊢ LipschitzWith (k * 1 * 1) fun x => g ‖(dualVector y) x‖

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
k11 : k = k * 1 * 1
⊢ LipschitzWith (k * 1 * 1) fun x => g ‖(dualVector y) x‖
Tactic:
apply (gk.comp lipschitzWith_one_norm).comp
State after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
k11 : k = k * 1 * 1
⊢ LipschitzWith 1 fun x => (dualVector y) x

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
k11 : k = k * 1 * 1
⊢ LipschitzWith 1 fun x => (dualVector y) x
Tactic:
exact (dualVector y).lipschitz.weaken (dualVector_nnnorm y)
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
⊢ k = k * 1 * 1
Tactic:
norm_num
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ g ‖y‖ + ↑k * 1 * dist x y ≤ g ‖y‖ + ↑k * 1 * (e / 2 / ↑k)
Tactic:
bound
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ g ‖y‖ + ↑k * 1 * (e / 2 / ↑k) = g ‖y‖ + ↑k / ↑k * e / 2
Tactic:
ring
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ g ‖y‖ + ↑k / ↑k * e / 2 ≤ g ‖y‖ + 1 * e / 2
Tactic:
bound
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ g ‖y‖ + 1 * e / 2 = g ‖y‖ + e / 2
Tactic:
simp only [one_mul]
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ g ‖y‖ + e / 2 = g (Complex.abs ((dualVector y) y)) + e / 2
Tactic:
simp only [dualVector_apply, Complex.abs_ofReal, abs_norm]
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ g (Complex.abs ((dualVector y) y)) + e / 2 ≤ g (Complex.abs ((dualVector y) x)) + ↑k * dist y x + e / 2
Tactic:
bound [gk'.le]
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ g (Complex.abs ((dualVector y) x)) + ↑k * dist y x + e / 2 ≤ s + ↑k * dist y x + e / 2
Tactic:
linarith
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ s + ↑k * dist y x + e / 2 = s + ↑k * dist x y + e / 2
Tactic:
rw [dist_comm]
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ s + ↑k * dist x y + e / 2 ≤ s + ↑k * (e / 2 / ↑k) + e / 2
Tactic:
bound
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ s + ↑k * (e / 2 / ↑k) + e / 2 = s + ↑k / ↑k * e / 2 + e / 2
Tactic:
ring_nf
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ s + ↑k / ↑k * e / 2 + e / 2 ≤ s + 1 * e / 2 + e / 2
Tactic:
bound
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
e : ℝ
ep : 0 < e
n : ℕ
y : E
nx : dist x y < e / 2 / ↑k
s : ℝ
h : g (Complex.abs ((dualVector y) x)) ≤ s
gk' : LipschitzWith k fun x => g (Complex.abs ((dualVector y) x))
⊢ s + 1 * e / 2 + e / 2 = s + e
Tactic:
ring_nf
State after:
no goals

State before:
case neg.a
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
⊢ ⨆ n, g ‖(duals n) x‖ ≤ g ‖x‖
Tactic:
apply ciSup_le
State after:
case neg.a.H
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
⊢ ∀ (x_1 : ℕ), g ‖(duals x_1) x‖ ≤ g ‖x‖

State before:
case neg.a.H
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
⊢ ∀ (x_1 : ℕ), g ‖(duals x_1) x‖ ≤ g ‖x‖
Tactic:
intro n
State after:
case neg.a.H
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
n : ℕ
⊢ g ‖(duals n) x‖ ≤ g ‖x‖

State before:
case neg.a.H
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
n : ℕ
⊢ g ‖(duals n) x‖ ≤ g ‖x‖
Tactic:
apply gm
State after:
case neg.a.H.a
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
n : ℕ
⊢ ‖(duals n) x‖ ≤ ‖x‖

State before:
case neg.a.H.a
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
n : ℕ
⊢ ‖(duals n) x‖ ≤ ‖x‖
Tactic:
simp only [Complex.norm_eq_abs]
State after:
case neg.a.H.a
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
n : ℕ
⊢ Complex.abs ((duals n) x) ≤ ‖x‖

State before:
case neg.a.H.a
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
k : ℝ≥0
gm : Monotone g
gk : LipschitzWith k g
x : E
k0 : ¬k = 0
kp : 0 < ↑k
n : ℕ
⊢ Complex.abs ((duals n) x) ≤ ‖x‖
Tactic:
apply dualVector_le
State after:
no goals