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
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
U : Submodule 𝕜 E
inst_4 : CompleteSpace.{u_2} ↥U
⊢ Eq (α := ↥U →L[𝕜] E) ((adjoint : (a : E →L[𝕜] ↥U) → ↥U →L[𝕜] E) U.orthogonalProjection : ↥U →L[𝕜] E)
    (U.subtypeL : ↥U →L[𝕜] E)
have rw : Eq (α := ↥U →L[𝕜] E)
  ((adjoint : (a : E →L[𝕜] ↥U) → ↥U →L[𝕜] E) ((adjoint : (a : ↥U →L[𝕜] E) → E →L[𝕜] ↥U) U.subtypeL : E →L[𝕜] ↥U) :
    ↥U →L[𝕜] E)
  (U.subtypeL : ↥U →L[𝕜] E)
Tactic: rw [← U.adjoint_subtypeL, adjoint_adjoint]
-- 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
rw :
  Eq (α := ↥U →L[𝕜] E)
    ((adjoint : (a : E →L[𝕜] ↥U) → ↥U →L[𝕜] E) ((adjoint : (a : ↥U →L[𝕜] E) → E →L[𝕜] ↥U) U.subtypeL : E →L[𝕜] ↥U) :
      ↥U →L[𝕜] E)
    (U.subtypeL : ↥U →L[𝕜] E)
⊢ Eq (α := ↥U →L[𝕜] E) ((adjoint : (a : E →L[𝕜] ↥U) → ↥U →L[𝕜] E) U.orthogonalProjection : ↥U →L[𝕜] E)
    (U.subtypeL : ↥U →L[𝕜] E)
have rw₁ : Eq (α := ↥U →L[𝕜] E) U.subtypeL U.subtypeL
Tactic: rw [← U.adjoint_subtypeL, adjoint_adjoint]
-- 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
T : E →L[𝕜] F
⊢ (↑T : E →ₗ[𝕜] F).kerᗮ =
    Submodule.topologicalClosure
      (LinearMap.range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜)
        (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) : F →ₗ[𝕜] E))
have rw : (↑T : E →ₗ[𝕜] F).kerᗮ =
  (LinearMap.range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜)
        (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) : F →ₗ[𝕜] E))ᗮᗮ
Tactic: rw [← Submodule.orthogonal_orthogonal_eq_closure]
-- 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
T : E →L[𝕜] F
⊢ (↑T : E →ₗ[𝕜] F).kerᗮ =
    (LinearMap.range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜)
          (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) : F →ₗ[𝕜] E))ᗮᗮ
have a : (↑T : E →ₗ[𝕜] F).kerᗮ ≤
  (LinearMap.range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜)
        (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) : F →ₗ[𝕜] E))ᗮᗮ
Tactic: apply 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
T : E →L[𝕜] F
a :
  (↑T : E →ₗ[𝕜] F).kerᗮ ≤
    (LinearMap.range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜)
          (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) : F →ₗ[𝕜] E))ᗮᗮ
⊢ (↑T : E →ₗ[𝕜] F).kerᗮ =
    (LinearMap.range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜)
          (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) : F →ₗ[𝕜] E))ᗮᗮ
have a₁ : (LinearMap.range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜)
        (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) : F →ₗ[𝕜] E))ᗮᗮ ≤
  (↑T : E →ₗ[𝕜] F).kerᗮ
Tactic: apply 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
T : E →L[𝕜] F
⊢ (↑T : E →ₗ[𝕜] F).kerᗮ ≤
    (LinearMap.range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜)
          (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) : F →ₗ[𝕜] E))ᗮᗮ
have a : ∀ (x : E)
  (hx :
    Membership.mem (γ := Submodule 𝕜 E)
      (LinearMap.range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜)
          (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) : F →ₗ[𝕜] E))ᗮ
      x),
  x ∈ (↑T : E →ₗ[𝕜] F).ker
Tactic: refine Submodule.orthogonal_le fun x hx ↦ ?_
-- 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
T : E →L[𝕜] F
⊢ (LinearMap.range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜)
          (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) : F →ₗ[𝕜] E))ᗮᗮ ≤
    (↑T : E →ₗ[𝕜] F).kerᗮ
have a : ∀ (x : E) (hx : x ∈ (↑T : E →ₗ[𝕜] F).ker),
  Membership.mem (γ := Submodule 𝕜 E)
    (LinearMap.range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜)
        (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) : F →ₗ[𝕜] E))ᗮ
    x
Tactic: refine Submodule.orthogonal_le fun x hx ↦ ?_
-- 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
T : E →L[𝕜] F
x : E
hx :
  Membership.mem (γ := Submodule 𝕜 E)
    (LinearMap.range.{u_1, u_1, u_3, u_2} (R := 𝕜) (M := F) (τ₁₂ := RingHom.id 𝕜)
        (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) : F →ₗ[𝕜] E))ᗮ
    x
⊢ x ∈ (↑T : E →ₗ[𝕜] F).ker
have a : ∀ (y : F), ⟪y, ((↑T : E →ₗ[𝕜] F) : (a : E) → F) x⟫_𝕜 = ⟪y, 0⟫_𝕜
Tactic: refine ext_inner_left 𝕜 fun y ↦ ?_
-- 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
T : E →L[𝕜] F
⊢ (↑T : E →ₗ[𝕜] F).rangeᗮ =
    LinearMap.ker.{u_1, u_1, u_3, u_2} (R₂ := 𝕜) (M₂ := E) (τ₁₂ := RingHom.id 𝕜)
      (↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) : F →ₗ[𝕜] E)
have rw : (↑T : E →ₗ[𝕜] F).rangeᗮ =
  (Submodule.topologicalClosure
      (LinearMap.range.{u_1, u_1, u_2, u_3} (R := 𝕜) (M := E) (τ₁₂ := RingHom.id 𝕜)
        (↑((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T)) : E →ₗ[𝕜] F)))ᗮ
Tactic: rw [← T†.ker.orthogonal_orthogonal, T†.orthogonal_ker]
-- 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 : FiniteDimensional 𝕜 E
T U : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
hU : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑U : E →ₗ[𝕜] E)
⊢ (↑U : E →ₗ[𝕜] E).ker ≤ (↑T : E →ₗ[𝕜] E).ker ↔ (↑T : E →ₗ[𝕜] E).range ≤ (↑U : E →ₗ[𝕜] E).range
have refine : ∀ (h : (↑U : E →ₗ[𝕜] E).ker ≤ (↑T : E →ₗ[𝕜] E).ker), (↑T : E →ₗ[𝕜] E).range ≤ (↑U : E →ₗ[𝕜] E).range
Tactic: refine ⟨fun h ↦ ?_, LinearMap.ker_le_ker_of_range hT hU⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Adjoint (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : FiniteDimensional 𝕜 E
T U : E →L[𝕜] E
hT : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑T : E →ₗ[𝕜] E)
hU : LinearMap.IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑U : E →ₗ[𝕜] E)
h : (↑U : E →ₗ[𝕜] E).ker ≤ (↑T : E →ₗ[𝕜] E).ker
⊢ (↑T : E →ₗ[𝕜] E).range ≤ (↑U : E →ₗ[𝕜] E).range
have this : CompleteSpace E
Tactic: have := FiniteDimensional.complete 𝕜 E
-- 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
T : E →L[𝕜] F
⊢ LinearMap.ker (M₂ := E) (↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E) =
    (↑T : E →ₗ[𝕜] F).ker
have refine : ∀ x ∈ LinearMap.ker (M₂ := E) (↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E),
  x ∈ (↑T : E →ₗ[𝕜] F).ker
Tactic: refine le_antisymm (fun _ _ ↦ ?_) fun _ _ ↦ by simp_all
-- 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
T : E →L[𝕜] F
x : E
h :
  x ∈ LinearMap.ker (M₂ := E) (↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E)
⊢ x ∈ (↑T : E →ₗ[𝕜] F).ker
have rw : ⟪(((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T : F →L[𝕜] E) : (a : F) → E) ((T : (a : E) → F) x : F), x⟫_𝕜 = 0
Tactic: rw [LinearMap.mem_ker, ← inner_self_eq_zero (𝕜 := 𝕜), coe_coe, ← 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
T : E →L[𝕜] F
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := E) (β := E)
      (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := F)
        (⇑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T : F →L[𝕜] E) : (a : F) → E) (⇑T : (a : E) → F)) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
have rw : Function.Injective (α := E) (β := E)
    (⇑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : (a : E) → E) ↔
  Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
Tactic: rw [← coe_comp', ← coe_coe, ← LinearMap.ker_eq_bot, ← coe_coe, ← LinearMap.ker_eq_bot,
    ker_adjoint_comp_self]
-- 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
T : E →L[𝕜] F
rw :
  Function.Injective (α := E) (β := E)
      (⇑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : (a : E) → E) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := E) (β := E)
      (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := F)
        (⇑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T : F →L[𝕜] E) : (a : F) → E) (⇑T : (a : E) → F)) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
have rw₁ : Function.Injective (α := E) (β := E)
    (⇑(↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E) : (a : E) → E) ↔
  Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
Tactic: rw [← coe_comp', ← coe_coe, ← LinearMap.ker_eq_bot, ← coe_coe, ← LinearMap.ker_eq_bot,
    ker_adjoint_comp_self]
-- 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
T : E →L[𝕜] F
rw :
  Function.Injective (α := E) (β := E)
      (⇑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : (a : E) → E) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
rw₁ :
  Function.Injective (α := E) (β := E)
      (⇑(↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E) : (a : E) → E) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := E) (β := E)
      (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := F)
        (⇑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T : F →L[𝕜] E) : (a : F) → E) (⇑T : (a : E) → F)) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
have rw₂ : LinearMap.ker (M₂ := E) (↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E) = ⊥ ↔
  Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
Tactic: rw [← coe_comp', ← coe_coe, ← LinearMap.ker_eq_bot, ← coe_coe, ← LinearMap.ker_eq_bot,
    ker_adjoint_comp_self]
-- 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
T : E →L[𝕜] F
rw :
  Function.Injective (α := E) (β := E)
      (⇑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : (a : E) → E) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
rw₁ :
  Function.Injective (α := E) (β := E)
      (⇑(↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E) : (a : E) → E) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
rw₂ :
  LinearMap.ker (M₂ := E) (↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E) =
      ⊥ ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := E) (β := E)
      (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := F)
        (⇑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T : F →L[𝕜] E) : (a : F) → E) (⇑T : (a : E) → F)) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
have rw₃ : LinearMap.ker (M₂ := E) (↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E) = ⊥ ↔
  Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑(↑T : E →ₗ[𝕜] F) : (a : E) → F)
Tactic: rw [← coe_comp', ← coe_coe, ← LinearMap.ker_eq_bot, ← coe_coe, ← LinearMap.ker_eq_bot,
    ker_adjoint_comp_self]
-- 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
T : E →L[𝕜] F
rw :
  Function.Injective (α := E) (β := E)
      (⇑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : (a : E) → E) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
rw₁ :
  Function.Injective (α := E) (β := E)
      (⇑(↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E) : (a : E) → E) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
rw₂ :
  LinearMap.ker (M₂ := E) (↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E) =
      ⊥ ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
rw₃ :
  LinearMap.ker (M₂ := E) (↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E) =
      ⊥ ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑(↑T : E →ₗ[𝕜] F) : (a : E) → F)
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := E) (β := E)
      (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := F)
        (⇑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T : F →L[𝕜] E) : (a : F) → E) (⇑T : (a : E) → F)) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
have rw₄ : LinearMap.ker (M₂ := E) (↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E) = ⊥ ↔
  (↑T : E →ₗ[𝕜] F).ker = ⊥
Tactic: rw [← coe_comp', ← coe_coe, ← LinearMap.ker_eq_bot, ← coe_coe, ← LinearMap.ker_eq_bot,
    ker_adjoint_comp_self]
-- 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
T : E →L[𝕜] F
rw :
  Function.Injective (α := E) (β := E)
      (⇑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : (a : E) → E) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
rw₁ :
  Function.Injective (α := E) (β := E)
      (⇑(↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E) : (a : E) → E) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
rw₂ :
  LinearMap.ker (M₂ := E) (↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E) =
      ⊥ ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
rw₃ :
  LinearMap.ker (M₂ := E) (↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E) =
      ⊥ ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑(↑T : E →ₗ[𝕜] F) : (a : E) → F)
rw₄ :
  LinearMap.ker (M₂ := E) (↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E) =
      ⊥ ↔
    (↑T : E →ₗ[𝕜] F).ker = ⊥
⊢ Function.Injective.{u_2 + 1, u_2 + 1} (α := E) (β := E)
      (Function.comp.{u_2 + 1, u_3 + 1, u_2 + 1} (β := F)
        (⇑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T : F →L[𝕜] E) : (a : F) → E) (⇑T : (a : E) → F)) ↔
    Function.Injective.{u_2 + 1, u_3 + 1} (α := E) (β := F) (⇑T : (a : E) → F)
have rw₅ : (↑T : E →ₗ[𝕜] F).ker = ⊥ ↔ (↑T : E →ₗ[𝕜] F).ker = ⊥
Tactic: rw [← coe_comp', ← coe_coe, ← LinearMap.ker_eq_bot, ← coe_coe, ← LinearMap.ker_eq_bot,
    ker_adjoint_comp_self]
-- 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[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) = ‖A‖ * ‖A‖
have refine_1 : norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) ≤ ‖A‖ * ‖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 := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) ≤ ‖A‖ * ‖A‖
⊢ norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) = ‖A‖ * ‖A‖
have refine_2 : ‖A‖ * ‖A‖ ≤ norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) 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
⊢ norm (E := F →L[𝕜] E) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) * ‖A‖ = ‖A‖ * ‖A‖
have rw : ‖A‖ * ‖A‖ = ‖A‖ * ‖A‖
Tactic: rw [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
⊢ norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) ≤ ‖A‖ * ‖A‖
have opNorm_comp_le : norm (E := F →L[𝕜] E) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A : F →L[𝕜] E) * ‖A‖ = ‖A‖ * ‖A‖
Tactic: calc
      ‖A† ∘L A‖ ≤ ‖A†‖ * ‖A‖ := opNorm_comp_le _ _
      _ = ‖A‖ * ‖A‖ := by rw [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‖ * ‖A‖ ≤ norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A)
have refine_2 : ‖A‖ ≤ √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A))
Tactic: rw [← sq, ← Real.sqrt_le_sqrt_iff (norm_nonneg _), 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
⊢ ‖A‖ ≤ √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A))
have refine_2 : ∀ (x : E),
  norm.{u_3} (E := F) ((A : (a : E) → F) x : F) ≤
    √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A)) * ‖x‖
Tactic: refine opNorm_le_bound _ (Real.sqrt_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 (E := E) ((comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x : E) * ‖x‖ ≤
    norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) * ‖x‖ * ‖x‖
have hbc : norm (E := E) ((comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x : E) ≤
  norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) * ‖x‖
Tactic: gcongr
-- 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
⊢ norm.{u_3} (E := F) ((A : (a : E) → F) x : F) ≤
    √(norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A)) * ‖x‖
have this : (re : (a : 𝕜) → ℝ) ⟪(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A : (a : E) → E) x, x⟫_𝕜 ≤
  norm (E := E →L[𝕜] E) (comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) A) A) * ‖x‖ * ‖x‖
Tactic: have :=
      calc
        re ⟪(A† ∘L A) x, x⟫ ≤ ‖(A† ∘L A) x‖ * ‖x‖ := re_inner_le_norm _ _
        _ ≤ ‖A† ∘L A‖ * ‖x‖ * ‖x‖ := by gcongr; exact le_opNorm _ _