awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Completion
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : Completion E
c : 𝕜
a b : E
⊢ ⟪HSMul.hSMul (β := Completion E) c (↑a : Completion E), (↑b : Completion E)⟫ =
    HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) c : 𝕜)
      (inner 𝕜 (E := Completion E) (↑a : Completion E) (↑b : Completion E))

Tactic:
simp only [← coe_smul c a, inner_coe, inner_smul_left]

Premises used: UniformSpace.Completion.coe_smul, UniformSpace.Completion.inner_coe, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →L[ℝ] F
mp :
  IsConformalMap f →
    ∃ (c : ℝ),
      0 < c ∧ ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * ⟪u, v⟫
mpr :
  (∃ (c : ℝ),
      0 < c ∧ ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * ⟪u, v⟫) →
    IsConformalMap f
⊢ IsConformalMap f ↔
    ∃ (c : ℝ),
      0 < c ∧ ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * ⟪u, v⟫

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
c₁ : ℝ
hc₁ : c₁ ≠ 0
li : E →ₗᵢ[ℝ] F
⊢ ∃ (c : ℝ),
    0 < c ∧
      ∀ (u v : E),
        inner.{0, u_2} ℝ (E := F) ((c₁ • li.toContinuousLinearMap : (a : E) → F) u : F)
            ((c₁ • li.toContinuousLinearMap : (a : E) → F) v : F) =
          c * ⟪u, v⟫

Tactic:
⟨c₁ * c₁, mul_self_pos.2 hc₁, fun u v => ?_⟩

Premises used: Iff.mpr, HMul.hMul, mul_self_pos, And.intro, Exists.intro
-- Module: Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
c₁ : ℝ
hc₁ : c₁ ≠ 0
li : E →ₗᵢ[ℝ] F
mp :
  ∀ (u v : E),
    inner.{0, u_2} ℝ (E := F) ((c₁ • li.toContinuousLinearMap : (a : E) → F) u : F)
        ((c₁ • li.toContinuousLinearMap : (a : E) → F) v : F) =
      c₁ * c₁ * ⟪u, v⟫
⊢ ∃ (c : ℝ),
    0 < c ∧
      ∀ (u v : E),
        inner.{0, u_2} ℝ (E := F) ((c₁ • li.toContinuousLinearMap : (a : E) → F) u : F)
            ((c₁ • li.toContinuousLinearMap : (a : E) → F) v : F) =
          c * ⟪u, v⟫

Tactic:
refine ⟨c₁ * c₁, mul_self_pos.2 hc₁, fun u v => ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
c₁ : ℝ
hc₁ : c₁ ≠ 0
li : E →ₗᵢ[ℝ] F
u v : E
⊢ inner.{0, u_2} ℝ (E := F) ((c₁ • li.toContinuousLinearMap : (a : E) → F) u : F)
      ((c₁ • li.toContinuousLinearMap : (a : E) → F) v : F) =
    c₁ * c₁ * ⟪u, v⟫

Tactic:
simp only [real_inner_smul_left, real_inner_smul_right, mul_assoc, coe_smul',
      coe_toContinuousLinearMap, Pi.smul_apply, inner_map_map]

Premises used: ContinuousLinearMap.coe_smul', LinearIsometry.coe_toContinuousLinearMap, mul_assoc, LinearIsometry.inner_map_map, real_inner_smul_right, real_inner_smul_left, Pi.smul_apply
-- Module: Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →L[ℝ] F
c₁ : ℝ
hc₁ : 0 < c₁
huv : ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c₁ * ⟪u, v⟫
⊢ ∃ (c : ℝ), 0 < c ∧ c₁ = c * c

Tactic:
⟨√c₁, Real.sqrt_pos.2 hc₁, (Real.mul_self_sqrt hc₁.le).symm⟩

Premises used: Iff.mpr, Real.mul_self_sqrt, LT.lt.le, Real.sqrt_pos, And.intro, Exists.intro, Real.sqrt, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →L[ℝ] F
c₁ : ℝ
hc₁ : 0 < c₁
huv : ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c₁ * ⟪u, v⟫
mpr :
  ∀ (c : ℝ) (hc : 0 < c) (hc₁ : 0 < c * c)
    (huv : ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * c * ⟪u, v⟫),
    IsConformalMap f
⊢ IsConformalMap f

Tactic:
obtain ⟨c, hc, rfl⟩ : ∃ c : ℝ, 0 < c ∧ c₁ = c * c :=
      ⟨√c₁, Real.sqrt_pos.2 hc₁, (Real.mul_self_sqrt hc₁.le).symm⟩

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * c * ⟪u, v⟫
⊢ IsConformalMap f

Tactic:
⟨c, hc.ne', (c⁻¹ • f : E →ₗ[ℝ] F).isometryOfInner fun u v => ?_, ?_⟩

Premises used: ContinuousLinearMap.toLinearMap, LinearMap.isometryOfInner, LT.lt.ne', Inv.inv, And.intro, Exists.intro, HSMul.hSMul, IsConformalMap
-- Module: Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * c * ⟪u, v⟫
mpr :
  ∀ (u v : E),
    inner.{0, u_2} ℝ (E := F) ((c⁻¹ • (↑f : E →ₗ[ℝ] F) : (a : E) → F) u : F)
        ((c⁻¹ • (↑f : E →ₗ[ℝ] F) : (a : E) → F) v : F) =
      ⟪u, v⟫
mpr₁ : f = HSMul.hSMul (β := E →L[ℝ] F) c (toContinuousLinearMap ((c⁻¹ • (↑f : E →ₗ[ℝ] F)).isometryOfInner ⋯))
⊢ IsConformalMap f

Tactic:
refine ⟨c, hc.ne', (c⁻¹ • f : E →ₗ[ℝ] F).isometryOfInner fun u v => ?_, ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * c * ⟪u, v⟫
u v : E
⊢ inner.{0, u_2} ℝ (E := F) ((c⁻¹ • (↑f : E →ₗ[ℝ] F) : (a : E) → F) u : F)
      ((c⁻¹ • (↑f : E →ₗ[ℝ] F) : (a : E) → F) v : F) =
    ⟪u, v⟫

Tactic:
simp only [real_inner_smul_left, real_inner_smul_right, huv, mul_assoc,
        inv_mul_cancel_left₀ hc.ne', LinearMap.smul_apply, ContinuousLinearMap.coe_coe]

Premises used: LinearMap.smul_apply, inv_mul_cancel_left₀, mul_assoc, ContinuousLinearMap.coe_coe, real_inner_smul_right, LT.lt.ne', real_inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * c * ⟪u, v⟫
mpr :
  ∀ (x : E),
    Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x : F)
      ((HSMul.hSMul (β := E →L[ℝ] F) c (toContinuousLinearMap ((c⁻¹ • (↑f : E →ₗ[ℝ] F)).isometryOfInner ⋯)) :
            (a : E) → F)
          x :
        F)
⊢ f = HSMul.hSMul (β := E →L[ℝ] F) c (toContinuousLinearMap ((c⁻¹ • (↑f : E →ₗ[ℝ] F)).isometryOfInner ⋯))

Tactic:
ext1 x
-- Module: Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * c * ⟪u, v⟫
x : E
⊢ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x : F)
    ((HSMul.hSMul (β := E →L[ℝ] F) c (toContinuousLinearMap ((c⁻¹ • (↑f : E →ₗ[ℝ] F)).isometryOfInner ⋯)) : (a : E) → F)
        x :
      F)

Tactic:
(smul_inv_smul₀ hc.ne' (f x)).symm

Premises used: smul_inv_smul₀, LT.lt.ne', Eq.symm, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.ConformalLinearMap
Goal:
E : Type u_1
F : Type u_2
inst : NormedAddCommGroup E
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace ℝ E
inst_3 : InnerProductSpace ℝ F
f : E →L[ℝ] F
c : ℝ
hc : 0 < c
hc₁ : 0 < c * c
huv : ∀ (u v : E), inner.{0, u_2} ℝ (E := F) ((f : (a : E) → F) u : F) ((f : (a : E) → F) v : F) = c * c * ⟪u, v⟫
x : E
⊢ Eq.{u_2 + 1} (α := F) ((f : (a : E) → F) x : F)
    ((HSMul.hSMul (β := E →L[ℝ] F) c (toContinuousLinearMap ((c⁻¹ • (↑f : E →ₗ[ℝ] F)).isometryOfInner ⋯)) : (a : E) → F)
        x :
      F)

Tactic:
exact (smul_inv_smul₀ hc.ne' (f x)).symm

Premises used: smul_inv_smul₀, LT.lt.ne', Eq.symm, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
inst_4 : IsScalarTower ℝ 𝕜 E
r : ℝ
x y : E
⊢ ⟪(r • x, y).1, (r • x, y).2⟫ = r • ⟪(x, y).1, (x, y).2⟫

Tactic:
simp only [← algebraMap_smul 𝕜 r x, algebraMap_eq_ofReal, inner_smul_real_left]

Premises used: RCLike.algebraMap_eq_ofReal, algebraMap_smul, inner_smul_real_left
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
inst_4 : IsScalarTower ℝ 𝕜 E
r : ℝ
x y : E
⊢ ⟪(x, r • y).1, (x, r • y).2⟫ = r • ⟪(x, y).1, (x, y).2⟫

Tactic:
simp only [← algebraMap_smul 𝕜 r y, algebraMap_eq_ofReal, inner_smul_real_right]

Premises used: RCLike.algebraMap_eq_ofReal, algebraMap_smul, inner_smul_real_right
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
inst_4 : IsScalarTower ℝ 𝕜 E
x y : E
rw : ‖⟪(x, y).1, (x, y).2⟫‖ ≤ ‖x‖ * ‖y‖
⊢ ‖⟪(x, y).1, (x, y).2⟫‖ ≤ 1 * ‖x‖ * ‖y‖

Tactic:
rw [one_mul]

Premises used: one_mul
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
inst_4 : IsScalarTower ℝ 𝕜 E
x y : E
⊢ ‖⟪(x, y).1, (x, y).2⟫‖ ≤ ‖x‖ * ‖y‖

Tactic:
norm_inner_le_norm x y

Premises used: norm_inner_le_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedSpace ℝ E
inst_4 : IsScalarTower ℝ 𝕜 E
x y : E
⊢ ‖⟪(x, y).1, (x, y).2⟫‖ ≤ ‖x‖ * ‖y‖

Tactic:
exact norm_inner_le_norm x y

Premises used: norm_inner_le_norm
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Continuous[instTopologicalSpaceProd, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun (p : E × E) ↦ ⟪p.1, p.2⟫

Tactic:
letI : InnerProductSpace ℝ E := InnerProductSpace.rclikeToReal 𝕜 E
  haveI := IsScalarTower.restrictScalars ℝ 𝕜 E
  isBoundedBilinearMap_inner.continuous

Premises used: IsBoundedBilinearMap.continuous, isBoundedBilinearMap_inner
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
α : Type u_4
f g : α → E
l : Filter α
x y : E
hf : Tendsto f l (𝓝 x)
hg : Tendsto g l (𝓝 y)
⊢ Tendsto (fun (t : α) ↦ ⟪f t, g t⟫) l (𝓝 ⟪x, y⟫)

Tactic:
(continuous_inner.tendsto _).comp (hf.prodMk_nhds hg)

Premises used: continuous_inner, Continuous.tendsto, Filter.Tendsto.comp, Filter.Tendsto.prodMk_nhds
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
α : Type u_4
inst_3 : TopologicalSpace α
f g : α → E
x : α
s : Set α
hf : ContinuousWithinAt f s x
hg : ContinuousWithinAt g s x
⊢ ContinuousWithinAt.{u_4, u_1} (Y := 𝕜) (fun (t : α) ↦ ⟪f t, g t⟫) s x

Tactic:
Filter.Tendsto.inner hf hg

Premises used: ContinuousWithinAt, Filter.Tendsto.inner
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
α : Type u_4
inst_3 : TopologicalSpace α
f g : α → E
x : α
hf : ContinuousAt f x
hg : ContinuousAt g x
⊢ ContinuousAt.{u_4, u_1} (Y := 𝕜) (fun (t : α) ↦ ⟪f t, g t⟫) x

Tactic:
Filter.Tendsto.inner hf hg

Premises used: ContinuousAt, Filter.Tendsto.inner
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
α : Type u_4
inst_3 : TopologicalSpace α
f g : α → E
s : Set α
hf : ContinuousOn f s
hg : ContinuousOn g s
⊢ ContinuousOn.{u_4, u_1} (Y := 𝕜) (fun (t : α) ↦ ⟪f t, g t⟫) s

Tactic:
fun x hx => (hf x hx).inner (hg x hx)

Premises used: ContinuousOn, ContinuousWithinAt.inner
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
α : Type u_4
inst_3 : TopologicalSpace α
f g : α → E
hf : Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
hg : Continuous[inst_3, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] g
_x : α
⊢ ContinuousAt.{u_4, u_1} (Y := 𝕜) (fun (t : α) ↦ ⟪f t, g t⟫) _x

Tactic:
fun_prop
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = 0
K : Submodule 𝕜 E := span 𝕜 S
⊢ Dense (↑K : Set E)

Tactic:
have hK : Dense (K : Set E) := hS.mono subset_span
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = 0
K : Submodule 𝕜 E := span 𝕜 S
hK : Dense (↑K : Set E)
v : E
⊢ ⟪x, id 0⟫ = 0 0

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = 0
K : Submodule 𝕜 E := span 𝕜 S
hK : Dense (↑K : Set E)
v : E
⊢ ∀ (x_1 y : E) (hx : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 S) x_1)
    (hy : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 S) y),
    ⟪x, id x_1⟫ = 0 x_1 → ⟪x, id y⟫ = 0 y → ⟪x, id (x_1 + y)⟫ = 0 (x_1 + y)

Tactic:
simp +contextual [inner_add_right]

Premises used: inner_add_right
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = 0
K : Submodule 𝕜 E := span 𝕜 S
hK : Dense (↑K : Set E)
v : E
⊢ ∀ (a : 𝕜) (x_1 : E) (hx : Membership.mem (γ := Submodule 𝕜 E) (span 𝕜 S) x_1),
    ⟪x, id x_1⟫ = 0 x_1 → ⟪x, id (a • x_1)⟫ = 0 (a • x_1)

Tactic:
simp +contextual [inner_smul_right]

Premises used: inner_smul_right
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = 0
K : Submodule 𝕜 E := span 𝕜 S
hK : Dense (↑K : Set E)
⊢ Eq (α := E → 𝕜) (fun (x_1 : E) ↦ ⟪x, x_1⟫) 0

Tactic:
have : (⟪x, ·⟫) = 0 := (continuous_const.inner continuous_id).ext_on
    hK continuous_const fun v ↦ Submodule.span_induction h (by simp)
      (by simp +contextual [inner_add_right]) (by simp +contextual [inner_smul_right])
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = 0
K : Submodule 𝕜 E := span 𝕜 S
hK : Dense (↑K : Set E)
this : Eq (α := E → 𝕜) (fun (x_1 : E) ↦ ⟪x, x_1⟫) 0
⊢ x = 0

Tactic:
simpa using congr_fun this x

Premises used: congr_fun
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪v, x⟫ = 0
v : E
hv : v ∈ S
rw! : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪v, x⟫ : 𝕜) (0 : 𝕜)
⊢ ⟪x, v⟫ = 0

Tactic:
rw! [← inner_conj_symm]

Premises used: inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪v, x⟫ = 0
v : E
hv : v ∈ S
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪v, x⟫ : 𝕜) (0 : 𝕜)

Tactic:
simp [-inner_conj_symm, h, hv]

Premises used: inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = ⟪y, v⟫
rw : x - y = 0
⊢ x = y

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = ⟪y, v⟫
⊢ ∀ v ∈ S, ⟪x - y, v⟫ = 0

Tactic:
simpa [inner_sub_left, sub_eq_zero]

Premises used: sub_eq_zero, inner_sub_left
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪x, v⟫ = ⟪y, v⟫
⊢ x - y = 0

Tactic:
exact hS.eq_zero_of_inner_left 𝕜 (by simpa [inner_sub_left, sub_eq_zero])

Premises used: Dense.eq_zero_of_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪v, x⟫ = ⟪v, y⟫
rw : x - y = 0
⊢ x = y

Tactic:
rw [← sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪v, x⟫ = ⟪v, y⟫
⊢ ∀ v ∈ S, ⟪v, x - y⟫ = 0

Tactic:
simpa [inner_sub_right, sub_eq_zero]

Premises used: sub_eq_zero, inner_sub_right
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
S : Set E
hS : Dense S
h : ∀ v ∈ S, ⟪v, x⟫ = ⟪v, y⟫
⊢ x - y = 0

Tactic:
exact hS.eq_zero_of_inner_right 𝕜 (by simpa [inner_sub_right, sub_eq_zero])

Premises used: Dense.eq_zero_of_inner_right
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
ι : Type u_6
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
f : ι → E
hf : DenseRange f
h : ∀ (i : ι), ⟪x, f i⟫ = ⟪y, f i⟫
⊢ ∀ v ∈ Set.range f, ⟪x, v⟫ = ⟪y, v⟫

Tactic:
simpa
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
ι : Type u_6
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
f : ι → E
hf : DenseRange f
h : ∀ (i : ι), ⟪f i, x⟫ = ⟪f i, y⟫
⊢ ∀ v ∈ Set.range f, ⟪v, x⟫ = ⟪v, y⟫

Tactic:
simpa
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
ι : Type u_6
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
f : ι → E
hf : DenseRange f
h : ∀ (i : ι), ⟪x, f i⟫ = 0
⊢ ∀ v ∈ Set.range f, ⟪x, v⟫ = 0

Tactic:
simpa
-- Module: Mathlib.Analysis.InnerProductSpace.Continuous
Goal:
E : Type u_4
ι : Type u_6
𝕜 : Type u_7
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
f : ι → E
hf : DenseRange f
h : ∀ (i : ι), ⟪f i, x⟫ = 0
⊢ ∀ v ∈ Set.range f, ⟪v, x⟫ = 0

Tactic:
simpa
-- Module: Mathlib.Analysis.InnerProductSpace.Convex
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : F⦄, ‖x‖ = 1 → ∀ ⦃y : F⦄, ‖y‖ = 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ

Tactic:
⟨2 - √(4 - ε ^ 2), sub_pos_of_lt <| (sqrt_lt' zero_lt_two).2 ?_, fun x hx y hy hxy => ?_⟩

Premises used: Iff.mpr, HSub.hSub, Real.sqrt_lt', HPow.hPow, And.intro, Exists.intro, Real.sqrt, zero_lt_two, OfNat.ofNat, sub_pos_of_lt
-- Module: Mathlib.Analysis.InnerProductSpace.Convex
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
refine_1 : 4 - HPow.hPow (β := ℕ) ε 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2
refine_2 :
  ∀ (x : F) (hx : ‖x‖ = 1) (y : F) (hy : ‖y‖ = 1) (hxy : ε ≤ ‖x - y‖), ‖x + y‖ ≤ 2 - (2 - √(4 - HPow.hPow (β := ℕ) ε 2))
⊢ ∃ (δ : ℝ), 0 < δ ∧ ∀ ⦃x : F⦄, ‖x‖ = 1 → ∀ ⦃y : F⦄, ‖y‖ = 1 → ε ≤ ‖x - y‖ → ‖x + y‖ ≤ 2 - δ

Tactic:
refine
      ⟨2 - √(4 - ε ^ 2), sub_pos_of_lt <| (sqrt_lt' zero_lt_two).2 ?_, fun x hx y hy hxy => ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Convex
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
refine_1 : 0 < HPow.hPow (β := ℕ) ε 2
⊢ 4 - HPow.hPow (β := ℕ) ε 2 < HPow.hPow (α := ℝ) (β := ℕ) 2 2

Tactic:
norm_num
-- Module: Mathlib.Analysis.InnerProductSpace.Convex
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
⊢ 0 < HPow.hPow (β := ℕ) ε 2

Tactic:
pow_pos hε _

Premises used: pow_pos
-- Module: Mathlib.Analysis.InnerProductSpace.Convex
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
⊢ 0 < HPow.hPow (β := ℕ) ε 2

Tactic:
exact pow_pos hε _

Premises used: pow_pos
-- Module: Mathlib.Analysis.InnerProductSpace.Convex
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
refine_2 : ‖x + y‖ ≤ √(4 - HPow.hPow (β := ℕ) ε 2)
⊢ ‖x + y‖ ≤ 2 - (2 - √(4 - HPow.hPow (β := ℕ) ε 2))

Tactic:
rw [sub_sub_cancel]

Premises used: sub_sub_cancel
-- Module: Mathlib.Analysis.InnerProductSpace.Convex
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
⊢ ‖x + y‖ ≤ √(4 - HPow.hPow (β := ℕ) ε 2)

Tactic:
le_sqrt_of_sq_le ?_

Premises used: Real.le_sqrt_of_sq_le
-- Module: Mathlib.Analysis.InnerProductSpace.Convex
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
ε : ℝ
hε : 0 < ε
x : F
hx : ‖x‖ = 1
y : F
hy : ‖y‖ = 1
hxy : ε ≤ ‖x - y‖
refine_2 : HPow.hPow (β := ℕ) ‖x + y‖ 2 ≤ 4 - HPow.hPow (β := ℕ) ε 2
⊢ ‖x + y‖ ≤ √(4 - HPow.hPow (β := ℕ) ε 2)

Tactic:
refine le_sqrt_of_sq_le ?_

Premises used: Real.le_sqrt_of_sq_le