Theorem: SciLean.HasSemiAdjoint.Inner.inner.arg_a0.HasSemiAdjoint_rule (SciLean/Core/FunctionPropositions/HasSemiAdjoint.lean)

State before:
K✝¹ : Type ?u.52208
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.52214
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.52227
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.52238
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.52249
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.52260
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.52287
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.52303
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.52309
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.52322
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.52333
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.52344
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.52355
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.52382
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ HasSemiAdjoint K fun x => ⟪f x, y⟫_K
Tactic:
constructor
State after:
case semiAdjoint_exists
K✝¹ : Type ?u.52208
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.52214
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.52227
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.52238
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.52249
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.52260
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.52287
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.52303
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.52309
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.52322
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.52333
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.52344
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.52355
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.52382
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ ∃ f', ∀ (x : X) (y_1 : K), TestFunction x → ⟪y_1, ⟪f x, y⟫_K⟫_K = ⟪f' y_1, x⟫_K

case is_differentiable
K✝¹ : Type ?u.52208
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.52214
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.52227
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.52238
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.52249
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.52260
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.52287
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.52303
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.52309
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.52322
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.52333
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.52344
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.52355
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.52382
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ SciLean.CDifferentiable K fun x => ⟪f x, y⟫_K

State before:
case semiAdjoint_exists
K✝¹ : Type ?u.52208
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.52214
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.52227
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.52238
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.52249
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.52260
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.52287
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.52303
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.52309
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.52322
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.52333
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.52344
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.52355
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.52382
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ ∃ f', ∀ (x : X) (y_1 : K), TestFunction x → ⟪y_1, ⟪f x, y⟫_K⟫_K = ⟪f' y_1, x⟫_K

case is_differentiable
K✝¹ : Type ?u.52208
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.52214
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.52227
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.52238
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.52249
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.52260
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.52287
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.52303
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.52309
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.52322
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.52333
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.52344
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.52355
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.52382
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ SciLean.CDifferentiable K fun x => ⟪f x, y⟫_K
Tactic:
. apply Exists.intro (fun (c : K) => (conj c) • semiAdjoint K f y) _
  sorry_proof
State after:
case is_differentiable
K✝¹ : Type ?u.52208
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.52214
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.52227
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.52238
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.52249
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.52260
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.52287
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.52303
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.52309
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.52322
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.52333
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.52344
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.52355
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.52382
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ SciLean.CDifferentiable K fun x => ⟪f x, y⟫_K

State before:
case is_differentiable
K✝¹ : Type ?u.52208
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.52214
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.52227
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.52238
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.52249
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.52260
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.52287
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.52303
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.52309
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.52322
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.52333
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.52344
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.52355
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.52382
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ SciLean.CDifferentiable K fun x => ⟪f x, y⟫_K
Tactic:
. fun_prop
State after:
no goals

State before:
case semiAdjoint_exists
K✝¹ : Type ?u.52208
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.52214
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.52227
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.52238
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.52249
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.52260
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.52287
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.52303
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.52309
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.52322
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.52333
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.52344
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.52355
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.52382
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ ∃ f', ∀ (x : X) (y_1 : K), TestFunction x → ⟪y_1, ⟪f x, y⟫_K⟫_K = ⟪f' y_1, x⟫_K
Tactic:
apply Exists.intro (fun (c : K) => (conj c) • semiAdjoint K f y) _
State after:
K✝¹ : Type ?u.52208
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.52214
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.52227
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.52238
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.52249
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.52260
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.52287
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.52303
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.52309
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.52322
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.52333
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.52344
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.52355
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.52382
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ ∀ (x : X) (y_1 : K),
    TestFunction x → ⟪y_1, ⟪f x, y⟫_K⟫_K = ⟪(fun c => (starRingEnd K) c • semiAdjoint K f y) y_1, x⟫_K

State before:
K✝¹ : Type ?u.52208
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.52214
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.52227
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.52238
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.52249
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.52260
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.52287
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.52303
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.52309
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.52322
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.52333
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.52344
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.52355
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.52382
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ ∀ (x : X) (y_1 : K),
    TestFunction x → ⟪y_1, ⟪f x, y⟫_K⟫_K = ⟪(fun c => (starRingEnd K) c • semiAdjoint K f y) y_1, x⟫_K
Tactic:
sorry_proof
State after:
no goals

State before:
case is_differentiable
K✝¹ : Type ?u.52208
inst✝²⁰ : RCLike K✝¹
X✝¹ : Type ?u.52214
inst✝¹⁹ : SemiInnerProductSpace K✝¹ X✝¹
Y✝¹ : Type ?u.52227
inst✝¹⁸ : SemiInnerProductSpace K✝¹ Y✝¹
Z✝ : Type ?u.52238
inst✝¹⁷ : SemiInnerProductSpace K✝¹ Z✝
W✝ : Type ?u.52249
inst✝¹⁶ : SemiInnerProductSpace K✝¹ W✝
ι✝ : Type ?u.52260
inst✝¹⁵ : IndexType ι✝
inst✝¹⁴ : LawfulIndexType ι✝
inst✝¹³ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.52287
inst✝¹² : (i : ι✝) → SemiInnerProductSpace K✝¹ (E✝ i)
K✝ : Type ?u.52303
inst✝¹¹ : RCLike K✝
X✝ : Type ?u.52309
inst✝¹⁰ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.52322
inst✝⁹ : SemiInnerProductSpace K✝ Y✝
Z : Type ?u.52333
inst✝⁸ : SemiInnerProductSpace K✝ Z
W : Type ?u.52344
inst✝⁷ : SemiInnerProductSpace K✝ W
ι : Type ?u.52355
inst✝⁶ : IndexType ι
inst✝⁵ : LawfulIndexType ι
inst✝⁴ : DecidableEq ι
E : ι → Type ?u.52382
inst✝³ : (i : ι) → SemiInnerProductSpace K✝ (E i)
K : Type u_1
inst✝² : RealScalar K
X : Type u_2
inst✝¹ : SemiInnerProductSpace K X
Y : Type u_3
inst✝ : SemiHilbert K Y
f : X → Y
x✝ : HasSemiAdjoint K f
y : Y
⊢ SciLean.CDifferentiable K fun x => ⟪f x, y⟫_K
Tactic:
fun_prop
State after:
no goals