awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x y : E
⊢ (((innerSLFlip 𝕜 : (a : E) → E →L⋆[𝕜] 𝕜) x : E →L⋆[𝕜] 𝕜) : (a : E) → 𝕜) y = ⟪y, x⟫

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
h :
  ∀ (v w : F),
    Eq (α := ℝ) ((((ContinuousLinearMap.flip (innerSL ℝ) : (a : F) → F →L⋆[ℝ] ℝ) v : F →L⋆[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
      ((((innerSL ℝ : (a : F) → F →L⋆[ℝ] ℝ) v : F →L⋆[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
⊢ Eq.{u_3 + 1} (α := F →L[ℝ] F →L⋆[ℝ] ℝ) (ContinuousLinearMap.flip (innerSL ℝ)) (innerSL ℝ)

Tactic:
ext v w
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
⊢ Eq (α := ℝ) ((((ContinuousLinearMap.flip (innerSL ℝ) : (a : F) → F →L⋆[ℝ] ℝ) v : F →L⋆[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
    ((((innerSL ℝ : (a : F) → F →L⋆[ℝ] ℝ) v : F →L⋆[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)

Tactic:
real_inner_comm _ _

Premises used: real_inner_comm
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
F : Type u_3
inst : SeminormedAddCommGroup F
inst_1 : InnerProductSpace ℝ F
v w : F
⊢ Eq (α := ℝ) ((((ContinuousLinearMap.flip (innerSL ℝ) : (a : F) → F →L⋆[ℝ] ℝ) v : F →L⋆[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)
    ((((innerSL ℝ : (a : F) → F →L⋆[ℝ] ℝ) v : F →L⋆[ℝ] ℝ) : (a : F) → ℝ) w : ℝ)

Tactic:
exact real_inner_comm _ _

Premises used: real_inner_comm
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_4
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
x : E'
⊢ Eq (α := E →L[𝕜] 𝕜)
    ((((toSesqForm : (a : E →L[𝕜] E') → E' →L⋆[𝕜] E →L[𝕜] 𝕜) f : E' →L⋆[𝕜] E →L[𝕜] 𝕜) : (a : E') → E →L[𝕜] 𝕜) x :
      E →L[𝕜] 𝕜)
    (comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : E') → E' →L[𝕜] 𝕜) x) f : E →L[𝕜] 𝕜)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, LinearMap.mkContinuousOfExistsBound, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_4
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
⊢ 0 ≤ ‖f‖ * ‖v‖

Tactic:
positivity
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_4
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
refine :
  ∀ (x : E),
    Norm.norm.{u_1} (E := 𝕜)
        ((((((toSesqForm : (a : E →L[𝕜] E') → E' →L⋆[𝕜] E →L[𝕜] 𝕜) f : E' →L⋆[𝕜] E →L[𝕜] 𝕜) : (a : E') → E →L[𝕜] 𝕜) v :
                E →L[𝕜] 𝕜) :
              (a : E) → 𝕜)
            x :
          𝕜) ≤
      ‖f‖ * ‖v‖ * ‖x‖
⊢ Norm.norm (E := E →L[𝕜] 𝕜)
      ((((toSesqForm : (a : E →L[𝕜] E') → E' →L⋆[𝕜] E →L[𝕜] 𝕜) f : E' →L⋆[𝕜] E →L[𝕜] 𝕜) : (a : E') → E →L[𝕜] 𝕜) v :
        E →L[𝕜] 𝕜) ≤
    ‖f‖ * ‖v‖

Tactic:
refine opNorm_le_bound _ (by positivity) fun x ↦ ?_

Premises used: ContinuousLinearMap.opNorm_le_bound
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_4
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
⊢ Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E') ≤ ‖f‖ * ‖x‖

Tactic:
have h₁ : ‖f x‖ ≤ ‖f‖ * ‖x‖ := le_opNorm _ _
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_4
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
h₁ : Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E') ≤ ‖f‖ * ‖x‖
⊢ ‖⟪v, (f : (a : E) → E') x⟫‖ ≤ ‖v‖ * Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E')

Tactic:
have h₂ := @norm_inner_le_norm 𝕜 E' _ _ _ v (f x)
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_4
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
h₁ : Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E') ≤ ‖f‖ * ‖x‖
h₂ : ‖⟪v, (f : (a : E) → E') x⟫‖ ≤ ‖v‖ * Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E')
⊢ ‖⟪v, (f : (a : E) → E') x⟫‖ ≤ ‖v‖ * Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E')

Tactic:
h₂
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_4
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
h₁ : Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E') ≤ ‖f‖ * ‖x‖
h₂ : ‖⟪v, (f : (a : E) → E') x⟫‖ ≤ ‖v‖ * Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E')
ha : 0 ≤ ‖v‖
⊢ ‖v‖ * Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E') ≤ ‖v‖ * (‖f‖ * ‖x‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_4
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
h₁ : Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E') ≤ ‖f‖ * ‖x‖
h₂ : ‖⟪v, (f : (a : E) → E') x⟫‖ ≤ ‖v‖ * Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E')
⊢ ‖v‖ * (‖f‖ * ‖x‖) = ‖f‖ * ‖v‖ * ‖x‖

Tactic:
ring
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_4
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
h₁ : Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E') ≤ ‖f‖ * ‖x‖
h₂ : ‖⟪v, (f : (a : E) → E') x⟫‖ ≤ ‖v‖ * Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E')
f₁ : ‖v‖ * Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E') ≤ ‖v‖ * (‖f‖ * ‖x‖)
f₂ : ‖v‖ * (‖f‖ * ‖x‖) = ‖f‖ * ‖v‖ * ‖x‖
⊢ Norm.norm.{u_1} (E := 𝕜)
      ((((((toSesqForm : (a : E →L[𝕜] E') → E' →L⋆[𝕜] E →L[𝕜] 𝕜) f : E' →L⋆[𝕜] E →L[𝕜] 𝕜) : (a : E') → E →L[𝕜] 𝕜) v :
              E →L[𝕜] 𝕜) :
            (a : E) → 𝕜)
          x :
        𝕜) ≤
    ‖f‖ * ‖v‖ * ‖x‖

Tactic:
calc
    ‖⟪v, f x⟫‖ ≤ ‖v‖ * ‖f x‖ := h₂
    _ ≤ ‖v‖ * (‖f‖ * ‖x‖) := by gcongr
    _ = ‖f‖ * ‖v‖ * ‖x‖ := by ring

Premises used: Norm.norm, HMul.hMul, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) = ‖x‖

Tactic:
le_antisymm ((innerSL 𝕜 x).opNorm_le_bound (norm_nonneg _) fun y => norm_inner_le_norm _ _) ?_

Premises used: innerSL, ContinuousLinearMap.opNorm_le_bound, le_antisymm, DFunLike.coe, norm_nonneg, norm_inner_le_norm
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
le_antisymm : ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜)
⊢ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) = ‖x‖

Tactic:
refine
    le_antisymm ((innerSL 𝕜 x).opNorm_le_bound (norm_nonneg _) fun y => norm_inner_le_norm _ _) ?_

Premises used: innerSL, ContinuousLinearMap.opNorm_le_bound, le_antisymm, DFunLike.coe, norm_nonneg, norm_inner_le_norm
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
inl : ∀ (h : ‖x‖ = 0), ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜)
inr : ∀ (h : 0 < ‖x‖), ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜)
⊢ ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜)

Tactic:
rcases (norm_nonneg x).eq_or_lt' with (h | h)

Premises used: LE.le.eq_or_lt', norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
h : ‖x‖ = 0
⊢ ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜)

Tactic:
simp [h]
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
⊢ ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜)

Tactic:
(mul_le_mul_iff_left₀ h).mp ?_

Premises used: Iff.mp, mul_le_mul_iff_left₀
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
inr : ‖x‖ * ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) * ‖x‖
⊢ ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜)

Tactic:
refine (mul_le_mul_iff_left₀ h).mp ?_

Premises used: Iff.mp, mul_le_mul_iff_left₀
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
rw : HPow.hPow (β := ℕ) ‖x‖ 2 = ‖⟪x, x⟫‖
rw₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = ‖HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2‖
rw₂ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) (Norm.norm.{u_1} (E := 𝕜) (↑‖x‖ : 𝕜)) 2
rw₃ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) |‖x‖| 2
rw₄ rw₅ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2
⊢ ‖x‖ * ‖x‖ = ‖⟪x, x⟫‖

Tactic:
rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow, norm_ofReal, abs_norm]

Premises used: norm_pow, inner_self_eq_norm_sq_to_K, RCLike.norm_ofReal, sq, abs_norm
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
⊢ ‖⟪x, x⟫‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) * ‖x‖

Tactic:
(innerSL 𝕜 x).le_opNorm _

Premises used: innerSL, ContinuousLinearMap.le_opNorm, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
rw : ‖x‖ * ‖x‖ = ‖⟪x, x⟫‖
⊢ ‖x‖ * ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) * ‖x‖

Tactic:
calc
      ‖x‖ * ‖x‖ = ‖(⟪x, x⟫ : 𝕜)‖ := by
        rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow, norm_ofReal, abs_norm]
      _ ≤ ‖innerSL 𝕜 x‖ * ‖x‖ := (innerSL 𝕜 x).le_opNorm _

Premises used: innerSL, ContinuousLinearMap.le_opNorm, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ ∀ (x : E), Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) ≤ 1 * ‖x‖

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
G : Type u_4
inst : SeminormedAddCommGroup G
inst_1 : InnerProductSpace ℝ G
f : G ≃ₗᵢ[ℝ] ℂ
x y : G
rw : ⟪x, y⟫_ℝ = inner ℝ (E := ℂ) ((f : (a : G) → ℂ) x : ℂ) ((f : (a : G) → ℂ) y : ℂ)
rw₁ rw₂ : ⟪x, y⟫_ℝ = ⟪x, y⟫_ℝ
⊢ ⟪x, y⟫_ℝ =
    (HMul.hMul (α := ℂ) (β := ℂ) ((f : (a : G) → ℂ) y : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : G) → ℂ) x : ℂ) : ℂ)).re

Tactic:
rw [← Complex.inner, f.inner_map_map]

Premises used: Complex.inner, LinearIsometryEquiv.inner_map_map
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
⊢ T.reApplyInnerSelf x = (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → E) x, x⟫

Tactic:
rfl

Premises used: ContinuousLinearMap.reApplyInnerSelf, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, _] T.reApplyInnerSelf

Tactic:
reCLM.continuous.comp <| T.continuous.inner continuous_id

Premises used: Continuous.comp, RCLike.reCLM, ContinuousLinearMap.reApplyInnerSelf, ContinuousLinearMap.continuous, continuous_id, Continuous.inner
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
x : E
c : 𝕜
⊢ T.reApplyInnerSelf (c • x) = HPow.hPow (β := ℕ) ‖c‖ 2 * T.reApplyInnerSelf x

Tactic:
simp only [map_smul, ContinuousLinearMap.reApplyInnerSelf_apply, inner_smul_left,
    inner_smul_right, ← mul_assoc, mul_conj, ← ofReal_pow, ← smul_re,
    Algebra.smul_def (‖c‖ ^ 2) ⟪T x, x⟫, algebraMap_eq_ofReal]

Premises used: RCLike.algebraMap_eq_ofReal, RCLike.mul_conj, RCLike.smul_re, mul_assoc, ContinuousLinearMap.reApplyInnerSelf_apply, RCLike.ofReal_pow, inner_smul_right, map_smul, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y : F
⊢ Eq (α := F →L[𝕜] E)
    ((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y : F →L[𝕜] E)
    (smulRight (S := 𝕜) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y) x : F →L[𝕜] E)

Tactic:
rfl

Premises used: ContinuousLinearMap.smulRight, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y : F
⊢ Eq (α := F →L[𝕜] E)
    ((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y : F →L[𝕜] E)
    (comp (σ₁₂ := RingHom.id 𝕜) (toSpanSingleton 𝕜 x) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y) : F →L[𝕜] E)

Tactic:
rfl

Premises used: ContinuousLinearMap.comp, ContinuousLinearMap.smulRight, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y : F
⊢ Eq (α := F →ₗ[𝕜] E)
    (↑((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y) : F →ₗ[𝕜] E)
    (LinearMap.smulRight (S := 𝕜) ((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y) x)

Tactic:
rfl

Premises used: LinearMap.smulRight, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y : F
rw : Norm.norm (E := F →L[𝕜] E) (smulRight (S := 𝕜) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y) x) = ‖x‖ * ‖y‖
rw₁ : Norm.norm (E := StrongDual 𝕜 F) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y : F →L[𝕜] 𝕜) * ‖x‖ = ‖x‖ * ‖y‖
rw₂ : ‖y‖ * ‖x‖ = ‖x‖ * ‖y‖
rw₃ rw₄ : ‖x‖ * ‖y‖ = ‖x‖ * ‖y‖
⊢ Norm.norm (E := F →L[𝕜] E)
      ((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y : F →L[𝕜] E) =
    ‖x‖ * ‖y‖

Tactic:
rw [rankOne_def, norm_smulRight_apply, innerSL_apply_norm, mul_comm]

Premises used: InnerProductSpace.rankOne_def, ContinuousLinearMap.norm_smulRight_apply, innerSL_apply_norm, mul_comm
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y : F
⊢ nnnorm (E := F →L[𝕜] E)
      ((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y : F →L[𝕜] E) =
    ‖x‖₊ * ‖y‖₊

Tactic:
NNReal.eq <| norm_rankOne _ _

Premises used: NNReal.eq, InnerProductSpace.norm_rankOne
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y : F
⊢ enorm (E := F →L[𝕜] E)
      ((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y : F →L[𝕜] E) =
    ‖x‖ₑ * ‖y‖ₑ

Tactic:
ENNReal.coe_inj.mpr <| nnnorm_rankOne _ _

Premises used: Iff.mpr, ENNReal.ofNNReal, ENNReal.coe_inj, InnerProductSpace.nnnorm_rankOne, WithTop.some
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y z : F
⊢ (((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y : F →L[𝕜] E) :
        (a : F) → E)
      z =
    ⟪y, z⟫_𝕜 • x

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
G : Type u_8
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
y : F
f : E →L[𝕜] G
simp_rw :
  Eq (α := F →L[𝕜] G) (f ∘SL comp (σ₁₂ := RingHom.id 𝕜) (toSpanSingleton 𝕜 x) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y))
    (comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := 𝕜) (toSpanSingleton 𝕜 ((f : (a : E) → G) x))
      ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y))
simp_rw₁ :
  Eq (α := F →L[𝕜] G) (comp (σ₁₂ := RingHom.id 𝕜) (f ∘SL toSpanSingleton 𝕜 x) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y))
    (comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := 𝕜) (toSpanSingleton 𝕜 ((f : (a : E) → G) x))
      ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y))
⊢ Eq (α := F →L[𝕜] G)
    (f.comp (σ₁₂ := RingHom.id 𝕜)
      ((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y))
    ((((rankOne 𝕜 : (a : G) → F →L⋆[𝕜] F →L[𝕜] G) ((f : (a : E) → G) x) : F →L⋆[𝕜] F →L[𝕜] G) : (a : F) → F →L[𝕜] G) y)

Tactic:
simp_rw [rankOne_def', ← comp_assoc, comp_toSpanSingleton]

Premises used: InnerProductSpace.rankOne_def', ContinuousLinearMap.comp_assoc, ContinuousLinearMap.comp_toSpanSingleton
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
hx : ‖x‖ = 1
⊢ IsIdempotentElem (M := F →L[𝕜] F)
    ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F)

Tactic:
simp [IsIdempotentElem, mul_def, comp_rankOne, hx]

Premises used: InnerProductSpace.comp_rankOne, IsIdempotentElem, ContinuousLinearMap.mul_def
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
h :
  Eq.{u_6 + 1} (α := F)
    (((((rankOne 𝕜 : (a : F) → 𝕜 →L⋆[𝕜] 𝕜 →L[𝕜] F) x : 𝕜 →L⋆[𝕜] 𝕜 →L[𝕜] F) : (a : 𝕜) → 𝕜 →L[𝕜] F) 1 : (a : 𝕜) → F) 1 :
      F)
    ((toSpanSingleton 𝕜 x : (a : 𝕜) → F) 1 : F)
⊢ Eq (α := 𝕜 →L[𝕜] F) ((((rankOne 𝕜 : (a : F) → 𝕜 →L⋆[𝕜] 𝕜 →L[𝕜] F) x : 𝕜 →L⋆[𝕜] 𝕜 →L[𝕜] F) : (a : 𝕜) → 𝕜 →L[𝕜] F) 1)
    (toSpanSingleton 𝕜 x)

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
⊢ Eq.{u_6 + 1} (α := F)
    (((((rankOne 𝕜 : (a : F) → 𝕜 →L⋆[𝕜] 𝕜 →L[𝕜] F) x : 𝕜 →L⋆[𝕜] 𝕜 →L[𝕜] F) : (a : 𝕜) → 𝕜 →L[𝕜] F) 1 : (a : 𝕜) → F) 1 :
      F)
    ((toSpanSingleton 𝕜 x : (a : 𝕜) → F) 1 : F)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
h :
  ∀ (x_1 : F),
    Eq.{u_4 + 1} (α := 𝕜)
      (((((rankOne 𝕜 : (a : 𝕜) → F →L⋆[𝕜] F →L[𝕜] 𝕜) 1 : (a : F) → F →L[𝕜] 𝕜) x : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x_1 : 𝕜)
      ((((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) x : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x_1 : 𝕜)
⊢ Eq (α := F →L[𝕜] 𝕜) (((rankOne 𝕜 : (a : 𝕜) → F →L⋆[𝕜] F →L[𝕜] 𝕜) 1 : (a : F) → F →L[𝕜] 𝕜) x : F →L[𝕜] 𝕜)
    ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) x : F →L[𝕜] 𝕜)

Tactic:
ext
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x x_1 : F
⊢ Eq.{u_4 + 1} (α := 𝕜)
    (((((rankOne 𝕜 : (a : 𝕜) → F →L⋆[𝕜] F →L[𝕜] 𝕜) 1 : (a : F) → F →L[𝕜] 𝕜) x : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x_1 : 𝕜)
    ((((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) x : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x_1 : 𝕜)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
G : Type u_7
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : SeminormedAddCommGroup G
inst_6 : InnerProductSpace 𝕜 G
x : E
y z : F
w : G
⊢ comp.{u_4, u_4, u_4, u_7, u_6, u_5} (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := F)
      ((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y)
      ((((rankOne 𝕜 : (a : F) → G →L⋆[𝕜] G →L[𝕜] F) z : G →L⋆[𝕜] G →L[𝕜] F) : (a : G) → G →L[𝕜] F) w) =
    HSMul.hSMul (β := G →L[𝕜] E) ⟪y, z⟫_𝕜
      ((((rankOne 𝕜 : (a : E) → G →L⋆[𝕜] G →L[𝕜] E) x : G →L⋆[𝕜] G →L[𝕜] E) : (a : G) → G →L[𝕜] E) w : G →L[𝕜] E)

Tactic:
simp [comp_rankOne]

Premises used: InnerProductSpace.comp_rankOne
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
F : Type u_6
G : Type u_7
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : SeminormedAddCommGroup G
inst_4 : InnerProductSpace 𝕜 G
x : F
y z : G
w : F
⊢ ⟪(((((rankOne 𝕜 : (a : F) → G →L⋆[𝕜] G →L[𝕜] F) x : G →L⋆[𝕜] G →L[𝕜] F) : (a : G) → G →L[𝕜] F) y : G →L[𝕜] F) :
          (a : G) → F)
        z,
      w⟫_𝕜 =
    ⟪z, y⟫_𝕜 * ⟪x, w⟫_𝕜

Tactic:
simp [inner_smul_left, inner_conj_symm]

Premises used: inner_conj_symm, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
F : Type u_6
G : Type u_7
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : SeminormedAddCommGroup G
inst_4 : InnerProductSpace 𝕜 G
x y : F
z w : G
⊢ ⟪x,
      (((((rankOne 𝕜 : (a : F) → G →L⋆[𝕜] G →L[𝕜] F) y : G →L⋆[𝕜] G →L[𝕜] F) : (a : G) → G →L[𝕜] F) z : G →L[𝕜] F) :
          (a : G) → F)
        w⟫_𝕜 =
    ⟪x, y⟫_𝕜 * ⟪z, w⟫_𝕜

Tactic:
simp [inner_smul_right, mul_comm]

Premises used: inner_smul_right, mul_comm
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
E : Type u_5
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_8
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y : F
⊢ Eq (α := F →L[𝕜] E)
      ((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y : F →L[𝕜] E)
      (0 : F →L[𝕜] E) ↔
    x = 0 ∨ y = 0

Tactic:
simp [ContinuousLinearMap.ext_iff, rankOne_apply, forall_or_right, or_comm,
    ext_iff_inner_right 𝕜 (E := F)]

Premises used: InnerProductSpace.rankOne_apply, forall_or_right, ContinuousLinearMap.ext_iff, ext_iff_inner_right, or_comm