awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
E' : Type u_4
inst_3 : SeminormedAddCommGroup E'
inst_4 : InnerProductSpace 𝕜 E'
f : E →L[𝕜] E'
v : E'
x : E
h₁ : Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E') ≤ ‖f‖ * ‖x‖
h₂ : ‖⟪v, (f : (a : E) → E') x⟫‖ ≤ ‖v‖ * Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E')
f₁ : ‖v‖ * Norm.norm.{u_4} (E := E') ((f : (a : E) → E') x : E') ≤ ‖v‖ * (‖f‖ * ‖x‖)
⊢ Norm.norm.{u_1} (E := 𝕜)
      ((((((toSesqForm : (a : E →L[𝕜] E') → E' →L⋆[𝕜] E →L[𝕜] 𝕜) f : E' →L⋆[𝕜] E →L[𝕜] 𝕜) : (a : E') → E →L[𝕜] 𝕜) v :
              E →L[𝕜] 𝕜) :
            (a : E) → 𝕜)
          x :
        𝕜) ≤
    ‖f‖ * ‖v‖ * ‖x‖
have f₂ : ‖v‖ * (‖f‖ * ‖x‖) = ‖f‖ * ‖v‖ * ‖x‖
Tactic: calc
    ‖⟪v, f x⟫‖ ≤ ‖v‖ * ‖f x‖ := h₂
    _ ≤ ‖v‖ * (‖f‖ * ‖x‖) := by gcongr
    _ = ‖f‖ * ‖v‖ * ‖x‖ := by ring
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) = ‖x‖
have le_antisymm : ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜)
Tactic: refine
    le_antisymm ((innerSL 𝕜 x).opNorm_le_bound (norm_nonneg _) fun y => norm_inner_le_norm _ _) ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
⊢ ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜)
have inl : ∀ (h : ‖x‖ = 0), ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜)
Tactic: rcases (norm_nonneg x).eq_or_lt' with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
inl : ∀ (h : ‖x‖ = 0), ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜)
⊢ ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜)
have inr : ∀ (h : 0 < ‖x‖), ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜)
Tactic: rcases (norm_nonneg x).eq_or_lt' with (h | h)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
⊢ ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜)
have inr : ‖x‖ * ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) * ‖x‖
Tactic: refine (mul_le_mul_iff_left₀ h).mp ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
⊢ ‖x‖ * ‖x‖ = ‖⟪x, x⟫‖
have rw : HPow.hPow (β := ℕ) ‖x‖ 2 = ‖⟪x, x⟫‖
Tactic: rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow, norm_ofReal, abs_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
rw : HPow.hPow (β := ℕ) ‖x‖ 2 = ‖⟪x, x⟫‖
⊢ ‖x‖ * ‖x‖ = ‖⟪x, x⟫‖
have rw₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = ‖HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2‖
Tactic: rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow, norm_ofReal, abs_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
rw : HPow.hPow (β := ℕ) ‖x‖ 2 = ‖⟪x, x⟫‖
rw₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = ‖HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2‖
⊢ ‖x‖ * ‖x‖ = ‖⟪x, x⟫‖
have rw₂ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) (Norm.norm.{u_1} (E := 𝕜) (↑‖x‖ : 𝕜)) 2
Tactic: rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow, norm_ofReal, abs_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
rw : HPow.hPow (β := ℕ) ‖x‖ 2 = ‖⟪x, x⟫‖
rw₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = ‖HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2‖
rw₂ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) (Norm.norm.{u_1} (E := 𝕜) (↑‖x‖ : 𝕜)) 2
⊢ ‖x‖ * ‖x‖ = ‖⟪x, x⟫‖
have rw₃ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) |‖x‖| 2
Tactic: rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow, norm_ofReal, abs_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
rw : HPow.hPow (β := ℕ) ‖x‖ 2 = ‖⟪x, x⟫‖
rw₁ : HPow.hPow (β := ℕ) ‖x‖ 2 = ‖HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2‖
rw₂ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) (Norm.norm.{u_1} (E := 𝕜) (↑‖x‖ : 𝕜)) 2
rw₃ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) |‖x‖| 2
⊢ ‖x‖ * ‖x‖ = ‖⟪x, x⟫‖
have rw₄ : HPow.hPow (β := ℕ) ‖x‖ 2 = HPow.hPow (β := ℕ) ‖x‖ 2
Tactic: rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow, norm_ofReal, abs_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
x : E
h : 0 < ‖x‖
⊢ ‖x‖ * ‖x‖ ≤ Norm.norm (E := E →L[𝕜] 𝕜) ((innerSL 𝕜 : (a : E) → E →L[𝕜] 𝕜) x : E →L[𝕜] 𝕜) * ‖x‖
have rw : ‖x‖ * ‖x‖ = ‖⟪x, x⟫‖
Tactic: calc
      ‖x‖ * ‖x‖ = ‖(⟪x, x⟫ : 𝕜)‖ := by
        rw [← sq, inner_self_eq_norm_sq_to_K, norm_pow, norm_ofReal, abs_norm]
      _ ≤ ‖innerSL 𝕜 x‖ * ‖x‖ := (innerSL 𝕜 x).le_opNorm _
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
G : Type u_4
inst : SeminormedAddCommGroup G
inst_1 : InnerProductSpace ℝ G
f : G ≃ₗᵢ[ℝ] ℂ
x y : G
⊢ ⟪x, y⟫_ℝ =
    (HMul.hMul (α := ℂ) (β := ℂ) ((f : (a : G) → ℂ) y : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : G) → ℂ) x : ℂ) : ℂ)).re
have rw : ⟪x, y⟫_ℝ = inner ℝ (E := ℂ) ((f : (a : G) → ℂ) x : ℂ) ((f : (a : G) → ℂ) y : ℂ)
Tactic: rw [← Complex.inner, f.inner_map_map]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
G : Type u_4
inst : SeminormedAddCommGroup G
inst_1 : InnerProductSpace ℝ G
f : G ≃ₗᵢ[ℝ] ℂ
x y : G
rw : ⟪x, y⟫_ℝ = inner ℝ (E := ℂ) ((f : (a : G) → ℂ) x : ℂ) ((f : (a : G) → ℂ) y : ℂ)
⊢ ⟪x, y⟫_ℝ =
    (HMul.hMul (α := ℂ) (β := ℂ) ((f : (a : G) → ℂ) y : ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((f : (a : G) → ℂ) x : ℂ) : ℂ)).re
have rw₁ : ⟪x, y⟫_ℝ = ⟪x, y⟫_ℝ
Tactic: rw [← Complex.inner, f.inner_map_map]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y : F
⊢ Norm.norm (E := F →L[𝕜] E)
      ((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y : F →L[𝕜] E) =
    ‖x‖ * ‖y‖
have rw : Norm.norm (E := F →L[𝕜] E) (smulRight (S := 𝕜) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y) x) = ‖x‖ * ‖y‖
Tactic: rw [rankOne_def, norm_smulRight_apply, innerSL_apply_norm, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y : F
rw : Norm.norm (E := F →L[𝕜] E) (smulRight (S := 𝕜) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y) x) = ‖x‖ * ‖y‖
⊢ Norm.norm (E := F →L[𝕜] E)
      ((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y : F →L[𝕜] E) =
    ‖x‖ * ‖y‖
have rw₁ : Norm.norm (E := StrongDual 𝕜 F) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y : F →L[𝕜] 𝕜) * ‖x‖ = ‖x‖ * ‖y‖
Tactic: rw [rankOne_def, norm_smulRight_apply, innerSL_apply_norm, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y : F
rw : Norm.norm (E := F →L[𝕜] E) (smulRight (S := 𝕜) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y) x) = ‖x‖ * ‖y‖
rw₁ : Norm.norm (E := StrongDual 𝕜 F) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y : F →L[𝕜] 𝕜) * ‖x‖ = ‖x‖ * ‖y‖
⊢ Norm.norm (E := F →L[𝕜] E)
      ((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y : F →L[𝕜] E) =
    ‖x‖ * ‖y‖
have rw₂ : ‖y‖ * ‖x‖ = ‖x‖ * ‖y‖
Tactic: rw [rankOne_def, norm_smulRight_apply, innerSL_apply_norm, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
x : E
y : F
rw : Norm.norm (E := F →L[𝕜] E) (smulRight (S := 𝕜) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y) x) = ‖x‖ * ‖y‖
rw₁ : Norm.norm (E := StrongDual 𝕜 F) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y : F →L[𝕜] 𝕜) * ‖x‖ = ‖x‖ * ‖y‖
rw₂ : ‖y‖ * ‖x‖ = ‖x‖ * ‖y‖
⊢ Norm.norm (E := F →L[𝕜] E)
      ((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y : F →L[𝕜] E) =
    ‖x‖ * ‖y‖
have rw₃ : ‖x‖ * ‖y‖ = ‖x‖ * ‖y‖
Tactic: rw [rankOne_def, norm_smulRight_apply, innerSL_apply_norm, mul_comm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
G : Type u_8
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
y : F
f : E →L[𝕜] G
⊢ Eq (α := F →L[𝕜] G)
    (f.comp (σ₁₂ := RingHom.id 𝕜)
      ((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y))
    ((((rankOne 𝕜 : (a : G) → F →L⋆[𝕜] F →L[𝕜] G) ((f : (a : E) → G) x) : F →L⋆[𝕜] F →L[𝕜] G) : (a : F) → F →L[𝕜] G) y)
have simp_rw : Eq (α := F →L[𝕜] G) (f ∘SL comp (σ₁₂ := RingHom.id 𝕜) (toSpanSingleton 𝕜 x) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y))
  (comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := 𝕜) (toSpanSingleton 𝕜 ((f : (a : E) → G) x))
    ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y))
Tactic: simp_rw [rankOne_def', ← comp_assoc, comp_toSpanSingleton]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_4
E : Type u_5
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : SeminormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
G : Type u_8
inst_5 : SeminormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
x : E
y : F
f : E →L[𝕜] G
simp_rw :
  Eq (α := F →L[𝕜] G) (f ∘SL comp (σ₁₂ := RingHom.id 𝕜) (toSpanSingleton 𝕜 x) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y))
    (comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := 𝕜) (toSpanSingleton 𝕜 ((f : (a : E) → G) x))
      ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y))
⊢ Eq (α := F →L[𝕜] G)
    (f.comp (σ₁₂ := RingHom.id 𝕜)
      ((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y))
    ((((rankOne 𝕜 : (a : G) → F →L⋆[𝕜] F →L[𝕜] G) ((f : (a : E) → G) x) : F →L⋆[𝕜] F →L[𝕜] G) : (a : F) → F →L[𝕜] G) y)
have simp_rw₁ : Eq (α := F →L[𝕜] G) (comp (σ₁₂ := RingHom.id 𝕜) (f ∘SL toSpanSingleton 𝕜 x) ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y))
  (comp (R₂ := 𝕜) (σ₁₂ := RingHom.id 𝕜) (σ₂₃ := RingHom.id 𝕜) (M₂ := 𝕜) (toSpanSingleton 𝕜 ((f : (a : E) → G) x))
    ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) y))
Tactic: simp_rw [rankOne_def', ← comp_assoc, comp_toSpanSingleton]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_4
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
⊢ Eq (α := 𝕜 →L[𝕜] F) ((((rankOne 𝕜 : (a : F) → 𝕜 →L⋆[𝕜] 𝕜 →L[𝕜] F) x : 𝕜 →L⋆[𝕜] 𝕜 →L[𝕜] F) : (a : 𝕜) → 𝕜 →L[𝕜] F) 1)
    (toSpanSingleton 𝕜 x)
have h : Eq.{u_6 + 1} (α := F)
  (((((rankOne 𝕜 : (a : F) → 𝕜 →L⋆[𝕜] 𝕜 →L[𝕜] F) x : 𝕜 →L⋆[𝕜] 𝕜 →L[𝕜] F) : (a : 𝕜) → 𝕜 →L[𝕜] F) 1 : (a : 𝕜) → F) 1 : F)
  ((toSpanSingleton 𝕜 x : (a : 𝕜) → F) 1 : F)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_4
F : Type u_6
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
⊢ Eq (α := F →L[𝕜] 𝕜) (((rankOne 𝕜 : (a : 𝕜) → F →L⋆[𝕜] F →L[𝕜] 𝕜) 1 : (a : F) → F →L[𝕜] 𝕜) x : F →L[𝕜] 𝕜)
    ((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) x : F →L[𝕜] 𝕜)
have h : ∀ (x_1 : F),
  Eq.{u_4 + 1} (α := 𝕜)
    (((((rankOne 𝕜 : (a : 𝕜) → F →L⋆[𝕜] F →L[𝕜] 𝕜) 1 : (a : F) → F →L[𝕜] 𝕜) x : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x_1 : 𝕜)
    ((((innerSL 𝕜 : (a : F) → F →L[𝕜] 𝕜) x : F →L[𝕜] 𝕜) : (a : F) → 𝕜) x_1 : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
⊢ IsIdempotentElem (M := F →L[𝕜] F)
      ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) ↔
    ‖x‖ = 1
have refine : IsIdempotentElem (M := F →L[𝕜] F)
    ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) →
  ‖x‖ = 1
Tactic: refine ⟨?_, isIdempotentElem_rankOne_self⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
⊢ IsIdempotentElem (M := F →L[𝕜] F)
      ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) →
    ‖x‖ = 1
have simp : HSMul.hSMul (β := F →L[𝕜] F) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2)
      ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) =
    (((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x →
  ‖x‖ = 1
Tactic: simp only [IsIdempotentElem, mul_def, comp_rankOne, rankOne_apply, inner_self_eq_norm_sq_to_K,
    map_smul, coe_smul', Pi.smul_apply]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
⊢ HSMul.hSMul (β := F →L[𝕜] F) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2)
        ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) =
      (((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x →
    ‖x‖ = 1
have nth_rw : HSMul.hSMul (β := F →L[𝕜] F) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2)
      ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) =
    HSMul.hSMul.{u_4, u_8, u_8} (α := 𝕜) (β := F →L[𝕜] F) 1
      ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) →
  ‖x‖ = 1
Tactic: nth_rw 2 [← one_smul 𝕜 (rankOne 𝕜 x x)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
⊢ HSMul.hSMul (β := F →L[𝕜] F) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2)
        ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) =
      HSMul.hSMul.{u_4, u_8, u_8} (α := 𝕜) (β := F →L[𝕜] F) 1
        ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) →
    ‖x‖ = 1
have rw : HSMul.hSMul (β := F →L[𝕜] F) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2 - 1)
      ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) =
    0 →
  ‖x‖ = 1
Tactic: rw [← sub_eq_zero, ← sub_smul]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.LinearMap (goal)
Goal:
𝕜 : Type u_4
inst : RCLike 𝕜
F : Type u_8
inst_1 : NormedAddCommGroup F
inst_2 : InnerProductSpace 𝕜 F
x : F
hx : x ≠ 0
⊢ HSMul.hSMul (β := F →L[𝕜] F) (HPow.hPow (α := 𝕜) (β := ℕ) (↑‖x‖ : 𝕜) 2 - 1)
        ((((rankOne 𝕜 : (a : F) → F →L⋆[𝕜] F →L[𝕜] F) x : F →L⋆[𝕜] F →L[𝕜] F) : (a : F) → F →L[𝕜] F) x : F →L[𝕜] F) =
      0 →
    ‖x‖ = 1
have simp : ‖x‖ = 1 ∨ ‖x‖ = -1 → ‖x‖ = 1
Tactic: simp only [smul_eq_zero, rankOne_eq_zero, hx, or_self, or_false, sub_eq_zero, sq_eq_one_iff,
    FaithfulSMul.algebraMap_eq_one_iff, ← show ((-(1 : ℝ) : ℝ) : 𝕜) = -1 by grind, ofReal_inj]
-- 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
⊢ Eq (α := H →L[𝕜] F)
      ((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) a : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) b : H →L[𝕜] F)
      ((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) c : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) d : H →L[𝕜] F) ↔
    Eq (α := F →L[𝕜] H)
      ((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) b : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) a : F →L[𝕜] H)
      ((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) d : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) c : F →L[𝕜] H)
have simp_rw : (∀ (x : H) (v : F),
    ⟪v,
        (((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) a : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) b : H →L[𝕜] F) :
            (a : H) → F)
          x⟫_𝕜 =
      ⟪v,
        (((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) c : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) d : H →L[𝕜] F) :
            (a : H) → F)
          x⟫_𝕜) ↔
  ∀ (x : F) (v : H),
    ⟪(((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) b : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) a : F →L[𝕜] H) :
            (a : F) → H)
          x,
        v⟫_𝕜 =
      ⟪(((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) d : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) c : F →L[𝕜] H) :
            (a : F) → H)
          x,
        v⟫_𝕜
Tactic: simp_rw [ContinuousLinearMap.ext_iff, ext_iff_inner_left 𝕜 (E := F),
    ext_iff_inner_right 𝕜 (E := 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
⊢ (∀ (x : H) (v : F),
      ⟪v,
          (((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) a : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) b : H →L[𝕜] F) :
              (a : H) → F)
            x⟫_𝕜 =
        ⟪v,
          (((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) c : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) d : H →L[𝕜] F) :
              (a : H) → F)
            x⟫_𝕜) ↔
    ∀ (x : F) (v : H),
      ⟪(((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) b : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) a : F →L[𝕜] H) :
              (a : F) → H)
            x,
          v⟫_𝕜 =
        ⟪(((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) d : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) c : F →L[𝕜] H) :
              (a : F) → H)
            x,
          v⟫_𝕜
have rw : (∀ (b_1 : F) (a_1 : H),
    ⟪b_1,
        (((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) a : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) b : H →L[𝕜] F) :
            (a : H) → F)
          a_1⟫_𝕜 =
      ⟪b_1,
        (((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) c : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) d : H →L[𝕜] F) :
            (a : H) → F)
          a_1⟫_𝕜) ↔
  ∀ (x : F) (v : H),
    ⟪(((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) b : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) a : F →L[𝕜] H) :
            (a : F) → H)
          x,
        v⟫_𝕜 =
      ⟪(((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) d : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) c : F →L[𝕜] H) :
            (a : F) → H)
          x,
        v⟫_𝕜
Tactic: rw [forall_comm]
-- 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 :
  Eq (α := H →L[𝕜] F)
    ((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) a : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) b : H →L[𝕜] F)
    ((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) c : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) d : H →L[𝕜] F)
⊢ ∃ (α : 𝕜) (β : 𝕜) (_ : α ≠ 0) (_ : 0 < β), a = α • c ∧ b = (α * β) • d
have h₂ : Eq (α := F →L[𝕜] H)
  ((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) b : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) a : F →L[𝕜] H)
  ((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) d : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) c : F →L[𝕜] H)
Tactic: have h₂ := rankOne_eq_rankOne_iff_comm.mp 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 :
  Eq (α := H →L[𝕜] F)
    ((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) a : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) b : H →L[𝕜] F)
    ((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) c : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) d : H →L[𝕜] F)
h₂ :
  Eq (α := F →L[𝕜] H)
    ((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) b : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) a : F →L[𝕜] H)
    ((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) d : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) c : F →L[𝕜] H)
⊢ ∃ (α : 𝕜) (β : 𝕜) (_ : α ≠ 0) (_ : 0 < β), a = α • c ∧ b = (α * β) • d
have h₁ : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
Tactic: simp only [ContinuousLinearMap.ext_iff, rankOne_apply] at h h₂
Cleared hypotheses: h, 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 :
  Eq (α := H →L[𝕜] F)
    ((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) a : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) b : H →L[𝕜] F)
    ((((rankOne 𝕜 : (a : F) → H →L⋆[𝕜] H →L[𝕜] F) c : H →L⋆[𝕜] H →L[𝕜] F) : (a : H) → H →L[𝕜] F) d : H →L[𝕜] F)
h₂ :
  Eq (α := F →L[𝕜] H)
    ((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) b : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) a : F →L[𝕜] H)
    ((((rankOne 𝕜 : (a : H) → F →L⋆[𝕜] F →L[𝕜] H) d : F →L⋆[𝕜] F →L[𝕜] H) : (a : F) → F →L[𝕜] H) c : F →L[𝕜] H)
h₁ : ∀ (x : H), ⟪b, x⟫_𝕜 • a = ⟪d, x⟫_𝕜 • c
⊢ ∃ (α : 𝕜) (β : 𝕜) (_ : α ≠ 0) (_ : 0 < β), a = α • c ∧ b = (α * β) • d
have h₃ : ∀ (x : F), ⟪a, x⟫_𝕜 • b = ⟪c, x⟫_𝕜 • d
Tactic: simp only [ContinuousLinearMap.ext_iff, rankOne_apply] at h h₂
Cleared hypotheses: h, 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
⊢ (⟪b, b⟫_𝕜 / ⟪b, b⟫_𝕜) • a = (1 / ⟪b, b⟫_𝕜) • ⟪b, b⟫_𝕜 • a
have simp : (⟪b, b⟫_𝕜 / ⟪b, b⟫_𝕜) • a = (1 / ⟪b, b⟫_𝕜 * ⟪b, b⟫_𝕜) • a
Tactic: simp only [smul_smul]