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
g : Submodule 𝕜 (E × F)
x : F × E
h : ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0
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
⊢ ∃ (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:
refine ⟨toLp 2 x, ?_, 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
h : ∀ (a : E) (b : F), (a, b) ∈ g → ⟪b, x.1⟫ - ⟪a, x.2⟫ = 0
u : WithLp 2 (F × E)
a : E
b : F
hab : (a, b) ∈ g
hu : toLp 2 (b, -a) = u
⊢ ⟪u.fst, WithLp.fst (p := 2) (toLp 2 x)⟫ + ⟪u.snd, WithLp.snd (p := 2) (toLp 2 x)⟫ = 0

Tactic:
simp [← hu, ← sub_eq_add_neg, h a b hab]

Premises used: sub_eq_add_neg
-- 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)
h : ∀ (x : F × E), x ∈ T†.graph ↔ x ∈ T.graph.adjoint
⊢ T†.graph = T.graph.adjoint

Tactic:
ext x
-- 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)
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 ∈ T†.graph ↔ x ∈ T.graph.adjoint

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]

Premises used: Subtype.exists, forall_exists_index, exists_and_left, exists_eq_left, LinearPMap.mem_graph_iff, Submodule.mem_adjoint_iff, forall_apply_eq_imp_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)
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
h₁ :
  (∀ (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
⊢ (∃ (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

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
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
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 ⋯)⟫ =
    0
h₃ h₄ : Eq.{u_1 + 1} (α := 𝕜) 0 0
⊢ ⟪(↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a ⋯), x.1⟫ - ⟪a, x.2⟫ = 0

Tactic:
rw [← h, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩, sub_self]

Premises used: sub_self, LinearPMap.adjoint_isFormalAdjoint, LinearPMap.IsFormalAdjoint.symm, Prod.fst, Subtype.mk
-- 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)
x : F × E
h :
  ∀ (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
⊢ ∀ (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⟫

Tactic:
simp_rw [sub_eq_zero] at h

Premises used: sub_eq_zero
-- 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)
x : F × E
h :
  ∀ (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⟫
h₁ : ∃ (w : E), ∀ (x_1 : ↥T.domain), ⟪w, (↑x_1 : E)⟫ = ⟪x.1, (↑T : ↥T.domain → F) x_1⟫
⊢ x.1 ∈ T†.domain

Tactic:
apply mem_adjoint_domain_of_exists

Premises used: LinearPMap.mem_adjoint_domain_of_exists
-- 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)
x : F × E
h :
  ∀ (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⟫
h₁ : ∀ (x_1 : ↥T.domain), ⟪x.2, (↑x_1 : E)⟫ = ⟪x.1, (↑T : ↥T.domain → F) x_1⟫
⊢ ∃ (w : E), ∀ (x_1 : ↥T.domain), ⟪w, (↑x_1 : E)⟫ = ⟪x.1, (↑T : ↥T.domain → F) x_1⟫

Tactic:
use x.snd

Premises used: Prod.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
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
hT : Dense (↑T.domain : Set E)
x : F × E
h :
  ∀ (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⟫
a : E
ha : a ∈ T.domain
h₁ :
  (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑(Subtype.mk (p := fun (x : E) ↦ x ∈ T.domain) a ha) : E), x.2⟫ =
    ⟪x.1, (↑T : ↥T.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ T.domain) a ha)⟫
h₂ :
  (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a ⋯), x.1⟫ =
    ⟪x.1, (↑T : ↥T.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ T.domain) a ha)⟫
h₃ h₄ :
  ⟪x.1, (↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a ⋯)⟫ =
    ⟪x.1, (↑T : ↥T.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ T.domain) a ha)⟫
⊢ ⟪x.2, (↑(Subtype.mk (p := fun (x : E) ↦ x ∈ T.domain) a ha) : E)⟫ =
    ⟪x.1, (↑T : ↥T.domain → F) (Subtype.mk (p := fun (x : E) ↦ x ∈ T.domain) a ha)⟫

Tactic:
rw [← inner_conj_symm, ← h a ha, inner_conj_symm]

Premises used: inner_conj_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)
x : F × E
h :
  ∀ (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⟫
⊢ x.1 ∈ T†.domain

Tactic:
have hx : x.fst ∈ T†.domain := by
      apply mem_adjoint_domain_of_exists
      use x.snd
      rintro ⟨a, ha⟩
      rw [← inner_conj_symm, ← h a ha, inner_conj_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)
x : F × E
h :
  ∀ (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⟫
hx : x.1 ∈ T†.domain
h₁ : (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯) = x.2
⊢ ∃ (x_1 : x.1 ∈ T†.domain), (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯) = x.2

Tactic:
use hx
-- 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)
x : F × E
h :
  ∀ (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⟫
hx : x.1 ∈ T†.domain
h₁ :
  ∀ v ∈ (↑T.domain : Set E),
    ⟪v, (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯)⟫ = ⟪v, x.2⟫
⊢ (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯) = x.2

Tactic:
apply hT.eq_of_inner_right 𝕜

Premises used: Dense.eq_of_inner_right
-- 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)
x : F × E
h :
  ∀ (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⟫
hx : x.1 ∈ T†.domain
a : E
ha : a ∈ (↑T.domain : Set E)
h₁ :
  ⟪a, (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯)⟫ =
    ⟪(↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a ⋯), x.1⟫
h₂ h₃ :
  ⟪a, (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯)⟫ =
    ⟪(↑(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 ⋯)⟫ = ⟪a, x.2⟫

Tactic:
rw [← h a ha, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩]

Premises used: LinearPMap.adjoint_isFormalAdjoint, LinearPMap.IsFormalAdjoint.symm, Prod.fst, Subtype.mk
-- 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)
h : T.graph.adjoint.toLinearPMap.graph = T†.graph
⊢ T.graph.adjoint.toLinearPMap = T†

Tactic:
apply eq_of_eq_graph

Premises used: LinearPMap.eq_of_eq_graph
-- 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)
h : T.graph.adjoint.toLinearPMap.graph = T.graph.adjoint
⊢ T.graph.adjoint.toLinearPMap.graph = T†.graph

Tactic:
rw [adjoint_graph_eq_graph_adjoint hT]

Premises used: LinearPMap.adjoint_graph_eq_graph_adjoint
-- 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)
h : ∀ (x : F × E) (_hx : x ∈ T.graph.adjoint) (_hx' : x.1 = 0), x.2 = 0
⊢ T.graph.adjoint.toLinearPMap.graph = T.graph.adjoint

Tactic:
apply Submodule.toLinearPMap_graph_eq

Premises used: Submodule.toLinearPMap_graph_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
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
hT : Dense (↑T.domain : Set E)
x : F × E
hx : x ∈ T.graph.adjoint
hx' : x.1 = 0
⊢ ∀ (a : E) (a_1 : a ∈ T.domain), ⟪a, x.2⟫ = 0

Tactic:
simp only [mem_adjoint_iff, mem_graph_iff, Subtype.exists, exists_and_left, exists_eq_left, hx',
    inner_zero_right, zero_sub, neg_eq_zero, forall_exists_index, forall_apply_eq_imp_iff] at hx

Premises used: Subtype.exists, forall_exists_index, neg_eq_zero, exists_and_left, exists_eq_left, inner_zero_right, LinearPMap.mem_graph_iff, Submodule.mem_adjoint_iff, forall_apply_eq_imp_iff, zero_sub
-- 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)
x : F × E
hx' : x.1 = 0
hx : ∀ (a : E) (a_1 : a ∈ T.domain), ⟪a, x.2⟫ = 0
h : ∀ v ∈ (↑T.domain : Set E), ⟪v, x.2⟫ = 0
⊢ x.2 = 0

Tactic:
apply hT.eq_zero_of_inner_right 𝕜

Premises used: Dense.eq_zero_of_inner_right
-- 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)
x : F × E
hx' : x.1 = 0
hx : ∀ (a : E) (a_1 : a ∈ T.domain), ⟪a, x.2⟫ = 0
⊢ ∀ v ∈ (↑T.domain : Set E), ⟪v, x.2⟫ = 0

Tactic:
fun a ha ↦ hx a ha
-- 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)
x : F × E
hx' : x.1 = 0
hx : ∀ (a : E) (a_1 : a ∈ T.domain), ⟪a, x.2⟫ = 0
⊢ ∀ v ∈ (↑T.domain : Set E), ⟪v, x.2⟫ = 0

Tactic:
exact fun a ha ↦ hx a ha
-- 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)
rw :
  _root_.IsClosed
    (↑(Submodule.map (M := WithLp 2 (F × E)) (σ₁₂ := RingHom.id 𝕜)
            ((↑(WithLp.linearEquiv 2 𝕜 (F × E)) : WithLp 2 (F × E) →ₗ[𝕜] F × E) : WithLp 2 (F × E) →ₗ[𝕜] F × E)
            ((Submodule.map
                  (↑(LinearEquiv.trans (σ₂₃ := RingHom.id 𝕜) (σ₃₂ := RingHom.id 𝕜) (re₂₃ := ⋯) (re₃₂ := ⋯)
                        (LinearEquiv.symm (LinearEquiv.skewSwap 𝕜 F E))
                        (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (F × E)))) :
                    E × F →ₗ[𝕜] WithLp 2 (F × E))
                  T.graph)ᗮ :
              Submodule 𝕜 (WithLp 2 (F × E))) :
          Submodule 𝕜 (F × E)) :
      Set (F × E))
⊢ T†.IsClosed

Tactic:
rw [IsClosed, adjoint_graph_eq_graph_adjoint hT, Submodule.adjoint]

Premises used: LinearPMap.IsClosed, Submodule.adjoint, LinearPMap.adjoint_graph_eq_graph_adjoint
-- 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)
rw :
  _root_.IsClosed (X := F × E)
    ((⇑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (F × E)) : (F × E) ≃ₗ[𝕜] WithLp 2 (F × E)) :
        (a : F × E) → WithLp 2 (F × E)) ⁻¹'
      (↑((Submodule.map
                (↑(LinearEquiv.trans (σ₂₃ := RingHom.id 𝕜) (σ₃₂ := RingHom.id 𝕜) (re₂₃ := ⋯) (re₃₂ := ⋯)
                      (LinearEquiv.symm (LinearEquiv.skewSwap 𝕜 F E))
                      (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (F × E)))) :
                  E × F →ₗ[𝕜] WithLp 2 (F × E))
                T.graph)ᗮ :
            Submodule 𝕜 (WithLp 2 (F × E))) :
        Set (WithLp 2 (F × E))))
⊢ _root_.IsClosed (X := F × E)
    ((⇑((↑(WithLp.linearEquiv 2 𝕜 (F × E)) : WithLp 2 (F × E) →ₗ[𝕜] F × E) : WithLp 2 (F × E) →ₗ[𝕜] F × E) :
        (a : WithLp 2 (F × E)) → F × E) ''
      (↑((Submodule.map
                (↑(LinearEquiv.trans (σ₂₃ := RingHom.id 𝕜) (σ₃₂ := RingHom.id 𝕜) (re₂₃ := ⋯) (re₃₂ := ⋯)
                      (LinearEquiv.symm (LinearEquiv.skewSwap 𝕜 F E))
                      (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (F × E)))) :
                  E × F →ₗ[𝕜] WithLp 2 (F × E))
                T.graph)ᗮ :
            Submodule 𝕜 (WithLp 2 (F × E))) :
        Set (WithLp 2 (F × E))))

Tactic:
rw [LinearEquiv.coe_coe, LinearEquiv.image_eq_preimage_symm]

Premises used: LinearEquiv.image_eq_preimage_symm, 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
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
hT : Dense (↑T.domain : Set E)
⊢ _root_.IsClosed (X := F × E)
    ((⇑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (F × E)) : (F × E) ≃ₗ[𝕜] WithLp 2 (F × E)) :
        (a : F × E) → WithLp 2 (F × E)) ⁻¹'
      (↑((Submodule.map
                (↑(LinearEquiv.trans (σ₂₃ := RingHom.id 𝕜) (σ₃₂ := RingHom.id 𝕜) (re₂₃ := ⋯) (re₃₂ := ⋯)
                      (LinearEquiv.symm (LinearEquiv.skewSwap 𝕜 F E))
                      (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (F × E)))) :
                  E × F →ₗ[𝕜] WithLp 2 (F × E))
                T.graph)ᗮ :
            Submodule 𝕜 (WithLp 2 (F × E))) :
        Set (WithLp 2 (F × E))))

Tactic:
(Submodule.isClosed_orthogonal _).preimage (WithLp.prod_continuous_toLp _ _ _)

Premises used: WithLp.prod_continuous_toLp, IsClosed.preimage
-- 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)
⊢ _root_.IsClosed (X := F × E)
    ((⇑(LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (F × E)) : (F × E) ≃ₗ[𝕜] WithLp 2 (F × E)) :
        (a : F × E) → WithLp 2 (F × E)) ⁻¹'
      (↑((Submodule.map
                (↑(LinearEquiv.trans (σ₂₃ := RingHom.id 𝕜) (σ₃₂ := RingHom.id 𝕜) (re₂₃ := ⋯) (re₃₂ := ⋯)
                      (LinearEquiv.symm (LinearEquiv.skewSwap 𝕜 F E))
                      (LinearEquiv.symm (WithLp.linearEquiv 2 𝕜 (F × E)))) :
                  E × F →ₗ[𝕜] WithLp 2 (F × E))
                T.graph)ᗮ :
            Submodule 𝕜 (WithLp 2 (F × E))) :
        Set (WithLp 2 (F × E))))

Tactic:
exact (Submodule.isClosed_orthogonal _).preimage (WithLp.prod_continuous_toLp _ _ _)

Premises used: WithLp.prod_continuous_toLp, IsClosed.preimage
-- 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
hA : IsSelfAdjoint A
rw : A†.IsClosed
⊢ A.IsClosed

Tactic:
rw [← isSelfAdjoint_def.mp hA]

Premises used: LinearPMap.isSelfAdjoint_def, Iff.mp
-- 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
hA : IsSelfAdjoint A
⊢ A†.IsClosed

Tactic:
adjoint_isClosed hA.dense_domain

Premises used: IsSelfAdjoint.dense_domain, LinearPMap.adjoint_isClosed
-- 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
hA : IsSelfAdjoint A
⊢ A†.IsClosed

Tactic:
exact adjoint_isClosed hA.dense_domain

Premises used: IsSelfAdjoint.dense_domain, LinearPMap.adjoint_isClosed
-- Module: Mathlib.Analysis.InnerProductSpace.MeanErgodic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
hg_proj :
  ∀ (x : ↥(LinearMap.eqLocus (↑f : E →ₗ[𝕜] E) 1)),
    (Submodule.orthogonalProjection (LinearMap.eqLocus f 1) : (a : E) → ↥(LinearMap.eqLocus (↑f : E →ₗ[𝕜] E) 1))
        (↑x : E) =
      x
hg_ker :
  (↑(LinearMap.ker (M₂ := ↥(LinearMap.eqLocus (↑f : E →ₗ[𝕜] E) 1))
          (↑(Submodule.orthogonalProjection (LinearMap.eqLocus f 1)) :
            E →ₗ[𝕜] ↥(LinearMap.eqLocus (↑f : E →ₗ[𝕜] E) 1))) :
      Set E) ⊆
    closure[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] (↑((↑f : E →ₗ[𝕜] E) - 1).range : Set E)
⊢ Tendsto.{0, u_2} (β := E) (fun (x_1 : ℕ) ↦ birkhoffAverage 𝕜 (⇑f : (a : E) → E) id x_1 x) atTop
    (𝓝 (↑((Submodule.orthogonalProjection (LinearMap.eqLocus f 1) : (a : E) → ↥(LinearMap.eqLocus f 1)) x) : E))

Tactic:
apply (f : E →ₗ[𝕜] E).tendsto_birkhoffAverage_of_ker_subset_closure (f.lipschitz.weaken hf)

Premises used: ContinuousLinearMap.lipschitz, ContinuousLinearMap.toLinearMap, LipschitzWith.weaken, LinearMap.tendsto_birkhoffAverage_of_ker_subset_closure
-- Module: Mathlib.Analysis.InnerProductSpace.MeanErgodic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
⊢ ∀ (x : ↥(LinearMap.eqLocus (↑f : E →ₗ[𝕜] E) 1)),
    (Submodule.orthogonalProjection (LinearMap.eqLocus f 1) : (a : E) → ↥(LinearMap.eqLocus (↑f : E →ₗ[𝕜] E) 1))
        (↑x : E) =
      x

Tactic:
(LinearMap.eqLocus f 1).orthogonalProjection_mem_subspace_eq_self

Premises used: Submodule.orthogonalProjection_mem_subspace_eq_self, Set.Mem, setOf
-- Module: Mathlib.Analysis.InnerProductSpace.MeanErgodic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
hf : ‖f‖ ≤ 1
x : E
⊢ ∀ (x : ↥(LinearMap.eqLocus (↑f : E →ₗ[𝕜] E) 1)),
    (Submodule.orthogonalProjection (LinearMap.eqLocus f 1) : (a : E) → ↥(LinearMap.eqLocus (↑f : E →ₗ[𝕜] E) 1))
        (↑x : E) =
      x

Tactic:
exact (LinearMap.eqLocus f 1).orthogonalProjection_mem_subspace_eq_self

Premises used: Submodule.orthogonalProjection_mem_subspace_eq_self