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
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
⊢ ⟪(↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a ⋯), x.1⟫ - ⟪a, x.2⟫ = 0
have h₃ : Eq.{u_1 + 1} (α := 𝕜) 0 0
Tactic: rw [← h, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, hx⟩, sub_self]
-- 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
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
⊢ ∃ (x_1 : x.1 ∈ T†.domain), (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯) = x.2
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⟫
Tactic: simp_rw [sub_eq_zero] at 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
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
have h₁ : ∃ (w : E), ∀ (x_1 : ↥T.domain), ⟪w, (↑x_1 : E)⟫ = ⟪x.1, (↑T : ↥T.domain → F) x_1⟫
Tactic: apply mem_adjoint_domain_of_exists
-- 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 :
  ∀ (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⟫
⊢ ∃ (w : E), ∀ (x_1 : ↥T.domain), ⟪w, (↑x_1 : E)⟫ = ⟪x.1, (↑T : ↥T.domain → F) x_1⟫
have h₁ : ∀ (x_1 : ↥T.domain), ⟪x.2, (↑x_1 : E)⟫ = ⟪x.1, (↑T : ↥T.domain → F) x_1⟫
Tactic: use x.snd
-- 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 :
  ∀ (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
⊢ ⟪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)⟫
have 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)⟫
Tactic: rw [← inner_conj_symm, ← h a ha, inner_conj_symm]
-- 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 :
  ∀ (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)⟫
⊢ ⟪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)⟫
have h₂ : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a sorry), x.1⟫ =
  ⟪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]
-- 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 :
  ∀ (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)⟫
⊢ ⟪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)⟫
have h₃ : ⟪x.1, (↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a sorry)⟫ =
  ⟪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]
-- 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
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 : x.1 ∈ T†.domain), (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯) = x.2
have hx : 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]
-- 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 :
  ∀ (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
⊢ ∃ (x_1 : x.1 ∈ T†.domain), (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯) = x.2
have h₁ : (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 sorry) = x.2
Tactic: use 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
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
⊢ (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯) = x.2
have h₁ : ∀ v ∈ (↑T.domain : Set E), ⟪v, (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 sorry)⟫ = ⟪v, x.2⟫
Tactic: apply hT.eq_of_inner_right 𝕜
-- 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 :
  ∀ (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)
⊢ ⟪a, (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯)⟫ = ⟪a, x.2⟫
have h₁ : ⟪a, (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 sorry)⟫ =
  ⟪(↑T : ↥T.domain → F) (Subtype.mk (p := fun (a : E) ↦ a ∈ T.domain) a sorry), x.1⟫
Tactic: rw [← h a ha, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, 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
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⟫
⊢ ⟪a, (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 ⋯)⟫ = ⟪a, x.2⟫
have h₂ : ⟪a, (↑T† : ↥T†.domain → E) (Subtype.mk (p := fun (a : F) ↦ a ∈ T†.domain) x.1 sorry)⟫ =
  ⟪(↑(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)⟫
Tactic: rw [← h a ha, (adjoint_isFormalAdjoint hT).symm ⟨a, ha⟩ ⟨x.fst, 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
hT : Dense (↑T.domain : Set E)
⊢ T.graph.adjoint.toLinearPMap = T†
have h : T.graph.adjoint.toLinearPMap.graph = T†.graph
Tactic: apply eq_of_eq_graph
-- 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.adjoint.toLinearPMap.graph = T†.graph
have h : T.graph.adjoint.toLinearPMap.graph = T.graph.adjoint
Tactic: rw [adjoint_graph_eq_graph_adjoint hT]
-- 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.adjoint.toLinearPMap.graph = T.graph.adjoint
have h : ∀ (x : F × E) (_hx : x ∈ T.graph.adjoint) (_hx' : x.1 = 0), x.2 = 0
Tactic: apply Submodule.toLinearPMap_graph_eq
-- 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
hT : Dense (↑T.domain : Set E)
x : F × E
hx : x ∈ T.graph.adjoint
hx' : x.1 = 0
⊢ x.2 = 0
have hx₁ : ∀ (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
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
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
⊢ x.2 = 0
have h : ∀ v ∈ (↑T.domain : Set E), ⟪v, x.2⟫ = 0
Tactic: apply hT.eq_zero_of_inner_right 𝕜
-- 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†.IsClosed
have 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₂₃ := sorry) (re₃₂ := sorry)
                      (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))
Tactic: rw [IsClosed, adjoint_graph_eq_graph_adjoint hT, Submodule.adjoint]
-- 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)
⊢ _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))))
have 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₂₃ := sorry) (re₃₂ := sorry)
                    (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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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
have rw : A†.IsClosed
Tactic: rw [← isSelfAdjoint_def.mp hA]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.MeanErgodic (goal)
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
⊢ 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))
have 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
Tactic: apply (f : E →ₗ[𝕜] E).tendsto_birkhoffAverage_of_ker_subset_closure (f.lipschitz.weaken hf)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.MeanErgodic (goal)
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
⊢ 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))
have 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)
Tactic: apply (f : E →ₗ[𝕜] E).tendsto_birkhoffAverage_of_ker_subset_closure (f.lipschitz.weaken hf)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.MeanErgodic (goal)
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
⊢ (↑(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)
have hg_ker : (LinearMap.eqLocus f 1)ᗮ ≤ ((↑f : E →ₗ[𝕜] E) - 1).rangeᗮᗮ
Tactic: rw [Submodule.ker_orthogonalProjection, ← Submodule.topologicalClosure_coe,
      SetLike.coe_subset_coe, ← Submodule.orthogonal_orthogonal_eq_closure]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.MeanErgodic (goal)
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
⊢ (LinearMap.eqLocus f 1)ᗮ ≤ ((↑f : E →ₗ[𝕜] E) - 1).rangeᗮᗮ
have hg_ker : ∀ (x : E) (hx : x ∈ ((↑f : E →ₗ[𝕜] E) - 1).rangeᗮ),
  norm (E := E) ((f : (a : E) → E) x : E) ≤ norm (E := E) ((1 : (a : E) → E) x : E)
Tactic: refine Submodule.orthogonal_le fun x hx ↦ eq_of_norm_le_re_inner_eq_norm_sq (𝕜 := 𝕜) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.MeanErgodic (goal)
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
hg_ker :
  ∀ (x : E) (hx : x ∈ ((↑f : E →ₗ[𝕜] E) - 1).rangeᗮ),
    norm (E := E) ((f : (a : E) → E) x : E) ≤ norm (E := E) ((1 : (a : E) → E) x : E)
⊢ (LinearMap.eqLocus f 1)ᗮ ≤ ((↑f : E →ₗ[𝕜] E) - 1).rangeᗮᗮ
have hg_ker₁ : ∀ (x : E) (hx : x ∈ ((↑f : E →ₗ[𝕜] E) - 1).rangeᗮ),
  (RCLike.re : (a : 𝕜) → ℝ) (inner 𝕜 (E := E) ((f : (a : E) → E) x : E) ((1 : (a : E) → E) x : E)) =
    HPow.hPow (β := ℕ) (norm (E := E) ((1 : (a : E) → E) x : E)) 2
Tactic: refine Submodule.orthogonal_le fun x hx ↦ eq_of_norm_le_re_inner_eq_norm_sq (𝕜 := 𝕜) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.MeanErgodic (hypothesis)
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
hx : x ∈ ((↑f : E →ₗ[𝕜] E) - 1).rangeᗮ
⊢ (RCLike.re : (a : 𝕜) → ℝ) (inner 𝕜 (E := E) ((f : (a : E) → E) x : E) ((1 : (a : E) → E) x : E)) =
    HPow.hPow (β := ℕ) (norm (E := E) ((1 : (a : E) → E) x : E)) 2
have this : ∀ (y : E), ⟪(f : (a : E) → E) y, x⟫ = ⟪y, x⟫
Tactic: have : ∀ y, ⟪f y, x⟫ = ⟪y, x⟫ := by
        simpa [Submodule.mem_orthogonal, inner_sub_left, sub_eq_zero] using hx
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
⊢ HasFDerivAt (fun (x : E) ↦ ‖x‖ ^ p)
    (HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x
have pos : ∀ (hx : x = 0),
  HasFDerivAt (fun (x : E) ↦ ‖x‖ ^ p)
    (HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
pos :
  ∀ (hx : x = 0),
    HasFDerivAt (fun (x : E) ↦ ‖x‖ ^ p)
      (HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x
⊢ HasFDerivAt (fun (x : E) ↦ ‖x‖ ^ p)
    (HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x
have neg : ∀ (hx : ¬x = 0),
  HasFDerivAt (fun (x : E) ↦ ‖x‖ ^ p)
    (HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x
Tactic: by_cases hx : x = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
⊢ HasFDerivAt (fun (x : E) ↦ ‖x‖ ^ p)
    (HSMul.hSMul (β := E →L[ℝ] ℝ) (p * ‖x‖ ^ (p - 2)) ((innerSL ℝ : (a : E) → E →L[ℝ] ℝ) x : E →L[ℝ] ℝ)) x
have pos : HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (x : E) ↦ ‖x‖ ^ p) 0 0
Tactic: simp only [hx, norm_zero, map_zero, smul_zero]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
⊢ HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (x : E) ↦ ‖x‖ ^ p) 0 0
have h2p : 0 < p - 1
Tactic: have h2p : 0 < p - 1 := sub_pos.mpr hp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ HasFDerivAt (𝕜 := ℝ) (F := ℝ) (fun (x : E) ↦ ‖x‖ ^ p) 0 0
have pos : IsLittleO (E := ℝ) (F := E) (𝓝 0)
  (fun (x' : E) ↦ HSub.hSub (β := ℝ) (‖x'‖ ^ p - Norm.norm.{u_1} (E := E) 0 ^ p) ((0 : (a : E) → ℝ) (x' - 0) : ℝ))
  fun (x' : E) ↦ x' - 0
Tactic: refine .of_isLittleO ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x : E
p : ℝ
hp : 1 < p
hx : x = 0
h2p : 0 < p - 1
⊢ Eq.{u_1 + 1} (α := (x : E) → ℝ) (fun (x : E) ↦ ‖x‖ ^ p) fun (x : E) ↦ ‖x‖ * ‖x‖ ^ (p - 1)
have h : ∀ (x : E), ‖x‖ ^ p = ‖x‖ * ‖x‖ ^ (p - 1)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.NormPow (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : InnerProductSpace ℝ E
x_1 : E
p : ℝ
hp : 1 < p
hx : x_1 = 0
h2p : 0 < p - 1
x : E
⊢ ‖x‖ ^ p = ‖x‖ * ‖x‖ ^ (p - 1)
have h : ‖x‖ ^ p = ‖x‖ ^ (1 + (p - 1))
Tactic: rw [← rpow_one_add' (norm_nonneg x) (by positivity)]