awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
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
⊢ (1 / ⟪b, b⟫_𝕜) • ⟪b, b⟫_𝕜 • a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
have simp : (1 / ⟪b, b⟫_𝕜 * ⟪d, b⟫_𝕜) • c = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
Tactic: simp only [h, smul_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (hypothesis)
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
⊢ ∃ (α : 𝕜) (β : 𝕜) (_ : α ≠ 0) (_ : 0 < β), a = α • c ∧ b = (α * β) • d
have h₃ : a = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c
Tactic: have h₃ := calc
    a = (⟪b, b⟫_𝕜 / ⟪b, b⟫_𝕜) • a := by simp_all
    _ = (1 / ⟪b, b⟫_𝕜) • (⟪b, b⟫_𝕜 • a) := by simp only [smul_smul]; ring_nf
    _ = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c := by simp only [h, smul_smul]; ring_nf
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
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
⊢ (⟪a, a⟫_𝕜 / ⟪a, a⟫_𝕜) • b = (1 / ⟪a, a⟫_𝕜) • ⟪a, a⟫_𝕜 • b
have simp : (⟪a, a⟫_𝕜 / ⟪a, a⟫_𝕜) • b = (1 / ⟪a, a⟫_𝕜 * ⟪a, a⟫_𝕜) • b
Tactic: simp only [smul_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
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
⊢ (1 / ⟪a, a⟫_𝕜) • ⟪a, a⟫_𝕜 • b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
have simp_rw : (1 / (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * ⟪(⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c, c⟫_𝕜) * (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * ⟪c, c⟫_𝕜)) • d =
  (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * ⟪(⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) • c, c⟫_𝕜))) • d
Tactic: simp_rw [h₂, h₃, inner_smul_right, smul_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (hypothesis)
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
⊢ ∃ (α : 𝕜) (β : 𝕜) (_ : α ≠ 0) (_ : 0 < β), a = α • c ∧ b = (α * β) • d
have h₄ : b = (⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜 * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d
Tactic: have h₄ := calc
    b = (⟪a, a⟫_𝕜 / ⟪a, a⟫_𝕜) • b := by simp_all
    _ = (1 / ⟪a, a⟫_𝕜) • (⟪a, a⟫_𝕜 • b) := by simp only [smul_smul]; ring_nf
    _ = ((⟪d, b⟫_𝕜 / ⟪b, b⟫_𝕜) * (⟪c, c⟫_𝕜 / ⟪a, a⟫_𝕜)) • d := by
      simp_rw [h₂, h₃, inner_smul_right, smul_smul]; ring_nf
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (hypothesis)
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
⊢ ∃ (α : 𝕜) (β : 𝕜) (_ : α ≠ 0) (_ : 0 < β), a = α • c ∧ b = (α * β) • d
have h₅ : ⟪d, b⟫_𝕜 ≠ 0
Tactic: have h₅ : ⟪d, b⟫_𝕜 ≠ 0 := fun h ↦ by simp [h, hb] at h₄
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (hypothesis)
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
⊢ ∃ (α : 𝕜) (β : 𝕜) (_ : α ≠ 0) (_ : 0 < β), a = α • c ∧ b = (α * β) • d
have h₆ : c ≠ 0
Tactic: have h₆ : c ≠ 0 := fun h ↦ by simp [h, ha] at h₃
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
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) (_ : 0 < β), a = α • c ∧ b = (α * β) • d
have refine : 0 < HPow.hPow (α := 𝕜) (β := ℕ) (↑‖c‖ : 𝕜) 2 / HPow.hPow (α := 𝕜) (β := ℕ) (↑‖a‖ : 𝕜) 2
Tactic: refine ⟨_, ‖c‖ ^ 2 / ‖a‖ ^ 2, div_ne_zero h₅ <| by simpa, ?_, h₃, by simpa using h₄⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
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
have simp_rw : 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]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
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
have refine : ∀ (x : E) (hx : ‖x‖ = 1), Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
Tactic: refine opNorm_le_of_unit_norm hC fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
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
⊢ Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
have 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
Tactic: by_cases hTx : ‖T x‖ = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
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
⊢ Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
have 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
Tactic: by_cases hTx : ‖T x‖ = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (hypothesis)
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
⊢ Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
have 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
Tactic: specialize h x (((‖T x‖⁻¹ : ℝ) : 𝕜) • T x) hx (by simp [norm_smul, hTx])
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
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
⊢ Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
have 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
Tactic: rwa [inner_smul_right, re_ofReal_mul, ← norm_sq_eq_re_inner,
      inv_mul_eq_div, sq, mul_self_div_self] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
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
⊢ Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
have 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
Tactic: rwa [inner_smul_right, re_ofReal_mul, ← norm_sq_eq_re_inner,
      inv_mul_eq_div, sq, mul_self_div_self] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
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
⊢ Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
have 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
Tactic: rwa [inner_smul_right, re_ofReal_mul, ← norm_sq_eq_re_inner,
      inv_mul_eq_div, sq, mul_self_div_self] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
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
⊢ Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
have 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
Tactic: rwa [inner_smul_right, re_ofReal_mul, ← norm_sq_eq_re_inner,
      inv_mul_eq_div, sq, mul_self_div_self] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
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
⊢ Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
have 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
Tactic: rwa [inner_smul_right, re_ofReal_mul, ← norm_sq_eq_re_inner,
      inv_mul_eq_div, sq, mul_self_div_self] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
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
⊢ Norm.norm.{u_3} (E := F) ((T : (a : E) → F) x : F) ≤ C
have 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
Tactic: rwa [inner_smul_right, re_ofReal_mul, ← norm_sq_eq_re_inner,
      inv_mul_eq_div, sq, mul_self_div_self] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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
⊢ ⟪(↑S : ↥S.domain → E) y, (↑x : E)⟫ = ⟪(↑y : F), (↑T : ↥T.domain → F) x⟫
have rw : (starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑x : E), (↑S : ↥S.domain → E) y⟫ = ⟪(↑y : F), (↑T : ↥T.domain → F) x⟫
Tactic: rw [← inner_conj_symm, ← inner_conj_symm (y : F), h]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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⟫
⊢ ⟪(↑S : ↥S.domain → E) y, (↑x : E)⟫ = ⟪(↑y : F), (↑T : ↥T.domain → F) x⟫
have rw₁ : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑x : E), (↑S : ↥S.domain → E) y⟫ : 𝕜)
  ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑T : ↥T.domain → F) x, (↑y : F)⟫ : 𝕜)
Tactic: rw [← inner_conj_symm, ← inner_conj_symm (y : F), h]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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)⟫ : 𝕜)
⊢ ⟪(↑S : ↥S.domain → E) y, (↑x : E)⟫ = ⟪(↑y : F), (↑T : ↥T.domain → F) x⟫
have rw₂ : Eq (α := 𝕜) ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑x : E), (↑S : ↥S.domain → E) y⟫ : 𝕜)
  ((starRingEnd 𝕜 : (a : 𝕜) → 𝕜) ⟪(↑x : E), (↑S : ↥S.domain → E) y⟫ : 𝕜)
Tactic: rw [← inner_conj_symm, ← inner_conj_symm (y : F), h]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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
⊢ 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)
have 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) → 𝕜)
Tactic: rw [Set.mem_setOf_eq, LinearMap.map_add] at *
Cleared hypotheses: hx, hy
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearPMap (goal)
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
⊢ 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
have rw : Continuous.{u_2, u_1} (X := ↥T.domain) (Y := 𝕜) (⇑0 : (a : ↥T.domain) → 𝕜)
Tactic: rw [Set.mem_setOf_eq, LinearMap.map_zero, LinearMap.zero_comp]