awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
⊢ WithSeminorms.{u_1, u_3, 0} (𝕜 := 𝕜) (E := F) (ι := Fin 1) fun (i : Fin 1) ↦ p
have this : p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
Tactic: have : p.ball 0 1 = {v | re (cd.inner v v) < 1} := by
    ext v
    simp only [ball_normSeminorm, Metric.mem_ball, dist_eq_norm, sub_zero, Set.mem_setOf_eq, p]
    change √(re (cd.inner v v)) < 1 ↔ re (cd.inner v v) < 1
    conv_lhs => rw [show (1 : ℝ) = √1 by simp]
    rw [sqrt_lt_sqrt_iff]
    exact InnerProductSpace.Core.inner_self_nonneg
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
⊢ WithSeminorms.{u_1, u_3, 0} (𝕜 := 𝕜) (E := F) (ι := Fin 1) fun (i : Fin 1) ↦ p
have rw : Membership.mem (γ := Filter F) (𝓝 0) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)} ∧
  IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
Tactic: rw [withSeminorms_iff_mem_nhds_isVonNBounded, this]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
⊢ Membership.mem (γ := Filter F) (𝓝 0) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)} ∧
    IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
have refine : Membership.mem (γ := Filter F) (𝓝 0) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
Tactic: refine ⟨?_, h'⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
⊢ Membership.mem (γ := Filter F) (𝓝 0) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
have A : ContinuousAt (Y := ℝ) (fun (v : F) ↦ (re : (a : 𝕜) → ℝ) ⟪v, v⟫) 0
Tactic: have A : ContinuousAt (fun (v : F) ↦ re (cd.inner v v)) 0 := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
A : ContinuousAt (Y := ℝ) (fun (v : F) ↦ (re : (a : 𝕜) → ℝ) ⟪v, v⟫) 0
⊢ Membership.mem (γ := Filter ℝ) (𝓝 ((re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) 0 0)) : Filter ℝ) (Set.Iio 1)
have simp : Membership.mem (γ := Filter ℝ) (𝓝 0) (Set.Iio 1)
Tactic: simp only [InnerProductSpace.Core.inner_zero_left, map_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
Goal:
𝕜 : Type u_1
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
p : Seminorm 𝕜 F := normSeminorm 𝕜 F
this : p.ball 0 1 = {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
A : ContinuousAt (Y := ℝ) (fun (v : F) ↦ (re : (a : 𝕜) → ℝ) ⟪v, v⟫) 0
⊢ Membership.mem (γ := Filter F) (𝓝 0) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
have B : Membership.mem (γ := Filter ℝ) (𝓝 ((re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) 0 0)) : Filter ℝ) (Set.Iio 1)
Tactic: have B : Set.Iio 1 ∈ 𝓝 (re (cd.inner 0 0)) := by
    simp only [InnerProductSpace.Core.inner_zero_left, map_zero]
    exact Iio_mem_nhds (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
this : NormedAddCommGroup F := toNormedAddCommGroupOfTopology h h'
r : 𝕜
x : F
⊢ ‖r • x‖ ≤ ‖r‖ * ‖x‖
have rw : √((re : (a : 𝕜) → ℝ) (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) r * ⟪x, x⟫)) ≤ ‖r‖ * ‖x‖
Tactic: rw [norm_eq_sqrt_re_inner, inner_smul_left, inner_smul_right, ← mul_assoc]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
this : NormedAddCommGroup F := toNormedAddCommGroupOfTopology h h'
r : 𝕜
x : F
⊢ √((re : (a : 𝕜) → ℝ) (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) r * ⟪x, x⟫)) ≤ ‖r‖ * ‖x‖
have rw : √(HPow.hPow (β := ℕ) ‖r‖ 2) * √(normSq.{u_1, u_3} (𝕜 := 𝕜) x) ≤ ‖r‖ * ‖x‖
Tactic: rw [RCLike.conj_mul, ← ofReal_pow, re_ofReal_mul, sqrt_mul, ← ofReal_normSq_eq_inner_self,
        ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : Core 𝕜 F
tF : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫ : ℝ) (1 : ℝ)}
this : NormedAddCommGroup F := toNormedAddCommGroupOfTopology h h'
r : 𝕜
x : F
rw : √(HPow.hPow (β := ℕ) ‖r‖ 2) * √(normSq.{u_1, u_3} (𝕜 := 𝕜) x) ≤ ‖r‖ * ‖x‖
⊢ √((re : (a : 𝕜) → ℝ) (HMul.hMul (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) r : 𝕜) r * ⟪x, x⟫)) ≤ ‖r‖ * ‖x‖
have hx : 0 ≤ HPow.hPow (β := ℕ) ‖r‖ 2
Tactic: rw [RCLike.conj_mul, ← ofReal_pow, re_ofReal_mul, sqrt_mul, ← ofReal_normSq_eq_inner_self,
        ofReal_re]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : PreInnerProductSpace.Core 𝕜 F
this : NormedSpace 𝕜 F := Core.toNormedSpace
x : F
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜
have h₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) (√((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜)) 2
Tactic: have h₁ : ‖x‖ ^ 2 = √(re (cd.inner x x)) ^ 2 := rfl
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
inst_2 : Module 𝕜 F
cd : PreInnerProductSpace.Core 𝕜 F
this : NormedSpace 𝕜 F := Core.toNormedSpace
x : F
h₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) (√((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜)) 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜
have h₂ : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜 : ℝ)
Tactic: have h₂ : 0 ≤ re (cd.inner x x) := InnerProductSpace.Core.inner_self_nonneg
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
hF : Module 𝕜 F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
cd : Core 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫_𝕜) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫_𝕜 : ℝ) (1 : ℝ)}
this_1 : NormedAddCommGroup F := Core.toNormedAddCommGroupOfTopology h h'
this : NormedSpace 𝕜 F := Core.toNormedSpaceOfTopology h h'
x : F
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜
have h₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) (√((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜)) 2
Tactic: have h₁ : ‖x‖ ^ 2 = √(re (cd.inner x x)) ^ 2 := rfl
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Defs (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : AddCommGroup F
hF : Module 𝕜 F
inst_2 : TopologicalSpace F
inst_3 : IsTopologicalAddGroup F
inst_4 : ContinuousConstSMul 𝕜 F
cd : Core 𝕜 F
h : ContinuousAt.{u_3, u_1} (Y := 𝕜) (fun (v : F) ↦ ⟪v, v⟫_𝕜) 0
h' : IsVonNBounded.{u_1, u_3} 𝕜 (E := F) {v : F | LT.lt (α := ℝ) ((re : (a : 𝕜) → ℝ) ⟪v, v⟫_𝕜 : ℝ) (1 : ℝ)}
this_1 : NormedAddCommGroup F := Core.toNormedAddCommGroupOfTopology h h'
this : NormedSpace 𝕜 F := Core.toNormedSpaceOfTopology h h'
x : F
h₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) (√((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜)) 2
⊢ HPow.hPow (β := ℕ) ‖x‖ 2 = (re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜
have h₂ : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, x⟫_𝕜 : ℝ)
Tactic: have h₂ : 0 ≤ re (cd.inner x x) := InnerProductSpace.Core.inner_self_nonneg
-- 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
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪(b : (a : ι) → E) i, x⟫ = ⟪(b : (a : ι) → E) i, y⟫
⊢ x = y
have apply : Eq (α := StrongDual 𝕜 E) ((toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) x : StrongDual 𝕜 E)
  ((toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) y : StrongDual 𝕜 E)
Tactic: apply (toDualMap 𝕜 E).map_eq_iff.mp
-- 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
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪(b : (a : ι) → E) i, x⟫ = ⟪(b : (a : ι) → E) i, y⟫
⊢ Eq (α := StrongDual 𝕜 E) ((toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) x : StrongDual 𝕜 E)
    ((toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) y : StrongDual 𝕜 E)
have refine : ∀ (i : ι),
  Eq.{u_1 + 1} (α := 𝕜)
    (((↑((toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) x) : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) ((b : (a : ι) → E) i : E) : 𝕜)
    (((↑((toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) y) : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) ((b : (a : ι) → E) i : E) : 𝕜)
Tactic: refine (Function.Injective.eq_iff ContinuousLinearMap.coe_injective).mp (b.ext ?_)
-- 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
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪(b : (a : ι) → E) i, x⟫ = ⟪(b : (a : ι) → E) i, y⟫
i : ι
⊢ Eq.{u_1 + 1} (α := 𝕜)
    (((↑((toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) x) : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) ((b : (a : ι) → E) i : E) : 𝕜)
    (((↑((toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) y) : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) ((b : (a : ι) → E) i : E) : 𝕜)
have simp : ⟪x, (b : (a : ι) → E) i⟫ = ⟪y, (b : (a : ι) → E) i⟫
Tactic: simp only [ContinuousLinearMap.coe_coe, toDualMap_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
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪(b : (a : ι) → E) i, x⟫ = ⟪(b : (a : ι) → E) i, y⟫
i : ι
⊢ ⟪x, (b : (a : ι) → E) i⟫ = ⟪y, (b : (a : ι) → E) i⟫
have rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(b : (a : ι) → E) i, x⟫ = ⟪y, (b : (a : ι) → E) i⟫
Tactic: rw [← inner_conj_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
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪(b : (a : ι) → E) i, x⟫ = ⟪(b : (a : ι) → E) i, y⟫
i : ι
| ⟪y, (b : (a : ι) → E) i⟫
have rw : ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(b : (a : ι) → E) i, y⟫ : 𝕜)
Tactic: rw [← inner_conj_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
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪(b : (a : ι) → E) i, x⟫ = ⟪(b : (a : ι) → E) i, y⟫
i : ι
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(b : (a : ι) → E) i, x⟫ = ⟪y, (b : (a : ι) → E) i⟫
have conv_rhs : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(b : (a : ι) → E) i, x⟫ : 𝕜)
  ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(b : (a : ι) → E) i, y⟫ : 𝕜)
Tactic: conv_rhs => rw [← inner_conj_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
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, (b : (a : ι) → E) i⟫ = ⟪y, (b : (a : ι) → E) i⟫
⊢ x = y
have refine : ∀ (i : ι), ⟪(b : (a : ι) → E) i, x⟫ = ⟪(b : (a : ι) → E) i, y⟫
Tactic: refine ext_inner_left_basis b fun i => ?_
-- 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
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, (b : (a : ι) → E) i⟫ = ⟪y, (b : (a : ι) → E) i⟫
i : ι
⊢ ⟪(b : (a : ι) → E) i, x⟫ = ⟪(b : (a : ι) → E) i, y⟫
have rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, (b : (a : ι) → E) i⟫ = ⟪(b : (a : ι) → E) i, y⟫
Tactic: rw [← inner_conj_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
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, (b : (a : ι) → E) i⟫ = ⟪y, (b : (a : ι) → E) i⟫
i : ι
| ⟪(b : (a : ι) → E) i, y⟫
have rw : ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, (b : (a : ι) → E) i⟫ : 𝕜)
Tactic: rw [← inner_conj_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
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, (b : (a : ι) → E) i⟫ = ⟪y, (b : (a : ι) → E) i⟫
i : ι
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, (b : (a : ι) → E) i⟫ = ⟪(b : (a : ι) → E) i, y⟫
have conv_rhs : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, (b : (a : ι) → E) i⟫ : 𝕜)
  ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, (b : (a : ι) → E) i⟫ : 𝕜)
Tactic: conv_rhs => rw [← inner_conj_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
⊢ ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ
have pos : ∀ (htriv : Y = ⊤), ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ
Tactic: by_cases htriv : Y = ⊤
-- 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
pos : ∀ (htriv : Y = ⊤), ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ
⊢ ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ
have neg : ∀ (htriv : ¬Y = ⊤), ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ
Tactic: by_cases htriv : Y = ⊤
-- 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
htriv : Y = ⊤
⊢ ℓ = 0
have h' : (↑ℓ : E →ₗ[𝕜] 𝕜) = 0
Tactic: have h' := LinearMap.ker_eq_top.mp htriv
-- 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
htriv : Y = ⊤
h' : (↑ℓ : E →ₗ[𝕜] 𝕜) = 0
⊢ ℓ = 0
have h'₁ : (↑ℓ : E →ₗ[𝕜] 𝕜) = (↑0 : E →ₗ[𝕜] 𝕜)
Tactic: rw [← coe_zero] at h'
Cleared hypotheses: 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
htriv : Y = ⊤
⊢ ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ
have hℓ : ℓ = 0
Tactic: have hℓ : ℓ = 0 := by
          have h' := LinearMap.ker_eq_top.mp htriv
          rw [← coe_zero] at h'
          apply coe_injective
          exact 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
htriv : ¬Y = ⊤
⊢ ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ
have htriv₁ : ¬Yᗮ = ⊥
Tactic: rw [← Submodule.orthogonal_eq_bot_iff] at htriv
Cleared hypotheses: htriv
-- 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
htriv : ¬Yᗮ = ⊥
⊢ ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ
have htriv₁ : Yᗮ ≠ ⊥
Tactic: change Yᗮ ≠ ⊥ at htriv
Cleared hypotheses: htriv
-- 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
htriv : Yᗮ ≠ ⊥
⊢ ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ
have htriv₁ : ∃ x ∈ Yᗮ, x ≠ 0
Tactic: rw [Submodule.ne_bot_iff] at htriv
Cleared hypotheses: htriv
-- 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
htriv : ∃ x ∈ Yᗮ, x ≠ 0
⊢ ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ
have neg : ∀ (z : E) (hz : z ∈ Yᗮ) (z_ne_0 : z ≠ 0), ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ
Tactic: obtain ⟨z : E, hz : z ∈ Yᗮ, z_ne_0 : z ≠ 0⟩ := htriv
Cleared hypotheses: htriv
-- 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
⊢ ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ
have neg : (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E)
    (HDiv.hDiv (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) : 𝕜) ⟪z, z⟫ • z) =
  ℓ
Tactic: refine ⟨(starRingEnd (R := 𝕜) (ℓ z) / ⟪z, z⟫) • z, ?_⟩
-- 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
⊢ (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E)
      (HDiv.hDiv (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) : 𝕜) ⟪z, z⟫ • z) =
    ℓ
have neg : ∀ (x : E),
  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: apply ContinuousLinearMap.ext
-- 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
⊢ 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
have rw : HMul.hMul (α := 𝕜) (β := 𝕜) (((↑ℓ : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) x : 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) -
    HMul.hMul (α := 𝕜) (β := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) (((↑ℓ : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) z : 𝕜) =
  0
Tactic: rw [LinearMap.mem_ker, map_sub, map_smul, map_smul, smul_eq_mul,
            smul_eq_mul, mul_comm]
-- 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
⊢ 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₁ : 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
Tactic: have h₁ : ℓ z • x - ℓ x • z ∈ Y := by
          rw [LinearMap.mem_ker, map_sub, map_smul, map_smul, smul_eq_mul,
            smul_eq_mul, mul_comm]
          exact sub_self (ℓ x * ℓ z)