Theorem: duals_bddAbove (Ray/Hartogs/Duals.lean)

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
⊢ BddAbove (range fun n => g ‖(duals n) x‖)
Tactic:
rw [bddAbove_def]
State after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
⊢ ∃ x_1, ∀ y ∈ range fun n => g ‖(duals n) x‖, y ≤ x_1

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
⊢ ∃ x_1, ∀ y ∈ range fun n => g ‖(duals n) x‖, y ≤ x_1
Tactic:
use g ‖x‖
State after:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
⊢ ∀ y ∈ range fun n => g ‖(duals n) x‖, y ≤ g ‖x‖

State before:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
⊢ ∀ y ∈ range fun n => g ‖(duals n) x‖, y ≤ g ‖x‖
Tactic:
simp only [Complex.norm_eq_abs, Set.mem_range, forall_exists_index,
  forall_apply_eq_imp_iff']
State after:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
⊢ ∀ (y : ℝ) (x_1 : ℕ), g (Complex.abs ((duals x_1) x)) = y → y ≤ g ‖x‖

State before:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
⊢ ∀ (y : ℝ) (x_1 : ℕ), g (Complex.abs ((duals x_1) x)) = y → y ≤ g ‖x‖
Tactic:
intro _ _ h
State after:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
y✝ : ℝ
x✝ : ℕ
h : g (Complex.abs ((duals x✝) x)) = y✝
⊢ y✝ ≤ g ‖x‖

State before:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
y✝ : ℝ
x✝ : ℕ
h : g (Complex.abs ((duals x✝) x)) = y✝
⊢ y✝ ≤ g ‖x‖
Tactic:
rw [←h]
State after:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
y✝ : ℝ
x✝ : ℕ
h : g (Complex.abs ((duals x✝) x)) = y✝
⊢ g (Complex.abs ((duals x✝) x)) ≤ g ‖x‖

State before:
case h
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
y✝ : ℝ
x✝ : ℕ
h : g (Complex.abs ((duals x✝) x)) = y✝
⊢ g (Complex.abs ((duals x✝) x)) ≤ g ‖x‖
Tactic:
apply gm
State after:
case h.a
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
y✝ : ℝ
x✝ : ℕ
h : g (Complex.abs ((duals x✝) x)) = y✝
⊢ Complex.abs ((duals x✝) x) ≤ ‖x‖

State before:
case h.a
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
g : ℝ → ℝ
gm : Monotone g
x : E
y✝ : ℝ
x✝ : ℕ
h : g (Complex.abs ((duals x✝) x)) = y✝
⊢ Complex.abs ((duals x✝) x) ≤ ‖x‖
Tactic:
apply dualVector_le
State after:
no goals