-- Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
theorem toPMap_adjoint_eq_adjoint_toPMap_of_dense (hp : Dense (p : Set E)) :
    (A.toPMap p).adjoint = A.adjoint.toPMap ⊤

Proof state:
case h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : F
⊢ Continuous ((fun w => inner x w) ∘ ⇑((↑A).toPMap p).toFun)

Tactic:
exact ((innerSL 𝕜 x).comp <| A.comp <| Submodule.subtypeL _).cont

Result:
no goals

Proof state:
case h'.refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : F
y : x ∈ ((↑A).toPMap p).adjoint.domain
hxy : x ∈ ((↑(adjoint A)).toPMap ⊤).domain
⊢ Dense ↑((↑A).toPMap p).domain

Tactic:
simpa using hp

Result:
no goals

Proof state:
case h'
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : F
y : x ∈ ((↑A).toPMap p).adjoint.domain
hxy : x ∈ ((↑(adjoint A)).toPMap ⊤).domain
⊢ ↑((↑A).toPMap p).adjoint ⟨x, y⟩ = ↑((↑(adjoint A)).toPMap ⊤) ⟨x, hxy⟩

Tactic:
refine LinearPMap.adjoint_apply_eq ?_ _ fun v => ?_

Result:
case h'.refine_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : F
y : x ∈ ((↑A).toPMap p).adjoint.domain
hxy : x ∈ ((↑(adjoint A)).toPMap ⊤).domain
⊢ Dense ↑((↑A).toPMap p).domain

case h'.refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : F
y : x ∈ ((↑A).toPMap p).adjoint.domain
hxy : x ∈ ((↑(adjoint A)).toPMap ⊤).domain
v : ↥((↑A).toPMap p).domain
⊢ inner (↑((↑(adjoint A)).toPMap ⊤) ⟨x, hxy⟩) ↑v = inner (↑⟨x, y⟩) (↑((↑A).toPMap p) v)

Proof state:
case h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : F
⊢ x ∈ ((↑A).toPMap p).adjoint.domain ↔ x ∈ ((↑(adjoint A)).toPMap ⊤).domain

Tactic:
simp only [LinearMap.toPMap_domain, Submodule.mem_top, iff_true,
  LinearPMap.mem_adjoint_domain_iff, LinearMap.coe_comp, innerₛₗ_apply_coe]

Result:
case h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : F
⊢ Continuous ((fun w => inner x w) ∘ ⇑((↑A).toPMap p).toFun)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
⊢ ((↑A).toPMap p).adjoint = (↑(adjoint A)).toPMap ⊤

Tactic:
ext x y hxy

Result:
case h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : F
⊢ x ∈ ((↑A).toPMap p).adjoint.domain ↔ x ∈ ((↑(adjoint A)).toPMap ⊤).domain

case h'
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : F
y : x ∈ ((↑A).toPMap p).adjoint.domain
hxy : x ∈ ((↑(adjoint A)).toPMap ⊤).domain
⊢ ↑((↑A).toPMap p).adjoint ⟨x, y⟩ = ↑((↑(adjoint A)).toPMap ⊤) ⟨x, hxy⟩

Proof state:
case h'.refine_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : F
y : x ∈ ((↑A).toPMap p).adjoint.domain
hxy : x ∈ ((↑(adjoint A)).toPMap ⊤).domain
v : ↥((↑A).toPMap p).domain
⊢ inner (↑((↑(adjoint A)).toPMap ⊤) ⟨x, hxy⟩) ↑v = inner (↑⟨x, y⟩) (↑((↑A).toPMap p) v)

Tactic:
simp only [adjoint_inner_left, hxy, LinearMap.toPMap_apply, coe_coe]

Result:
no goals