awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
a : ‖z₁‖ = r
⊢ Membership.mem (γ := Set E) (sphere 0 r) z₁

Tactic:
rw [mem_sphere_zero_iff_norm]

Premises used: mem_sphere_zero_iff_norm
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
⊢ ‖z₁‖ = r

Tactic:
norm_smul_inv_norm' r_pos.le z_zero

Premises used: norm_smul_inv_norm', LT.lt.le
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
⊢ ‖z₁‖ = r

Tactic:
exact norm_smul_inv_norm' r_pos.le z_zero

Premises used: norm_smul_inv_norm', LT.lt.le
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c

Tactic:
have norm_f_z₁ : ‖f z₁‖ ≤ c := by
    apply h
    rw [mem_sphere_zero_iff_norm]
    exact norm_smul_inv_norm' r_pos.le z_zero
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0

Tactic:
have r_ne_zero : (r : 𝕜) ≠ 0 := RCLike.ofReal_ne_zero.mpr r_pos.ne'
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
r_ne_zero : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
rw :
  (f : (a : E) → 𝕜) z =
    HDiv.hDiv (α := 𝕜) (↑‖z‖ : 𝕜) (↑r : 𝕜) *
      HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹) ((f : (a : E) → 𝕜) z : 𝕜)
⊢ (f : (a : E) → 𝕜) z = HMul.hMul (β := 𝕜) (HDiv.hDiv (α := 𝕜) (↑‖z‖ : 𝕜) (↑r : 𝕜)) ((f : (a : E) → 𝕜) z₁ : 𝕜)

Tactic:
rw [hz₁, map_smul, smul_eq_mul]

Premises used: smul_eq_mul, map_smul
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
r_ne_zero : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
rw : Ne.{u_1 + 1} (α := 𝕜) (↑‖z‖ : 𝕜) 0
⊢ (f : (a : E) → 𝕜) z =
    HDiv.hDiv (α := 𝕜) (↑‖z‖ : 𝕜) (↑r : 𝕜) *
      HMul.hMul (β := 𝕜) (HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹) ((f : (a : E) → 𝕜) z : 𝕜)

Tactic:
rw [← mul_assoc, ← mul_assoc, div_mul_cancel₀ _ r_ne_zero, mul_inv_cancel₀, one_mul]

Premises used: div_mul_cancel₀, mul_inv_cancel₀, mul_assoc, one_mul
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
r_ne_zero : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
⊢ Ne.{u_1 + 1} (α := 𝕜) (↑‖z‖ : 𝕜) 0

Tactic:
simp only [z_zero, RCLike.ofReal_eq_zero, norm_eq_zero, Ne, not_false_iff]

Premises used: norm_eq_zero, Ne, RCLike.ofReal_eq_zero, not_false_iff
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
r_ne_zero : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
⊢ (f : (a : E) → 𝕜) z = HMul.hMul (β := 𝕜) (HDiv.hDiv (α := 𝕜) (↑‖z‖ : 𝕜) (↑r : 𝕜)) ((f : (a : E) → 𝕜) z₁ : 𝕜)

Tactic:
have eq : f z = ‖z‖ / r * f z₁ := by
    rw [hz₁, map_smul, smul_eq_mul]
    rw [← mul_assoc, ← mul_assoc, div_mul_cancel₀ _ r_ne_zero, mul_inv_cancel₀, one_mul]
    simp only [z_zero, RCLike.ofReal_eq_zero, norm_eq_zero, Ne, not_false_iff]
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
r_ne_zero : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
eq : (f : (a : E) → 𝕜) z = HMul.hMul (β := 𝕜) (HDiv.hDiv (α := 𝕜) (↑‖z‖ : 𝕜) (↑r : 𝕜)) ((f : (a : E) → 𝕜) z₁ : 𝕜)
neg : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) * ‖z‖ / r ≤ c * ‖z‖ / r
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c / r * ‖z‖

Tactic:
rw [eq, norm_mul, norm_div, RCLike.norm_coe_norm, RCLike.norm_of_nonneg r_pos.le,
    div_mul_eq_mul_div, div_mul_eq_mul_div, mul_comm]

Premises used: LT.lt.le, norm_mul, div_mul_eq_mul_div, norm_div, mul_comm, RCLike.norm_coe_norm, RCLike.norm_of_nonneg
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
r_ne_zero : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
eq : (f : (a : E) → 𝕜) z = HMul.hMul (β := 𝕜) (HDiv.hDiv (α := 𝕜) (↑‖z‖ : 𝕜) (↑r : 𝕜)) ((f : (a : E) → 𝕜) z₁ : 𝕜)
apply : 0 ≤ c * ‖z‖
apply₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) * ‖z‖ ≤ c * ‖z‖
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) * ‖z‖ / r ≤ c * ‖z‖ / r

Tactic:
apply div_le_div₀ _ _ r_pos rfl.ge

Premises used: div_le_div₀, Eq.ge, rfl
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
r_ne_zero : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
eq : (f : (a : E) → 𝕜) z = HMul.hMul (β := 𝕜) (HDiv.hDiv (α := 𝕜) (↑‖z‖ : 𝕜) (↑r : 𝕜)) ((f : (a : E) → 𝕜) z₁ : 𝕜)
⊢ 0 ≤ c * ‖z‖

Tactic:
mul_nonneg ((norm_nonneg _).trans norm_f_z₁) (norm_nonneg z)

Premises used: mul_nonneg, LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
r_ne_zero : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
eq : (f : (a : E) → 𝕜) z = HMul.hMul (β := 𝕜) (HDiv.hDiv (α := 𝕜) (↑‖z‖ : 𝕜) (↑r : 𝕜)) ((f : (a : E) → 𝕜) z₁ : 𝕜)
⊢ 0 ≤ c * ‖z‖

Tactic:
exact mul_nonneg ((norm_nonneg _).trans norm_f_z₁) (norm_nonneg z)

Premises used: mul_nonneg, LE.le.trans, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (sphere 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
z_zero : ¬z = 0
z₁ : E := HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
hz₁ : z₁ = HMul.hMul (α := 𝕜) (↑r : 𝕜) (↑‖z‖ : 𝕜)⁻¹ • z
norm_f_z₁ : norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) ≤ c
r_ne_zero : Ne.{u_1 + 1} (α := 𝕜) (↑r : 𝕜) 0
eq : (f : (a : E) → 𝕜) z = HMul.hMul (β := 𝕜) (HDiv.hDiv (α := 𝕜) (↑‖z‖ : 𝕜) (↑r : 𝕜)) ((f : (a : E) → 𝕜) z₁ : 𝕜)
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z₁ : 𝕜) * ‖z‖ ≤ c * ‖z‖

Tactic:
apply mul_le_mul norm_f_z₁ rfl.le (norm_nonneg z) ((norm_nonneg _).trans norm_f_z₁)

Premises used: Eq.le, mul_le_mul, LE.le.trans, norm_nonneg, rfl
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : E →ₗ[𝕜] 𝕜
h : ∀ (z : E), Membership.mem (γ := Set E) (closedBall 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
z : E
⊢ norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c / r * ‖z‖

Tactic:
f.bound_of_sphere_bound r_pos c (fun z hz => h z hz.le) z

Premises used: Eq.le, LinearMap.bound_of_sphere_bound
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : StrongDual 𝕜 E
h : ∀ (z : E), Membership.mem (γ := Set E) (closedBall 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
hMp : 0 ≤ c / r
hM : ∀ (x : E), norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) x : 𝕜) ≤ c / r * ‖x‖
⊢ ‖f‖ ≤ c / r

Tactic:
apply ContinuousLinearMap.opNorm_le_bound

Premises used: ContinuousLinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : StrongDual 𝕜 E
h : ∀ (z : E), Membership.mem (γ := Set E) (closedBall 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
apply : 0 ≤ c
⊢ 0 ≤ c / r

Tactic:
apply div_nonneg _ r_pos.le

Premises used: LT.lt.le, div_nonneg
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : StrongDual 𝕜 E
h : ∀ (z : E), Membership.mem (γ := Set E) (closedBall 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
⊢ Membership.mem (γ := Set E) (closedBall 0 r) 0

Tactic:
simp only [norm_zero, mem_closedBall, dist_zero_left, r_pos.le]

Premises used: norm_zero, LT.lt.le, dist_zero_left, Metric.mem_closedBall
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : StrongDual 𝕜 E
h : ∀ (z : E), Membership.mem (γ := Set E) (closedBall 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
⊢ 0 ≤ c

Tactic:
exact
      (norm_nonneg _).trans
        (h 0 (by simp only [norm_zero, mem_closedBall, dist_zero_left, r_pos.le]))

Premises used: LE.le.trans, OfNat.ofNat, norm_nonneg
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : StrongDual 𝕜 E
h : ∀ (z : E), Membership.mem (γ := Set E) (closedBall 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
hM :
  ∀ (z : E),
    Membership.mem (γ := Set E) (closedBall 0 r) z → norm.{u_1} (E := 𝕜) (((↑f : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) z : 𝕜) ≤ c
⊢ ∀ (x : E), norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) x : 𝕜) ≤ c / r * ‖x‖

Tactic:
apply LinearMap.bound_of_ball_bound' r_pos

Premises used: LinearMap.bound_of_ball_bound'
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : StrongDual 𝕜 E
h : ∀ (z : E), Membership.mem (γ := Set E) (closedBall 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
⊢ ∀ (z : E),
    Membership.mem (γ := Set E) (closedBall 0 r) z → norm.{u_1} (E := 𝕜) (((↑f : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) z : 𝕜) ≤ c

Tactic:
fun z hz => h z hz
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
r : ℝ
r_pos : 0 < r
c : ℝ
f : StrongDual 𝕜 E
h : ∀ (z : E), Membership.mem (γ := Set E) (closedBall 0 r) z → norm.{u_1} (E := 𝕜) ((f : (a : E) → 𝕜) z : 𝕜) ≤ c
⊢ ∀ (z : E),
    Membership.mem (γ := Set E) (closedBall 0 r) z → norm.{u_1} (E := 𝕜) (((↑f : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) z : 𝕜) ≤ c

Tactic:
exact fun z hz => h z hz
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
𝓕 : Type u_3
E : Type u_4
F : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
inst_5 : FunLike 𝓕 E F
inst_6 : AddMonoidHomClass 𝓕 E F
inst_7 : MulActionHomClass 𝓕 𝕜 E F
f : 𝓕
K : NNReal
h : ∀ (x : E), ‖x‖ = 1 → 1 ≤ (↑K : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
x : E
inl : norm.{u_4} (E := E) 0 ≤ (↑K : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) 0 : F)
inr : ∀ (hx : x ≠ 0), ‖x‖ ≤ (↑K : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ ‖x‖ ≤ (↑K : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
obtain rfl | hx := eq_or_ne x 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
𝓕 : Type u_3
E : Type u_4
F : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
inst_5 : FunLike 𝓕 E F
inst_6 : AddMonoidHomClass 𝓕 E F
inst_7 : MulActionHomClass 𝓕 𝕜 E F
f : 𝓕
K : NNReal
h : ∀ (x : E), ‖x‖ = 1 → 1 ≤ (↑K : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
⊢ norm.{u_4} (E := E) 0 ≤ (↑K : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) 0 : F)

Tactic:
simp
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
𝓕 : Type u_3
E : Type u_4
F : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedSpace 𝕜 E
inst_4 : NormedSpace 𝕜 F
inst_5 : FunLike 𝓕 E F
inst_6 : AddMonoidHomClass 𝓕 E F
inst_7 : MulActionHomClass 𝓕 𝕜 E F
f : 𝓕
K : NNReal
h : ∀ (x : E), ‖x‖ = 1 → 1 ≤ (↑K : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)
x : E
hx : x ≠ 0
⊢ ‖x‖ ≤ (↑K : ℝ) * norm.{u_5} (E := F) ((f : (a : E) → F) x : F)

Tactic:
simpa [norm_smul, field] using h ((‖x‖⁻¹ : 𝕜) • x) (norm_smul_inv_norm hx)

Premises used: Norm.norm, norm_smul, norm_smul_inv_norm, RCLike.ofReal, Inv.inv, HSMul.hSMul
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Basic
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : Nontrivial E
r : ℝ
hr : 0 ≤ r
⊢ Nonempty.{u_2 + 1} (↑(sphere 0 r) : Type u_2)

Tactic:
letI : NormedSpace ℝ E := NormedSpace.restrictScalars ℝ 𝕜 E
  (NormedSpace.sphere_nonempty.mpr hr).coe_sort

Premises used: Iff.mpr, Set.Nonempty.coe_sort, NormedSpace.sphere_nonempty
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Extend
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
set :
  let lm : StrongDual 𝕜 F := fr.extendRCLike;
  norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) ≤ ‖fr‖ * ‖x‖
⊢ norm.{u_1} (E := 𝕜) ((fr.extendRCLike : (a : F) → 𝕜) x : 𝕜) ≤ ‖fr‖ * ‖x‖

Tactic:
set lm : StrongDual 𝕜 F := fr.extendRCLike

Premises used: StrongDual.extendRCLike, StrongDual
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Extend
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
lm : StrongDual 𝕜 F := fr.extendRCLike
pos :
  ∀ (h : Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)),
    norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) ≤ ‖fr‖ * ‖x‖
neg :
  ∀ (h : ¬Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)),
    norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) ≤ ‖fr‖ * ‖x‖
⊢ norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) ≤ ‖fr‖ * ‖x‖

Tactic:
by_cases h : lm x = 0

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Extend
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
lm : StrongDual 𝕜 F := fr.extendRCLike
h : Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)
pos : 0 ≤ ‖fr‖ * ‖x‖
⊢ norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) ≤ ‖fr‖ * ‖x‖

Tactic:
rw [h, norm_zero]

Premises used: norm_zero
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Extend
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
lm : StrongDual 𝕜 F := fr.extendRCLike
h : Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ 0 ≤ ‖fr‖ * ‖x‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Extend
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
lm : StrongDual 𝕜 F := fr.extendRCLike
h : ¬Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)
neg :
  HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜)) 2 ≤
    norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)
⊢ norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) ≤ ‖fr‖ * ‖x‖

Tactic:
rw [← mul_le_mul_iff_right₀ (norm_pos_iff.2 h), ← sq]

Premises used: Iff.mpr, norm_pos_iff, sq, mul_le_mul_iff_right₀
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Extend
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
lm : StrongDual 𝕜 F := fr.extendRCLike
h : ¬Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜)) 2 =
    (fr : (a : F) → ℝ) (HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) : 𝕜) x)

Tactic:
Module.Dual.norm_extendRCLike_apply_sq fr.toLinearMap x

Premises used: Module.Dual.norm_extendRCLike_apply_sq, ContinuousLinearMap.toLinearMap
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Extend
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
lm : StrongDual 𝕜 F := fr.extendRCLike
h : ¬Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ (fr : (a : F) → ℝ) (HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) : 𝕜) x) ≤
    norm (E := ℝ)
      ((fr : (a : F) → ℝ) (HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) : 𝕜) x) : ℝ)

Tactic:
le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Extend
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
lm : StrongDual 𝕜 F := fr.extendRCLike
h : ¬Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)
⊢ norm (E := ℝ)
      ((fr : (a : F) → ℝ) (HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) : 𝕜) x) : ℝ) ≤
    ‖fr‖ * ‖HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) : 𝕜) x‖

Tactic:
le_opNorm _ _

Premises used: ContinuousLinearMap.le_opNorm
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Extend
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
lm : StrongDual 𝕜 F := fr.extendRCLike
h : ¬Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)
rw :
  ‖fr‖ * (norm (E := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) : 𝕜) * ‖x‖) =
    norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)
rw₁ :
  ‖fr‖ * (norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * ‖x‖) =
    norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)
rw₂ rw₃ :
  norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖) =
    norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)
⊢ ‖fr‖ * ‖HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) : 𝕜) x‖ =
    norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)

Tactic:
rw [norm_smul, norm_conj, mul_left_comm]

Premises used: norm_smul, RCLike.norm_conj, mul_left_comm
-- Module: Mathlib.Analysis.Normed.Module.RCLike.Extend
Goal:
𝕜 : Type u_1
F : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedSpace ℝ F
inst_4 : IsScalarTower ℝ 𝕜 F
fr : StrongDual ℝ F
x : F
lm : StrongDual 𝕜 F := fr.extendRCLike
h : ¬Eq.{u_1 + 1} (α := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) (0 : 𝕜)
fr₁ :
  ‖fr‖ * ‖HSMul.hSMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) : 𝕜) x‖ =
    norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)
⊢ HPow.hPow (β := ℕ) (norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜)) 2 ≤
    norm.{u_1} (E := 𝕜) ((lm : (a : F) → 𝕜) x : 𝕜) * (‖fr‖ * ‖x‖)

Tactic:
calc
    ‖lm x‖ ^ 2 = fr (conj (lm x : 𝕜) • x) := Module.Dual.norm_extendRCLike_apply_sq fr.toLinearMap x
    _ ≤ ‖fr (conj (lm x : 𝕜) • x)‖ := le_abs_self _
    _ ≤ ‖fr‖ * ‖conj (lm x : 𝕜) • x‖ := le_opNorm _ _
    _ = ‖(lm x : 𝕜)‖ * (‖fr‖ * ‖x‖) := by rw [norm_smul, norm_conj, mul_left_comm]

Premises used: Norm.norm, le_abs_self, HMul.hMul, ContinuousLinearMap.le_opNorm, Module.Dual.norm_extendRCLike_apply_sq, ContinuousLinearMap.toLinearMap, HSMul.hSMul, starRingEnd, DFunLike.coe