Theorem: SciLean.HasSemiAdjoint.comp_rule
Proof state before:
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_2
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type u_3
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.18668
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.18679
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18706
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : Y → Z
g : X → Y
hf : HasSemiAdjoint K f
hg : HasSemiAdjoint K g
x✝ : X
y✝ : Z
a✝ : TestFunction x✝
⊢ ⟪y✝, f (g x✝)⟫_K = ⟪semiAdjoint K f y✝, g x✝⟫_K

case hx
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_2
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type u_3
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.18668
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.18679
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18706
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : Y → Z
g : X → Y
hf : HasSemiAdjoint K f
hg : HasSemiAdjoint K g
x✝ : X
y✝ : Z
a✝ : TestFunction x✝
⊢ TestFunction x✝

case hf
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_2
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type u_3
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.18668
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.18679
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18706
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : Y → Z
g : X → Y
hf : HasSemiAdjoint K f
hg : HasSemiAdjoint K g
x✝ : X
y✝ : Z
a✝ : TestFunction x✝
⊢ HasSemiAdjoint K g
Tactic:
rw[semiAdjoint_move]
Proof state after:
case hx
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_2
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type u_3
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.18668
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.18679
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18706
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : Y → Z
g : X → Y
hf : HasSemiAdjoint K f
hg : HasSemiAdjoint K g
x✝ : X
y✝ : Z
a✝ : TestFunction x✝
⊢ TestFunction (g x✝)

case hf
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_2
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type u_3
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.18668
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.18679
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18706
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : Y → Z
g : X → Y
hf : HasSemiAdjoint K f
hg : HasSemiAdjoint K g
x✝ : X
y✝ : Z
a✝ : TestFunction x✝
⊢ HasSemiAdjoint K f

case hx
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_2
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type u_3
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.18668
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.18679
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18706
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : Y → Z
g : X → Y
hf : HasSemiAdjoint K f
hg : HasSemiAdjoint K g
x✝ : X
y✝ : Z
a✝ : TestFunction x✝
⊢ TestFunction x✝

case hf
K : Type u_1
inst✝⁸ : RCLike K
X : Type u_4
inst✝⁷ : SemiInnerProductSpace K X
Y : Type u_2
inst✝⁶ : SemiInnerProductSpace K Y
Z : Type u_3
inst✝⁵ : SemiInnerProductSpace K Z
W : Type ?u.18668
inst✝⁴ : SemiInnerProductSpace K W
ι : Type ?u.18679
inst✝³ : IndexType ι
inst✝² : LawfulIndexType ι
inst✝¹ : DecidableEq ι
E : ι → Type ?u.18706
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
f : Y → Z
g : X → Y
hf : HasSemiAdjoint K f
hg : HasSemiAdjoint K g
x✝ : X
y✝ : Z
a✝ : TestFunction x✝
⊢ HasSemiAdjoint K g