awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
v : E
⊢ Eq.{u_3 + 1} (α := F)
    ((((adjointAux : (a : F →L[𝕜] E) → E →L[𝕜] F) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : E →L[𝕜] F) :
          (a : E) → F)
        v :
      F)
    ((A : (a : E) → F) v : F)
have h : ∀ (w : F),
  ⟪w,
      (((adjointAux : (a : F →L[𝕜] E) → E →L[𝕜] F) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : E →L[𝕜] F) :
          (a : E) → F)
        v⟫_𝕜 =
    ⟪w, (A : (a : E) → F) v⟫_𝕜
Tactic: refine ext_inner_left 𝕜 fun w => ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
v : E
w : F
⊢ ⟪w,
      (((adjointAux : (a : F →L[𝕜] E) → E →L[𝕜] F) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : E →L[𝕜] F) :
          (a : E) → F)
        v⟫_𝕜 =
    ⟪w, (A : (a : E) → F) v⟫_𝕜
have h : ⟪(((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) : (a : F) → E) w, v⟫_𝕜 = ⟪w, (A : (a : E) → F) v⟫_𝕜
Tactic: rw [adjointAux_inner_right, adjointAux_inner_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
v : E
w : F
h : ⟪(((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) : (a : F) → E) w, v⟫_𝕜 = ⟪w, (A : (a : E) → F) v⟫_𝕜
⊢ ⟪w,
      (((adjointAux : (a : F →L[𝕜] E) → E →L[𝕜] F) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : E →L[𝕜] F) :
          (a : E) → F)
        v⟫_𝕜 =
    ⟪w, (A : (a : E) → F) v⟫_𝕜
have h₁ : ⟪w, (A : (a : E) → F) v⟫_𝕜 = ⟪w, (A : (a : E) → F) v⟫_𝕜
Tactic: rw [adjointAux_inner_right, adjointAux_inner_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
⊢ norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) = ‖A‖
have refine_1 : norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) ≤ ‖A‖
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
refine_1 : norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) ≤ ‖A‖
⊢ norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) = ‖A‖
have refine_2 : ‖A‖ ≤ norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E)
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
⊢ norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) ≤ ‖A‖
have refine_1 : ∀ (x : F),
  norm.{u_2} (E := E) ((((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) : (a : F) → E) x : E) ≤ ‖A‖ * ‖x‖
Tactic: refine ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun x => ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : F
⊢ norm.{u_2} (E := E) ((((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) : (a : F) → E) x : E) ≤ ‖A‖ * ‖x‖
have refine_1 : norm (E := StrongDual 𝕜 E)
    ((((toSesqForm : (a : E →L[𝕜] F) → F →L⋆[𝕜] E →L[𝕜] 𝕜) A : F →L⋆[𝕜] E →L[𝕜] 𝕜) : (a : F) → E →L[𝕜] 𝕜) x :
      E →L[𝕜] 𝕜) ≤
  ‖A‖ * ‖x‖
Tactic: rw [adjointAux_apply, LinearIsometryEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
⊢ ‖A‖ ≤ norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E)
have refine_2 : norm (E := E →L[𝕜] F)
    ((adjointAux : (a : F →L[𝕜] E) → E →L[𝕜] F) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : E →L[𝕜] F) ≤
  norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E)
Tactic: nth_rw 1 [← adjointAux_adjointAux A]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
⊢ norm (E := E →L[𝕜] F)
      ((adjointAux : (a : F →L[𝕜] E) → E →L[𝕜] F) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : E →L[𝕜] F) ≤
    norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E)
have refine_2 : ∀ (x : E),
  norm.{u_3} (E := F)
      ((((adjointAux : (a : F →L[𝕜] E) → E →L[𝕜] F) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : E →L[𝕜] F) :
            (a : E) → F)
          x :
        F) ≤
    norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) * ‖x‖
Tactic: refine ContinuousLinearMap.opNorm_le_bound _ (norm_nonneg _) fun x => ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ norm.{u_3} (E := F)
      ((((adjointAux : (a : F →L[𝕜] E) → E →L[𝕜] F) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) : E →L[𝕜] F) :
            (a : E) → F)
          x :
        F) ≤
    norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) * ‖x‖
have refine_2 : norm (E := StrongDual 𝕜 F)
    ((((toSesqForm : (a : F →L[𝕜] E) → E →L⋆[𝕜] F →L[𝕜] 𝕜) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A) :
            E →L⋆[𝕜] F →L[𝕜] 𝕜) :
          (a : E) → F →L[𝕜] 𝕜)
        x :
      F →L[𝕜] 𝕜) ≤
  norm (E := F →L[𝕜] E) ((adjointAux : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) * ‖x‖
Tactic: rw [adjointAux_apply, LinearIsometryEquiv.norm_map]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : InnerProductSpace 𝕜 E
inst_5 : InnerProductSpace 𝕜 F
inst_6 : InnerProductSpace 𝕜 G
inst_7 : CompleteSpace E
inst_8 : CompleteSpace G
inst_9 : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
⊢ Eq (α := G →L[𝕜] E) ((adjoint : (a : E →L[𝕜] G) → G →L[𝕜] E) (A ∘SL B) : G →L[𝕜] E)
    (comp.{u_1, u_1, u_1, u_4, u_3, u_2} (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := F)
        ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) B) ((adjoint : (a : F →L[𝕜] G) → G →L[𝕜] F) A) :
      G →L[𝕜] E)
have h : ∀ (v : G),
  Eq.{u_2 + 1} (α := E) ((((adjoint : (a : E →L[𝕜] G) → G →L[𝕜] E) (A ∘SL B) : G →L[𝕜] E) : (a : G) → E) v : E)
    ((comp.{u_1, u_1, u_1, u_4, u_3, u_2} (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := F)
            ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) B) ((adjoint : (a : F →L[𝕜] G) → G →L[𝕜] F) A) :
          (a : G) → E)
        v :
      E)
Tactic: ext v
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : NormedAddCommGroup G
inst_4 : InnerProductSpace 𝕜 E
inst_5 : InnerProductSpace 𝕜 F
inst_6 : InnerProductSpace 𝕜 G
inst_7 : CompleteSpace E
inst_8 : CompleteSpace G
inst_9 : CompleteSpace F
A : F →L[𝕜] G
B : E →L[𝕜] F
v : G
⊢ Eq.{u_2 + 1} (α := E) ((((adjoint : (a : E →L[𝕜] G) → G →L[𝕜] E) (A ∘SL B) : G →L[𝕜] E) : (a : G) → E) v : E)
    ((comp.{u_1, u_1, u_1, u_4, u_3, u_2} (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := F)
            ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) B) ((adjoint : (a : F →L[𝕜] G) → G →L[𝕜] F) A) :
          (a : G) → E)
        v :
      E)
have h : ∀ (w : E),
  ⟪w, (((adjoint : (a : E →L[𝕜] G) → G →L[𝕜] E) (A ∘SL B) : G →L[𝕜] E) : (a : G) → E) v⟫_𝕜 =
    ⟪w,
      (comp.{u_1, u_1, u_1, u_4, u_3, u_2} (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := F)
            ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) B) ((adjoint : (a : F →L[𝕜] G) → G →L[𝕜] F) A) :
          (a : G) → E)
        v⟫_𝕜
Tactic: refine ext_inner_left 𝕜 fun w => ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜 =
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)
have rw : ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜 =
  ⟪(((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) : (a : F) → E) ((A : (a : E) → F) x : F), x⟫_𝕜
Tactic: rw [← adjoint_inner_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2 =
    (re : (a : 𝕜) → ℝ) ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜
have h : ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜 =
  inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)
Tactic: have h : ⟪(A† ∘L A) x, x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_left]; rfl
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
h :
  ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜 =
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)
⊢ HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2 =
    (re : (a : 𝕜) → ℝ) ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜
have rw : HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2 =
  (re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F))
Tactic: rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
h :
  ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜 =
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)
rw :
  HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2 =
    (re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F))
⊢ HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2 =
    (re : (a : 𝕜) → ℝ) ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜
have rw₁ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)) : ℝ)
  ((re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)) : ℝ)
Tactic: rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ norm.{u_3} (E := F) ((A : (a : E) → F) x : F) =
    √((re : (a : 𝕜) → ℝ)
        ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜)
have rw : norm.{u_3} (E := F) ((A : (a : E) → F) x : F) = √(HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2)
Tactic: rw [← apply_norm_sq_eq_inner_adjoint_left, Real.sqrt_sq (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
rw :
  norm.{u_3} (E := F) ((A : (a : E) → F) x : F) =
    √(HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2)
⊢ norm.{u_3} (E := F) ((A : (a : E) → F) x : F) =
    √((re : (a : 𝕜) → ℝ)
        ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜)
have rw₁ : norm.{u_3} (E := F) ((A : (a : E) → F) x : F) = norm.{u_3} (E := F) ((A : (a : E) → F) x : F)
Tactic: rw [← apply_norm_sq_eq_inner_adjoint_left, Real.sqrt_sq (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ ⟪x, (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x⟫_𝕜 =
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)
have rw : ⟪x, (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x⟫_𝕜 =
  ⟪x, (((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) : (a : F) → E) ((A : (a : E) → F) x : F)⟫_𝕜
Tactic: rw [← adjoint_inner_right]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2 =
    (re : (a : 𝕜) → ℝ) ⟪x, (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x⟫_𝕜
have h : ⟪x, (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x⟫_𝕜 =
  inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)
Tactic: have h : ⟪x, (A† ∘L A) x⟫ = ⟪A x, A x⟫ := by rw [← adjoint_inner_right]; rfl
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
h :
  ⟪x, (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x⟫_𝕜 =
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)
⊢ HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2 =
    (re : (a : 𝕜) → ℝ) ⟪x, (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x⟫_𝕜
have rw : HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2 =
  (re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F))
Tactic: rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
h :
  ⟪x, (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x⟫_𝕜 =
    inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)
rw :
  HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2 =
    (re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F))
⊢ HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2 =
    (re : (a : 𝕜) → ℝ) ⟪x, (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x⟫_𝕜
have rw₁ : Eq (α := ℝ) ((re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)) : ℝ)
  ((re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) ((A : (a : E) → F) x : F) ((A : (a : E) → F) x : F)) : ℝ)
Tactic: rw [h, ← inner_self_eq_norm_sq (𝕜 := 𝕜) _]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
⊢ norm.{u_3} (E := F) ((A : (a : E) → F) x : F) =
    √((re : (a : 𝕜) → ℝ)
        ⟪x, (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x⟫_𝕜)
have rw : norm.{u_3} (E := F) ((A : (a : E) → F) x : F) = √(HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2)
Tactic: rw [← apply_norm_sq_eq_inner_adjoint_right, Real.sqrt_sq (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
x : E
rw :
  norm.{u_3} (E := F) ((A : (a : E) → F) x : F) =
    √(HPow.hPow (β := ℕ) (norm.{u_3} (E := F) ((A : (a : E) → F) x : F)) 2)
⊢ norm.{u_3} (E := F) ((A : (a : E) → F) x : F) =
    √((re : (a : 𝕜) → ℝ)
        ⟪x, (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x⟫_𝕜)
have rw₁ : norm.{u_3} (E := F) ((A : (a : E) → F) x : F) = norm.{u_3} (E := F) ((A : (a : E) → F) x : F)
Tactic: rw [← apply_norm_sq_eq_inner_adjoint_right, Real.sqrt_sq (norm_nonneg _)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
h : A = (adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) B
x : E
y : F
⊢ ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
have rw : ⟪(((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) B : E →L[𝕜] F) : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
Tactic: rw [h, adjoint_inner_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
h : A = (adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) B
x : E
y : F
rw : ⟪(((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) B : E →L[𝕜] F) : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
⊢ ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
have rw₁ : ⟪x, (B : (a : F) → E) y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
Tactic: rw [h, adjoint_inner_left]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
⊢ A = (adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) B ↔
    ∀ (x : E) (y : F), ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
have refine : ∀ (h : ∀ (x : E) (y : F), ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜),
  A = (adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) B
Tactic: refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedAddCommGroup F
inst_3 : InnerProductSpace 𝕜 E
inst_4 : InnerProductSpace 𝕜 F
inst_5 : CompleteSpace E
inst_6 : CompleteSpace F
A : E →L[𝕜] F
B : F →L[𝕜] E
h : ∀ (x : E) (y : F), ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
⊢ A = (adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) B
have h₁ : ∀ (x : E),
  Eq.{u_3 + 1} (α := F) ((A : (a : E) → F) x : F)
    ((((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) B : E →L[𝕜] F) : (a : E) → F) x : F)
Tactic: ext x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (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 →L[𝕜] E
hA : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑A : E →ₗ[𝕜] E)
⊢ (adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) A = A
have rwa : A = (adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) A
Tactic: rwa [eq_comm, eq_adjoint_iff A A]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (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 →L[𝕜] E
hA : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑A : E →ₗ[𝕜] E)
rwa : A = (adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) A
⊢ (adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) A = A
have rwa₁ : ∀ (x y : E), ⟪(A : (a : E) → E) x, y⟫_𝕜 = ⟪x, (A : (a : E) → E) y⟫_𝕜
Tactic: rwa [eq_comm, eq_adjoint_iff A A]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
U : Submodule 𝕜 E
inst_4 : CompleteSpace.{u_2} ↥U
⊢ (adjoint : (a : ↥U →L[𝕜] E) → E →L[𝕜] ↥U) U.subtypeL = U.orthogonalProjection
have symm : U.orthogonalProjection = (adjoint : (a : ↥U →L[𝕜] E) → E →L[𝕜] ↥U) U.subtypeL
Tactic: symm