awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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
a : 𝕜
x : F
hx :
  Membership.mem (γ := Set F)
    {y : F |
      Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
        (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)}
    x
⊢ Membership.mem (γ := Set F)
    {y : F |
      Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
        (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)}
    (a • x)
have rw : ∀
  (hx :
    Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
      (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) x ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)),
  Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑(HSMul.hSMul (α := 𝕜) (β := F →ₗ[𝕜] 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜)
            ((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) ∘ₗ
          T.toFun) :
      (a : ↥T.domain) → 𝕜)
Tactic: rw [Set.mem_setOf_eq, LinearMap.map_smulₛₗ] at *
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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
h : ∃ (w : E), ∀ (x : ↥T.domain), ⟪w, (↑x : E)⟫ = ⟪y, (↑T : ↥T.domain → F) x⟫
⊢ y ∈ T†.domain
have obtain : ∀ (w : E) (hw : ∀ (x : ↥T.domain), ⟪w, (↑x : E)⟫ = ⟪y, (↑T : ↥T.domain → F) x⟫), y ∈ T†.domain
Tactic: obtain ⟨w, hw⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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⟫
⊢ y ∈ T†.domain
have rw : Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
  (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)
Tactic: rw [T.mem_adjoint_domain_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (hypothesis)
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⟫
⊢ Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)
have 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) → 𝕜)
Tactic: have : Continuous ((innerSL 𝕜 w).comp T.domain.subtypeL) := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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 := 𝕜)
    (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)
have 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) → 𝕜)
Tactic: convert! this using 1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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
⊢ (↑T† : ↥T†.domain → E) y = 0
have 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)
Tactic: change (if hT : Dense (T.domain : Set E) then adjointAux hT else 0) y = _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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
⊢ (↑T† : ↥T†.domain → E) y = 0
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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
⊢ (↑T† : ↥T†.domain → E) y = (adjointAux hT : (a : ↥T.adjointDomain) → E) y
have 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)
Tactic: change (if hT : Dense (T.domain : Set E) then adjointAux hT else 0) y = _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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
⊢ (↑T† : ↥T†.domain → E) y = (adjointAux hT : (a : ↥T.adjointDomain) → E) y
have 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)
Tactic: classical
  change (if hT : Dense (T.domain : Set E) then adjointAux hT else 0) y = _
  simp only [hT, dif_pos]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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
⊢ ⟪(↑S : ↥S.domain → E) x, (↑x_2 : E)⟫ = ⟪(↑x_1 : F), (↑T : ↥T.domain → F) x_2⟫
have rw : ⟪(↑x : F), (↑T : ↥T.domain → F) x_2⟫ = ⟪(↑x_1 : F), (↑T : ↥T.domain → F) x_2⟫
Tactic: rw [h.symm, hxy]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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⟫
⊢ ⟪(↑S : ↥S.domain → E) x, (↑x_2 : E)⟫ = ⟪(↑x_1 : F), (↑T : ↥T.domain → F) x_2⟫
have rw₁ : ⟪(↑x_1 : F), (↑T : ↥T.domain → F) x_2⟫ = ⟪(↑x_1 : F), (↑T : ↥T.domain → F) x_2⟫
Tactic: rw [h.symm, hxy]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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)
⊢ ((↑A : E →ₗ[𝕜] F).toPMap p)† = LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤
have 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
Tactic: ext x y hxy
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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
⊢ ((↑A : E →ₗ[𝕜] F).toPMap p)† = LinearMap.toPMap (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : F →ₗ[𝕜] E) ⊤
have 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)
Tactic: ext x y hxy
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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
⊢ 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
have h : Continuous.{u_2, u_1} (X := ↥p) (Y := 𝕜)
  (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) x ∘ₗ ((↑A : E →ₗ[𝕜] F).toPMap p).toFun) : (a : ↥p) → 𝕜)
Tactic: simp only [LinearMap.toPMap_domain, Submodule.mem_top, iff_true,
      LinearPMap.mem_adjoint_domain_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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)
have 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⟫
Tactic: refine LinearPMap.adjoint_apply_eq hp _ fun v => ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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
⊢ x ∈ g.adjoint ↔ ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0
have 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
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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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)),
      (∀ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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
⊢ (∃ (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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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
⊢ ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0
have mp : ⟪b, y.fst⟫ - ⟪a, y.snd⟫ = 0
Tactic: rw [← h2, WithLp.ofLp_fst, WithLp.ofLp_snd]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (hypothesis)
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
⊢ ⟪b, y.fst⟫ - ⟪a, y.snd⟫ = 0
have h1₁ : ⟪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
Cleared hypotheses: h1
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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
have mpr : ∀ (u : WithLp 2 (F × E)) (x_1 : E) (x_2 : F),
  (x_1, x_2) ∈ g →
    toLp 2 (x_2, -x_1) = u → ⟪u.fst, WithLp.fst (p := 2) (toLp 2 x)⟫ + ⟪u.snd, WithLp.snd (p := 2) (toLp 2 x)⟫ = 0
Tactic: refine ⟨toLp 2 x, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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†.graph = T.graph.adjoint
have h : ∀ (x : F × E), x ∈ T†.graph ↔ x ∈ T.graph.adjoint
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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)
x : F × E
⊢ x ∈ T†.graph ↔ x ∈ T.graph.adjoint
have h : (∃ (x_1 : x.1 ∈ T†.domain), (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 sorry) = x.2) ↔
  ∀ (a : E) (a_1 : a ∈ T.domain),
    ⟪(↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a sorry), x.1⟫ - ⟪a, x.2⟫ = 0
Tactic: simp only [mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left, mem_adjoint_iff,
    forall_exists_index, forall_apply_eq_imp_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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)
x : F × E
⊢ (∃ (x_1 : x.1 ∈ T†.domain), (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯) = x.2) ↔
    ∀ (a : E) (a_1 : a ∈ T.domain),
      ⟪(↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a ⋯), x.1⟫ - ⟪a, x.2⟫ = 0
have h : (∃ (x_1 : x.1 ∈ T†.domain), (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 sorry) = x.2) →
  ∀ (a : E) (a_1 : a ∈ T.domain),
    ⟪(↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a sorry), x.1⟫ - ⟪a, x.2⟫ = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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)
x : F × E
h :
  (∃ (x_1 : x.1 ∈ T†.domain), (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯) = x.2) →
    ∀ (a : E) (a_1 : a ∈ T.domain),
      ⟪(↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a ⋯), x.1⟫ - ⟪a, x.2⟫ = 0
⊢ (∃ (x_1 : x.1 ∈ T†.domain), (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯) = x.2) ↔
    ∀ (a : E) (a_1 : a ∈ T.domain),
      ⟪(↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a ⋯), x.1⟫ - ⟪a, x.2⟫ = 0
have h₁ : (∀ (a : E) (a_1 : a ∈ T.domain),
    ⟪(↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a sorry), x.1⟫ - ⟪a, x.2⟫ = 0) →
  ∃ (x_1 : x.1 ∈ T†.domain), (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 sorry) = x.2
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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)
x : F × E
hx : x.1 ∈ T†.domain
h : (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯) = x.2
a : E
ha : a ∈ T.domain
⊢ ⟪(↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a ⋯), x.1⟫ - ⟪a, x.2⟫ = 0
have h₁ : ⟪(↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a sorry), x.1⟫ -
    ⟪a, (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 sorry)⟫ =
  0
Tactic: rw [← h, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩, sub_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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)
x : F × E
hx : x.1 ∈ T†.domain
h : (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯) = x.2
a : E
ha : a ∈ T.domain
h₁ :
  ⟪(↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a ⋯), x.1⟫ -
      ⟪a, (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯)⟫ =
    0
⊢ ⟪(↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a ⋯), x.1⟫ - ⟪a, x.2⟫ = 0
have h₂ : ⟪(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ T.domain) a ha) : E),
      (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (x : F) ↦ x ∈ T†.domain) x.1 hx)⟫ -
    ⟪a, (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 sorry)⟫ =
  0
Tactic: rw [← h, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩, sub_self]