awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ LE.le (α := Submodule 𝕜 E) (nullSubmodule 𝕜 E : Submodule 𝕜 E)
    (ker (R₂ := 𝕜) (M₂ := 𝕜) (τ₁₂ := RingHom.id 𝕜) (↑((toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) x) : E →ₗ[𝕜] 𝕜) :
      Submodule 𝕜 E)

Tactic:
fun _ hx ↦ inner_eq_zero_of_right x (mem_nullSubmodule_iff.mp hx)

Premises used: Set.Mem, inner_eq_zero_of_right, setOf, Set.preimage, mem_nullSubmodule_iff, Set.singleton, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
⊢ LE.le (α := Submodule 𝕜 E) (nullSubmodule 𝕜 E : Submodule 𝕜 E)
    (ker (LinearIsometry.toLinearMap (E₂ := StrongDual 𝕜 E) (toDualMap 𝕜 E)) : Submodule 𝕜 E)

Tactic:
fun _ hx ↦ ContinuousLinearMap.ext <| fun y ↦ inner_eq_zero_of_left y hx

Premises used: Set.Mem, setOf, inner_eq_zero_of_left, Set.preimage, Set.singleton, ContinuousLinearMap.ext
-- 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 : Nontrivial E
⊢ norm (E := E →L⋆[𝕜] E →L[𝕜] 𝕜) (innerSL 𝕜) = 1

Tactic:
show ‖(toDualMap 𝕜 E).toContinuousLinearMap‖ = 1 from LinearIsometry.norm_toContinuousLinearMap _

Premises used: innerSL, LinearIsometry.norm_toContinuousLinearMap, LinearMap.mkContinuous₂, LinearMap.mkContinuousOfExistsBound, InnerProductSpace.toDualMap, LinearMap.mkContinuousOfExistsBound₂, LinearIsometry.toContinuousLinearMap
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
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⟫
apply :
  Eq (α := StrongDual 𝕜 E) ((toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) x : StrongDual 𝕜 E)
    ((toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) y : StrongDual 𝕜 E)
⊢ x = y

Tactic:
apply (toDualMap 𝕜 E).map_eq_iff.mp

Premises used: InnerProductSpace.toDualMap, LinearIsometry.map_eq_iff, Iff.mp
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
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)

Tactic:
(Function.Injective.eq_iff ContinuousLinearMap.coe_injective).mp (b.ext ?_)

Premises used: Function.Injective.eq_iff, Iff.mp, ContinuousLinearMap.coe_injective, Module.Basis.ext
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
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⟫
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) : 𝕜)
⊢ Eq (α := StrongDual 𝕜 E) ((toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) x : StrongDual 𝕜 E)
    ((toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) y : StrongDual 𝕜 E)

Tactic:
refine (Function.Injective.eq_iff ContinuousLinearMap.coe_injective).mp (b.ext ?_)

Premises used: Function.Injective.eq_iff, Iff.mp, ContinuousLinearMap.coe_injective, Module.Basis.ext
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
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 : ι
simp : ⟪x, (b : (a : ι) → E) i⟫ = ⟪y, (b : (a : ι) → E) 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:
simp only [ContinuousLinearMap.coe_coe, toDualMap_apply_apply]

Premises used: InnerProductSpace.toDualMap_apply_apply, ContinuousLinearMap.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
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪(b : (a : ι) → E) i, x⟫ = ⟪(b : (a : ι) → E) i, y⟫
i : ι
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(b : (a : ι) → E) i, x⟫ = ⟪y, (b : (a : ι) → E) i⟫
⊢ ⟪x, (b : (a : ι) → E) i⟫ = ⟪y, (b : (a : ι) → E) i⟫

Tactic:
rw [← inner_conj_symm]

Premises used: inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
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 : ι
rw : ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(b : (a : ι) → E) i, y⟫ : 𝕜)
| ⟪y, (b : (a : ι) → E) i⟫

Tactic:
rw [← inner_conj_symm]

Premises used: inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
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 : ι
conv_rhs :
  Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(b : (a : ι) → E) i, x⟫ : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(b : (a : ι) → E) i, y⟫ : 𝕜)
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(b : (a : ι) → E) i, x⟫ = ⟪y, (b : (a : ι) → E) i⟫

Tactic:
conv_rhs => rw [← inner_conj_symm]

Premises used: inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
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 (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(b : (a : ι) → E) i, x⟫ : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(b : (a : ι) → E) i, y⟫ : 𝕜)

Tactic:
congr_arg conj (h i)

Premises used: congr_arg, starRingEnd, 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
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪(b : (a : ι) → E) i, x⟫ = ⟪(b : (a : ι) → E) i, y⟫
i : ι
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(b : (a : ι) → E) i, x⟫ : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(b : (a : ι) → E) i, y⟫ : 𝕜)

Tactic:
exact congr_arg conj (h i)

Premises used: congr_arg, starRingEnd, 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
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, (b : (a : ι) → E) i⟫ = ⟪y, (b : (a : ι) → E) i⟫
⊢ x = y

Tactic:
ext_inner_left_basis b fun i => ?_

Premises used: InnerProductSpace.ext_inner_left_basis
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
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⟫
refine : ∀ (i : ι), ⟪(b : (a : ι) → E) i, x⟫ = ⟪(b : (a : ι) → E) i, y⟫
⊢ x = y

Tactic:
refine ext_inner_left_basis b fun i => ?_

Premises used: InnerProductSpace.ext_inner_left_basis
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
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 : ι
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, (b : (a : ι) → E) i⟫ = ⟪(b : (a : ι) → E) i, y⟫
⊢ ⟪(b : (a : ι) → E) i, x⟫ = ⟪(b : (a : ι) → E) i, y⟫

Tactic:
rw [← inner_conj_symm]

Premises used: inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
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 : ι
rw : ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, (b : (a : ι) → E) i⟫ : 𝕜)
| ⟪(b : (a : ι) → E) i, y⟫

Tactic:
rw [← inner_conj_symm]

Premises used: inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
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 : ι
conv_rhs :
  Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, (b : (a : ι) → E) i⟫ : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, (b : (a : ι) → E) i⟫ : 𝕜)
⊢ (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, (b : (a : ι) → E) i⟫ = ⟪(b : (a : ι) → E) i, y⟫

Tactic:
conv_rhs => rw [← inner_conj_symm]

Premises used: inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.Dual
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 : ι
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, (b : (a : ι) → E) i⟫ : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, (b : (a : ι) → E) i⟫ : 𝕜)

Tactic:
congr_arg conj (h i)

Premises used: congr_arg, starRingEnd, 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
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), ⟪x, (b : (a : ι) → E) i⟫ = ⟪y, (b : (a : ι) → E) i⟫
i : ι
⊢ Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪x, (b : (a : ι) → E) i⟫ : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪y, (b : (a : ι) → E) i⟫ : 𝕜)

Tactic:
exact congr_arg conj (h i)

Premises used: congr_arg, starRingEnd, 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
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ : E →ₗ[𝕜] 𝕜).ker
pos : ∀ (htriv : Y = ⊤), ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ
neg : ∀ (htriv : ¬Y = ⊤), ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ
⊢ ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ

Tactic:
by_cases htriv : Y = ⊤
-- 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
htriv : Y = ⊤
⊢ (↑ℓ : E →ₗ[𝕜] 𝕜) = 0

Tactic:
have h' := LinearMap.ker_eq_top.mp htriv
-- 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
htriv : Y = ⊤
h' : (↑ℓ : E →ₗ[𝕜] 𝕜) = 0
⊢ (↑ℓ : E →ₗ[𝕜] 𝕜) = (↑0 : E →ₗ[𝕜] 𝕜)

Tactic:
rw [← coe_zero] at h'

Premises used: ContinuousLinearMap.coe_zero
-- 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
htriv : Y = ⊤
h' : (↑ℓ : E →ₗ[𝕜] 𝕜) = (↑0 : E →ₗ[𝕜] 𝕜)
a : (↑ℓ : E →ₗ[𝕜] 𝕜) = (↑0 : E →ₗ[𝕜] 𝕜)
⊢ ℓ = 0

Tactic:
apply coe_injective

Premises used: ContinuousLinearMap.coe_injective
-- 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
htriv : Y = ⊤
h' : (↑ℓ : E →ₗ[𝕜] 𝕜) = (↑0 : E →ₗ[𝕜] 𝕜)
⊢ (↑ℓ : E →ₗ[𝕜] 𝕜) = (↑0 : E →ₗ[𝕜] 𝕜)

Tactic:
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
htriv : Y = ⊤
h' : (↑ℓ : E →ₗ[𝕜] 𝕜) = (↑0 : E →ₗ[𝕜] 𝕜)
⊢ (↑ℓ : E →ₗ[𝕜] 𝕜) = (↑0 : E →ₗ[𝕜] 𝕜)

Tactic:
exact 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
htriv : Y = ⊤
⊢ ℓ = 0

Tactic:
have hℓ : ℓ = 0 := by
          have h' := LinearMap.ker_eq_top.mp htriv
          rw [← coe_zero] at h'
          apply coe_injective
          exact 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
htriv : Y = ⊤
hℓ : ℓ = 0
⊢ (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) 0 = ℓ

Tactic:
simp [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
htriv : Y = ⊤
hℓ : ℓ = 0
⊢ ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ

Tactic:
exact ⟨0, by simp [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
htriv : ¬Y = ⊤
⊢ ¬Yᗮ = ⊥

Tactic:
rw [← Submodule.orthogonal_eq_bot_iff] at htriv

Premises used: Submodule.orthogonal_eq_bot_iff
-- 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
htriv : ¬Yᗮ = ⊥
⊢ Yᗮ ≠ ⊥

Tactic:
change Yᗮ ≠ ⊥ at htriv
-- 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
htriv : Yᗮ ≠ ⊥
⊢ ∃ x ∈ Yᗮ, x ≠ 0

Tactic:
rw [Submodule.ne_bot_iff] at htriv

Premises used: Submodule.ne_bot_iff
-- 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
htriv : ∃ x ∈ Yᗮ, x ≠ 0
neg : ∀ (z : E) (hz : z ∈ Yᗮ) (z_ne_0 : z ≠ 0), ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ
⊢ ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ

Tactic:
obtain ⟨z : E, hz : z ∈ Yᗮ, z_ne_0 : z ≠ 0⟩ := htriv
-- 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
⊢ ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ

Tactic:
⟨(starRingEnd (R := 𝕜) (ℓ z) / ⟪z, z⟫) • z, ?_⟩

Premises used: Inner.inner, HDiv.hDiv, Exists.intro, HSMul.hSMul, starRingEnd, 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
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ : E →ₗ[𝕜] 𝕜).ker
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
neg :
  (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E)
      (HDiv.hDiv (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) : 𝕜) ⟪z, z⟫ • z) =
    ℓ
⊢ ∃ (a : E), (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E) a = ℓ

Tactic:
refine ⟨(starRingEnd (R := 𝕜) (ℓ z) / ⟪z, z⟫) • z, ?_⟩
-- 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
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 : 𝕜)
⊢ (toDualMap 𝕜 E : (a : E) → StrongDual 𝕜 E)
      (HDiv.hDiv (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) : 𝕜) ⟪z, z⟫ • z) =
    ℓ

Tactic:
apply ContinuousLinearMap.ext

Premises used: ContinuousLinearMap.ext
-- 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
rw :
  HMul.hMul (α := 𝕜) (β := 𝕜) (((↑ℓ : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) x : 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) -
      HMul.hMul (α := 𝕜) (β := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) (((↑ℓ : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) z : 𝕜) =
    0
⊢ 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:
rw [LinearMap.mem_ker, map_sub, map_smul, map_smul, smul_eq_mul,
            smul_eq_mul, mul_comm]

Premises used: map_sub, LinearMap.mem_ker, mul_comm, smul_eq_mul, map_smul
-- 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
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) (((↑ℓ : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) x : 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) -
      HMul.hMul (α := 𝕜) (β := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) (((↑ℓ : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) z : 𝕜) =
    0

Tactic:
sub_self (ℓ x * ℓ z)

Premises used: HMul.hMul, sub_self, 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
ℓ : StrongDual 𝕜 E
Y : Submodule 𝕜 E := (↑ℓ : E →ₗ[𝕜] 𝕜).ker
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
⊢ HMul.hMul (α := 𝕜) (β := 𝕜) (((↑ℓ : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) x : 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) -
      HMul.hMul (α := 𝕜) (β := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) (((↑ℓ : E →ₗ[𝕜] 𝕜) : (a : E) → 𝕜) z : 𝕜) =
    0

Tactic:
exact sub_self (ℓ x * ℓ z)

Premises used: HMul.hMul, sub_self, 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
ℓ : 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

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)
-- 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₁ a :
  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
⊢ 0 =
    ⟪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⟫

Tactic:
rw [(Y.mem_orthogonal' z).mp hz]

Premises used: Submodule.mem_orthogonal', Iff.mp
-- 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
⊢ 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:
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
⊢ 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:
exact 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
rw 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⟫
⊢ ⟪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⟫

Tactic:
rw [inner_sub_right]

Premises used: inner_sub_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
ℓ : 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⟫ -
      ⟪z, HSMul.hSMul.{u_1, u_2, u_2} (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) z⟫ =
    HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) z : 𝕜) ⟪z, x⟫ - HMul.hMul (α := 𝕜) ((ℓ : (a : E) → 𝕜) x : 𝕜) ⟪z, z⟫

Tactic:
simp [inner_smul_right]

Premises used: inner_smul_right