awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ : E →ₗ[𝕜] 𝕜).ker
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) x -
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) z ∈
    Y
⊢ HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, x⟫ = HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫

Tactic:
have h₂ : ℓ z * ⟪z, x⟫ = ℓ x * ⟪z, z⟫ :=
          haveI h₃ :=
            calc
              0 = ⟪z, ℓ z • x - ℓ x • z⟫ := by
                rw [(Y.mem_orthogonal' z).mp hz]
                exact h₁
              _ = ⟪z, ℓ z • x⟫ - ⟪z, ℓ x • z⟫ := by rw [inner_sub_right]
              _ = ℓ z * ⟪z, x⟫ - ℓ x * ⟪z, z⟫ := by simp [inner_smul_right]
          sub_eq_zero.mp h₃.symm
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ : E →ₗ[𝕜] 𝕜).ker
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) x -
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) z ∈
    Y
h₂ : HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, x⟫ = HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫
⊢ ⟪HDiv.hDiv (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) : 𝕜) ⟪z, z⟫ • z, x⟫ =
    HDiv.hDiv (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, z⟫ * ⟪z, x⟫

Tactic:
simp [inner_smul_left]

Premises used: inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ : E →ₗ[𝕜] 𝕜).ker
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) x -
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) z ∈
    Y
h₂ : HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, x⟫ = HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫
rw rw₁ :
  HDiv.hDiv (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, z⟫ * ⟪z, x⟫ =
    HDiv.hDiv (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, z⟫ * ⟪z, x⟫
⊢ HDiv.hDiv (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, z⟫ * ⟪z, x⟫ =
    HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, x⟫ / ⟪z, z⟫

Tactic:
rw [← div_mul_eq_mul_div]

Premises used: div_mul_eq_mul_div
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ : E →ₗ[𝕜] 𝕜).ker
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) x -
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) z ∈
    Y
h₂ : HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, x⟫ = HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫
rw rw₁ :
  HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫ / ⟪z, z⟫ =
    HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫ / ⟪z, z⟫
⊢ HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, x⟫ / ⟪z, z⟫ =
    HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫ / ⟪z, z⟫

Tactic:
rw [h₂]
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ : E →ₗ[𝕜] 𝕜).ker
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) x -
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) z ∈
    Y
h₂ : HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, x⟫ = HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫
⊢ ⟪z, z⟫ ≠ 0

Tactic:
have : ⟪z, z⟫ ≠ 0 := inner_self_ne_zero.mpr z_ne_0
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ : E →ₗ[𝕜] 𝕜).ker
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) x -
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) z ∈
    Y
h₂ : HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, x⟫ = HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫
this : ⟪z, z⟫ ≠ 0
⊢ HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫ / ⟪z, z⟫ = (ℓ : (a : E) → 𝕜) x

Tactic:
field
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ : E →ₗ[𝕜] 𝕜).ker
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ :
  HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) x -
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) z ∈
    Y
h₂ : HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, x⟫ = HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫
ℓ₁ :
  ⟪HDiv.hDiv (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) : 𝕜) ⟪z, z⟫ • z, x⟫ =
    HDiv.hDiv (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, z⟫ * ⟪z, x⟫
ℓ₂ :
  HDiv.hDiv (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, z⟫ * ⟪z, x⟫ =
    HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, x⟫ / ⟪z, z⟫
ℓ₃ :
  HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, x⟫ / ⟪z, z⟫ =
    HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫ / ⟪z, z⟫
ℓ₄ : HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫ / ⟪z, z⟫ = (ℓ : (a : E) → 𝕜) x
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((((toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E)
              (HDiv.hDiv (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) : 𝕜) ⟪z, z⟫ • z) :
            StrongDual 𝕜 E) :
          (a : E) → 𝕜)
        x :
      𝕜)
    ((ℓ : (a : E) → 𝕜) x : 𝕜)

Tactic:
calc
          ⟪(ℓ z† / ⟪z, z⟫) • z, x⟫ = ℓ z / ⟪z, z⟫ * ⟪z, x⟫ := by simp [inner_smul_left]
          _ = ℓ z * ⟪z, x⟫ / ⟪z, z⟫ := by rw [← div_mul_eq_mul_div]
          _ = ℓ x * ⟪z, z⟫ / ⟪z, z⟫ := by rw [h₂]
          _ = ℓ x := by have : ⟪z, z⟫ ≠ 0 := inner_self_ne_zero.mpr z_ne_0; field

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
x y : E
⊢ (((toDual 𝕜 E : (a : E) → StrongDual 𝕜 E) x : StrongDual 𝕜 E) : (a : E) → 𝕜) y = ⟪x, y⟫

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
x : E
y : StrongDual 𝕜 E
rw :
  Eq.{u_1 + 1} (α := 𝕜)
    ((((toDual 𝕜 E : (a : E) → StrongDual 𝕜 E) ((LinearIsometryEquiv.symm (toDual 𝕜 E) : (a : StrongDual 𝕜 E) → E) y) :
            StrongDual 𝕜 E) :
          (a : E) → 𝕜)
        x :
      𝕜)
    ((y : (a : E) → 𝕜) x : 𝕜)
⊢ ⟪(LinearIsometryEquiv.symm (toDual 𝕜 E) : (a : StrongDual 𝕜 E) → E) y, x⟫ = (y : (a : E) → 𝕜) x

Tactic:
rw [← toDual_apply_apply]

Premises used: InnerProductSpace.toDual_apply_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
x : E
y : StrongDual 𝕜 E
⊢ Eq.{u_1 + 1} (α := 𝕜)
    ((((toDual 𝕜 E : (a : E) → StrongDual 𝕜 E) ((LinearIsometryEquiv.symm (toDual 𝕜 E) : (a : StrongDual 𝕜 E) → E) y) :
            StrongDual 𝕜 E) :
          (a : E) → 𝕜)
        x :
      𝕜)
    ((y : (a : E) → 𝕜) x : 𝕜)

Tactic:
simp only [LinearIsometryEquiv.apply_symm_apply]

Premises used: LinearIsometryEquiv.apply_symm_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
⊢ Eq (α := E →ₗᵢ⋆[𝕜] StrongDual 𝕜 E) (LinearIsometryEquiv.toLinearIsometry (toDual 𝕜 E)) (toDualMap 𝕜 E)

Tactic:
rfl

Premises used: LinearIsometryEquiv.toLinearIsometry, LinearMap.mkContinuousOfExistsBound, InnerProductSpace.toDualMap, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
x : E
⊢ Eq (α := StrongDual 𝕜 E) ((toDual 𝕜 E : (a : E) → StrongDual 𝕜 E) x : StrongDual 𝕜 E)
    ((toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) x : StrongDual 𝕜 E)

Tactic:
rfl

Premises used: LinearMap.mkContinuousOfExistsBound, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
⊢ Eq.{u_2 + 1} (α := E →L[𝕜] E) 0♯ 0

Tactic:
simp [continuousLinearMapOfBilin]

Premises used: InnerProductSpace.continuousLinearMapOfBilin
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v w : E
rw :
  ⟪((↑(↑(LinearIsometryEquiv.symm (toDual 𝕜 E)) : StrongDual 𝕜 E ≃L⋆[𝕜] E) : StrongDual 𝕜 E →L⋆[𝕜] E) ∘SL B :
          (a : E) → E)
        v,
      w⟫ =
    (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
rw₁ :
  ⟪Function.comp (β := StrongDual 𝕜 E)
        (⇑(↑(↑(LinearIsometryEquiv.symm (toDual 𝕜 E)) : StrongDual 𝕜 E ≃L⋆[𝕜] E) : StrongDual 𝕜 E →L⋆[𝕜] E) :
          (a : StrongDual 𝕜 E) → E)
        (⇑B : (a : E) → StrongDual 𝕜 E) v,
      w⟫ =
    (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
rw₂ :
  ⟪Function.comp (β := StrongDual 𝕜 E)
        (⇑(↑(LinearIsometryEquiv.symm (toDual 𝕜 E)) : StrongDual 𝕜 E ≃L⋆[𝕜] E) : (a : StrongDual 𝕜 E) → E)
        (⇑B : (a : E) → StrongDual 𝕜 E) v,
      w⟫ =
    (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
rw₃ :
  ⟪Function.comp (β := StrongDual 𝕜 E) (⇑(LinearIsometryEquiv.symm (toDual 𝕜 E)) : (a : StrongDual 𝕜 E) → E)
        (⇑B : (a : E) → StrongDual 𝕜 E) v,
      w⟫ =
    (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
rw₄ :
  ⟪(LinearIsometryEquiv.symm (toDual 𝕜 E) : (a : StrongDual 𝕜 E) → E)
        ((B : (a : E) → StrongDual 𝕜 E) v : StrongDual 𝕜 E),
      w⟫ =
    (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
rw₅ rw₆ :
  Eq.{u_1 + 1} (α := 𝕜) ((((B : (a : E) → StrongDual 𝕜 E) v : StrongDual 𝕜 E) : (a : E) → 𝕜) w : 𝕜)
    ((((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w : 𝕜)
⊢ ⟪(B♯ : (a : E) → E) v, w⟫ = (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w

Tactic:
rw [continuousLinearMapOfBilin, coe_comp', ContinuousLinearEquiv.coe_coe,
    LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply, toDual_symm_apply]

Premises used: ContinuousLinearMap.coe_comp', InnerProductSpace.toDual_symm_apply, LinearIsometryEquiv.coe_toContinuousLinearEquiv, InnerProductSpace.continuousLinearMapOfBilin, Function.comp_apply, ContinuousLinearEquiv.coe_coe
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), ⟪f, w⟫ = (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
⊢ f = (B♯ : (a : E) → E) v

Tactic:
ext_inner_right 𝕜 ?_

Premises used: ext_inner_right
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), ⟪f, w⟫ = (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
refine : ∀ (v_1 : E), ⟪f, v_1⟫ = ⟪(B♯ : (a : E) → E) v, v_1⟫
⊢ f = (B♯ : (a : E) → E) v

Tactic:
refine ext_inner_right 𝕜 ?_

Premises used: ext_inner_right
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), ⟪f, w⟫ = (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
w : E
rw : ⟪f, w⟫ = (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
⊢ ⟪f, w⟫ = ⟪(B♯ : (a : E) → E) v, w⟫

Tactic:
rw [continuousLinearMapOfBilin_apply]

Premises used: InnerProductSpace.continuousLinearMapOfBilin_apply
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), ⟪f, w⟫ = (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
w : E
⊢ ⟪f, w⟫ = (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w

Tactic:
is_lax_milgram w
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), ⟪f, w⟫ = (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
w : E
⊢ ⟪f, w⟫ = (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w

Tactic:
exact is_lax_milgram w
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
inst_2 : InnerProductSpace ℝ E
⊢ Function.Bijective (α := E) (β := StrongDual ℝ E) (⇑(toDual ℝ E) : (a : E) → StrongDual ℝ E)

Tactic:
(toDual ℝ E).bijective

Premises used: InnerProductSpace.toDual, Real, LinearIsometryEquiv.bijective
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
inst_2 : InnerProductSpace ℝ E
h :
  ∀ (x : E),
    Eq (α := Semiring ℝ) CommSemiring.toSemiring DivisionSemiring.toSemiring →
      HEq (α := ℝ →+* ℝ) (RingHom.id ℝ) (β := ℝ →+* ℝ) (RingHom.id ℝ) →
        Eq (α := AddCommMonoid ℝ) NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid →
          HEq.{u_2 + 1} (α := Module ℝ E) (NormedSpace.toModule : Module ℝ E) (β := Module ℝ E)
              (NormedSpace.toModule : Module ℝ E) →
            HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) Semiring.toModule →
              Eq (α := E →ₗ[ℝ] ℝ)
                (((LinearMap.flip (innerₗ E) : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ)
                ((↑((toDual ℝ E : (a : E) → StrongDual ℝ E) x) : E →ₗ[ℝ] ℝ) : E →ₗ[ℝ] ℝ)
⊢ Function.Bijective (β := E →L[ℝ] ℝ) fun (y : E) ↦
    { toLinearMap := ((LinearMap.flip (innerₗ E) : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) y, cont := ⋯ }

Tactic:
convert! (toDual ℝ E).bijective

Premises used: InnerProductSpace.toDual, Real, LinearIsometryEquiv.bijective
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
inst_2 : InnerProductSpace ℝ E
x : E
e_3 : Eq (α := Semiring ℝ) CommSemiring.toSemiring DivisionSemiring.toSemiring
e_5 : HEq (α := ℝ →+* ℝ) (RingHom.id ℝ) (β := ℝ →+* ℝ) (RingHom.id ℝ)
e_11 : Eq (α := AddCommMonoid ℝ) NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid
e_12 :
  HEq.{u_2 + 1} (α := Module ℝ E) (NormedSpace.toModule : Module ℝ E) (β := Module ℝ E)
    (NormedSpace.toModule : Module ℝ E)
e_13 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) Semiring.toModule
h :
  ∀ (y : E),
    Eq (α := ℝ)
      (((((LinearMap.flip (innerₗ E) : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
      (((↑((toDual ℝ E : (a : E) → StrongDual ℝ E) x) : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
⊢ Eq (α := E →ₗ[ℝ] ℝ) (((LinearMap.flip (innerₗ E) : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ)
    ((↑((toDual ℝ E : (a : E) → StrongDual ℝ E) x) : E →ₗ[ℝ] ℝ) : E →ₗ[ℝ] ℝ)

Tactic:
ext y
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
inst_2 : InnerProductSpace ℝ E
x : E
e_3 : Eq (α := Semiring ℝ) CommSemiring.toSemiring DivisionSemiring.toSemiring
e_5 : HEq (α := ℝ →+* ℝ) (RingHom.id ℝ) (β := ℝ →+* ℝ) (RingHom.id ℝ)
e_11 : Eq (α := AddCommMonoid ℝ) NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid
e_12 :
  HEq.{u_2 + 1} (α := Module ℝ E) (NormedSpace.toModule : Module ℝ E) (β := Module ℝ E)
    (NormedSpace.toModule : Module ℝ E)
e_13 : HEq (α := Module ℝ ℝ) Semiring.toModule (β := Module ℝ ℝ) Semiring.toModule
y : E
⊢ Eq (α := ℝ)
    (((((LinearMap.flip (innerₗ E) : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)
    (((↑((toDual ℝ E : (a : E) → StrongDual ℝ E) x) : E →ₗ[ℝ] ℝ) : (a : E) → ℝ) y : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y : F
hx : x ≠ 0
hy : y ≠ 0
rw : finrank.{u_3, u_4} 𝕜 ↥(𝕜 ∙ x) = 1
hf : Ne (α := F →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y : F →L[𝕜] 𝕜) (0 : F →L[𝕜] 𝕜)
⊢ LinearMap.rank.{u_3, u_5, u_4} (K := 𝕜) (V := F) (V' := E)
      (↑((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y) : F →ₗ[𝕜] E) =
    1

Tactic:
rw [LinearMap.rank, rankOne_def, range_smulRight_apply, Module.rank_eq_one_iff_finrank_eq_one]

Premises used: InnerProductSpace.rankOne_def, ContinuousLinearMap.range_smulRight_apply, LinearMap.rank, Module.rank_eq_one_iff_finrank_eq_one
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ finrank.{u_3, u_4} 𝕜 ↥(𝕜 ∙ x) = 1

Tactic:
finrank_span_singleton hx

Premises used: Set.Mem, setOf, finrank_span_singleton
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ finrank.{u_3, u_4} 𝕜 ↥(𝕜 ∙ x) = 1

Tactic:
exact finrank_span_singleton hx

Premises used: finrank_span_singleton
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ Ne (α := F →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y : F →L[𝕜] 𝕜) (0 : F →L[𝕜] 𝕜)

Tactic:
map_eq_zero_iff _ (toDualMap 𝕜 F).injective |>.not.mpr hy

Premises used: Iff.mpr, Iff.not, LinearIsometry.injective, InnerProductSpace.toDualMap, map_eq_zero_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y : F
hx : x ≠ 0
hy : y ≠ 0
⊢ Ne (α := F →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y : F →L[𝕜] 𝕜) (0 : F →L[𝕜] 𝕜)

Tactic:
exact map_eq_zero_iff _ (toDualMap 𝕜 F).injective |>.not.mpr hy

Premises used: Iff.mpr, Iff.not, LinearIsometry.injective, InnerProductSpace.toDualMap, map_eq_zero_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
b : OrthonormalBasis ι ℝ E
L : StrongDual ℝ E
⊢ FiniteDimensional ℝ E

Tactic:
have := b.toBasis.finiteDimensional_of_finite
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
ι : Type u_1
E : Type u_2
inst : Fintype ι
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace ℝ E
b : OrthonormalBasis ι ℝ E
L : StrongDual ℝ E
this : FiniteDimensional ℝ E
simp_rw :
  HPow.hPow (β := ℕ)
      (norm (E := E) ((LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E) : (a : StrongDual ℝ E) → E) L : E)) 2 =
    ∑ i : ι, HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : E) → ℝ) ((b : (a : ι) → E) i : E) : ℝ) 2
simp_rw₁ :
  Eq (α := ℝ)
    (∑ i : ι,
      HPow.hPow (β := ℕ)
        (inner ℝ (E := E) ((LinearIsometryEquiv.symm (InnerProductSpace.toDual ℝ E) : (a : StrongDual ℝ E) → E) L : E)
          ((b : (a : ι) → E) i : E))
        2)
    (∑ i : ι, HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : E) → ℝ) ((b : (a : ι) → E) i : E) : ℝ) 2)
⊢ HPow.hPow (β := ℕ) ‖L‖ 2 = ∑ i : ι, HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : E) → ℝ) ((b : (a : ι) → E) i : E) : ℝ) 2

Tactic:
simp_rw [← (InnerProductSpace.toDual ℝ E).symm.norm_map, ← b.sum_sq_inner_left,
    InnerProductSpace.toDual_symm_apply]

Premises used: InnerProductSpace.toDual, Real, InnerProductSpace.toDual_symm_apply, LinearIsometryEquiv.symm, LinearIsometryEquiv.norm_map, OrthonormalBasis.sum_sq_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : Inner 𝕜 E
v : n → E
i j : n
⊢ gram 𝕜 v i j = ⟪v i, v j⟫_𝕜

Tactic:
rfl

Premises used: Matrix.gram, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ Eq (α := Matrix n n 𝕜) (gram.{u_1, u_2, u_4} (E := E) 𝕜 0) 0

Tactic:
Matrix.ext fun _ _ ↦ inner_zero_left _

Premises used: inner_zero_left, OfNat.ofNat, Matrix.ext
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : DecidableEq n
i : n
x : E
a : ∀ (j k : n), gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) j k = single i i (⟪x, x⟫_𝕜) j k
⊢ gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) = single i i ⟪x, x⟫_𝕜

Tactic:
ext j k
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : DecidableEq n
i : n
x : E
j k : n
a :
  ∀ (hij : i ≠ j),
    gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) j k = single i i (⟪x, x⟫_𝕜) j k
a₁ : gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) i k = single i i (⟪x, x⟫_𝕜) i k
⊢ gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) j k = single i i (⟪x, x⟫_𝕜) j k

Tactic:
obtain hij | rfl := ne_or_eq i j

Premises used: ne_or_eq, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : DecidableEq n
i : n
x : E
j k : n
hij : i ≠ j
⊢ gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) j k = single i i (⟪x, x⟫_𝕜) j k

Tactic:
simp [hij]
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : DecidableEq n
i : n
x : E
k : n
a :
  ∀ (hik : i ≠ k),
    gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) i k = single i i (⟪x, x⟫_𝕜) i k
a₁ : gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) i i = single i i (⟪x, x⟫_𝕜) i i
⊢ gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) i k = single i i (⟪x, x⟫_𝕜) i k

Tactic:
obtain hik | rfl := ne_or_eq i k

Premises used: ne_or_eq, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.GramMatrix
Goal:
E : Type u_1
n : Type u_2
𝕜 : Type u_4
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : DecidableEq n
i : n
x : E
k : n
hik : i ≠ k
⊢ gram.{u_1, u_2, u_4} (E := E) 𝕜 (Pi.single (M := fun (a : n) ↦ E) i x) i k = single i i (⟪x, x⟫_𝕜) i k

Tactic:
simp [hik]