[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
h : IsFormalAdjoint T S
y : { x // x ∈ S.domain }
x✝ : { x // x ∈ T.domain }
⊢ inner (↑S y) ↑x✝ = inner (↑y) (↑T x✝)
[PROOFSTEP]
rw [← inner_conj_symm, ← inner_conj_symm (y : F), h]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
a✝ b✝ : F
hx : a✝ ∈ {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)}
hy : b✝ ∈ {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)}
⊢ a✝ + b✝ ∈ {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)}
[PROOFSTEP]
rw [Set.mem_setOf_eq, LinearMap.map_add] at *
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
a✝ b✝ : F
hx : Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) a✝) T.toFun)
hy : Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) b✝) T.toFun)
⊢ Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) a✝ + ↑(innerₛₗ 𝕜) b✝) T.toFun)
[PROOFSTEP]
exact hx.add hy
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
⊢ 0 ∈
    { carrier := {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)},
        add_mem' :=
          (_ :
            ∀ {a b : F},
              a ∈ {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)} →
                b ∈ {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)} →
                  a + b ∈ {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)}) }.carrier
[PROOFSTEP]
rw [Set.mem_setOf_eq, LinearMap.map_zero, LinearMap.zero_comp]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
⊢ Continuous ↑0
[PROOFSTEP]
exact continuous_zero
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
a : 𝕜
x : F
hx :
  x ∈
    {
          toAddSubsemigroup :=
            { carrier := {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)},
              add_mem' :=
                (_ :
                  ∀ {a b : F},
                    a ∈ {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)} →
                      b ∈ {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)} →
                        a + b ∈ {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)}) },
          zero_mem' :=
            (_ :
              0 ∈
                { carrier := {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)},
                    add_mem' :=
                      (_ :
                        ∀ {a b : F},
                          a ∈ {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)} →
                            b ∈ {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)} →
                              a + b ∈
                                {y |
                                  Continuous
                                    ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)}) }.carrier) }.toAddSubsemigroup.carrier
⊢ a • x ∈
    {
          toAddSubsemigroup :=
            { carrier := {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)},
              add_mem' :=
                (_ :
                  ∀ {a b : F},
                    a ∈ {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)} →
                      b ∈ {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)} →
                        a + b ∈ {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)}) },
          zero_mem' :=
            (_ :
              0 ∈
                { carrier := {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)},
                    add_mem' :=
                      (_ :
                        ∀ {a b : F},
                          a ∈ {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)} →
                            b ∈ {y | Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)} →
                              a + b ∈
                                {y |
                                  Continuous
                                    ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)}) }.carrier) }.toAddSubsemigroup.carrier
[PROOFSTEP]
rw [Set.mem_setOf_eq, LinearMap.map_smulₛₗ] at *
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
a : 𝕜
x : F
hx : Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) x) T.toFun)
⊢ Continuous ↑(LinearMap.comp (↑(starRingEnd 𝕜) a • ↑(innerₛₗ 𝕜) x) T.toFun)
[PROOFSTEP]
exact hx.const_smul (conj a)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
x y : { x // x ∈ adjointDomain T }
x✝ : { x // x ∈ T.domain }
⊢ inner ((fun y => ↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E)) (adjointDomainMkClmExtend hT y)) (x + y))
      ↑x✝ =
    inner
      ((fun y => ↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E)) (adjointDomainMkClmExtend hT y)) x +
        (fun y => ↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E)) (adjointDomainMkClmExtend hT y)) y)
      ↑x✝
[PROOFSTEP]
simp only [inner_add_left, Submodule.coe_add, InnerProductSpace.toDual_symm_apply, adjointDomainMkClmExtend_apply]
  -- Porting note(https://github.com/leanprover-community/mathlib4/issues/5026):
        -- mathlib3 was finished here
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
x y : { x // x ∈ adjointDomain T }
x✝ : { x // x ∈ T.domain }
⊢ ↑(adjointDomainMkClmExtend hT (x + y)) ↑x✝ =
    ↑(adjointDomainMkClmExtend hT x) ↑x✝ + ↑(adjointDomainMkClmExtend hT y) ↑x✝
[PROOFSTEP]
rw [adjointDomainMkClmExtend_apply, adjointDomainMkClmExtend_apply, adjointDomainMkClmExtend_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
x y : { x // x ∈ adjointDomain T }
x✝ : { x // x ∈ T.domain }
⊢ inner (↑(x + y)) (↑T x✝) = inner (↑x) (↑T x✝) + inner (↑y) (↑T x✝)
[PROOFSTEP]
simp only [AddSubmonoid.coe_add, Submodule.coe_toAddSubmonoid, inner_add_left]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
x✝² : 𝕜
x✝¹ : { x // x ∈ adjointDomain T }
x✝ : { x // x ∈ T.domain }
⊢ inner
      (AddHom.toFun
        { toFun := fun y => ↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E)) (adjointDomainMkClmExtend hT y),
          map_add' :=
            (_ :
              ∀ (x y : { x // x ∈ adjointDomain T }),
                (fun y => ↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E)) (adjointDomainMkClmExtend hT y))
                    (x + y) =
                  (fun y => ↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E)) (adjointDomainMkClmExtend hT y))
                      x +
                    (fun y =>
                        ↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E)) (adjointDomainMkClmExtend hT y))
                      y) }
        (x✝² • x✝¹))
      ↑x✝ =
    inner
      (↑(RingHom.id 𝕜) x✝² •
        AddHom.toFun
          {
            toFun := fun y =>
              ↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E)) (adjointDomainMkClmExtend hT y),
            map_add' :=
              (_ :
                ∀ (x y : { x // x ∈ adjointDomain T }),
                  (fun y => ↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E)) (adjointDomainMkClmExtend hT y))
                      (x + y) =
                    (fun y =>
                          ↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E)) (adjointDomainMkClmExtend hT y))
                        x +
                      (fun y =>
                          ↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E)) (adjointDomainMkClmExtend hT y))
                        y) }
          x✝¹)
      ↑x✝
[PROOFSTEP]
simp only [inner_smul_left, Submodule.coe_smul_of_tower, RingHom.id_apply, InnerProductSpace.toDual_symm_apply,
  adjointDomainMkClmExtend_apply]
  -- Porting note(https://github.com/leanprover-community/mathlib4/issues/5026):
        -- mathlib3 was finished here
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
x✝² : 𝕜
x✝¹ : { x // x ∈ adjointDomain T }
x✝ : { x // x ∈ T.domain }
⊢ ↑(adjointDomainMkClmExtend hT (x✝² • x✝¹)) ↑x✝ = ↑(starRingEnd 𝕜) x✝² * ↑(adjointDomainMkClmExtend hT x✝¹) ↑x✝
[PROOFSTEP]
rw [adjointDomainMkClmExtend_apply, adjointDomainMkClmExtend_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
x✝² : 𝕜
x✝¹ : { x // x ∈ adjointDomain T }
x✝ : { x // x ∈ T.domain }
⊢ inner (↑(x✝² • x✝¹)) (↑T x✝) = ↑(starRingEnd 𝕜) x✝² * inner (↑x✝¹) (↑T x✝)
[PROOFSTEP]
simp only [Submodule.coe_smul_of_tower, inner_smul_left]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : { x // x ∈ adjointDomain T }
x : { x // x ∈ T.domain }
⊢ inner (↑(adjointAux hT) y) ↑x = inner (↑y) (↑T x)
[PROOFSTEP]
simp only [adjointAux, LinearMap.coe_mk, InnerProductSpace.toDual_symm_apply, adjointDomainMkClmExtend_apply]
  -- Porting note(https://github.com/leanprover-community/mathlib4/issues/5026):
    -- mathlib3 was finished here
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : { x // x ∈ adjointDomain T }
x : { x // x ∈ T.domain }
⊢ inner
      (↑{ toFun := fun y => ↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E)) (adjointDomainMkClmExtend hT y),
            map_add' :=
              (_ :
                ∀ (x y : { x // x ∈ adjointDomain T }),
                  (fun y => ↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E)) (adjointDomainMkClmExtend hT y))
                      (x + y) =
                    (fun y =>
                          ↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E)) (adjointDomainMkClmExtend hT y))
                        x +
                      (fun y =>
                          ↑(LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E)) (adjointDomainMkClmExtend hT y))
                        y) }
        y)
      ↑x =
    inner (↑y) (↑T x)
[PROOFSTEP]
simp only [AddHom.coe_mk, InnerProductSpace.toDual_symm_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : { x // x ∈ adjointDomain T }
x : { x // x ∈ T.domain }
⊢ ↑(adjointDomainMkClmExtend hT y) ↑x = inner (↑y) (↑T x)
[PROOFSTEP]
rw [adjointDomainMkClmExtend_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : F
h : ∃ w, ∀ (x : { x // x ∈ T.domain }), inner w ↑x = inner y (↑T x)
⊢ y ∈ T†.domain
[PROOFSTEP]
cases' h with w hw
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : F
w : E
hw : ∀ (x : { x // x ∈ T.domain }), inner w ↑x = inner y (↑T x)
⊢ y ∈ T†.domain
[PROOFSTEP]
rw [T.mem_adjoint_domain_iff]
  -- Porting note: was `by continuity`
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : F
w : E
hw : ∀ (x : { x // x ∈ T.domain }), inner w ↑x = inner y (↑T x)
⊢ Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)
[PROOFSTEP]
have : Continuous ((innerSL 𝕜 w).comp T.domain.subtypeL) := ContinuousLinearMap.continuous _
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : F
w : E
hw : ∀ (x : { x // x ∈ T.domain }), inner w ↑x = inner y (↑T x)
this : Continuous ↑(ContinuousLinearMap.comp (↑(innerSL 𝕜) w) (Submodule.subtypeL T.domain))
⊢ Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun)
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_5
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : F
w : E
hw : ∀ (x : { x // x ∈ T.domain }), inner w ↑x = inner y (↑T x)
this : Continuous ↑(ContinuousLinearMap.comp (↑(innerSL 𝕜) w) (Submodule.subtypeL T.domain))
⊢ ↑(LinearMap.comp (↑(innerₛₗ 𝕜) y) T.toFun) =
    ↑(ContinuousLinearMap.comp (↑(innerSL 𝕜) w) (Submodule.subtypeL T.domain))
[PROOFSTEP]
exact funext fun x => (hw x).symm
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT✝ : Dense ↑T.domain
inst✝ : CompleteSpace E
hT : ¬Dense ↑T.domain
y : { x // x ∈ T†.domain }
⊢ ↑T† y = 0
[PROOFSTEP]
change (if hT : Dense (T.domain : Set E) then adjointAux hT else 0) y = _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT✝ : Dense ↑T.domain
inst✝ : CompleteSpace E
hT : ¬Dense ↑T.domain
y : { x // x ∈ T†.domain }
⊢ ↑(if hT : Dense ↑T.domain then adjointAux hT else 0) y = 0
[PROOFSTEP]
simp only [hT, not_false_iff, dif_neg, LinearMap.zero_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : { x // x ∈ T†.domain }
⊢ ↑T† y = ↑(adjointAux hT) y
[PROOFSTEP]
change (if hT : Dense (T.domain : Set E) then adjointAux hT else 0) y = _
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
y : { x // x ∈ T†.domain }
⊢ ↑(if hT : Dense ↑T.domain then adjointAux hT else 0) y = ↑(adjointAux hT) y
[PROOFSTEP]
simp only [hT, dif_pos, LinearMap.coe_mk]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
hT : Dense ↑T.domain
inst✝ : CompleteSpace E
h : IsFormalAdjoint T S
x✝² : { x // x ∈ S.domain }
x✝¹ : { x // x ∈ T†.domain }
hxy : ↑x✝² = ↑x✝¹
x✝ : { x // x ∈ T.domain }
⊢ inner (↑S x✝²) ↑x✝ = inner (↑x✝¹) (↑T x✝)
[PROOFSTEP]
rw [h.symm, hxy]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
⊢ LinearPMap.adjoint (LinearMap.toPMap (↑A) p) = LinearMap.toPMap ↑(↑adjoint A) ⊤
[PROOFSTEP]
ext x y hxy
[GOAL]
case h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : F
⊢ x ∈ (LinearPMap.adjoint (LinearMap.toPMap (↑A) p)).domain ↔ x ∈ (LinearMap.toPMap ↑(↑adjoint A) ⊤).domain
[PROOFSTEP]
simp only [LinearMap.toPMap_domain, Submodule.mem_top, iff_true_iff, LinearPMap.mem_adjoint_domain_iff,
  LinearMap.coe_comp, innerₛₗ_apply_coe]
[GOAL]
case h.h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : F
⊢ Continuous ((fun w => inner x w) ∘ ↑(LinearMap.toPMap (↑A) p).toFun)
[PROOFSTEP]
exact ((innerSL 𝕜 x).comp <| A.comp <| Submodule.subtypeL _).cont
[GOAL]
case h'
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : { x // x ∈ (LinearPMap.adjoint (LinearMap.toPMap (↑A) p)).domain }
y : { x // x ∈ (LinearMap.toPMap ↑(↑adjoint A) ⊤).domain }
hxy : ↑x = ↑y
⊢ ↑(LinearPMap.adjoint (LinearMap.toPMap (↑A) p)) x = ↑(LinearMap.toPMap ↑(↑adjoint A) ⊤) y
[PROOFSTEP]
refine' LinearPMap.adjoint_apply_eq _ _ fun v => _
[GOAL]
case h'.refine'_1
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : { x // x ∈ (LinearPMap.adjoint (LinearMap.toPMap (↑A) p)).domain }
y : { x // x ∈ (LinearMap.toPMap ↑(↑adjoint A) ⊤).domain }
hxy : ↑x = ↑y
⊢ Dense ↑(LinearMap.toPMap (↑A) p).domain
[PROOFSTEP]
simpa using hp
[GOAL]
case h'.refine'_2
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : IsROrC 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : InnerProductSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 F
inst✝¹ : CompleteSpace E
inst✝ : CompleteSpace F
A : E →L[𝕜] F
p : Submodule 𝕜 E
hp : Dense ↑p
x : { x // x ∈ (LinearPMap.adjoint (LinearMap.toPMap (↑A) p)).domain }
y : { x // x ∈ (LinearMap.toPMap ↑(↑adjoint A) ⊤).domain }
hxy : ↑x = ↑y
v : { x // x ∈ (LinearMap.toPMap (↑A) p).domain }
⊢ inner (↑(LinearMap.toPMap ↑(↑adjoint A) ⊤) y) ↑v = inner (↑x) (↑(LinearMap.toPMap (↑A) p) v)
[PROOFSTEP]
simp only [adjoint_inner_left, hxy, LinearMap.toPMap_apply, coe_coe]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : IsSelfAdjoint A
⊢ Dense ↑A.domain
[PROOFSTEP]
by_contra h
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : IsSelfAdjoint A
h : ¬Dense ↑A.domain
⊢ False
[PROOFSTEP]
rw [isSelfAdjoint_def] at hA
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : A† = A
h : ¬Dense ↑A.domain
⊢ False
[PROOFSTEP]
have h' : A.domain = ⊤ := by
  rw [← hA, Submodule.eq_top_iff']
  intro x
  rw [mem_adjoint_domain_iff, ← hA]
  refine (innerSL 𝕜 x).cont.comp ?_
  simp [adjoint, h, continuous_const]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : A† = A
h : ¬Dense ↑A.domain
⊢ A.domain = ⊤
[PROOFSTEP]
rw [← hA, Submodule.eq_top_iff']
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : A† = A
h : ¬Dense ↑A.domain
⊢ ∀ (x : E), x ∈ A†.domain
[PROOFSTEP]
intro x
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : A† = A
h : ¬Dense ↑A.domain
x : E
⊢ x ∈ A†.domain
[PROOFSTEP]
rw [mem_adjoint_domain_iff, ← hA]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : A† = A
h : ¬Dense ↑A.domain
x : E
⊢ Continuous ↑(LinearMap.comp (↑(innerₛₗ 𝕜) x) A†.toFun)
[PROOFSTEP]
refine (innerSL 𝕜 x).cont.comp ?_
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : A† = A
h : ¬Dense ↑A.domain
x : E
⊢ Continuous fun x => ↑A†.toFun x
[PROOFSTEP]
simp [adjoint, h, continuous_const]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace 𝕜 E
inst✝² : NormedAddCommGroup F
inst✝¹ : InnerProductSpace 𝕜 F
inst✝ : CompleteSpace E
A : E →ₗ.[𝕜] E
hA : A† = A
h : ¬Dense ↑A.domain
h' : A.domain = ⊤
⊢ False
[PROOFSTEP]
simp [h'] at h


[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
a✝ b✝ : E
hx : a✝ ∈ {v | ∀ (u : E), u ∈ K → inner u v = 0}
hy : b✝ ∈ {v | ∀ (u : E), u ∈ K → inner u v = 0}
u : E
hu : u ∈ K
⊢ inner u (a✝ + b✝) = 0
[PROOFSTEP]
rw [inner_add_right, hx u hu, hy u hu, add_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
c : 𝕜
x : E
hx :
  x ∈
    {
          toAddSubsemigroup :=
            { carrier := {v | ∀ (u : E), u ∈ K → inner u v = 0},
              add_mem' :=
                (_ :
                  ∀ {a b : E},
                    a ∈ {v | ∀ (u : E), u ∈ K → inner u v = 0} →
                      b ∈ {v | ∀ (u : E), u ∈ K → inner u v = 0} → ∀ (u : E), u ∈ K → inner u (a + b) = 0) },
          zero_mem' := (_ : ∀ (x : E), x ∈ K → inner x 0 = 0) }.toAddSubsemigroup.carrier
u : E
hu : u ∈ K
⊢ inner u (c • x) = 0
[PROOFSTEP]
rw [inner_smul_right, hx u hu, mul_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
v : E
⊢ v ∈ Kᗮ ↔ ∀ (u : E), u ∈ K → inner v u = 0
[PROOFSTEP]
simp_rw [mem_orthogonal, inner_eq_zero_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
u v : E
hu : u ∈ K
hv : v ∈ Kᗮ
⊢ inner v u = 0
[PROOFSTEP]
rw [inner_eq_zero_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
u v : E
hu : u ∈ K
hv : v ∈ Kᗮ
⊢ inner u v = 0
[PROOFSTEP]
exact inner_right_of_mem_orthogonal hu hv
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
u v : E
⊢ v ∈ (span 𝕜 {u})ᗮ ↔ inner u v = 0
[PROOFSTEP]
refine' ⟨inner_right_of_mem_orthogonal (mem_span_singleton_self u), _⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
u v : E
⊢ inner u v = 0 → v ∈ (span 𝕜 {u})ᗮ
[PROOFSTEP]
intro hv w hw
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
u v : E
hv : inner u v = 0
w : E
hw : w ∈ span 𝕜 {u}
⊢ inner w v = 0
[PROOFSTEP]
rw [mem_span_singleton] at hw
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
u v : E
hv : inner u v = 0
w : E
hw : ∃ a, a • u = w
⊢ inner w v = 0
[PROOFSTEP]
obtain ⟨c, rfl⟩ := hw
[GOAL]
case intro
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
u v : E
hv : inner u v = 0
c : 𝕜
⊢ inner (c • u) v = 0
[PROOFSTEP]
simp [inner_smul_left, hv]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
u v : E
⊢ v ∈ (span 𝕜 {u})ᗮ ↔ inner v u = 0
[PROOFSTEP]
rw [mem_orthogonal_singleton_iff_inner_right, inner_eq_zero_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner x ↑v = inner y ↑v
⊢ x - y ∈ Kᗮ
[PROOFSTEP]
rw [mem_orthogonal']
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner x ↑v = inner y ↑v
⊢ ∀ (u : E), u ∈ K → inner (x - y) u = 0
[PROOFSTEP]
intro u hu
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner x ↑v = inner y ↑v
u : E
hu : u ∈ K
⊢ inner (x - y) u = 0
[PROOFSTEP]
rw [inner_sub_left, sub_eq_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner x ↑v = inner y ↑v
u : E
hu : u ∈ K
⊢ inner x u = inner y u
[PROOFSTEP]
exact h ⟨u, hu⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner (↑v) x = inner (↑v) y
⊢ x - y ∈ Kᗮ
[PROOFSTEP]
intro u hu
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner (↑v) x = inner (↑v) y
u : E
hu : u ∈ K
⊢ inner u (x - y) = 0
[PROOFSTEP]
rw [inner_sub_right, sub_eq_zero]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x y : E
h : ∀ (v : { x // x ∈ K }), inner (↑v) x = inner (↑v) y
u : E
hu : u ∈ K
⊢ inner u x = inner u y
[PROOFSTEP]
exact h ⟨u, hu⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ K ⊓ Kᗮ = ⊥
[PROOFSTEP]
rw [eq_bot_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ K ⊓ Kᗮ ≤ ⊥
[PROOFSTEP]
intro x
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x : E
⊢ x ∈ K ⊓ Kᗮ → x ∈ ⊥
[PROOFSTEP]
rw [mem_inf]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x : E
⊢ x ∈ K ∧ x ∈ Kᗮ → x ∈ ⊥
[PROOFSTEP]
exact fun ⟨hx, ho⟩ => inner_self_eq_zero.1 (ho x hx)
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ Disjoint K Kᗮ
[PROOFSTEP]
simp [disjoint_iff, K.inf_orthogonal_eq_bot]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ Kᗮ = ⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v)
[PROOFSTEP]
apply le_antisymm
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ Kᗮ ≤ ⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v)
[PROOFSTEP]
rw [le_iInf_iff]
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ ∀ (i : { x // x ∈ K }), Kᗮ ≤ LinearMap.ker (↑(innerSL 𝕜) ↑i)
[PROOFSTEP]
rintro ⟨v, hv⟩ w hw
[GOAL]
case a.mk
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
v : E
hv : v ∈ K
w : E
hw : w ∈ Kᗮ
⊢ w ∈ LinearMap.ker (↑(innerSL 𝕜) ↑{ val := v, property := hv })
[PROOFSTEP]
simpa using hw _ hv
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ ⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v) ≤ Kᗮ
[PROOFSTEP]
intro v hv w hw
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
v : E
hv : v ∈ ⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v)
w : E
hw : w ∈ K
⊢ inner w v = 0
[PROOFSTEP]
simp only [mem_iInf] at hv
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
v w : E
hw : w ∈ K
hv : ∀ (i : { x // x ∈ K }), v ∈ LinearMap.ker (↑(innerSL 𝕜) ↑i)
⊢ inner w v = 0
[PROOFSTEP]
exact hv ⟨w, hw⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ IsClosed ↑Kᗮ
[PROOFSTEP]
rw [orthogonal_eq_inter K]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ IsClosed ↑(⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v))
[PROOFSTEP]
have := fun v : K => ContinuousLinearMap.isClosed_ker (innerSL 𝕜 (v : E))
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
this : ∀ (v : { x // x ∈ K }), IsClosed ↑(LinearMap.ker (↑(innerSL 𝕜) ↑v))
⊢ IsClosed ↑(⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v))
[PROOFSTEP]
convert isClosed_iInter this
[GOAL]
case h.e'_3
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
this : ∀ (v : { x // x ∈ K }), IsClosed ↑(LinearMap.ker (↑(innerSL 𝕜) ↑v))
⊢ ↑(⨅ (v : { x // x ∈ K }), LinearMap.ker (↑(innerSL 𝕜) ↑v)) =
    ⋂ (i : { x // x ∈ K }), ↑(LinearMap.ker (↑(innerSL 𝕜) ↑i))
[PROOFSTEP]
simp only [iInf_coe]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ ⊤ᗮ = ⊥
[PROOFSTEP]
ext x
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x : E
⊢ x ∈ ⊤ᗮ ↔ x ∈ ⊥
[PROOFSTEP]
rw [mem_bot, mem_orthogonal]
[GOAL]
case h
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x : E
⊢ (∀ (u : E), u ∈ ⊤ → inner u x = 0) ↔ x = 0
[PROOFSTEP]
exact
  ⟨fun h => inner_self_eq_zero.mp (h x mem_top), by
    rintro rfl
    simp⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
x : E
⊢ x = 0 → ∀ (u : E), u ∈ ⊤ → inner u x = 0
[PROOFSTEP]
rintro rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ ∀ (u : E), u ∈ ⊤ → inner u 0 = 0
[PROOFSTEP]
simp
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ ⊥ᗮ = ⊤
[PROOFSTEP]
rw [← top_orthogonal_eq_bot, eq_top_iff]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ ⊤ ≤ ⊤ᗮᗮ
[PROOFSTEP]
exact le_orthogonal_orthogonal ⊤
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ Kᗮ = ⊤ ↔ K = ⊥
[PROOFSTEP]
refine'
  ⟨_, by
    rintro rfl
    exact bot_orthogonal_eq_top⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ K = ⊥ → Kᗮ = ⊤
[PROOFSTEP]
rintro rfl
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
⊢ ⊥ᗮ = ⊤
[PROOFSTEP]
exact bot_orthogonal_eq_top
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
⊢ Kᗮ = ⊤ → K = ⊥
[PROOFSTEP]
intro h
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
h : Kᗮ = ⊤
⊢ K = ⊥
[PROOFSTEP]
have : K ⊓ Kᗮ = ⊥ := K.orthogonal_disjoint.eq_bot
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
K : Submodule 𝕜 E
h : Kᗮ = ⊤
this : K ⊓ Kᗮ = ⊥
⊢ K = ⊥
[PROOFSTEP]
rwa [h, inf_comm, top_inf_eq] at this
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
U : Submodule 𝕜 E
V : Set (Submodule 𝕜 E)
⊢ (∀ (Uᵢ : Submodule 𝕜 E), Uᵢ ∈ V → Uᵢ ⟂ U) ↔ ∀ (Vᵢ : Submodule 𝕜 E), Vᵢ ∈ V → U ⟂ Vᵢ
[PROOFSTEP]
simp_rw [isOrtho_comm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
ι : Sort u_4
U : Submodule 𝕜 E
V : ι → Submodule 𝕜 E
⊢ (∀ (i : ι), V i ⟂ U) ↔ ∀ (i : ι), U ⟂ V i
[PROOFSTEP]
simp_rw [isOrtho_comm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
s t : Set E
⊢ span 𝕜 s ⟂ span 𝕜 t ↔ ∀ ⦃u : E⦄, u ∈ s → ∀ ⦃v : E⦄, v ∈ t → inner u v = 0
[PROOFSTEP]
simp_rw [span_eq_iSup_of_singleton_spans s, span_eq_iSup_of_singleton_spans t, isOrtho_iSup_left, isOrtho_iSup_right,
  isOrtho_iff_le, span_le, Set.subset_def, SetLike.mem_coe, mem_orthogonal_singleton_iff_inner_left,
  Set.mem_singleton_iff, forall_eq]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : U ⟂ V
⊢ Submodule.map f U ⟂ Submodule.map f V
[PROOFSTEP]
rw [isOrtho_iff_inner_eq] at *
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : ∀ (u : E), u ∈ U → ∀ (v : E), v ∈ V → inner u v = 0
⊢ ∀ (u : F), u ∈ Submodule.map f U → ∀ (v : F), v ∈ Submodule.map f V → inner u v = 0
[PROOFSTEP]
simp_rw [mem_map, forall_exists_index, and_imp, forall_apply_eq_imp_iff₂, LinearIsometry.inner_map_map]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : ∀ (u : E), u ∈ U → ∀ (v : E), v ∈ V → inner u v = 0
⊢ ∀ (a : E), a ∈ U → ∀ (a_2 : E), a_2 ∈ V → inner a a_2 = 0
[PROOFSTEP]
exact h
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : U ⟂ V
⊢ Submodule.comap f U ⟂ Submodule.comap f V
[PROOFSTEP]
rw [isOrtho_iff_inner_eq] at *
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : ∀ (u : F), u ∈ U → ∀ (v : F), v ∈ V → inner u v = 0
⊢ ∀ (u : E), u ∈ Submodule.comap f U → ∀ (v : E), v ∈ Submodule.comap f V → inner u v = 0
[PROOFSTEP]
simp_rw [mem_comap, ← f.inner_map_map]
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : ∀ (u : F), u ∈ U → ∀ (v : F), v ∈ V → inner u v = 0
⊢ ∀ (u : E), ↑f u ∈ U → ∀ (v : E), ↑f v ∈ V → inner (↑f u) (↑f v) = 0
[PROOFSTEP]
intro u hu v hv
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E →ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : ∀ (u : F), u ∈ U → ∀ (v : F), v ∈ V → inner u v = 0
u : E
hu : ↑f u ∈ U
v : E
hv : ↑f v ∈ V
⊢ inner (↑f u) (↑f v) = 0
[PROOFSTEP]
exact h _ hu _ hv
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : Submodule.map f U ⟂ Submodule.map f V
⊢ U ⟂ V
[PROOFSTEP]
have hf : ∀ p : Submodule 𝕜 E, (p.map f).comap f.toLinearIsometry = p := comap_map_eq_of_injective f.injective
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 E
h : Submodule.map f U ⟂ Submodule.map f V
hf : ∀ (p : Submodule 𝕜 E), Submodule.comap (LinearIsometryEquiv.toLinearIsometry f) (Submodule.map f p) = p
⊢ U ⟂ V
[PROOFSTEP]
simpa only [hf] using h.comap f.toLinearIsometry
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : Submodule.comap f U ⟂ Submodule.comap f V
⊢ U ⟂ V
[PROOFSTEP]
have hf : ∀ p : Submodule 𝕜 F, (p.comap f).map f.toLinearIsometry = p := map_comap_eq_of_surjective f.surjective
[GOAL]
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : IsROrC 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : InnerProductSpace 𝕜 F
f : E ≃ₗᵢ[𝕜] F
U V : Submodule 𝕜 F
h : Submodule.comap f U ⟂ Submodule.comap f V
hf : ∀ (p : Submodule 𝕜 F), Submodule.map (LinearIsometryEquiv.toLinearIsometry f) (Submodule.comap f p) = p
⊢ U ⟂ V
[PROOFSTEP]
simpa only [hf] using h.map f.toLinearIsometry


[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' ↑z
⊢ HasStrictDerivAt (fun x => (e ↑x).re) e'.re z
[PROOFSTEP]
have A : HasStrictFDerivAt ((↑) : ℝ → ℂ) ofRealClm z := ofRealClm.hasStrictFDerivAt
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' ↑z
A : HasStrictFDerivAt ofReal' ofRealClm z
⊢ HasStrictDerivAt (fun x => (e ↑x).re) e'.re z
[PROOFSTEP]
have B : HasStrictFDerivAt e ((ContinuousLinearMap.smulRight 1 e' : ℂ →L[ℂ] ℂ).restrictScalars ℝ) (ofRealClm z) :=
  h.hasStrictFDerivAt.restrictScalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' ↑z
A : HasStrictFDerivAt ofReal' ofRealClm z
B : HasStrictFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm z)
⊢ HasStrictDerivAt (fun x => (e ↑x).re) e'.re z
[PROOFSTEP]
have C : HasStrictFDerivAt re reClm (e (ofRealClm z)) := reClm.hasStrictFDerivAt
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' ↑z
A : HasStrictFDerivAt ofReal' ofRealClm z
B : HasStrictFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm z)
C : HasStrictFDerivAt re reClm (e (↑ofRealClm z))
⊢ HasStrictDerivAt (fun x => (e ↑x).re) e'.re z
[PROOFSTEP]
convert (C.comp z (B.comp z A)).hasStrictDerivAt
[GOAL]
case h.e'_7
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' ↑z
A : HasStrictFDerivAt ofReal' ofRealClm z
B : HasStrictFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm z)
C : HasStrictFDerivAt re reClm (e (↑ofRealClm z))
⊢ e'.re =
    ↑(ContinuousLinearMap.comp reClm
          (ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e'))
            ofRealClm))
      1
[PROOFSTEP]
rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.comp_apply]
[GOAL]
case h.e'_7
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasStrictDerivAt e e' ↑z
A : HasStrictFDerivAt ofReal' ofRealClm z
B : HasStrictFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm z)
C : HasStrictFDerivAt re reClm (e (↑ofRealClm z))
⊢ e'.re = ↑reClm (↑(ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm 1))
[PROOFSTEP]
simp
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' ↑z
⊢ HasDerivAt (fun x => (e ↑x).re) e'.re z
[PROOFSTEP]
have A : HasFDerivAt ((↑) : ℝ → ℂ) ofRealClm z := ofRealClm.hasFDerivAt
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' ↑z
A : HasFDerivAt ofReal' ofRealClm z
⊢ HasDerivAt (fun x => (e ↑x).re) e'.re z
[PROOFSTEP]
have B : HasFDerivAt e ((ContinuousLinearMap.smulRight 1 e' : ℂ →L[ℂ] ℂ).restrictScalars ℝ) (ofRealClm z) :=
  h.hasFDerivAt.restrictScalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' ↑z
A : HasFDerivAt ofReal' ofRealClm z
B : HasFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm z)
⊢ HasDerivAt (fun x => (e ↑x).re) e'.re z
[PROOFSTEP]
have C : HasFDerivAt re reClm (e (ofRealClm z)) := reClm.hasFDerivAt
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' ↑z
A : HasFDerivAt ofReal' ofRealClm z
B : HasFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm z)
C : HasFDerivAt re reClm (e (↑ofRealClm z))
⊢ HasDerivAt (fun x => (e ↑x).re) e'.re z
[PROOFSTEP]
convert (C.comp z (B.comp z A)).hasDerivAt
[GOAL]
case h.e'_7
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' ↑z
A : HasFDerivAt ofReal' ofRealClm z
B : HasFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm z)
C : HasFDerivAt re reClm (e (↑ofRealClm z))
⊢ e'.re =
    ↑(ContinuousLinearMap.comp reClm
          (ContinuousLinearMap.comp (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e'))
            ofRealClm))
      1
[PROOFSTEP]
rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.comp_apply]
[GOAL]
case h.e'_7
e : ℂ → ℂ
e' : ℂ
z : ℝ
h : HasDerivAt e e' ↑z
A : HasFDerivAt ofReal' ofRealClm z
B : HasFDerivAt e (ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm z)
C : HasFDerivAt re reClm (e (↑ofRealClm z))
⊢ e'.re = ↑reClm (↑(ContinuousLinearMap.restrictScalars ℝ (ContinuousLinearMap.smulRight 1 e')) (↑ofRealClm 1))
[PROOFSTEP]
simp
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
n : ℕ∞
h : ContDiffAt ℂ n e ↑z
⊢ ContDiffAt ℝ n (fun x => (e ↑x).re) z
[PROOFSTEP]
have A : ContDiffAt ℝ n ((↑) : ℝ → ℂ) z := ofRealClm.contDiff.contDiffAt
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
n : ℕ∞
h : ContDiffAt ℂ n e ↑z
A : ContDiffAt ℝ n ofReal' z
⊢ ContDiffAt ℝ n (fun x => (e ↑x).re) z
[PROOFSTEP]
have B : ContDiffAt ℝ n e z := h.restrict_scalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
n : ℕ∞
h : ContDiffAt ℂ n e ↑z
A : ContDiffAt ℝ n ofReal' z
B : ContDiffAt ℝ n e ↑z
⊢ ContDiffAt ℝ n (fun x => (e ↑x).re) z
[PROOFSTEP]
have C : ContDiffAt ℝ n re (e z) := reClm.contDiff.contDiffAt
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
n : ℕ∞
h : ContDiffAt ℂ n e ↑z
A : ContDiffAt ℝ n ofReal' z
B : ContDiffAt ℝ n e ↑z
C : ContDiffAt ℝ n re (e ↑z)
⊢ ContDiffAt ℝ n (fun x => (e ↑x).re) z
[PROOFSTEP]
exact C.comp z (B.comp z A)
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
x : ℂ
f' : E
h : HasStrictDerivAt f f' x
⊢ HasStrictFDerivAt f (ContinuousLinearMap.smulRight reClm f' + I • ContinuousLinearMap.smulRight imClm f') x
[PROOFSTEP]
simpa only [Complex.restrictScalars_one_smulRight'] using h.hasStrictFDerivAt.restrictScalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
x : ℂ
f' : E
h : HasDerivAt f f' x
⊢ HasFDerivAt f (ContinuousLinearMap.smulRight reClm f' + I • ContinuousLinearMap.smulRight imClm f') x
[PROOFSTEP]
simpa only [Complex.restrictScalars_one_smulRight'] using h.hasFDerivAt.restrictScalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
s : Set ℂ
x : ℂ
f' : E
h : HasDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f (ContinuousLinearMap.smulRight reClm f' + I • ContinuousLinearMap.smulRight imClm f') s x
[PROOFSTEP]
simpa only [Complex.restrictScalars_one_smulRight'] using h.hasFDerivWithinAt.restrictScalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
h : HasStrictDerivAt f f' x
⊢ HasStrictFDerivAt f (f' • 1) x
[PROOFSTEP]
simpa only [Complex.restrictScalars_one_smulRight] using h.hasStrictFDerivAt.restrictScalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
h : HasDerivAt f f' x
⊢ HasFDerivAt f (f' • 1) x
[PROOFSTEP]
simpa only [Complex.restrictScalars_one_smulRight] using h.hasFDerivAt.restrictScalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
s : Set ℂ
f' x : ℂ
h : HasDerivWithinAt f f' s x
⊢ HasFDerivWithinAt f (f' • 1) s x
[PROOFSTEP]
simpa only [Complex.restrictScalars_one_smulRight] using h.hasFDerivWithinAt.restrictScalars ℝ
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
hf : HasDerivAt e e' ↑z
⊢ HasDerivAt (fun y => e ↑y) e' z
[PROOFSTEP]
simpa only [ofRealClm_apply, ofReal_one, mul_one] using hf.comp z ofRealClm.hasDerivAt
[GOAL]
e : ℂ → ℂ
e' : ℂ
z : ℝ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → ℝ
u : ℝ
hf : HasDerivAt f u z
⊢ HasDerivAt (fun y => ↑(f y)) (↑u) z
[PROOFSTEP]
simpa only [ofRealClm_apply, ofReal_one, real_smul, mul_one] using ofRealClm.hasDerivAt.scomp z hf
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ ConformalAt f z
[PROOFSTEP]
rw [conformalAt_iff_isConformalMap_fderiv, (h.hasFDerivAt.restrictScalars ℝ).fderiv]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ IsConformalMap (ContinuousLinearMap.restrictScalars ℝ (fderiv ℂ f z))
[PROOFSTEP]
apply isConformalMap_complex_linear
[GOAL]
case nonzero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z : ℂ
f : ℂ → E
h : DifferentiableAt ℂ f z
hf' : deriv f z ≠ 0
⊢ fderiv ℂ f z ≠ 0
[PROOFSTEP]
simpa only [Ne.def, ext_ring_iff]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
⊢ ConformalAt f z ↔
    (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
[PROOFSTEP]
rw [conformalAt_iff_isConformalMap_fderiv]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
⊢ IsConformalMap (fderiv ℝ f z) ↔
    (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
[PROOFSTEP]
rw [isConformalMap_iff_is_complex_or_conj_linear]
[GOAL]
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
⊢ ((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ∧
      fderiv ℝ f z ≠ 0 ↔
    (DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)) ∧ fderiv ℝ f z ≠ 0
[PROOFSTEP]
apply and_congr_left
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
⊢ fderiv ℝ f z ≠ 0 →
    (((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
      DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z))
[PROOFSTEP]
intro h
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
⊢ ((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
[PROOFSTEP]
have h_diff := h.imp_symm fderiv_zero_of_not_differentiableAt
[GOAL]
case h
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ ((∃ map, restrictScalars ℝ map = fderiv ℝ f z) ∨ ∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    DifferentiableAt ℂ f z ∨ DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
[PROOFSTEP]
apply or_congr
[GOAL]
case h.h₁
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ (∃ map, restrictScalars ℝ map = fderiv ℝ f z) ↔ DifferentiableAt ℂ f z
[PROOFSTEP]
rw [differentiableAt_iff_restrictScalars ℝ h_diff]
[GOAL]
case h.h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f z
⊢ (∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
[PROOFSTEP]
rw [← conj_conj z] at h_diff
[GOAL]
case h.h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f (↑(starRingEnd ℂ) (↑(starRingEnd ℂ) z))
⊢ (∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    DifferentiableAt ℂ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
[PROOFSTEP]
rw [differentiableAt_iff_restrictScalars ℝ (h_diff.comp _ conjCle.differentiableAt)]
[GOAL]
case h.h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f (↑(starRingEnd ℂ) (↑(starRingEnd ℂ) z))
⊢ (∃ map, restrictScalars ℝ map = comp (fderiv ℝ f z) ↑conjCle) ↔
    ∃ g', restrictScalars ℝ g' = fderiv ℝ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
[PROOFSTEP]
refine' exists_congr fun g => rfl.congr _
[GOAL]
case h.h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f (↑(starRingEnd ℂ) (↑(starRingEnd ℂ) z))
g : ℂ →L[ℂ] ℂ
⊢ comp (fderiv ℝ f z) ↑conjCle = fderiv ℝ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
[PROOFSTEP]
have : fderiv ℝ conj (conj z) = _ := conjCle.fderiv
[GOAL]
case h.h₂
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
z✝ : ℂ
f✝ : ℂ → E
f : ℂ → ℂ
z : ℂ
h : fderiv ℝ f z ≠ 0
h_diff : DifferentiableAt ℝ f (↑(starRingEnd ℂ) (↑(starRingEnd ℂ) z))
g : ℂ →L[ℂ] ℂ
this : fderiv ℝ (↑(starRingEnd ((fun x => ℂ) z))) (↑(starRingEnd ℂ) z) = ↑conjCle
⊢ comp (fderiv ℝ f z) ↑conjCle = fderiv ℝ (f ∘ ↑(starRingEnd ℂ)) (↑(starRingEnd ℂ) z)
[PROOFSTEP]
simp [fderiv.comp _ h_diff conjCle.differentiableAt, this, conj_conj]


[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
⊢ x = y
[PROOFSTEP]
apply (toDualMap 𝕜 E).map_eq_iff.mp
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
⊢ ↑(toDualMap 𝕜 E) x = ↑(toDualMap 𝕜 E) y
[PROOFSTEP]
refine' (Function.Injective.eq_iff ContinuousLinearMap.coe_injective).mp (Basis.ext b _)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
⊢ ∀ (i : ι), ↑↑(↑(toDualMap 𝕜 E) x) (↑b i) = ↑↑(↑(toDualMap 𝕜 E) y) (↑b i)
[PROOFSTEP]
intro i
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ ↑↑(↑(toDualMap 𝕜 E) x) (↑b i) = ↑↑(↑(toDualMap 𝕜 E) y) (↑b i)
[PROOFSTEP]
simp only [ContinuousLinearMap.coe_coe]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ ↑(↑(toDualMap 𝕜 E) x) (↑b i) = ↑(↑(toDualMap 𝕜 E) y) (↑b i)
[PROOFSTEP]
rw [toDualMap_apply, toDualMap_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ inner x (↑b i) = inner y (↑b i)
[PROOFSTEP]
rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ ↑(starRingEnd 𝕜) (inner (↑b i) x) = inner y (↑b i)
[PROOFSTEP]
conv_rhs => rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
| inner y (↑b i)
[PROOFSTEP]
rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
| inner y (↑b i)
[PROOFSTEP]
rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
| inner y (↑b i)
[PROOFSTEP]
rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner (↑b i) x = inner (↑b i) y
i : ι
⊢ ↑(starRingEnd 𝕜) (inner (↑b i) x) = ↑(starRingEnd 𝕜) (inner (↑b i) y)
[PROOFSTEP]
exact congr_arg conj (h i)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner x (↑b i) = inner y (↑b i)
⊢ x = y
[PROOFSTEP]
refine' ext_inner_left_basis b fun i => _
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner x (↑b i) = inner y (↑b i)
i : ι
⊢ inner (↑b i) x = inner (↑b i) y
[PROOFSTEP]
rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner x (↑b i) = inner y (↑b i)
i : ι
⊢ ↑(starRingEnd 𝕜) (inner x (↑b i)) = inner (↑b i) y
[PROOFSTEP]
conv_rhs => rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner x (↑b i) = inner y (↑b i)
i : ι
| inner (↑b i) y
[PROOFSTEP]
rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner x (↑b i) = inner y (↑b i)
i : ι
| inner (↑b i) y
[PROOFSTEP]
rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner x (↑b i) = inner y (↑b i)
i : ι
| inner (↑b i) y
[PROOFSTEP]
rw [← inner_conj_symm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝² : IsROrC 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
ι : Type u_3
x y : E
b : Basis ι 𝕜 E
h : ∀ (i : ι), inner x (↑b i) = inner y (↑b i)
i : ι
⊢ ↑(starRingEnd 𝕜) (inner x (↑b i)) = ↑(starRingEnd 𝕜) (inner y (↑b i))
[PROOFSTEP]
exact congr_arg conj (h i)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
⊢ Function.Surjective ↑(toDualMap 𝕜 E)
[PROOFSTEP]
intro ℓ
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
set Y := LinearMap.ker ℓ
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
by_cases htriv : Y = ⊤
[GOAL]
case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : Y = ⊤
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
have hℓ : ℓ = 0 := by
  have h' := LinearMap.ker_eq_top.mp htriv
  rw [← coe_zero] at h'
  apply coe_injective
  exact h'
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : Y = ⊤
⊢ ℓ = 0
[PROOFSTEP]
have h' := LinearMap.ker_eq_top.mp htriv
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : Y = ⊤
h' : ↑ℓ = 0
⊢ ℓ = 0
[PROOFSTEP]
rw [← coe_zero] at h'
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : Y = ⊤
h'✝ : ↑ℓ = 0
h' : ↑ℓ = ↑0
⊢ ℓ = 0
[PROOFSTEP]
apply coe_injective
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : Y = ⊤
h'✝ : ↑ℓ = 0
h' : ↑ℓ = ↑0
⊢ ↑ℓ = ↑0
[PROOFSTEP]
exact h'
[GOAL]
case pos
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : Y = ⊤
hℓ : ℓ = 0
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
exact ⟨0, by simp [hℓ]⟩
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : Y = ⊤
hℓ : ℓ = 0
⊢ ↑(toDualMap 𝕜 E) 0 = ℓ
[PROOFSTEP]
simp [hℓ]
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : ¬Y = ⊤
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
rw [← Submodule.orthogonal_eq_bot_iff] at htriv
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : ¬Yᗮ = ⊥
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
change Yᗮ ≠ ⊥ at htriv
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : Yᗮ ≠ ⊥
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
rw [Submodule.ne_bot_iff] at htriv
[GOAL]
case neg
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
htriv : ∃ x, x ∈ Yᗮ ∧ x ≠ 0
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
obtain ⟨z : E, hz : z ∈ Yᗮ, z_ne_0 : z ≠ 0⟩ := htriv
[GOAL]
case neg.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
⊢ ∃ a, ↑(toDualMap 𝕜 E) a = ℓ
[PROOFSTEP]
refine' ⟨(starRingEnd (R := 𝕜) (ℓ z) / ⟪z, z⟫) • z, _⟩
[GOAL]
case neg.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
⊢ ↑(toDualMap 𝕜 E) ((↑(starRingEnd 𝕜) (↑ℓ z) / inner z z) • z) = ℓ
[PROOFSTEP]
apply ContinuousLinearMap.ext
[GOAL]
case neg.intro.intro.h
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
⊢ ∀ (x : E), ↑(↑(toDualMap 𝕜 E) ((↑(starRingEnd 𝕜) (↑ℓ z) / inner z z) • z)) x = ↑ℓ x
[PROOFSTEP]
intro x
[GOAL]
case neg.intro.intro.h
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
⊢ ↑(↑(toDualMap 𝕜 E) ((↑(starRingEnd 𝕜) (↑ℓ z) / inner z z) • z)) x = ↑ℓ x
[PROOFSTEP]
have h₁ : ℓ z • x - ℓ x • z ∈ Y :=
  by
  rw [LinearMap.mem_ker, map_sub, ContinuousLinearMap.map_smul, ContinuousLinearMap.map_smul, Algebra.id.smul_eq_mul,
    Algebra.id.smul_eq_mul, mul_comm]
  exact sub_self (ℓ x * ℓ z)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
⊢ ↑ℓ z • x - ↑ℓ x • z ∈ Y
[PROOFSTEP]
rw [LinearMap.mem_ker, map_sub, ContinuousLinearMap.map_smul, ContinuousLinearMap.map_smul, Algebra.id.smul_eq_mul,
  Algebra.id.smul_eq_mul, mul_comm]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
⊢ ↑ℓ x * ↑ℓ z - ↑ℓ x * ↑ℓ z = 0
[PROOFSTEP]
exact sub_self (ℓ x * ℓ z)
[GOAL]
case neg.intro.intro.h
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
⊢ ↑(↑(toDualMap 𝕜 E) ((↑(starRingEnd 𝕜) (↑ℓ z) / inner z z) • z)) x = ↑ℓ x
[PROOFSTEP]
have h₂ : ℓ z * ⟪z, x⟫ = ℓ x * ⟪z, z⟫ :=
  haveI h₃ :=
    calc
      0 = ⟪z, ℓ z • x - ℓ x • z⟫ := by
        rw [(Y.mem_orthogonal' z).mp hz]
        exact h₁
      _ = ⟪z, ℓ z • x⟫ - ⟪z, ℓ x • z⟫ := by rw [inner_sub_right]
      _ = ℓ z * ⟪z, x⟫ - ℓ x * ⟪z, z⟫ := by simp [inner_smul_right]
  sub_eq_zero.mp (Eq.symm h₃)
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
⊢ 0 = inner z (↑ℓ z • x - ↑ℓ x • z)
[PROOFSTEP]
rw [(Y.mem_orthogonal' z).mp hz]
[GOAL]
case a
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
⊢ ↑ℓ z • x - ↑ℓ x • z ∈ Y
[PROOFSTEP]
exact h₁
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
⊢ inner z (↑ℓ z • x - ↑ℓ x • z) = inner z (↑ℓ z • x) - inner z (↑ℓ x • z)
[PROOFSTEP]
rw [inner_sub_right]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
⊢ inner z (↑ℓ z • x) - inner z (↑ℓ x • z) = ↑ℓ z * inner z x - ↑ℓ x * inner z z
[PROOFSTEP]
simp [inner_smul_right]
[GOAL]
case neg.intro.intro.h
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
h₂ : ↑ℓ z * inner z x = ↑ℓ x * inner z z
⊢ ↑(↑(toDualMap 𝕜 E) ((↑(starRingEnd 𝕜) (↑ℓ z) / inner z z) • z)) x = ↑ℓ x
[PROOFSTEP]
have h₄ :=
  calc
    ⟪(ℓ z† / ⟪z, z⟫) • z, x⟫ = ℓ z / ⟪z, z⟫ * ⟪z, x⟫ := by simp [inner_smul_left, conj_conj]
    _ = ℓ z * ⟪z, x⟫ / ⟪z, z⟫ := by rw [← div_mul_eq_mul_div]
    _ = ℓ x * ⟪z, z⟫ / ⟪z, z⟫ := by rw [h₂]
    _ = ℓ x := by field_simp [inner_self_ne_zero.2 z_ne_0]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
h₂ : ↑ℓ z * inner z x = ↑ℓ x * inner z z
⊢ inner ((↑(starRingEnd ((fun a => 𝕜) z)) (↑ℓ z) / inner z z) • z) x = ↑ℓ z / inner z z * inner z x
[PROOFSTEP]
simp [inner_smul_left, conj_conj]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
h₂ : ↑ℓ z * inner z x = ↑ℓ x * inner z z
⊢ ↑ℓ z / inner z z * inner z x = ↑ℓ z * inner z x / inner z z
[PROOFSTEP]
rw [← div_mul_eq_mul_div]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
h₂ : ↑ℓ z * inner z x = ↑ℓ x * inner z z
⊢ ↑ℓ z * inner z x / inner z z = ↑ℓ x * inner z z / inner z z
[PROOFSTEP]
rw [h₂]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
h₂ : ↑ℓ z * inner z x = ↑ℓ x * inner z z
⊢ ↑ℓ x * inner z z / inner z z = ↑ℓ x
[PROOFSTEP]
field_simp [inner_self_ne_zero.2 z_ne_0]
[GOAL]
case neg.intro.intro.h
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
ℓ : NormedSpace.Dual 𝕜 E
Y : Submodule 𝕜 E := LinearMap.ker ℓ
z : E
hz : z ∈ Yᗮ
z_ne_0 : z ≠ 0
x : E
h₁ : ↑ℓ z • x - ↑ℓ x • z ∈ Y
h₂ : ↑ℓ z * inner z x = ↑ℓ x * inner z z
h₄ : inner ((↑(starRingEnd ((fun a => 𝕜) z)) (↑ℓ z) / inner z z) • z) x = ↑ℓ x
⊢ ↑(↑(toDualMap 𝕜 E) ((↑(starRingEnd 𝕜) (↑ℓ z) / inner z z) • z)) x = ↑ℓ x
[PROOFSTEP]
exact h₄
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
x : E
y : NormedSpace.Dual 𝕜 E
⊢ inner (↑(LinearIsometryEquiv.symm (toDual 𝕜 E)) y) x = ↑y x
[PROOFSTEP]
rw [← toDual_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
x : E
y : NormedSpace.Dual 𝕜 E
⊢ ↑(↑(toDual 𝕜 E) (↑(LinearIsometryEquiv.symm (toDual 𝕜 E)) y)) x = ↑y x
[PROOFSTEP]
simp only [LinearIsometryEquiv.apply_symm_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v w : E
⊢ inner (↑B♯ v) w = ↑(↑B v) w
[PROOFSTEP]
simp [continuousLinearMapOfBilin]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), inner f w = ↑(↑B v) w
⊢ f = ↑B♯ v
[PROOFSTEP]
refine' ext_inner_right 𝕜 _
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), inner f w = ↑(↑B v) w
⊢ ∀ (v_1 : E), inner f v_1 = inner (↑B♯ v) v_1
[PROOFSTEP]
intro w
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), inner f w = ↑(↑B v) w
w : E
⊢ inner f w = inner (↑B♯ v) w
[PROOFSTEP]
rw [continuousLinearMapOfBilin_apply]
[GOAL]
𝕜 : Type u_1
E : Type u_2
inst✝³ : IsROrC 𝕜
inst✝² : NormedAddCommGroup E
inst✝¹ : InnerProductSpace 𝕜 E
inst✝ : CompleteSpace E
B : E →L⋆[𝕜] E →L[𝕜] 𝕜
v f : E
is_lax_milgram : ∀ (w : E), inner f w = ↑(↑B v) w
w : E
⊢ inner f w = ↑(↑B v) w
[PROOFSTEP]
exact is_lax_milgram w