diff --git a/SciLean/Core/Simp.lean b/SciLean/Core/Simp.lean
index 11882dfc..25a4ee51 100644
--- a/SciLean/Core/Simp.lean
+++ b/SciLean/Core/Simp.lean
@@ -10,3 +10,6 @@ register_simp_attr neg_pull
 register_simp_attr neg_push
 register_simp_attr smul_pull
 register_simp_attr smul_push
+
+
+register_simp_attr simp_core
diff --git a/SciLean/Mathlib/Analysis/AdjointSpace/Adjoint.lean b/SciLean/Mathlib/Analysis/AdjointSpace/Adjoint.lean
new file mode 100644
index 00000000..5b91cbd2
--- /dev/null
+++ b/SciLean/Mathlib/Analysis/AdjointSpace/Adjoint.lean
@@ -0,0 +1,461 @@
+import SciLean.Mathlib.Analysis.AdjointSpace.Basic
+
+import SciLean.Core.FunctionPropositions.IsContinuousLinearMap
+import SciLean.Core.Objects.SemiInnerProductSpace
+
+import SciLean.Tactic.FunTrans.Elab
+import SciLean.Tactic.FunTrans.Attr
+
+set_option linter.unusedVariables false
+
+open RCLike
+
+open scoped ComplexConjugate
+
+variable {𝕜 E F G : Type*} [RCLike 𝕜]
+variable [NormedAddCommGroup E] [NormedAddCommGroup F] [NormedAddCommGroup G]
+variable [AdjointSpace 𝕜 E] [AdjointSpace 𝕜 F] [AdjointSpace 𝕜 G]
+
+set_default_scalar 𝕜
+
+/-! ### Adjoint operator -/
+
+open AdjointSpace SciLean
+
+variable [CompleteSpace E] [CompleteSpace G]
+
+
+variable (𝕜)
+open Classical in
+/-- The adjoint of a bounded operator from Hilbert space `E` to Hilbert space `F`. -/
+@[fun_trans]
+noncomputable
+def adjoint (f : E → F) : F → E :=
+  if h : ∃ g : F → E, ∀ x y, ⟪f x, y⟫ = ⟪x, g y⟫ then
+    choose h
+  else
+    0
+variable {𝕜}
+
+
+postfix:1000 "†" => adjoint defaultScalar%
+
+
+theorem adjoint_ex (A : E → F) (hA : IsContinuousLinearMap 𝕜 A) :
+    ∀ x y, ⟪A x, y⟫ = ⟪x, (A†) y⟫ := sorry_proof
+
+theorem adjoint_clm {A : E → F} (hA : IsContinuousLinearMap 𝕜 A) : IsContinuousLinearMap 𝕜 (A†) :=
+    sorry_proof
+
+
+/-- The fundamental property of the adjoint. -/
+theorem adjoint_inner_left (A : E → F) (hA : IsContinuousLinearMap 𝕜 A) (x : E) (y : F) :
+    ⟪(A†) y, x⟫ = ⟪y, A x⟫ := by
+  rw[← AdjointSpace.conj_symm]
+  rw[← adjoint_ex _ hA]
+  rw[AdjointSpace.conj_symm]
+
+
+/-- The fundamental property of the adjoint. -/
+theorem adjoint_inner_right (A : E → F) (hA : IsContinuousLinearMap 𝕜 A) (x : E) (y : F) :
+    ⟪x, (A†) y⟫ = ⟪A x, y⟫ := by
+  rw[← adjoint_ex _ hA]
+
+/-- The adjoint is involutive. -/
+@[simp]
+theorem adjoint_adjoint (A : E → F) (hA : IsContinuousLinearMap 𝕜 A) : A†† = A := by
+  funext u
+  apply AdjointSpace.ext_inner_left 𝕜
+  intro v
+  rw[← adjoint_ex _ (adjoint_clm hA)]
+  apply adjoint_inner_left _ hA
+
+
+/-- The adjoint of the composition of two operators is the composition of the two adjoints
+in reverse order. -/
+theorem adjoint_comp (A : F → G) (B : E → F)
+    (hA : IsContinuousLinearMap 𝕜 A) (hB : IsContinuousLinearMap 𝕜 B) :
+    (A ∘ B)† = B† ∘ A† := by
+  funext u
+  apply AdjointSpace.ext_inner_left 𝕜
+  intro v; dsimp
+  rw[← adjoint_ex _ (by fun_prop), ← adjoint_ex _ hB,← adjoint_ex _ hA]
+  rfl
+
+/-- The adjoint is unique: a map `A` is the adjoint of `B` iff it satisfies `⟪A x, y⟫ = ⟪x, B y⟫`
+for all `x` and `y`. -/
+theorem eq_adjoint_iff (A : E → F) (B : F → E) (hB : IsContinuousLinearMap 𝕜 B) :
+    A = B† ↔ ∀ x y, ⟪A x, y⟫ = ⟪x, B y⟫ := by
+  constructor
+  . intro h x y; rw[h,adjoint_inner_left _ hB]
+  . intro h; funext u
+    apply AdjointSpace.ext_inner_right 𝕜
+    intro v
+    rw[adjoint_inner_left _ hB]
+    apply h u v
+
+
+
+----------------------------------------------------------------------------------------------------
+
+namespace adjoint
+
+
+variable
+  {K : Type _} [RCLike K]
+  {X : Type _} [NormedAddCommGroup X] [AdjointSpace K X] [CompleteSpace X]
+  {Y : Type _} [NormedAddCommGroup Y] [AdjointSpace K Y] [CompleteSpace Y]
+  {Z : Type _} [NormedAddCommGroup Z] [AdjointSpace K Z] [CompleteSpace Z]
+  {ι : Type _} [Fintype ι]
+  {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, AdjointSpace K (E i)] [∀ i, CompleteSpace (E i)]
+
+set_default_scalar K
+
+@[fun_trans]
+theorem adjoint_id :
+    (fun x : X => x)† = fun x => x := by
+  rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
+  intros; rfl
+
+
+@[fun_trans]
+theorem const_rule :
+    (fun (x : X) =>L[K] (0 : Y))† = fun x =>L[K] 0 := by
+  rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
+  simp
+
+@[fun_trans]
+theorem proj_rule [DecidableEq ι]
+    (i : ι) :
+    (fun (f : (i' : ι) → E i') => f i)†
+    =
+    fun x => (fun j => if h : i=j then h ▸ x else 0) := by
+  rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
+  intro x y
+  simp[Inner.inner]
+  sorry_proof
+
+@[fun_trans]
+theorem prod_rule
+    (f : X → Y) (g : X → Z)
+    (hf : IsContinuousLinearMap K f) (hg : IsContinuousLinearMap K g) :
+    (fun x => (f x, g x))†
+    =
+    fun yz =>
+      let x₁ := (f†) yz.1
+      let x₂ := (g†) yz.2
+      x₁ + x₂ :=
+by
+  sorry_proof
+
+@[fun_trans]
+theorem comp_rule
+    (f : Y → Z) (g : X → Y)
+    (hf : IsContinuousLinearMap K f) (hg : IsContinuousLinearMap K g) :
+    (fun x => f (g x))†
+    =
+    fun z =>
+      let y := (f†) z
+      let x := (g†) y
+      x := by
+  funext u
+  apply AdjointSpace.ext_inner_left K
+  intro v; dsimp
+  rw[← adjoint_ex _ (by fun_prop), adjoint_ex _ hf,← adjoint_ex _ hg]
+
+
+@[fun_trans]
+theorem let_rule
+    (f : X → Y → Z) (g : X → Y)
+    (hf : IsContinuousLinearMap K (fun xy : X×Y => f xy.1 xy.2)) (hg : IsContinuousLinearMap K g) :
+    (fun x => let y := g x; f x y)†
+    =
+    fun z =>
+      let xy := ((fun (x,y) => f x y)†) z
+      let x' := (g†) xy.2
+      xy.1 + x' :=
+by
+  have h : (fun x => let y := g x; f x y)†
+           =
+           (fun x => (x, g x))† ∘ (fun (x,y) => f x y)†
+         := comp_rule (K:=K) (f:=_) (g:=(fun x => (x, g x))) (hf:=hf) (hg:=by fun_prop)
+  rw[h]
+  fun_trans
+  rfl
+
+
+@[fun_trans]
+theorem pi_rule
+    (f : X → (i : ι) → E i) (hf : ∀ i, IsContinuousLinearMap K (f · i)) :
+    (fun (x : X) (i : ι) => f x i)†
+    =
+    (fun x' => Finset.sum Finset.univ fun i => ((f · i)†) (x' i)) := by
+
+  rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
+  intro x y
+  rw[AdjointSpace.sum_inner]
+  simp (disch:=fun_prop) [adjoint_inner_left]
+  rfl
+
+
+
+
+--------------------------------------------------------------------------------
+-- Function Rules --------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+variable
+  {K : Type _} [RCLike K]
+  {X : Type _} [NormedAddCommGroup X] [AdjointSpace K X] [CompleteSpace X]
+  {Y : Type _} [NormedAddCommGroup Y] [AdjointSpace K Y] [CompleteSpace Y]
+  {Z : Type _} [NormedAddCommGroup Z] [AdjointSpace K Z] [CompleteSpace Z]
+  {ι : Type _} [Fintype ι]
+  {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, AdjointSpace K (E i)] [∀ i, CompleteSpace (E i)]
+
+open SciLean
+
+set_default_scalar K
+
+
+-- Prod ------------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[fun_trans]
+theorem Prod.fst.arg_self.adjoint_rule
+  (f : X → Y×Z) (hf : SciLean.IsContinuousLinearMap K f)
+  : (fun x => (f x).1)†
+    =
+    fun y => (f†) (y,0) :=
+by
+  rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
+  simp (disch:=fun_prop) [adjoint_inner_left]
+  sorry_proof -- todo some lemma about inner product on product spaces
+
+@[fun_trans]
+theorem Prod.snd.arg_self.adjoint_rule
+  (f : X → Y×Z) (hf : SciLean.IsContinuousLinearMap K f)
+  : (fun x => (f x).2)†
+    =
+    fun z => (f†) (0,z) :=
+by
+  rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
+  simp (disch:=fun_prop) [adjoint_inner_left]
+  sorry_proof -- todo some lemma about inner product on product spaces
+
+
+-- HAdd.hAdd -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[fun_trans]
+theorem HAdd.hAdd.arg_a0a1.adjoint_rule
+    (f g : X → Y) (hf : IsContinuousLinearMap K f) (hg : IsContinuousLinearMap K g) :
+    (fun x => f x + g x)†
+    =
+    fun y =>
+      let x₁ := (f†) y
+      let x₂ := (g†) y
+      x₁ + x₂ := by
+  rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
+  simp (disch:=fun_prop) [adjoint_inner_left,AdjointSpace.inner_add_left,AdjointSpace.inner_add_right]
+
+
+
+-- HSub.hSub -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[fun_trans]
+theorem HSub.hSub.arg_a0a1.adjoint_rule
+    (f g : X → Y) (hf : IsContinuousLinearMap K f) (hg : IsContinuousLinearMap K g) :
+    (fun x => f x - g x)†
+    =
+    fun y =>
+      let x₁ := (f†) y
+      let x₂ := (g†) y
+      x₁ - x₂ := by
+  rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
+  simp (disch:=fun_prop) [adjoint_inner_left,AdjointSpace.inner_sub_left,AdjointSpace.inner_sub_right]
+
+
+-- Neg.neg ---------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[fun_trans]
+theorem Neg.neg.arg_a0.adjoint_rule
+  (f : X → Y) (hf : IsContinuousLinearMap K f)
+  : (fun x => - f x)†
+    =
+    fun y => - (f†) y :=
+by
+  rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
+  simp (disch:=fun_prop) [adjoint_inner_left,AdjointSpace.inner_neg_left,AdjointSpace.inner_neg_right]
+
+
+-- HMul.hmul -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+open ComplexConjugate in
+@[fun_trans]
+theorem HMul.hMul.arg_a0.adjoint_rule
+  (c : K) (f : X → K) (hf : IsContinuousLinearMap K f)
+  : (fun x => f x * c)†
+    =
+    fun y => conj c • (f†) y :=
+by
+  rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
+  simp (disch:=fun_prop)
+    [adjoint_inner_left,AdjointSpace.inner_smul_left,AdjointSpace.inner_smul_right]
+  intros; ac_rfl
+
+open ComplexConjugate in
+@[fun_trans]
+theorem HMul.hMul.arg_a1.adjoint_rule
+  (c : K) (f : X → K) (hf : IsContinuousLinearMap K f)
+  : (fun x => c * f x)†
+    =
+    fun y => conj c • (f†) y :=
+by
+  rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
+  simp (disch:=fun_prop)
+    [adjoint_inner_left,AdjointSpace.inner_smul_left,AdjointSpace.inner_smul_right]
+  intros; ac_rfl
+
+
+-- SMul.smul -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+open ComplexConjugate in
+@[fun_trans]
+theorem HSMul.hSMul.arg_a0.adjoint_rule
+  (x' : X) (f : X → K) (hf : IsContinuousLinearMap K f)
+  : (fun x => f x • x')†
+    =
+    fun y => ⟪x', y⟫ • ((fun x =>L[K] f x)†) 1 :=
+by
+  rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
+  simp (disch:=fun_prop)
+    [adjoint_inner_left,AdjointSpace.inner_smul_left,AdjointSpace.inner_smul_right]
+  intros; ac_rfl
+
+open ComplexConjugate in
+@[fun_trans]
+theorem HSMul.hSMul.arg_a1.adjoint_rule
+  (c : K) (g : X → Y) (hg : IsContinuousLinearMap K g)
+  : (fun x => c • g x)†
+    =
+    fun y => (conj c) • ((fun x =>L[K] g x)†) y :=
+by
+  rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
+  simp (disch:=fun_prop)
+    [adjoint_inner_left,AdjointSpace.inner_smul_left,AdjointSpace.inner_smul_right]
+
+
+-- HDiv.hDiv -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+open ComplexConjugate in
+@[fun_trans]
+theorem HDiv.hDiv.arg_a0.adjoint_rule
+  (f : X → K) (c : K)
+  (hf : IsContinuousLinearMap K f)
+  : (fun x => f x / c)†
+    =
+    fun y => (conj c)⁻¹ • (fun x =>L[K] f x)† y :=
+by
+  rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
+  simp (disch:=fun_prop)
+    [adjoint_inner_left,AdjointSpace.inner_smul_left,AdjointSpace.inner_smul_right]
+  simp [div_eq_mul_inv]
+  intros; ac_rfl
+
+
+
+-- Finset.sum ------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+open BigOperators in
+@[fun_trans]
+theorem Finset.sum.arg_f.adjoint_rule
+  (f : X → ι → Y) (hf : ∀ i, IsContinuousLinearMap K (f · i)) (A : Finset ι)
+  : (fun x => Finset.sum Finset.univ fun i => f x i)†
+    =
+    (fun y => Finset.sum Finset.univ fun i => ((f · i)†) y) :=
+by
+  rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
+  simp (disch:=fun_prop) [adjoint_inner_left,AdjointSpace.sum_inner,AdjointSpace.inner_sum]
+
+
+-- d/ite -----------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[fun_trans]
+theorem ite.arg_te.adjoint_rule
+  (c : Prop) [dec : Decidable c]
+  (t e : X → Y) (ht : IsContinuousLinearMap K t) (he : IsContinuousLinearMap K e)
+  : (fun x => if c then t x else e x)†
+    =
+    fun y =>
+      if c then (t†) y else (e†) y :=
+by
+  induction dec
+  case isTrue h  => ext y; simp[h]
+  case isFalse h => ext y; simp[h]
+
+@[fun_trans]
+theorem dite.arg_te.adjoint_rule
+  (c : Prop) [dec : Decidable c]
+  (t : c  → X → Y) (ht : ∀ p, IsContinuousLinearMap K (t p))
+  (e : ¬c → X → Y) (he : ∀ p, IsContinuousLinearMap K (e p))
+  : (fun x => if h : c then t h x else e h x)†
+    =
+    fun y =>
+      if h : c then ((t h ·)†) y else ((e h ·)†) y :=
+by
+  induction dec
+  case isTrue h  => ext y; simp[h]
+  case isFalse h => ext y; simp[h]
+
+
+
+-- Inner -----------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[fun_trans]
+theorem Inner.inner.arg_a1.adjoint_rule
+  (f : X → Y) (hf : IsContinuousLinearMap K f) (y : Y)
+  : (fun x => ⟪y, f x⟫)†
+    =
+    fun z => z • (f†) y :=
+by
+  rw[← (eq_adjoint_iff _ _ (by sorry_proof)).2]
+  simp (disch:=fun_prop)
+    [adjoint_inner_left,AdjointSpace.inner_smul_left,AdjointSpace.conj_symm]
+
+
+section OnRealSpace
+
+variable
+  {R : Type _} [RealScalar R]
+  {X : Type _} [NormedAddCommGroup X] [AdjointSpace R X] [CompleteSpace X]
+  {Y : Type _} [NormedAddCommGroup Y] [AdjointSpace R Y] [CompleteSpace Y]
+
+open SciLean
+
+set_default_scalar R
+
+-- inner product is not ℂ-linear in its first argument thus it can't have an adjoint
+open ComplexConjugate in
+@[fun_trans]
+theorem Inner.inner.arg_a0.adjoint_rule
+  (f : X → Y) (hf : IsContinuousLinearMap R f) (y : Y)
+  : (fun x => ⟪f x, y⟫)†
+    =
+    fun z => (conj z) • (f†) y :=
+by
+  rw[← (eq_adjoint_iff _ _ (by sorry_proof)).2]
+  simp (disch:=fun_prop)
+    [adjoint_inner_left,AdjointSpace.inner_smul_left,AdjointSpace.conj_symm]
+  intros
+  rw[← AdjointSpace.conj_symm]; simp
+
+
+end OnRealSpace
diff --git a/SciLean/Mathlib/Analysis/AdjointSpace/Basic.lean b/SciLean/Mathlib/Analysis/AdjointSpace/Basic.lean
new file mode 100644
index 00000000..aeb9bc0e
--- /dev/null
+++ b/SciLean/Mathlib/Analysis/AdjointSpace/Basic.lean
@@ -0,0 +1,257 @@
+import Mathlib.Analysis.NormedSpace.Basic
+import Mathlib.Analysis.InnerProductSpace.Basic
+
+import SciLean.Util.SorryProof
+import SciLean.Core.Simp
+
+open ComplexConjugate RCLike
+/--
+This is almost `InnerProductSpace` but we do not require that norm originates from the inner product.
+
+The reason for this class it to be able to have inner product on spaces line `ℝ×ℝ` and `ι → ℝ`
+as they are by default equiped by max norm which is not compatible with inner product. -/
+class AdjointSpace (𝕜 : Type*) (E : Type*) [RCLike 𝕜] [NormedAddCommGroup E] extends
+  NormedSpace 𝕜 E, Inner 𝕜 E where
+  /-- Norm induced by inner is topologicaly equivalent to the given norm -/
+  inner_top_equiv_norm : ∃ c d : ℝ,
+    c > 0 ∧ d > 0 ∧
+    ∀ x : E, (c • ‖x‖ ≤ (re (inner x x)).sqrt) ∧ ((re (inner x x)).sqrt ≤ d • ‖x‖)
+  /-- The inner product is *hermitian*, taking the `conj` swaps the arguments. -/
+  conj_symm : ∀ x y, conj (inner y x) = inner x y
+  /-- The inner product is additive in the first coordinate. -/
+  add_left : ∀ x y z, inner (x + y) z = inner x z + inner y z
+  /-- The inner product is conjugate linear in the first coordinate. -/
+  smul_left : ∀ x y r, inner (r • x) y = conj r * inner x y
+
+
+/-! ### Properties of inner product spaces -/
+
+namespace AdjointSpace
+
+variable {𝕜 E F : Type*} [RCLike 𝕜]
+
+variable [NormedAddCommGroup E] [AdjointSpace 𝕜 E]
+variable [NormedAddCommGroup F] [AdjointSpace ℝ F]
+
+local notation "⟪" x ", " y "⟫" => @inner 𝕜 E _ x y
+
+local notation "IK" => @RCLike.I 𝕜 _
+
+local postfix:90 "†" => starRingEnd _
+
+export InnerProductSpace (norm_sq_eq_inner)
+
+open RCLike ComplexConjugate
+
+section BasicProperties
+
+@[simp mid+1, simp_core mid+1]
+theorem inner_conj_symm (x y : E) : ⟪y, x⟫† = ⟪x, y⟫ := sorry_proof
+
+theorem real_inner_comm (x y : F) : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := sorry_proof
+
+theorem inner_eq_zero_symm {x y : E} : ⟪x, y⟫ = 0 ↔ ⟪y, x⟫ = 0 := by
+  rw [← inner_conj_symm]
+  exact star_eq_zero
+
+@[simp mid+1, simp_core mid+1]
+theorem inner_self_im (x : E) : RCLike.im ⟪x, x⟫ = 0 := by
+  rw [← @ofReal_inj 𝕜, im_eq_conj_sub]; simp
+
+theorem inner_add_left (x y z : E) : ⟪x + y, z⟫ = ⟪x, z⟫ + ⟪y, z⟫ :=  sorry_proof
+
+theorem inner_add_right (x y z : E) : ⟪x, y + z⟫ = ⟪x, y⟫ + ⟪x, z⟫ := by
+  rw [← inner_conj_symm, inner_add_left, RingHom.map_add]
+  simp only [inner_conj_symm]
+
+theorem inner_re_symm (x y : E) : re ⟪x, y⟫ = re ⟪y, x⟫ := by rw [← inner_conj_symm, conj_re]
+
+theorem inner_im_symm (x y : E) : im ⟪x, y⟫ = -im ⟪y, x⟫ := by rw [← inner_conj_symm, conj_im]
+
+theorem inner_smul_left (x y : E) (r : 𝕜) : ⟪r • x, y⟫ = r† * ⟪x, y⟫ := sorry_proof
+
+theorem real_inner_smul_left (x y : F) (r : ℝ) : ⟪r • x, y⟫_ℝ = r * ⟪x, y⟫_ℝ :=
+  inner_smul_left _ _ _
+
+theorem inner_smul_real_left (x y : E) (r : ℝ) : ⟪(r : 𝕜) • x, y⟫ = r • ⟪x, y⟫ := by
+  rw [inner_smul_left, conj_ofReal, Algebra.smul_def]
+  rfl
+
+theorem inner_smul_right (x y : E) (r : 𝕜) : ⟪x, r • y⟫ = r * ⟪x, y⟫ := by
+  rw [← inner_conj_symm, inner_smul_left, RingHom.map_mul, conj_conj, inner_conj_symm]
+
+theorem real_inner_smul_right (x y : F) (r : ℝ) : ⟪x, r • y⟫_ℝ = r * ⟪x, y⟫_ℝ :=
+  inner_smul_right _ _ _
+
+theorem inner_smul_real_right (x y : E) (r : ℝ) : ⟪x, (r : 𝕜) • y⟫ = r • ⟪x, y⟫ := by
+  rw [inner_smul_right, Algebra.smul_def]
+  rfl
+
+/-- The inner product as a sesquilinear form.
+
+Note that in the case `𝕜 = ℝ` this is a bilinear form. -/
+@[simps!]
+def sesqFormOfInner : E →ₗ[𝕜] E →ₗ⋆[𝕜] 𝕜 :=
+  LinearMap.mk₂'ₛₗ (RingHom.id 𝕜) (starRingEnd _) (fun x y => ⟪y, x⟫)
+    (fun _x _y _z => inner_add_right _ _ _) (fun _r _x _y => inner_smul_right _ _ _)
+    (fun _x _y _z => inner_add_left _ _ _) fun _r _x _y => inner_smul_left _ _ _
+
+
+/-- An inner product with a sum on the left. -/
+theorem sum_inner {ι : Type*} (s : Finset ι) (f : ι → E) (x : E) :
+    ⟪∑ i ∈ s, f i, x⟫ = ∑ i ∈ s, ⟪f i, x⟫ :=
+  map_sum (sesqFormOfInner (𝕜 := 𝕜) (E := E) x) _ _
+
+/-- An inner product with a sum on the right. -/
+theorem inner_sum {ι : Type*} (s : Finset ι) (f : ι → E) (x : E) :
+    ⟪x, ∑ i ∈ s, f i⟫ = ∑ i ∈ s, ⟪x, f i⟫ :=
+  map_sum (LinearMap.flip sesqFormOfInner x) _ _
+
+@[simp mid+1, simp_core mid+1]
+theorem inner_zero_left (x : E) : ⟪0, x⟫ = 0 := by
+  rw [← zero_smul 𝕜 (0 : E), inner_smul_left, RingHom.map_zero, zero_mul]
+
+theorem inner_re_zero_left (x : E) : re ⟪0, x⟫ = 0 := by
+  simp only [inner_zero_left, AddMonoidHom.map_zero]
+
+@[simp mid+1, simp_core mid+1]
+theorem inner_zero_right (x : E) : ⟪x, 0⟫ = 0 := by
+  rw [← inner_conj_symm, inner_zero_left, RingHom.map_zero]
+
+theorem inner_re_zero_right (x : E) : re ⟪x, 0⟫ = 0 := by
+  simp only [inner_zero_right, AddMonoidHom.map_zero]
+
+theorem inner_self_nonneg {x : E} : 0 ≤ re ⟪x, x⟫ := sorry_proof
+
+theorem real_inner_self_nonneg {x : F} : 0 ≤ ⟪x, x⟫_ℝ :=
+  @inner_self_nonneg ℝ F _ _ _ x
+
+@[simp mid+1, simp_core mid+1]
+theorem inner_self_ofReal_re (x : E) : (re ⟪x, x⟫ : 𝕜) = ⟪x, x⟫ :=
+  ((RCLike.is_real_TFAE (⟪x, x⟫ : 𝕜)).out 2 3).2 (inner_self_im _)
+
+
+@[simp mid+1, simp_core mid+1]
+theorem inner_self_eq_zero {x : E} : ⟪x, x⟫ = 0 ↔ x = 0 := sorry_proof
+
+theorem inner_self_ne_zero {x : E} : ⟪x, x⟫ ≠ 0 ↔ x ≠ 0 :=
+  inner_self_eq_zero.not
+
+@[simp mid+1, simp_core mid+1]
+theorem inner_self_nonpos {x : E} : re ⟪x, x⟫ ≤ 0 ↔ x = 0 := sorry_proof
+
+theorem real_inner_self_nonpos {x : F} : ⟪x, x⟫_ℝ ≤ 0 ↔ x = 0 :=
+  @inner_self_nonpos ℝ F _ _ _ x
+
+theorem norm_inner_symm (x y : E) : ‖⟪x, y⟫‖ = ‖⟪y, x⟫‖ := by rw [← inner_conj_symm, norm_conj]
+
+
+@[simp mid+1, simp_core mid+1]
+theorem inner_neg_left (x y : E) : ⟪-x, y⟫ = -⟪x, y⟫ := by
+  rw [← neg_one_smul 𝕜 x, inner_smul_left]
+  simp
+
+@[simp mid+1, simp_core mid+1]
+theorem inner_neg_right (x y : E) : ⟪x, -y⟫ = -⟪x, y⟫ := by
+  rw [← inner_conj_symm, inner_neg_left]; simp only [RingHom.map_neg, inner_conj_symm]
+
+theorem inner_neg_neg (x y : E) : ⟪-x, -y⟫ = ⟪x, y⟫ := by simp
+
+-- Porting note: removed `simp` because it can prove it using `inner_conj_symm`
+theorem inner_self_conj (x : E) : ⟪x, x⟫† = ⟪x, x⟫ := inner_conj_symm _ _
+
+theorem inner_sub_left (x y z : E) : ⟪x - y, z⟫ = ⟪x, z⟫ - ⟪y, z⟫ := by
+  simp [sub_eq_add_neg, inner_add_left]
+
+theorem inner_sub_right (x y z : E) : ⟪x, y - z⟫ = ⟪x, y⟫ - ⟪x, z⟫ := by
+  simp [sub_eq_add_neg, inner_add_right]
+
+theorem inner_mul_symm_re_eq_norm (x y : E) : re (⟪x, y⟫ * ⟪y, x⟫) = ‖⟪x, y⟫ * ⟪y, x⟫‖ := by
+  rw [← inner_conj_symm, mul_comm]
+  exact re_eq_norm_of_mul_conj (inner y x)
+
+/-- Expand `⟪x + y, x + y⟫` -/
+theorem inner_add_add_self (x y : E) : ⟪x + y, x + y⟫ = ⟪x, x⟫ + ⟪x, y⟫ + ⟪y, x⟫ + ⟪y, y⟫ := by
+  simp only [inner_add_left, inner_add_right]; ring
+
+/-- Expand `⟪x + y, x + y⟫_ℝ` -/
+theorem real_inner_add_add_self (x y : F) :
+    ⟪x + y, x + y⟫_ℝ = ⟪x, x⟫_ℝ + 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ := by
+  have : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := by rw [← inner_conj_symm]; rfl
+  simp only [inner_add_add_self, this, add_left_inj]
+  ring
+
+-- Expand `⟪x - y, x - y⟫`
+theorem inner_sub_sub_self (x y : E) : ⟪x - y, x - y⟫ = ⟪x, x⟫ - ⟪x, y⟫ - ⟪y, x⟫ + ⟪y, y⟫ := by
+  simp only [inner_sub_left, inner_sub_right]; ring
+
+/-- Expand `⟪x - y, x - y⟫_ℝ` -/
+theorem real_inner_sub_sub_self (x y : F) :
+    ⟪x - y, x - y⟫_ℝ = ⟪x, x⟫_ℝ - 2 * ⟪x, y⟫_ℝ + ⟪y, y⟫_ℝ := by
+  have : ⟪y, x⟫_ℝ = ⟪x, y⟫_ℝ := by rw [← inner_conj_symm]; rfl
+  simp only [inner_sub_sub_self, this, add_left_inj]
+  ring
+
+variable (𝕜)
+
+theorem ext_inner_left {x y : E} (h : ∀ v, ⟪v, x⟫ = ⟪v, y⟫) : x = y := by
+  rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_right, sub_eq_zero, h (x - y)]
+
+theorem ext_inner_right {x y : E} (h : ∀ v, ⟪x, v⟫ = ⟪y, v⟫) : x = y := by
+  rw [← sub_eq_zero, ← @inner_self_eq_zero 𝕜, inner_sub_left, sub_eq_zero, h (x - y)]
+
+
+
+
+/-- The inner product as a sesquilinear map. -/
+def innerₛₗ : E →ₗ⋆[𝕜] E →ₗ[𝕜] 𝕜 :=
+  LinearMap.mk₂'ₛₗ _ _ (fun v w => ⟪v, w⟫) inner_add_left (fun _ _ _ => inner_smul_left _ _ _)
+    inner_add_right fun _ _ _ => inner_smul_right _ _ _
+
+@[simp mid+1, simp_core mid+1]
+theorem innerₛₗ_apply_coe (v : E) : ⇑(innerₛₗ 𝕜 v) = fun w => ⟪v, w⟫ :=
+  rfl
+
+@[simp]
+theorem innerₛₗ_apply (v w : E) : innerₛₗ 𝕜 v w = ⟪v, w⟫ :=
+  rfl
+
+variable (F)
+/-- The inner product as a bilinear map in the real case. -/
+noncomputable
+def innerₗ : F →ₗ[ℝ] F →ₗ[ℝ] ℝ := innerₛₗ ℝ
+
+@[simp] lemma flip_innerₗ : (innerₗ F).flip = innerₗ F := by
+  ext v w
+  exact real_inner_comm v w
+
+
+
+----------------------------------------------------------------------------------------------------
+
+
+variable
+  {X} [NormedAddCommGroup X] [AdjointSpace 𝕜 X]
+  {Y} [NormedAddCommGroup Y] [AdjointSpace 𝕜 Y]
+  {ι} [Fintype ι]
+  {E : ι → Type} [∀ i, NormedAddCommGroup (E i)] [∀ i, AdjointSpace 𝕜 (E i)]
+
+instance : AdjointSpace 𝕜 𝕜 where
+  inner_top_equiv_norm := by sorry_proof
+  conj_symm := by simp[mul_comm]
+  add_left := by simp[add_mul]
+  smul_left := by simp[mul_assoc]
+
+instance : AdjointSpace 𝕜 (X×Y) where
+  inner := fun (x,y) (x',y') => ⟪x,x'⟫_𝕜 + ⟪y,y'⟫_𝕜
+  inner_top_equiv_norm := sorry_proof
+  conj_symm := by simp
+  add_left := by simp[inner_add_left]; intros; ac_rfl
+  smul_left := by simp[inner_smul_left,mul_add]
+
+instance : AdjointSpace 𝕜 ((i : ι) → E i) where
+  inner := fun x y => ∑ i, ⟪x i, y i⟫_𝕜
+  inner_top_equiv_norm := sorry_proof
+  conj_symm := by simp
+  add_left := by simp[inner_add_left,Finset.sum_add_distrib]
+  smul_left := by simp[inner_smul_left,Finset.mul_sum]
diff --git a/SciLean/Mathlib/Analysis/AdjointSpace/Dual.lean b/SciLean/Mathlib/Analysis/AdjointSpace/Dual.lean
new file mode 100644
index 00000000..4a7b8932
--- /dev/null
+++ b/SciLean/Mathlib/Analysis/AdjointSpace/Dual.lean
@@ -0,0 +1,187 @@
+/-
+Copyright (c) 2020 Frédéric Dupuis. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Frédéric Dupuis
+-/
+import SciLean.Mathlib.Analysis.AdjointSpace.Basic
+import Mathlib.Analysis.NormedSpace.Dual
+import Mathlib.Analysis.NormedSpace.Star.Basic
+
+
+/-!
+# The Fréchet-Riesz representation theorem
+
+We consider an inner product space `E` over `𝕜`, which is either `ℝ` or `ℂ`. We define
+`toDualMap`, a conjugate-linear isometric embedding of `E` into its dual, which maps an element
+`x` of the space to `fun y => ⟪x, y⟫`.
+
+Under the hypothesis of completeness (i.e., for Hilbert spaces), we upgrade this to `toDual`, a
+conjugate-linear isometric *equivalence* of `E` onto its dual; that is, we establish the
+surjectivity of `toDualMap`.  This is the Fréchet-Riesz representation theorem: every element of
+the dual of a Hilbert space `E` has the form `fun u => ⟪x, u⟫` for some `x : E`.
+
+For a bounded sesquilinear form `B : E →L⋆[𝕜] E →L[𝕜] 𝕜`,
+we define a map `AdjointSpace.continuousLinearMapOfBilin B : E →L[𝕜] E`,
+given by substituting `E →L[𝕜] 𝕜` with `E` using `toDual`.
+
+
+## References
+
+* [M. Einsiedler and T. Ward, *Functional Analysis, Spectral Theory, and Applications*]
+  [EinsiedlerWard2017]
+
+## Tags
+
+dual, Fréchet-Riesz
+-/
+
+
+noncomputable section
+
+open scoped Classical
+open ComplexConjugate
+
+universe u v
+
+namespace AdjointSpace
+
+open RCLike ContinuousLinearMap
+
+variable (𝕜 : Type*)
+variable (E : Type*) [RCLike 𝕜] [NormedAddCommGroup E] [AdjointSpace 𝕜 E]
+
+local notation "⟪" x ", " y "⟫" => @inner 𝕜 E _ x y
+
+local postfix:90 "†" => starRingEnd _
+
+/-- An element `x` of an inner product space `E` induces an element of the dual space `Dual 𝕜 E`,
+the map `fun y => ⟪x, y⟫`; moreover this operation is a conjugate-linear isometric embedding of `E`
+into `Dual 𝕜 E`.
+If `E` is complete, this operation is surjective, hence a conjugate-linear isometric equivalence;
+see `toDual`.
+-/
+
+def toDualMap : E →ₗᵢ⋆[𝕜] NormedSpace.Dual 𝕜 E :=
+  { innerSL 𝕜 with norm_map' := sorry_proof }
+
+
+variable {E}
+
+@[simp]
+theorem toDualMap_apply {x y : E} : toDualMap 𝕜 E x y = ⟪x, y⟫ :=
+  rfl
+
+theorem innerSL_norm [Nontrivial E] : ‖(innerSL 𝕜 : E →L⋆[𝕜] E →L[𝕜] 𝕜)‖ = 1 :=
+  show ‖(toDualMap 𝕜 E).toContinuousLinearMap‖ = 1 from LinearIsometry.norm_toContinuousLinearMap _
+set_option linter.uppercaseLean3 false in
+#align inner_product_space.innerSL_norm AdjointSpace.innerSL_norm
+
+variable {𝕜}
+
+theorem ext_inner_left_basis {ι : Type*} {x y : E} (b : Basis ι 𝕜 E)
+    (h : ∀ i : ι, ⟪b i, x⟫ = ⟪b i, y⟫) : x = y := by
+  apply (toDualMap 𝕜 E).map_eq_iff.mp
+  refine (Function.Injective.eq_iff ContinuousLinearMap.coe_injective).mp (Basis.ext b ?_)
+  intro i
+  simp only [ContinuousLinearMap.coe_coe]
+  rw [toDualMap_apply, toDualMap_apply]
+  rw [← inner_conj_symm]
+  conv_rhs => rw [← inner_conj_symm]
+  exact congr_arg conj (h i)
+#align inner_product_space.ext_inner_left_basis AdjointSpace.ext_inner_left_basis
+
+theorem ext_inner_right_basis {ι : Type*} {x y : E} (b : Basis ι 𝕜 E)
+    (h : ∀ i : ι, ⟪x, b i⟫ = ⟪y, b i⟫) : x = y := by
+  refine ext_inner_left_basis b fun i => ?_
+  rw [← inner_conj_symm]
+  conv_rhs => rw [← inner_conj_symm]
+  exact congr_arg conj (h i)
+#align inner_product_space.ext_inner_right_basis AdjointSpace.ext_inner_right_basis
+
+variable (𝕜) (E)
+variable [CompleteSpace E]
+
+/-- Fréchet-Riesz representation: any `ℓ` in the dual of a Hilbert space `E` is of the form
+`fun u => ⟪y, u⟫` for some `y : E`, i.e. `toDualMap` is surjective.
+-/
+def toDual : E ≃ₗᵢ⋆[𝕜] NormedSpace.Dual 𝕜 E :=
+  LinearIsometryEquiv.ofSurjective (toDualMap 𝕜 E)
+    (by
+      intro ℓ
+      set Y := LinearMap.ker ℓ
+      by_cases htriv : Y = ⊤
+      · have hℓ : ℓ = 0 := by
+          have h' := LinearMap.ker_eq_top.mp htriv
+          rw [← coe_zero] at h'
+          apply coe_injective
+          exact h'
+        exact ⟨0, by simp [hℓ]⟩
+      · rw [← Submodule.orthogonal_eq_bot_iff] at htriv
+        change Yᗮ ≠ ⊥ at htriv
+        rw [Submodule.ne_bot_iff] at htriv
+        obtain ⟨z : E, hz : z ∈ Yᗮ, z_ne_0 : z ≠ 0⟩ := htriv
+        refine ⟨(starRingEnd (R := 𝕜) (ℓ z) / ⟪z, z⟫) • z, ?_⟩
+        apply ContinuousLinearMap.ext
+        intro x
+        have h₁ : ℓ z • x - ℓ x • z ∈ Y := by
+          rw [LinearMap.mem_ker, map_sub, ContinuousLinearMap.map_smul,
+            ContinuousLinearMap.map_smul, Algebra.id.smul_eq_mul, Algebra.id.smul_eq_mul, mul_comm]
+          exact sub_self (ℓ x * ℓ z)
+        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 (Eq.symm h₃)
+        have h₄ :=
+          calc
+            ⟪(ℓ z† / ⟪z, z⟫) • z, x⟫ = ℓ z / ⟪z, z⟫ * ⟪z, x⟫ := by simp [inner_smul_left, conj_conj]
+            _ = ℓ z * ⟪z, x⟫ / ⟪z, z⟫ := by rw [← div_mul_eq_mul_div]
+            _ = ℓ x * ⟪z, z⟫ / ⟪z, z⟫ := by rw [h₂]
+            _ = ℓ x := by field_simp [inner_self_ne_zero.2 z_ne_0]
+        exact h₄)
+#align inner_product_space.to_dual AdjointSpace.toDual
+
+variable {𝕜} {E}
+
+@[simp]
+theorem toDual_apply {x y : E} : toDual 𝕜 E x y = ⟪x, y⟫ :=
+  rfl
+#align inner_product_space.to_dual_apply AdjointSpace.toDual_apply
+
+@[simp]
+theorem toDual_symm_apply {x : E} {y : NormedSpace.Dual 𝕜 E} : ⟪(toDual 𝕜 E).symm y, x⟫ = y x := by
+  rw [← toDual_apply]
+  simp only [LinearIsometryEquiv.apply_symm_apply]
+#align inner_product_space.to_dual_symm_apply AdjointSpace.toDual_symm_apply
+
+/-- Maps a bounded sesquilinear form to its continuous linear map,
+given by interpreting the form as a map `B : E →L⋆[𝕜] NormedSpace.Dual 𝕜 E`
+and dualizing the result using `toDual`.
+-/
+def continuousLinearMapOfBilin (B : E →L⋆[𝕜] E →L[𝕜] 𝕜) : E →L[𝕜] E :=
+  comp (toDual 𝕜 E).symm.toContinuousLinearEquiv.toContinuousLinearMap B
+#align inner_product_space.continuous_linear_map_of_bilin AdjointSpace.continuousLinearMapOfBilin
+
+local postfix:1024 "♯" => continuousLinearMapOfBilin
+
+variable (B : E →L⋆[𝕜] E →L[𝕜] 𝕜)
+
+@[simp]
+theorem continuousLinearMapOfBilin_apply (v w : E) : ⟪B♯ v, w⟫ = B v w := by
+  rw [continuousLinearMapOfBilin, coe_comp', ContinuousLinearEquiv.coe_coe,
+    LinearIsometryEquiv.coe_toContinuousLinearEquiv, Function.comp_apply, toDual_symm_apply]
+#align inner_product_space.continuous_linear_map_of_bilin_apply AdjointSpace.continuousLinearMapOfBilin_apply
+
+theorem unique_continuousLinearMapOfBilin {v f : E} (is_lax_milgram : ∀ w, ⟪f, w⟫ = B v w) :
+    f = B♯ v := by
+  refine ext_inner_right 𝕜 ?_
+  intro w
+  rw [continuousLinearMapOfBilin_apply]
+  exact is_lax_milgram w
+#align inner_product_space.unique_continuous_linear_map_of_bilin AdjointSpace.unique_continuousLinearMapOfBilin
+
+end AdjointSpace