-- Mathlib/Analysis/InnerProductSpace/LinearPMap.lean
theorem mem_adjoint_domain_of_exists (y : F) (h : ∃ w : E, ∀ x : T.domain, ⟪w, x⟫ = ⟪y, T x⟫) :
    y ∈ T†.domain

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
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
y : F
w : E
hw : ∀ (x : ↥T.domain), inner w ↑x = inner y (↑T x)
⊢ Continuous ⇑(((innerSL 𝕜) w).comp T.domain.subtypeL)

Tactic:
fun_prop

Result:
no goals

Proof state:
case intro
𝕜 : 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
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
y : F
w : E
hw : ∀ (x : ↥T.domain), inner w ↑x = inner y (↑T x)
this : Continuous ⇑(((innerSL 𝕜) w).comp T.domain.subtypeL)
⊢ Continuous ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun)

Tactic:
convert this using 1

Result:
case h.e'_5
𝕜 : 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
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
y : F
w : E
hw : ∀ (x : ↥T.domain), inner w ↑x = inner y (↑T x)
this : Continuous ⇑(((innerSL 𝕜) w).comp T.domain.subtypeL)
⊢ ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun) = ⇑(((innerSL 𝕜) w).comp T.domain.subtypeL)

Proof state:
case h.e'_5
𝕜 : 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
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
y : F
w : E
hw : ∀ (x : ↥T.domain), inner w ↑x = inner y (↑T x)
this : Continuous ⇑(((innerSL 𝕜) w).comp T.domain.subtypeL)
⊢ ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun) = ⇑(((innerSL 𝕜) w).comp T.domain.subtypeL)

Tactic:
exact funext fun x => (hw x).symm

Result:
no goals

Proof state:
case intro
𝕜 : 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
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
y : F
w : E
hw : ∀ (x : ↥T.domain), inner w ↑x = inner y (↑T x)
⊢ Continuous ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun)

Tactic:
have : Continuous ((innerSL 𝕜 w).comp T.domain.subtypeL) := by fun_prop

Result:
case intro
𝕜 : 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
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
y : F
w : E
hw : ∀ (x : ↥T.domain), inner w ↑x = inner y (↑T x)
this : Continuous ⇑(((innerSL 𝕜) w).comp T.domain.subtypeL)
⊢ Continuous ⇑((innerₛₗ 𝕜) y ∘ₗ T.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
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
y : F
h : ∃ w, ∀ (x : ↥T.domain), inner w ↑x = inner y (↑T x)
⊢ y ∈ T†.domain

Tactic:
obtain ⟨w, hw⟩ := h

Result:
case intro
𝕜 : 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
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
y : F
w : E
hw : ∀ (x : ↥T.domain), inner w ↑x = inner y (↑T x)
⊢ y ∈ T†.domain

Proof state:
case intro
𝕜 : 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
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
y : F
w : E
hw : ∀ (x : ↥T.domain), inner w ↑x = inner y (↑T x)
⊢ y ∈ T†.domain

Tactic:
rw [T.mem_adjoint_domain_iff]

Result:
case intro
𝕜 : 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
T : E →ₗ.[𝕜] F
inst✝ : CompleteSpace E
y : F
w : E
hw : ∀ (x : ↥T.domain), inner w ↑x = inner y (↑T x)
⊢ Continuous ⇑((innerₛₗ 𝕜) y ∘ₗ T.toFun)