awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
y : F
w : E
hw : ∀ (x : ↥T.domain), ⟪w, (↑x : E)⟫ = ⟪y, (↑T : ↥T.domain → F) x⟫
this :
  Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑(ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) w) T.domain.subtypeL) :
      (a : ↥T.domain) → 𝕜)
⊢ Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑(ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) w) T.domain.subtypeL) :
      (a : ↥T.domain) → 𝕜)

Tactic:
this
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
y : F
w : E
hw : ∀ (x : ↥T.domain), ⟪w, (↑x : E)⟫ = ⟪y, (↑T : ↥T.domain → F) x⟫
this :
  Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑(ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) w) T.domain.subtypeL) :
      (a : ↥T.domain) → 𝕜)
h :
  Eq (α := ↥T.domain → 𝕜) (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)
    (⇑(ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) w) T.domain.subtypeL) :
      (a : ↥T.domain) → 𝕜)
⊢ Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)

Tactic:
convert! this using 1
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
y : F
w : E
hw : ∀ (x : ↥T.domain), ⟪w, (↑x : E)⟫ = ⟪y, (↑T : ↥T.domain → F) x⟫
this :
  Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑(ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) w) T.domain.subtypeL) :
      (a : ↥T.domain) → 𝕜)
⊢ Eq (α := ↥T.domain → 𝕜) (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)
    (⇑(ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) w) T.domain.subtypeL) :
      (a : ↥T.domain) → 𝕜)

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

Premises used: funext, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
y : F
w : E
hw : ∀ (x : ↥T.domain), ⟪w, (↑x : E)⟫ = ⟪y, (↑T : ↥T.domain → F) x⟫
this :
  Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑(ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) w) T.domain.subtypeL) :
      (a : ↥T.domain) → 𝕜)
⊢ Eq (α := ↥T.domain → 𝕜) (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)
    (⇑(ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) w) T.domain.subtypeL) :
      (a : ↥T.domain) → 𝕜)

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

Premises used: funext, Eq.symm
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
hT : ¬Dense (↑T.domain : Set E)
y : ↥T†.domain
change :
  Eq.{u_2 + 1} (α := E)
    ((if hT : Dense (↑T.domain : Set E) then adjointAux hT else 0 : (a : ↥T.adjointDomain) → E) y : E) (0 : E)
⊢ (↑T† : ↥T†.domain → E) y = 0

Tactic:
change (if hT : Dense (T.domain : Set E) then adjointAux hT else 0) y = _

Premises used: LinearPMap.adjointAux, dite, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
hT : ¬Dense (↑T.domain : Set E)
y : ↥T†.domain
⊢ Eq.{u_2 + 1} (α := E)
    ((if hT : Dense (↑T.domain : Set E) then adjointAux hT else 0 : (a : ↥T.adjointDomain) → E) y : E) (0 : E)

Tactic:
simp only [hT, not_false_iff, dif_neg, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, dif_neg, not_false_iff
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
hT : ¬Dense (↑T.domain : Set E)
y : ↥T†.domain
change :
  Eq.{u_2 + 1} (α := E)
    ((if hT : Dense (↑T.domain : Set E) then adjointAux hT else 0 : (a : ↥T.adjointDomain) → E) y : E) (0 : E)
⊢ (↑T† : ↥T†.domain → E) y = 0

Tactic:
classical
  change (if hT : Dense (T.domain : Set E) then adjointAux hT else 0) y = _
  simp only [hT, not_false_iff, dif_neg, LinearMap.zero_apply]

Premises used: LinearMap.zero_apply, dif_neg, not_false_iff
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
hT : Dense (↑T.domain : Set E)
y : ↥T†.domain
change :
  Eq.{u_2 + 1} (α := E)
    ((if hT : Dense (↑T.domain : Set E) then adjointAux hT else 0 : (a : ↥T.adjointDomain) → E) y : E)
    ((adjointAux hT : (a : ↥T.adjointDomain) → E) y : E)
⊢ (↑T† : ↥T†.domain → E) y = (adjointAux hT : (a : ↥T.adjointDomain) → E) y

Tactic:
change (if hT : Dense (T.domain : Set E) then adjointAux hT else 0) y = _

Premises used: LinearPMap.adjointAux, dite, OfNat.ofNat, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
hT : Dense (↑T.domain : Set E)
y : ↥T†.domain
⊢ Eq.{u_2 + 1} (α := E)
    ((if hT : Dense (↑T.domain : Set E) then adjointAux hT else 0 : (a : ↥T.adjointDomain) → E) y : E)
    ((adjointAux hT : (a : ↥T.adjointDomain) → E) y : E)

Tactic:
simp only [hT, dif_pos]

Premises used: dif_pos
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
hT : Dense (↑T.domain : Set E)
y : ↥T†.domain
change :
  Eq.{u_2 + 1} (α := E)
    ((if hT : Dense (↑T.domain : Set E) then adjointAux hT else 0 : (a : ↥T.adjointDomain) → E) y : E)
    ((adjointAux hT : (a : ↥T.adjointDomain) → E) y : E)
⊢ (↑T† : ↥T†.domain → E) y = (adjointAux hT : (a : ↥T.adjointDomain) → E) y

Tactic:
classical
  change (if hT : Dense (T.domain : Set E) then adjointAux hT else 0) y = _
  simp only [hT, dif_pos]

Premises used: dif_pos
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
hT : Dense (↑T.domain : Set E)
y : ↥T†.domain
x₀ : E
hx₀ : ∀ (x : ↥T.domain), ⟪x₀, (↑x : E)⟫ = ⟪(↑y : F), (↑T : ↥T.domain → F) x⟫
⊢ (↑T† : ↥T†.domain → E) y = x₀

Tactic:
(adjoint_apply_of_dense hT y).symm ▸ adjointAux_unique hT _ hx₀

Premises used: LinearPMap.adjointAux_unique, Eq.rec, Eq.symm, LinearPMap.adjoint_apply_of_dense
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
hT : Dense (↑T.domain : Set E)
⊢ T†.IsFormalAdjoint T

Tactic:
fun x =>
  (adjoint_apply_of_dense hT x).symm ▸ adjointAux_inner hT x

Premises used: Eq.rec, LinearPMap.IsFormalAdjoint, Eq.symm, LinearPMap.adjointAux_inner, LinearPMap.adjoint_apply_of_dense
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
inst_5 : CompleteSpace E
hT : Dense (↑T.domain : Set E)
h : T.IsFormalAdjoint S
x : ↥S.domain
x_1 : ↥T†.domain
hxy : (↑x : F) = (↑x_1 : F)
x_2 : ↥T.domain
rw : ⟪(↑x : F), (↑T : ↥T.domain → F) x_2⟫ = ⟪(↑x_1 : F), (↑T : ↥T.domain → F) x_2⟫
rw₁ rw₂ : ⟪(↑x_1 : F), (↑T : ↥T.domain → F) x_2⟫ = ⟪(↑x_1 : F), (↑T : ↥T.domain → F) x_2⟫
⊢ ⟪(↑S : ↥S.domain → E) x, (↑x_2 : E)⟫ = ⟪(↑x_1 : F), (↑T : ↥T.domain → F) x_2⟫

Tactic:
rw [h.symm, hxy]

Premises used: LinearPMap.IsFormalAdjoint.symm
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense (↑p : Set E)
h :
  ∀ (x : F),
    x ∈ ((↑A : E →ₗ[𝕜] F).toPMap p)†.domain ↔
      Membership.mem (γ := Submodule 𝕜 F)
        (domain.{u_1, u_1, u_3, u_2} (S := 𝕜) (σ := RingHom.id 𝕜) (F := E)
          (LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤))
        x
h' :
  ∀ ⦃x : F⦄ ⦃y : x ∈ ((↑A : E →ₗ[𝕜] F).toPMap p)†.domain⦄
    ⦃hxy :
      Membership.mem (γ := Submodule 𝕜 F)
        (domain.{u_1, u_1, u_3, u_2} (S := 𝕜) (σ := RingHom.id 𝕜) (F := E)
          (LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤))
        x⦄,
    (↑((↑A : E →ₗ[𝕜] F).toPMap p)† : ↥((↑A : E →ₗ[𝕜] F).toPMap p)†.domain → E)
        (Subtype.mk (p := fun (x : F) ↦ x ∈ ((↑A : E →ₗ[𝕜] F).toPMap p)†.domain) x y) =
      (↑(LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤) :
          ↥((↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E).toPMap ⊤).domain → E)
        (Subtype.mk (p := fun (x : F) ↦
          Membership.mem (γ := Submodule 𝕜 F)
            (domain.{u_1, u_1, u_3, u_2} (S := 𝕜) (σ := RingHom.id 𝕜) (F := E)
              (LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤))
            x)
          x hxy)
⊢ ((↑A : E →ₗ[𝕜] F).toPMap p)† = LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤

Tactic:
ext x y hxy
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense (↑p : Set E)
x : F
h :
  Continuous.{u_2, u_1} (X := ↥p) (Y := 𝕜)
    (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) x ∘ₗ ((↑A : E →ₗ[𝕜] F).toPMap p).toFun) : (a : ↥p) → 𝕜)
⊢ x ∈ ((↑A : E →ₗ[𝕜] F).toPMap p)†.domain ↔
    Membership.mem (γ := Submodule 𝕜 F)
      (domain.{u_1, u_1, u_3, u_2} (S := 𝕜) (σ := RingHom.id 𝕜) (F := E)
        (LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤))
      x

Tactic:
simp only [LinearMap.toPMap_domain, Submodule.mem_top, iff_true,
      LinearPMap.mem_adjoint_domain_iff]

Premises used: iff_true, LinearMap.toPMap_domain, LinearPMap.mem_adjoint_domain_iff, Submodule.mem_top
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense (↑p : Set E)
x : F
⊢ Continuous.{u_2, u_1} (X := ↥p) (Y := 𝕜)
    (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) x ∘ₗ ((↑A : E →ₗ[𝕜] F).toPMap p).toFun) : (a : ↥p) → 𝕜)

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

Premises used: ContinuousLinearMap.comp, Submodule.subtypeL, innerSL, Set.Mem, ContinuousLinearMap.cont, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense (↑p : Set E)
x : F
⊢ Continuous.{u_2, u_1} (X := ↥p) (Y := 𝕜)
    (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) x ∘ₗ ((↑A : E →ₗ[𝕜] F).toPMap p).toFun) : (a : ↥p) → 𝕜)

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

Premises used: ContinuousLinearMap.comp, Submodule.subtypeL, innerSL, ContinuousLinearMap.cont, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense (↑p : Set E)
x : F
y : x ∈ ((↑A : E →ₗ[𝕜] F).toPMap p)†.domain
hxy :
  Membership.mem (γ := Submodule 𝕜 F)
    (domain.{u_1, u_1, u_3, u_2} (S := 𝕜) (σ := RingHom.id 𝕜) (F := E)
      (LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤))
    x
⊢ (↑((↑A : E →ₗ[𝕜] F).toPMap p)† : ↥((↑A : E →ₗ[𝕜] F).toPMap p)†.domain → E)
      (Subtype.mk (p := fun (x : F) ↦ x ∈ ((↑A : E →ₗ[𝕜] F).toPMap p)†.domain) x y) =
    (↑(LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤) :
        ↥((↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E).toPMap ⊤).domain → E)
      (Subtype.mk (p := fun (x : F) ↦
        Membership.mem (γ := Submodule 𝕜 F)
          (domain.{u_1, u_1, u_3, u_2} (S := 𝕜) (σ := RingHom.id 𝕜) (F := E)
            (LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤))
          x)
        x hxy)

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

Premises used: LinearPMap.adjoint_apply_eq
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense (↑p : Set E)
x : F
y : x ∈ ((↑A : E →ₗ[𝕜] F).toPMap p)†.domain
hxy :
  Membership.mem (γ := Submodule 𝕜 F)
    (domain.{u_1, u_1, u_3, u_2} (S := 𝕜) (σ := RingHom.id 𝕜) (F := E)
      (LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤))
    x
h' :
  ∀ (v : ↥((↑A : E →ₗ[𝕜] F).toPMap p).domain),
    ⟪(↑(LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤) :
            ↥((↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E).toPMap ⊤).domain → E)
          (Subtype.mk (p := fun (x : F) ↦
            Membership.mem (γ := Submodule 𝕜 F)
              (domain.{u_1, u_1, u_3, u_2} (S := 𝕜) (σ := RingHom.id 𝕜) (F := E)
                (LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤))
              x)
            x hxy),
        (↑v : E)⟫ =
      ⟪(↑(Subtype.mk (p := fun (x : F) ↦ x ∈ ((↑A : E →ₗ[𝕜] F).toPMap p)†.domain) x y) : F),
        (↑((↑A : E →ₗ[𝕜] F).toPMap p) : ↥((↑A : E →ₗ[𝕜] F).toPMap p).domain → F) v⟫
⊢ (↑((↑A : E →ₗ[𝕜] F).toPMap p)† : ↥((↑A : E →ₗ[𝕜] F).toPMap p)†.domain → E)
      (Subtype.mk (p := fun (x : F) ↦ x ∈ ((↑A : E →ₗ[𝕜] F).toPMap p)†.domain) x y) =
    (↑(LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤) :
        ↥((↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E).toPMap ⊤).domain → E)
      (Subtype.mk (p := fun (x : F) ↦
        Membership.mem (γ := Submodule 𝕜 F)
          (domain.{u_1, u_1, u_3, u_2} (S := 𝕜) (σ := RingHom.id 𝕜) (F := E)
            (LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤))
          x)
        x hxy)

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

Premises used: LinearPMap.adjoint_apply_eq
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense (↑p : Set E)
x : F
y : x ∈ ((↑A : E →ₗ[𝕜] F).toPMap p)†.domain
hxy :
  Membership.mem (γ := Submodule 𝕜 F)
    (domain.{u_1, u_1, u_3, u_2} (S := 𝕜) (σ := RingHom.id 𝕜) (F := E)
      (LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤))
    x
v : ↥((↑A : E →ₗ[𝕜] F).toPMap p).domain
⊢ ⟪(↑(LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤) :
          ↥((↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E).toPMap ⊤).domain → E)
        (Subtype.mk (p := fun (x : F) ↦
          Membership.mem (γ := Submodule 𝕜 F)
            (domain.{u_1, u_1, u_3, u_2} (S := 𝕜) (σ := RingHom.id 𝕜) (F := E)
              (LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤))
            x)
          x hxy),
      (↑v : E)⟫ =
    ⟪(↑(Subtype.mk (p := fun (x : F) ↦ x ∈ ((↑A : E →ₗ[𝕜] F).toPMap p)†.domain) x y) : F),
      (↑((↑A : E →ₗ[𝕜] F).toPMap p) : ↥((↑A : E →ₗ[𝕜] F).toPMap p).domain → F) v⟫

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

Premises used: LinearMap.toPMap_apply, ContinuousLinearMap.adjoint_inner_left, ContinuousLinearMap.coe_coe
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
A : E →ₗ.[𝕜] E
⊢ IsSelfAdjoint A ↔ A† = A

Tactic:
Iff.rfl

Premises used: IsSelfAdjoint, Iff.rfl
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
g : Submodule 𝕜 (E × F)
x : F × E
simp :
  (∃ (y : WithLp 2 (F × E)),
      (∀ (u : WithLp 2 (F × E)) (x : E) (x_1 : F),
          (x, x_1) ∈ g → toLp 2 (x_1, -x) = u → ⟪u.fst, y.fst⟫ + ⟪u.snd, y.snd⟫ = 0) ∧
        y.ofLp = x) ↔
    ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0
⊢ x ∈ g.adjoint ↔ ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0

Tactic:
simp only [Submodule.adjoint, mem_map, mem_orthogonal, LinearEquiv.coe_coe,
    LinearEquiv.trans_apply, LinearEquiv.skewSwap_symm_apply, coe_symm_linearEquiv, Prod.exists,
    prod_inner_apply, ofLp_fst, ofLp_snd, forall_exists_index, and_imp, coe_linearEquiv]

Premises used: WithLp.prod_inner_apply, WithLp.coe_linearEquiv, LinearEquiv.skewSwap_symm_apply, WithLp.ofLp_fst, Submodule.mem_map, and_imp, forall_exists_index, LinearEquiv.trans_apply, Submodule.mem_orthogonal, Submodule.adjoint, WithLp.ofLp_snd, Prod.exists, WithLp.coe_symm_linearEquiv, LinearEquiv.coe_coe
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
g : Submodule 𝕜 (E × F)
x : F × E
mp :
  (∃ (y : WithLp 2 (F × E)),
      (∀ (u : WithLp 2 (F × E)) (x : E) (x_1 : F),
          (x, x_1) ∈ g → toLp 2 (x_1, -x) = u → ⟪u.fst, y.fst⟫ + ⟪u.snd, y.snd⟫ = 0) ∧
        y.ofLp = x) →
    ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0
mpr :
  (∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0) →
    ∃ (y : WithLp 2 (F × E)),
      (∀ (u : WithLp 2 (F × E)) (x : E) (x_1 : F),
          (x, x_1) ∈ g → toLp 2 (x_1, -x) = u → ⟪u.fst, y.fst⟫ + ⟪u.snd, y.snd⟫ = 0) ∧
        y.ofLp = x
⊢ (∃ (y : WithLp 2 (F × E)),
      (∀ (u : WithLp 2 (F × E)) (x : E) (x_1 : F),
          (x, x_1) ∈ g → toLp 2 (x_1, -x) = u → ⟪u.fst, y.fst⟫ + ⟪u.snd, y.snd⟫ = 0) ∧
        y.ofLp = x) ↔
    ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0

Tactic:
constructor
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
g : Submodule 𝕜 (E × F)
x : F × E
y : WithLp 2 (F × E)
h1 :
  ∀ (u : WithLp 2 (F × E)) (x : E) (x_1 : F), (x, x_1) ∈ g → toLp 2 (x_1, -x) = u → ⟪u.fst, y.fst⟫ + ⟪u.snd, y.snd⟫ = 0
h2 : y.ofLp = x
a : E
b : F
hab : (a, b) ∈ g
mp : ⟪b, y.fst⟫ - ⟪a, y.snd⟫ = 0
⊢ ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0

Tactic:
rw [← h2, WithLp.ofLp_fst, WithLp.ofLp_snd]

Premises used: WithLp.ofLp_fst, WithLp.ofLp_snd
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
g : Submodule 𝕜 (E × F)
x : F × E
y : WithLp 2 (F × E)
h1 :
  ∀ (u : WithLp 2 (F × E)) (x : E) (x_1 : F), (x, x_1) ∈ g → toLp 2 (x_1, -x) = u → ⟪u.fst, y.fst⟫ + ⟪u.snd, y.snd⟫ = 0
h2 : y.ofLp = x
a : E
b : F
hab : (a, b) ∈ g
⊢ ⟪WithLp.fst (p := 2) (toLp 2 (b, -a)), y.fst⟫ + ⟪WithLp.snd (p := 2) (toLp 2 (b, -a)), y.snd⟫ = 0

Tactic:
specialize h1 (toLp 2 (b, -a)) a b hab rfl

Premises used: WithLp.toLp, Prod.mk, OfNat.ofNat, Neg.neg, rfl
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
g : Submodule 𝕜 (E × F)
x : F × E
y : WithLp 2 (F × E)
h2 : y.ofLp = x
a : E
b : F
hab : (a, b) ∈ g
h1 : ⟪b, y.fst⟫ + ⟪-a, y.snd⟫ = 0
⊢ ⟪b, y.fst⟫ - ⟪a, y.snd⟫ = 0

Tactic:
simp only [inner_neg_left, ← sub_eq_add_neg] at h1

Premises used: sub_eq_add_neg, inner_neg_left
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
g : Submodule 𝕜 (E × F)
x : F × E
y : WithLp 2 (F × E)
h2 : y.ofLp = x
a : E
b : F
hab : (a, b) ∈ g
h1 : ⟪b, y.fst⟫ - ⟪a, y.snd⟫ = 0
⊢ ⟪b, y.fst⟫ - ⟪a, y.snd⟫ = 0

Tactic:
h1
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
g : Submodule 𝕜 (E × F)
x : F × E
y : WithLp 2 (F × E)
h2 : y.ofLp = x
a : E
b : F
hab : (a, b) ∈ g
h1 : ⟪b, y.fst⟫ - ⟪a, y.snd⟫ = 0
⊢ ⟪b, y.fst⟫ - ⟪a, y.snd⟫ = 0

Tactic:
exact h1
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
g : Submodule 𝕜 (E × F)
x : F × E
h : ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0
⊢ ∃ (y : WithLp 2 (F × E)),
    (∀ (u : WithLp 2 (F × E)) (x : E) (x_1 : F),
        (x, x_1) ∈ g → toLp 2 (x_1, -x) = u → ⟪u.fst, y.fst⟫ + ⟪u.snd, y.snd⟫ = 0) ∧
      y.ofLp = x

Tactic:
⟨toLp 2 x, ?_, rfl⟩

Premises used: WithLp.toLp, And.intro, Exists.intro, OfNat.ofNat, rfl