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

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
x y : E
⊢ Complex.abs ((dualVector x) y) ≤ ‖y‖
Tactic:
rw [← Complex.norm_eq_abs]
State after:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
x y : E
⊢ ‖(dualVector x) y‖ ≤ ‖y‖

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
x y : E
⊢ ‖(dualVector x) y‖ ≤ ‖y‖
Tactic:
calc ‖dualVector x y‖
  _ ≤ ‖dualVector x‖ * ‖y‖ := (dualVector x).le_op_norm y
  _ ≤ 1 * ‖y‖ := by bound
  _ = ‖y‖ := by 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
x y : E
⊢ ‖dualVector x‖ * ‖y‖ ≤ 1 * ‖y‖
Tactic:
bound
State after:
no goals

State before:
G : Type
inst✝³ : NormedAddCommGroup G
E : Type
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : SecondCountableTopology E
x y : E
⊢ 1 * ‖y‖ = ‖y‖
Tactic:
simp only [one_mul]
State after:
no goals