awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
h₅ : ⟪d, b⟫_𝕜 ≠ 0
h₆ : c ≠ 0
simp_rw : 0 < HPow.hPow (β := ℕ) ‖c‖ 2 / HPow.hPow (β := ℕ) ‖a‖ 2
⊢ 0 < HPow.hPow (α := 𝕜) (β := ℕ) (↑‖c‖ : 𝕜) 2 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖a‖ : 𝕜) 2

Tactic:
simp_rw [← ofReal_pow, ← ofReal_div, pos_iff (K := 𝕜), ofReal_re, ofReal_im, and_true]

Premises used: RCLike.pos_iff, RCLike.ofReal_re, and_true, RCLike.ofReal_im, RCLike.ofReal_pow, RCLike.ofReal_div
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
h₅ : ⟪d, b⟫_𝕜 ≠ 0
h₆ : c ≠ 0
⊢ 0 < HPow.hPow (β := ℕ) ‖c‖ 2

Tactic:
simpa [sq_pos_iff]

Premises used: sq_pos_iff
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
h₅ : ⟪d, b⟫_𝕜 ≠ 0
h₆ : c ≠ 0
⊢ 0 < HPow.hPow (β := ℕ) ‖a‖ 2

Tactic:
simpa [sq_pos_iff]

Premises used: sq_pos_iff
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
H : Type u_9
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
inst_3 : NormedAddCommGroup H
inst_4 : InnerProductSpace 𝕜 H
a c : F
b d : H
ha : a ≠ 0
hb : b ≠ 0
h : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
h₂ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
h₅ : ⟪d, b⟫_𝕜 ≠ 0
h₆ : c ≠ 0
⊢ 0 < HPow.hPow (β := ℕ) ‖c‖ 2 / HPow.hPow (β := ℕ) ‖a‖ 2

Tactic:
exact div_pos (by simpa [sq_pos_iff]) (by simpa [sq_pos_iff])

Premises used: div_pos
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →L[𝕜] F
C : ℝ
hC : 0 ≤ C
h : ∀ (x : E) (y : F), ‖x‖ = 1 → ‖y‖ = 1 → (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → F) x, y⟫_𝕜 ≤ C
⊢ ‖T‖ ≤ C

Tactic:
opNorm_le_of_unit_norm hC fun x hx ↦ ?_

Premises used: ContinuousLinearMap.opNorm_le_of_unit_norm
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →L[𝕜] F
C : ℝ
hC : 0 ≤ C
h : ∀ (x : E) (y : F), ‖x‖ = 1 → ‖y‖ = 1 → (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → F) x, y⟫_𝕜 ≤ C
refine : ∀ (x : E) (hx : ‖x‖ = 1), Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
⊢ ‖T‖ ≤ C

Tactic:
refine opNorm_le_of_unit_norm hC fun x hx ↦ ?_

Premises used: ContinuousLinearMap.opNorm_le_of_unit_norm
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →L[𝕜] F
C : ℝ
hC : 0 ≤ C
h : ∀ (x : E) (y : F), ‖x‖ = 1 → ‖y‖ = 1 → (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → F) x, y⟫_𝕜 ≤ C
x : E
hx : ‖x‖ = 1
pos :
  ∀ (hTx : Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) = 0),
    Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
neg :
  ∀ (hTx : ¬Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) = 0),
    Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
⊢ Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C

Tactic:
by_cases hTx : ‖T x‖ = 0

Premises used: DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →L[𝕜] F
C : ℝ
hC : 0 ≤ C
h : ∀ (x : E) (y : F), ‖x‖ = 1 → ‖y‖ = 1 → (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → F) x, y⟫_𝕜 ≤ C
x : E
hx : ‖x‖ = 1
hTx : Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) = 0
pos pos₁ pos₂ pos₃ : 0 ≤ C
⊢ Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C

Tactic:
rwa [hTx]
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →L[𝕜] F
C : ℝ
hC : 0 ≤ C
h : ∀ (x : E) (y : F), ‖x‖ = 1 → ‖y‖ = 1 → (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → F) x, y⟫_𝕜 ≤ C
x : E
hx : ‖x‖ = 1
hTx : ¬Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) = 0
⊢ ‖HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (β := F) (↑(Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F))⁻¹ : 𝕜)
        ((T : (a : E) → F) x : F)‖ =
    1

Tactic:
simp [norm_smul, hTx]

Premises used: norm_smul
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →L[𝕜] F
C : ℝ
hC : 0 ≤ C
h : ∀ (x : E) (y : F), ‖x‖ = 1 → ‖y‖ = 1 → (re : (a : 𝕜) → ℝ) ⟪(T : (a : E) → F) x, y⟫_𝕜 ≤ C
x : E
hx : ‖x‖ = 1
hTx : ¬Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) = 0
⊢ (re : (a : 𝕜) → ℝ)
      ⟪(T : (a : E) → F) x,
        HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (β := F) (↑(Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F))⁻¹ : 𝕜)
          ((T : (a : E) → F) x : F)⟫_𝕜 ≤
    C

Tactic:
specialize h x (((‖T x‖⁻¹ : ℝ) : 𝕜) • T x) hx (by simp [norm_smul, hTx])

Premises used: Norm.norm, RCLike.ofReal, Inv.inv, HSMul.hSMul, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.LinearMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →L[𝕜] F
C : ℝ
hC : 0 ≤ C
x : E
hx : ‖x‖ = 1
hTx : ¬Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) = 0
h :
  (re : (a : 𝕜) → ℝ)
      ⟪(T : (a : E) → F) x,
        HSMul.hSMul.{u_1, u_3, u_3} (α := 𝕜) (β := F) (↑(Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F))⁻¹ : 𝕜)
          ((T : (a : E) → F) x : F)⟫_𝕜 ≤
    C
neg :
  ∀
    (h :
      (re : (a : 𝕜) → ℝ)
          ((↑(Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F))⁻¹ : 𝕜) *
            inner.{u_1, u_3} 𝕜 (E := F) ((T : (a : E) → F) x : F) ((T : (a : E) → F) x : F)) ≤
        C),
    Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
neg₁ :
  ∀
    (h :
      HMul.hMul (β := ℝ) (Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F))⁻¹
          ((re : (a : 𝕜) → ℝ) (inner.{u_1, u_3} 𝕜 (E := F) ((T : (a : E) → F) x : F) ((T : (a : E) → F) x : F)) : ℝ) ≤
        C),
    Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
neg₂ :
  ∀
    (h :
      (Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F))⁻¹ *
          HPow.hPow (β := ℕ) (Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F)) 2 ≤
        C),
    Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
neg₃ :
  ∀
    (h :
      HPow.hPow (β := ℕ) (Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F)) 2 /
          Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤
        C),
    Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
neg₄ :
  ∀
    (h :
      Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) * Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) /
          Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤
        C),
    Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
neg₅ neg₆ neg₇ neg₈ :
  ∀ (h : Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C), Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
⊢ Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C

Tactic:
rwa [inner_smul_right, re_ofReal_mul, ← norm_sq_eq_re_inner,
      inv_mul_eq_div, sq, mul_self_div_self] at h

Premises used: inv_mul_eq_div, sq, InnerProductSpace.norm_sq_eq_re_inner, inner_smul_right, RCLike.re_ofReal_mul, mul_self_div_self
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
h : T.IsFormalAdjoint S
y : ↥S.domain
x : ↥T.domain
rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑x : E), (↑S : ↥S.domain → E) y⟫ = ⟪(↑y : F), (↑T : ↥T.domain → F) x⟫
rw₁ :
  Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑x : E), (↑S : ↥S.domain → E) y⟫ : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑T : ↥T.domain → F) x, (↑y : F)⟫ : 𝕜)
rw₂ rw₃ :
  Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑x : E), (↑S : ↥S.domain → E) y⟫ : 𝕜)
    ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑x : E), (↑S : ↥S.domain → E) y⟫ : 𝕜)
⊢ ⟪(↑S : ↥S.domain → E) y, (↑x : E)⟫ = ⟪(↑y : F), (↑T : ↥T.domain → F) x⟫

Tactic:
rw [← inner_conj_symm, ← inner_conj_symm (y : F), h]

Premises used: Subtype.val, inner_conj_symm
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
a b : F
hx :
  Membership.mem (γ := Set F)
    {y : F |
      Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
        (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)}
    a
hy :
  Membership.mem (γ := Set F)
    {y : F |
      Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
        (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)}
    b
rw :
  ∀
    (hx :
      Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
        (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) a ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜))
    (hy :
      Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
        (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) b ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)),
    Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
      (⇑(HAdd.hAdd (α := F →ₗ[𝕜] 𝕜) (β := F →ₗ[𝕜] 𝕜) ((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) a : F →ₗ[𝕜] 𝕜)
              ((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) b : F →ₗ[𝕜] 𝕜) ∘ₗ
            T.toFun) :
        (a : ↥T.domain) → 𝕜)
⊢ Membership.mem (γ := Set F)
    {y : F |
      Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
        (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)}
    (a + b)

Tactic:
rw [Set.mem_setOf_eq, LinearMap.map_add] at *

Premises used: LinearMap.map_add, Set.mem_setOf_eq
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
a b : F
hx :
  Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) a ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)
hy :
  Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) b ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)
⊢ Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑(HAdd.hAdd (α := F →ₗ[𝕜] 𝕜) (β := F →ₗ[𝕜] 𝕜) ((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) a : F →ₗ[𝕜] 𝕜)
            ((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) b : F →ₗ[𝕜] 𝕜) ∘ₗ
          T.toFun) :
      (a : ↥T.domain) → 𝕜)

Tactic:
hx.add hy

Premises used: Continuous.add
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
a b : F
hx :
  Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) a ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)
hy :
  Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) b ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)
⊢ Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑(HAdd.hAdd (α := F →ₗ[𝕜] 𝕜) (β := F →ₗ[𝕜] 𝕜) ((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) a : F →ₗ[𝕜] 𝕜)
            ((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) b : F →ₗ[𝕜] 𝕜) ∘ₗ
          T.toFun) :
      (a : ↥T.domain) → 𝕜)

Tactic:
exact hx.add hy

Premises used: Continuous.add
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
rw : Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜) (⇑0 : (a : ↥T.domain) → 𝕜)
⊢ Membership.mem (γ := Set F)
    {y : F |
      Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
        (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)}
    0

Tactic:
rw [Set.mem_setOf_eq, LinearMap.map_zero, LinearMap.zero_comp]

Premises used: LinearMap.map_zero, Set.mem_setOf_eq, LinearMap.zero_comp
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
⊢ Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜) (⇑0 : (a : ↥T.domain) → 𝕜)

Tactic:
continuous_zero

Premises used: continuous_zero
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
⊢ Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜) (⇑0 : (a : ↥T.domain) → 𝕜)

Tactic:
exact continuous_zero

Premises used: continuous_zero
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
a : 𝕜
x : F
hx :
  Membership.mem (γ := Set F)
    {y : F |
      Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
        (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)}
    x
rw :
  ∀
    (hx :
      Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
        (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) x ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)),
    Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
      (⇑(HSMul.hSMul (α := 𝕜) (β := F →ₗ[𝕜] 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜)
              ((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) ∘ₗ
            T.toFun) :
        (a : ↥T.domain) → 𝕜)
⊢ Membership.mem (γ := Set F)
    {y : F |
      Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
        (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)}
    (a • x)

Tactic:
rw [Set.mem_setOf_eq, LinearMap.map_smulₛₗ] at *

Premises used: Set.mem_setOf_eq, LinearMap.map_smulₛₗ
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
a : 𝕜
x : F
hx :
  Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) x ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)
⊢ Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑(HSMul.hSMul (α := 𝕜) (β := F →ₗ[𝕜] 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜)
            ((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) ∘ₗ
          T.toFun) :
      (a : ↥T.domain) → 𝕜)

Tactic:
hx.const_smul (conj a)

Premises used: starRingEnd, Continuous.const_smul, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
a : 𝕜
x : F
hx :
  Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) x ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)
⊢ Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑(HSMul.hSMul (α := 𝕜) (β := F →ₗ[𝕜] 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) a : 𝕜)
            ((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) x : F →ₗ[𝕜] 𝕜) ∘ₗ
          T.toFun) :
      (a : ↥T.domain) → 𝕜)

Tactic:
exact hx.const_smul (conj a)

Premises used: starRingEnd, Continuous.const_smul, DFunLike.coe
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
y : ↥T.adjointDomain
x : ↥T.domain
⊢ (T.adjointDomainMkCLM y : (a : ↥T.domain) → 𝕜) x = ⟪(↑y : F), (↑T : ↥T.domain → F) x⟫

Tactic:
rfl

Premises used: rfl, LinearPMap.toFun'
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
hT : Dense (↑T.domain : Set E)
y : ↥T.adjointDomain
x : ↥T.domain
⊢ (T.adjointDomainMkCLMExtend y : (a : E) → 𝕜) (↑x : E) = ⟪(↑y : F), (↑T : ↥T.domain → F) x⟫

Tactic:
ContinuousLinearMap.extend_eq _ hT.denseRange_val
    isUniformEmbedding_subtype_val.isUniformInducing _

Premises used: ContinuousLinearMap.extend_eq, LinearPMap.toFun'
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
inst_5 : CompleteSpace E
hT : Dense (↑T.domain : Set E)
x y : ↥T.adjointDomain
z : E
zin : z ∈ (↑T.domain : Set E)
⊢ ⟪(LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E) : (a : StrongDual 𝕜 E) → E)
        (T.adjointDomainMkCLMExtend (x + y)),
      z⟫ =
    ⟪HAdd.hAdd (α := E) (β := E)
        ((LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E) : (a : StrongDual 𝕜 E) → E)
            (T.adjointDomainMkCLMExtend x) :
          E)
        ((LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E) : (a : StrongDual 𝕜 E) → E)
            (T.adjointDomainMkCLMExtend y) :
          E),
      z⟫

Tactic:
simp [InnerProductSpace.toDual_symm_apply, inner_add_left,
        adjointDomainMkCLMExtend_apply hT _ ⟨z, zin⟩, inner_add_left]

Premises used: InnerProductSpace.toDual_symm_apply, inner_add_left, Subtype.mk, LinearPMap.adjointDomainMkCLMExtend_apply
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
S : F →ₗ.[𝕜] E
inst_5 : CompleteSpace E
hT : Dense (↑T.domain : Set E)
x : 𝕜
x_1 : ↥T.adjointDomain
z : E
zin : z ∈ (↑T.domain : Set E)
⊢ ⟪(LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E) : (a : StrongDual 𝕜 E) → E)
        (T.adjointDomainMkCLMExtend (x • x_1)),
      z⟫ =
    ⟪HSMul.hSMul (α := 𝕜) (β := E) ((RingHom.id 𝕜 : (a : 𝕜) → 𝕜) x : 𝕜)
        ((LinearIsometryEquiv.symm (InnerProductSpace.toDual 𝕜 E) : (a : StrongDual 𝕜 E) → E)
            (T.adjointDomainMkCLMExtend x_1) :
          E),
      z⟫

Tactic:
simp [inner_smul_left, RingHom.id_apply,
        InnerProductSpace.toDual_symm_apply, adjointDomainMkCLMExtend_apply hT _ ⟨z, zin⟩]

Premises used: InnerProductSpace.toDual_symm_apply, RingHom.id_apply, Subtype.mk, LinearPMap.adjointDomainMkCLMExtend_apply, inner_smul_left
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
hT : Dense (↑T.domain : Set E)
y : ↥T.adjointDomain
x : ↥T.domain
⊢ ⟪(adjointAux hT : (a : ↥T.adjointDomain) → E) y, (↑x : E)⟫ = ⟪(↑y : F), (↑T : ↥T.domain → F) x⟫

Tactic:
simp [adjointAux, hT]

Premises used: LinearPMap.adjointAux
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
hT : Dense (↑T.domain : Set E)
y : ↥T.adjointDomain
x₀ : E
hx₀ : ∀ (x : ↥T.domain), ⟪x₀, (↑x : E)⟫ = ⟪(↑y : F), (↑T : ↥T.domain → F) x⟫
⊢ (adjointAux hT : (a : ↥T.adjointDomain) → E) y = x₀

Tactic:
hT.eq_of_inner_left 𝕜 fun v vin => (adjointAux_inner hT _ _).trans (hx₀ ⟨v, vin⟩).symm

Premises used: Dense.eq_of_inner_left, Subtype.mk, Eq.symm, LinearPMap.adjointAux_inner, Eq.trans
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
y : F
⊢ y ∈ T†.domain ↔
    Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
      (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
y : F
h : ∃ (w : E), ∀ (x : ↥T.domain), ⟪w, (↑x : E)⟫ = ⟪y, (↑T : ↥T.domain → F) x⟫
obtain : ∀ (w : E) (hw : ∀ (x : ↥T.domain), ⟪w, (↑x : E)⟫ = ⟪y, (↑T : ↥T.domain → F) x⟫), y ∈ T†.domain
⊢ y ∈ T†.domain

Tactic:
obtain ⟨w, hw⟩ := h
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
y : F
w : E
hw : ∀ (x : ↥T.domain), ⟪w, (↑x : E)⟫ = ⟪y, (↑T : ↥T.domain → F) x⟫
rw :
  Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑((innerₛₗ 𝕜 : (a : F) → F →ₗ[𝕜] 𝕜) y ∘ₗ T.toFun) : (a : ↥T.domain) → 𝕜)
⊢ y ∈ T†.domain

Tactic:
rw [T.mem_adjoint_domain_iff]

Premises used: LinearPMap.mem_adjoint_domain_iff
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
y : F
w : E
hw : ∀ (x : ↥T.domain), ⟪w, (↑x : E)⟫ = ⟪y, (↑T : ↥T.domain → F) x⟫
⊢ Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑(ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) w) T.domain.subtypeL) :
      (a : ↥T.domain) → 𝕜)

Tactic:
fun_prop
-- Module: Mathlib.Analysis.InnerProductSpace.LinearPMap
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
T : E →ₗ.[𝕜] F
inst_5 : CompleteSpace E
y : F
w : E
hw : ∀ (x : ↥T.domain), ⟪w, (↑x : E)⟫ = ⟪y, (↑T : ↥T.domain → F) x⟫
⊢ Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜)
    (⇑(ContinuousLinearMap.comp (σ₂₃ := RingHom.id 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) w) T.domain.subtypeL) :
      (a : ↥T.domain) → 𝕜)

Tactic:
have : Continuous ((innerSL 𝕜 w).comp T.domain.subtypeL) := by fun_prop