awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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
⊢ ⟪z,
      HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) x -
        HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) z⟫ =
    ⟪z, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) x⟫ -
      ⟪z, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) z⟫
have rw : ⟪z, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) x⟫ -
    ⟪z, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) z⟫ =
  ⟪z, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) x⟫ -
    ⟪z, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) z⟫
Tactic: rw [inner_sub_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (hypothesis)
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
⊢ 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 : 𝕜)
have h₂ : 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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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 (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, z⟫ * ⟪z, x⟫ =
    HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, x⟫ / ⟪z, z⟫
have rw : HDiv.hDiv (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, z⟫ * ⟪z, x⟫ =
  HDiv.hDiv (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, z⟫ * ⟪z, x⟫
Tactic: rw [← div_mul_eq_mul_div]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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⟫
⊢ HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, x⟫ / ⟪z, z⟫ =
    HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫ / ⟪z, z⟫
have rw : HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫ / ⟪z, z⟫ =
  HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫ / ⟪z, z⟫
Tactic: rw [h₂]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (hypothesis)
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⟫
⊢ HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫ / ⟪z, z⟫ = (ℓ : (a : E) → 𝕜) x
have this : ⟪z, z⟫ ≠ 0
Tactic: have : ⟪z, z⟫ ≠ 0 := inner_self_ne_zero.mpr z_ne_0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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⟫
⊢ 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 : 𝕜)
have ℓ₁ : ⟪HDiv.hDiv (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) : 𝕜) ⟪z, z⟫ • z, x⟫ =
  HDiv.hDiv (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, z⟫ * ⟪z, 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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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⟫
⊢ 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 : 𝕜)
have ℓ₂ : HDiv.hDiv (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, z⟫ * ⟪z, x⟫ =
  HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, x⟫ / ⟪z, z⟫
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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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⟫
⊢ 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 : 𝕜)
have ℓ₃ : HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, x⟫ / ⟪z, z⟫ =
  HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫ / ⟪z, z⟫
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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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⟫
⊢ 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 : 𝕜)
have ℓ₄ : HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫ / ⟪z, z⟫ = (ℓ : (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
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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
⊢ ⟪(LinearIsometryEquiv.symm (toDual 𝕜 E) : (a : StrongDual 𝕜 E) → E) y, x⟫ = (y : (a : E) → 𝕜) x
have 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 : 𝕜)
Tactic: rw [← toDual_apply_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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
⊢ ⟪(B♯ : (a : E) → E) v, w⟫ = (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
have 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
Tactic: rw [continuousLinearMapOfBilin, coe_comp', ContinuousLinearEquiv.coe_coe,
    LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply, toDual_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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
⊢ ⟪(B♯ : (a : E) → E) v, w⟫ = (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
have 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
Tactic: rw [continuousLinearMapOfBilin, coe_comp', ContinuousLinearEquiv.coe_coe,
    LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply, toDual_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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
⊢ ⟪(B♯ : (a : E) → E) v, w⟫ = (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
have 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
Tactic: rw [continuousLinearMapOfBilin, coe_comp', ContinuousLinearEquiv.coe_coe,
    LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply, toDual_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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
⊢ ⟪(B♯ : (a : E) → E) v, w⟫ = (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
have 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
Tactic: rw [continuousLinearMapOfBilin, coe_comp', ContinuousLinearEquiv.coe_coe,
    LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply, toDual_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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
⊢ ⟪(B♯ : (a : E) → E) v, w⟫ = (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
have 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
Tactic: rw [continuousLinearMapOfBilin, coe_comp', ContinuousLinearEquiv.coe_coe,
    LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply, toDual_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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
⊢ ⟪(B♯ : (a : E) → E) v, w⟫ = (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
have 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 : 𝕜)
Tactic: rw [continuousLinearMapOfBilin, coe_comp', ContinuousLinearEquiv.coe_coe,
    LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply, toDual_symm_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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
have refine : ∀ (v_1 : E), ⟪f, v_1⟫ = ⟪(B♯ : (a : E) → E) v, v_1⟫
Tactic: refine ext_inner_right 𝕜 ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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) v, w⟫
have rw : ⟪f, w⟫ = (((B : (a : E) → E →L[𝕜] 𝕜) v : E →L[𝕜] 𝕜) : (a : E) → 𝕜) w
Tactic: rw [continuousLinearMapOfBilin_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NormedAddCommGroup E
inst_1 : CompleteSpace E
inst_2 : InnerProductSpace ℝ E
⊢ Function.Bijective (β := E →L[ℝ] ℝ) fun (y : E) ↦
    { toLinearMap := ((LinearMap.flip (innerₗ E) : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) y, cont := ⋯ }
have 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 →ₗ[ℝ] ℝ)
Tactic: convert! (toDual ℝ E).bijective
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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
⊢ Eq (α := E →ₗ[ℝ] ℝ) (((LinearMap.flip (innerₗ E) : E →ₗ[ℝ] E →ₗ[ℝ] ℝ) : (a : E) → E →ₗ[ℝ] ℝ) x : E →ₗ[ℝ] ℝ)
    ((↑((toDual ℝ E : (a : E) → StrongDual ℝ E) x) : E →ₗ[ℝ] ℝ) : E →ₗ[ℝ] ℝ)
have 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 : ℝ)
Tactic: ext y
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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
⊢ 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
have rw : finrank.{u_3, u_4} 𝕜 ↥(𝕜 ∙ x) = 1
Tactic: rw [LinearMap.rank, rankOne_def, range_smulRight_apply, Module.rank_eq_one_iff_finrank_eq_one]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Dual (goal)
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
⊢ 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
have hf : Ne (α := F →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y : F →L[𝕜] 𝕜) (0 : F →L[𝕜] 𝕜)
Tactic: rw [LinearMap.rank, rankOne_def, range_smulRight_apply, Module.rank_eq_one_iff_finrank_eq_one]