awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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)
rw₁ rw₂ : norm.{u_3} (E := F) ((A : (a : E) → F) x : F) = norm.{u_3} (E := F) ((A : (a : E) → F) x : F)
⊢ 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⟫_𝕜)

Tactic:
rw [← apply_norm_sq_eq_inner_adjoint_right, Real.sqrt_sq (norm_nonneg _)]

Premises used: Real.sqrt_sq, ContinuousLinearMap.apply_norm_sq_eq_inner_adjoint_right, norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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⟫_𝕜
rw₁ rw₂ : ⟪x, (B : (a : F) → E) y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜
⊢ ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪x, (B : (a : F) → E) y⟫_𝕜

Tactic:
rw [h, adjoint_inner_left]

Premises used: ContinuousLinearMap.adjoint_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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
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
⊢ 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⟫_𝕜

Tactic:
refine ⟨fun h x y => by rw [h, adjoint_inner_left], fun h => ?_⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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⟫_𝕜
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)
⊢ A = (adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) B

Tactic:
ext x
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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⟫_𝕜
x : E
y : F
⊢ ⟪(A : (a : E) → F) x, y⟫_𝕜 = ⟪(((adjoint : (a : F →L[𝕜] E) → E →L[𝕜] F) B : E →L[𝕜] F) : (a : E) → F) x, y⟫_𝕜

Tactic:
simp only [adjoint_inner_left, h x y]

Premises used: ContinuousLinearMap.adjoint_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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⟫_𝕜
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:
exact ext_inner_right 𝕜 fun y => by simp only [adjoint_inner_left, h x y]

Premises used: ext_inner_right
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (x y : E), ⟪(A : (a : E) → E) x, y⟫_𝕜 = ⟪x, (A : (a : E) → E) y⟫_𝕜
⊢ (adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) A = A

Tactic:
rwa [eq_comm, eq_adjoint_iff A A]

Premises used: ContinuousLinearMap.eq_adjoint_iff, eq_comm
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
⊢ Eq (α := E →L[𝕜] E) ((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) (ContinuousLinearMap.id 𝕜 E) : E →L[𝕜] E)
    (ContinuousLinearMap.id 𝕜 E : E →L[𝕜] E)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
⊢ Eq.{u_2 + 1} (α := E →L[𝕜] E) ((adjoint : (a : E →L[𝕜] E) → E →L[𝕜] E) 1 : E →L[𝕜] E) (1 : E →L[𝕜] E)

Tactic:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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
symm : U.orthogonalProjection = (adjoint : (a : ↥U →L[𝕜] E) → E →L[𝕜] ↥U) U.subtypeL
⊢ (adjoint : (a : ↥U →L[𝕜] E) → E →L[𝕜] ↥U) U.subtypeL = U.orthogonalProjection

Tactic:
symm
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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
⊢ U.orthogonalProjection = (adjoint : (a : ↥U →L[𝕜] E) → E →L[𝕜] ↥U) U.subtypeL

Tactic:
simp [eq_adjoint_iff]

Premises used: ContinuousLinearMap.eq_adjoint_iff
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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)
rw₁ rw₂ : Eq (α := ↥U →L[𝕜] E) U.subtypeL U.subtypeL
⊢ Eq (α := ↥U →L[𝕜] E) ((adjoint : (a : E →L[𝕜] ↥U) → ↥U →L[𝕜] E) U.orthogonalProjection : ↥U →L[𝕜] E)
    (U.subtypeL : ↥U →L[𝕜] E)

Tactic:
rw [← U.adjoint_subtypeL, adjoint_adjoint]

Premises used: Submodule.adjoint_subtypeL, ContinuousLinearMap.adjoint_adjoint
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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 :
  (↑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ᗮ =
    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))

Tactic:
rw [← Submodule.orthogonal_orthogonal_eq_closure]

Premises used: Submodule.orthogonal_orthogonal_eq_closure
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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))ᗮᗮ
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ᗮ
⊢ (↑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

Premises used: le_antisymm
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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))ᗮᗮ

Tactic:
Submodule.orthogonal_le fun x hx ↦ ?_

Premises used: Submodule.orthogonal_le
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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 :
  ∀ (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
⊢ (↑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:
refine Submodule.orthogonal_le fun x hx ↦ ?_

Premises used: Submodule.orthogonal_le
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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ᗮ

Tactic:
Submodule.orthogonal_le fun x hx ↦ ?_

Premises used: Submodule.orthogonal_le
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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 :
  ∀ (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
⊢ (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:
refine Submodule.orthogonal_le fun x hx ↦ ?_

Premises used: Submodule.orthogonal_le
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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

Tactic:
ext_inner_left 𝕜 fun y ↦ ?_

Premises used: Set.Mem, setOf, Set.preimage, Set.singleton, ext_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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
a : ∀ (y : F), ⟪y, ((↑T : E →ₗ[𝕜] F) : (a : E) → F) x⟫_𝕜 = ⟪y, 0⟫_𝕜
⊢ x ∈ (↑T : E →ₗ[𝕜] F).ker

Tactic:
refine ext_inner_left 𝕜 fun y ↦ ?_

Premises used: ext_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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
y : F
⊢ ⟪y, ((↑T : E →ₗ[𝕜] F) : (a : E) → F) x⟫_𝕜 = ⟪y, 0⟫_𝕜

Tactic:
simp [← T.adjoint_inner_left, hx _]

Premises used: ContinuousLinearMap.adjoint_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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 : x ∈ (↑T : E →ₗ[𝕜] F).ker
y : F
⊢ ⟪((↑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) : F →ₗ[𝕜] E) : (a : F) → E) y, x⟫_𝕜 = 0

Tactic:
simp_all [T.adjoint_inner_left]

Premises used: ContinuousLinearMap.adjoint_inner_left
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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 :
  (↑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)))ᗮ
⊢ (↑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)

Tactic:
rw [← T†.ker.orthogonal_orthogonal, T†.orthogonal_ker]

Premises used: Submodule.orthogonal_orthogonal, LinearMap.ker, ContinuousLinearMap.toLinearMap, ContinuousLinearMap.adjoint, DFunLike.coe, ContinuousLinearMap.orthogonal_ker
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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ᗮ =
    (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:
simp
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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

Tactic:
⟨fun h ↦ ?_, LinearMap.ker_le_ker_of_range hT hU⟩

Premises used: Iff.intro, LinearMap.ker_le_ker_of_range
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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)
refine : ∀ (h : (↑U : E →ₗ[𝕜] E).ker ≤ (↑T : E →ₗ[𝕜] E).ker), (↑T : E →ₗ[𝕜] E).range ≤ (↑U : E →ₗ[𝕜] E).range
⊢ (↑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⟩
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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
⊢ CompleteSpace E

Tactic:
have := FiniteDimensional.complete 𝕜 E
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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
this : CompleteSpace E
⊢ (↑T : E →ₗ[𝕜] E).range ≤ (↑U : E →ₗ[𝕜] E).range

Tactic:
simpa [orthogonal_ker, hT, hU] using Submodule.orthogonal_le h

Premises used: Submodule.orthogonal_le, ContinuousLinearMap.orthogonal_ker
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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 ∈ (↑T : E →ₗ[𝕜] F).ker
⊢ x ∈ LinearMap.ker (M₂ := E) (↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E)

Tactic:
simp_all
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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
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
⊢ LinearMap.ker (M₂ := E) (↑(comp (σ₂₃ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T) T) : E →ₗ[𝕜] E) =
    (↑T : E →ₗ[𝕜] F).ker

Tactic:
refine le_antisymm (fun _ _ ↦ ?_) fun _ _ ↦ by simp_all

Premises used: le_antisymm
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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)
rw : ⟪(((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T : F →L[𝕜] E) : (a : F) → E) ((T : (a : E) → F) x : F), x⟫_𝕜 = 0
⊢ x ∈ (↑T : E →ₗ[𝕜] F).ker

Tactic:
rw [LinearMap.mem_ker, ← inner_self_eq_zero (𝕜 := 𝕜), coe_coe, ← adjoint_inner_left]

Premises used: ContinuousLinearMap.adjoint_inner_left, ContinuousLinearMap.coe_coe, inner_self_eq_zero, LinearMap.mem_ker
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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)
⊢ ⟪(((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T : F →L[𝕜] E) : (a : F) → E) ((T : (a : E) → F) x : F), x⟫_𝕜 = 0

Tactic:
simp_all
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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
⊢ Eq (α := Submodule 𝕜 F)
    (LinearMap.ker (↑(T.comp (σ₁₂ := RingHom.id 𝕜) ((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T)) : F →ₗ[𝕜] F))
    (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))

Tactic:
simpa using T†.ker_adjoint_comp_self

Premises used: ContinuousLinearMap.adjoint, ContinuousLinearMap.ker_adjoint_comp_self, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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 = ⊥
rw₅ rw₆ : (↑T : E →ₗ[𝕜] F).ker = ⊥ ↔ (↑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)

Tactic:
rw [← coe_comp', ← coe_coe, ← LinearMap.ker_eq_bot, ← coe_coe, ← LinearMap.ker_eq_bot,
    ker_adjoint_comp_self]

Premises used: ContinuousLinearMap.coe_comp', LinearMap.ker_eq_bot, ContinuousLinearMap.coe_coe, ContinuousLinearMap.ker_adjoint_comp_self
-- Module: Mathlib.Analysis.InnerProductSpace.Adjoint
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_3 + 1, u_3 + 1} (α := F) (β := F)
      (Function.comp.{u_3 + 1, u_2 + 1, u_3 + 1} (β := E) (⇑T : (a : E) → F)
        (⇑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T : F →L[𝕜] E) : (a : F) → E)) ↔
    Function.Injective.{u_3 + 1, u_2 + 1} (α := F) (β := E)
      (⇑((adjoint : (a : E →L[𝕜] F) → F →L[𝕜] E) T : F →L[𝕜] E) : (a : F) → E)

Tactic:
simpa using T†.adjoint_comp_self_injective_iff

Premises used: ContinuousLinearMap.adjoint_comp_self_injective_iff, ContinuousLinearMap.adjoint, DFunLike.coe