awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
simp_rw :
  (∀ (x y : ↥U),
      ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑y : E)⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑x : E)⟫
⊢ (∀ (x y : ↥U),
      ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), y⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), x⟫
have simp_rw₁ : (∀ (x y : ↥U),
    ⟪(T : (a : E) → E) (↑x : E), (↑y : E)⟫ =
      ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) (↑y : E))⟫) ∧
  ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫
Tactic: simp_rw [U.inner_orthogonalProjection_eq_of_mem_right, Submodule.subtypeL_apply,
    U.inner_orthogonalProjection_eq_of_mem_left, ← coe_coe, hT.isSymmetric _, coe_coe,
    hT.inner_nonneg_right, implies_true, and_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
simp_rw :
  (∀ (x y : ↥U),
      ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑y : E)⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑x : E)⟫
simp_rw₁ :
  (∀ (x y : ↥U),
      ⟪(T : (a : E) → E) (↑x : E), (↑y : E)⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) (↑y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫
⊢ (∀ (x y : ↥U),
      ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), y⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), x⟫
have simp_rw₂ : (∀ (x y : ↥U), ⟪(T : (a : E) → E) (↑x : E), (↑y : E)⟫ = ⟪(↑x : E), (T : (a : E) → E) (↑y : E)⟫) ∧
  ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫
Tactic: simp_rw [U.inner_orthogonalProjection_eq_of_mem_right, Submodule.subtypeL_apply,
    U.inner_orthogonalProjection_eq_of_mem_left, ← coe_coe, hT.isSymmetric _, coe_coe,
    hT.inner_nonneg_right, implies_true, and_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
simp_rw :
  (∀ (x y : ↥U),
      ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑y : E)⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑x : E)⟫
simp_rw₁ :
  (∀ (x y : ↥U),
      ⟪(T : (a : E) → E) (↑x : E), (↑y : E)⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) (↑y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫
simp_rw₂ :
  (∀ (x y : ↥U), ⟪(T : (a : E) → E) (↑x : E), (↑y : E)⟫ = ⟪(↑x : E), (T : (a : E) → E) (↑y : E)⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫
⊢ (∀ (x y : ↥U),
      ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), y⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), x⟫
have simp_rw₃ : (∀ (x y : ↥U),
    ⟪((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑x : E), (↑y : E)⟫ = ⟪(↑x : E), ((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑y : E)⟫) ∧
  ∀ (x : ↥U), 0 ≤ ⟪((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑x : E), (↑x : E)⟫
Tactic: simp_rw [U.inner_orthogonalProjection_eq_of_mem_right, Submodule.subtypeL_apply,
    U.inner_orthogonalProjection_eq_of_mem_left, ← coe_coe, hT.isSymmetric _, coe_coe,
    hT.inner_nonneg_right, implies_true, and_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
simp_rw :
  (∀ (x y : ↥U),
      ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑y : E)⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑x : E)⟫
simp_rw₁ :
  (∀ (x y : ↥U),
      ⟪(T : (a : E) → E) (↑x : E), (↑y : E)⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) (↑y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫
simp_rw₂ :
  (∀ (x y : ↥U), ⟪(T : (a : E) → E) (↑x : E), (↑y : E)⟫ = ⟪(↑x : E), (T : (a : E) → E) (↑y : E)⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫
simp_rw₃ :
  (∀ (x y : ↥U),
      ⟪((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑x : E), (↑y : E)⟫ = ⟪(↑x : E), ((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑y : E)⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑x : E), (↑x : E)⟫
⊢ (∀ (x y : ↥U),
      ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), y⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), x⟫
have simp_rw₄ : (∀ (x y : ↥U), True) ∧ ∀ (x : ↥U), 0 ≤ ⟪(↑x : E), ((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑x : E)⟫
Tactic: simp_rw [U.inner_orthogonalProjection_eq_of_mem_right, Submodule.subtypeL_apply,
    U.inner_orthogonalProjection_eq_of_mem_left, ← coe_coe, hT.isSymmetric _, coe_coe,
    hT.inner_nonneg_right, implies_true, and_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
simp_rw :
  (∀ (x y : ↥U),
      ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑y : E)⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑x : E)⟫
simp_rw₁ :
  (∀ (x y : ↥U),
      ⟪(T : (a : E) → E) (↑x : E), (↑y : E)⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) (↑y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫
simp_rw₂ :
  (∀ (x y : ↥U), ⟪(T : (a : E) → E) (↑x : E), (↑y : E)⟫ = ⟪(↑x : E), (T : (a : E) → E) (↑y : E)⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫
simp_rw₃ :
  (∀ (x y : ↥U),
      ⟪((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑x : E), (↑y : E)⟫ = ⟪(↑x : E), ((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑y : E)⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑x : E), (↑x : E)⟫
simp_rw₄ : (∀ (x y : ↥U), True) ∧ ∀ (x : ↥U), 0 ≤ ⟪(↑x : E), ((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑x : E)⟫
⊢ (∀ (x y : ↥U),
      ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), y⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), x⟫
have simp_rw₅ : (∀ (x y : ↥U), True) ∧ ∀ (x : ↥U), 0 ≤ ⟪(↑x : E), (T : (a : E) → E) (↑x : E)⟫
Tactic: simp_rw [U.inner_orthogonalProjection_eq_of_mem_right, Submodule.subtypeL_apply,
    U.inner_orthogonalProjection_eq_of_mem_left, ← coe_coe, hT.isSymmetric _, coe_coe,
    hT.inner_nonneg_right, implies_true, and_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
simp_rw :
  (∀ (x y : ↥U),
      ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑y : E)⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑x : E)⟫
simp_rw₁ :
  (∀ (x y : ↥U),
      ⟪(T : (a : E) → E) (↑x : E), (↑y : E)⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) (↑y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫
simp_rw₂ :
  (∀ (x y : ↥U), ⟪(T : (a : E) → E) (↑x : E), (↑y : E)⟫ = ⟪(↑x : E), (T : (a : E) → E) (↑y : E)⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫
simp_rw₃ :
  (∀ (x y : ↥U),
      ⟪((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑x : E), (↑y : E)⟫ = ⟪(↑x : E), ((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑y : E)⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑x : E), (↑x : E)⟫
simp_rw₄ : (∀ (x y : ↥U), True) ∧ ∀ (x : ↥U), 0 ≤ ⟪(↑x : E), ((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑x : E)⟫
simp_rw₅ : (∀ (x y : ↥U), True) ∧ ∀ (x : ↥U), 0 ≤ ⟪(↑x : E), (T : (a : E) → E) (↑x : E)⟫
⊢ (∀ (x y : ↥U),
      ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), y⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), x⟫
have simp_rw₆ : (∀ (x y : ↥U), True) ∧ ∀ (y : ↥U), True
Tactic: simp_rw [U.inner_orthogonalProjection_eq_of_mem_right, Submodule.subtypeL_apply,
    U.inner_orthogonalProjection_eq_of_mem_left, ← coe_coe, hT.isSymmetric _, coe_coe,
    hT.inner_nonneg_right, implies_true, and_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E →L[𝕜] E
hT : T.IsPositive
U : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
simp_rw :
  (∀ (x y : ↥U),
      ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑y : E)⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E), (↑x : E)⟫
simp_rw₁ :
  (∀ (x y : ↥U),
      ⟪(T : (a : E) → E) (↑x : E), (↑y : E)⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) (↑y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫
simp_rw₂ :
  (∀ (x y : ↥U), ⟪(T : (a : E) → E) (↑x : E), (↑y : E)⟫ = ⟪(↑x : E), (T : (a : E) → E) (↑y : E)⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(T : (a : E) → E) (↑x : E), (↑x : E)⟫
simp_rw₃ :
  (∀ (x y : ↥U),
      ⟪((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑x : E), (↑y : E)⟫ = ⟪(↑x : E), ((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑y : E)⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑x : E), (↑x : E)⟫
simp_rw₄ : (∀ (x y : ↥U), True) ∧ ∀ (x : ↥U), 0 ≤ ⟪(↑x : E), ((↑T : E →ₗ[𝕜] E) : (a : E) → E) (↑x : E)⟫
simp_rw₅ : (∀ (x y : ↥U), True) ∧ ∀ (x : ↥U), 0 ≤ ⟪(↑x : E), (T : (a : E) → E) (↑x : E)⟫
simp_rw₆ : (∀ (x y : ↥U), True) ∧ ∀ (y : ↥U), True
⊢ (∀ (x y : ↥U),
      ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), y⟫ =
        ⟪x, (U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) y : E))⟫) ∧
    ∀ (x : ↥U), 0 ≤ ⟪(U.orthogonalProjection : (a : E) → ↥U) ((T : (a : E) → E) ((U.subtypeL : (a : ↥U) → E) x : E)), x⟫
have simp_rw₇ : True ∧ True
Tactic: simp_rw [U.inner_orthogonalProjection_eq_of_mem_right, Submodule.subtypeL_apply,
    U.inner_orthogonalProjection_eq_of_mem_left, ← coe_coe, hT.isSymmetric _, coe_coe,
    hT.inner_nonneg_right, implies_true, and_self]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_4
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
h : ∀ (x : H), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖
⊢ AntilipschitzWith (α := H) (β := H) c⁻¹ (⇑f : (a : H) → H)
have refine : ∀ (x : H), ‖x‖ ≤ (↑c⁻¹ : ℝ) * norm (E := H) ((f : (a : H) → H) x : H)
Tactic: refine f.antilipschitz_of_bound (K := c⁻¹) fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_4
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
h : ∀ (x : H), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖
x : H
⊢ ‖x‖ ≤ (↑c⁻¹ : ℝ) * norm (E := H) ((f : (a : H) → H) x : H)
have rw : ‖x‖ * (↑c : ℝ) ≤ norm (E := H) ((f : (a : H) → H) x : H)
Tactic: rw [NNReal.coe_inv, inv_mul_eq_div, le_div_iff₀ (by exact_mod_cast hc)]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (hypothesis)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_4
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
h : ∀ (x : H), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖
x : H
⊢ ‖x‖ * (↑c : ℝ) ≤ norm (E := H) ((f : (a : H) → H) x : H)
have h₁ : ∀ (x : H), ‖x‖ * (‖x‖ * (↑c : ℝ)) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖
Tactic: simp_rw [sq, mul_assoc] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_4
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * (↑c : ℝ)) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖
⊢ ‖x‖ * (↑c : ℝ) ≤ norm (E := H) ((f : (a : H) → H) x : H)
have pos : ∀ (hx0 : x = 0), ‖x‖ * (↑c : ℝ) ≤ norm (E := H) ((f : (a : H) → H) x : H)
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_4
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * (↑c : ℝ)) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖
pos : ∀ (hx0 : x = 0), ‖x‖ * (↑c : ℝ) ≤ norm (E := H) ((f : (a : H) → H) x : H)
⊢ ‖x‖ * (↑c : ℝ) ≤ norm (E := H) ((f : (a : H) → H) x : H)
have neg : ∀ (hx0 : ¬x = 0), ‖x‖ * (↑c : ℝ) ≤ norm (E := H) ((f : (a : H) → H) x : H)
Tactic: by_cases hx0 : x = 0
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
inst : RCLike 𝕜
H : Type u_4
inst_1 : NormedAddCommGroup H
inst_2 : InnerProductSpace 𝕜 H
f : H →L[𝕜] H
c : ℝ≥0
hc : 0 < c
x : H
h : ∀ (x : H), ‖x‖ * (‖x‖ * (↑c : ℝ)) ≤ ‖⟪(f : (a : H) → H) x, x⟫‖
hx0 : ¬x = 0
⊢ ‖x‖ * (↑c : ℝ) ≤ norm (E := H) ((f : (a : H) → H) x : H)
have neg : LE.le (α := ℝ) ((OrderIso.mulLeft₀ ‖x‖ sorry : (a : ℝ) → ℝ) (‖x‖ * (↑c : ℝ)) : ℝ)
  ((OrderIso.mulLeft₀ ‖x‖ sorry : (a : ℝ) → ℝ) (norm (E := H) ((f : (a : H) → H) x : H)) : ℝ)
Tactic: apply (map_le_map_iff <| OrderIso.mulLeft₀ ‖x‖ (norm_pos_iff.mpr hx0)).mp
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : E) → E) x, x⟫‖
⊢ IsUnit f
have rw : (↑f : E →ₗ[𝕜] E).range.topologicalClosure = ⊤ ∧ ∃ (c : ℝ≥0), AntilipschitzWith (α := E) (β := E) c (⇑f : (a : E) → E)
Tactic: rw [isUnit_iff_bijective, bijective_iff_dense_range_and_antilipschitz]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : E) → E) x, x⟫‖
⊢ (↑f : E →ₗ[𝕜] E).range.topologicalClosure = ⊤ ∧ ∃ (c : ℝ≥0), AntilipschitzWith (α := E) (β := E) c (⇑f : (a : E) → E)
have h_anti : AntilipschitzWith (α := E) (β := E) c⁻¹ (⇑f : (a : E) → E)
Tactic: have h_anti : AntilipschitzWith c⁻¹ f := antilipschitz_of_forall_le_inner_map f hc h
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : E) → E) x, x⟫‖
h_anti : AntilipschitzWith (α := E) (β := E) c⁻¹ (⇑f : (a : E) → E)
⊢ (↑f : E →ₗ[𝕜] E).range.topologicalClosure = ⊤ ∧ ∃ (c : ℝ≥0), AntilipschitzWith (α := E) (β := E) c (⇑f : (a : E) → E)
have refine : (↑f : E →ₗ[𝕜] E).range.topologicalClosure = ⊤
Tactic: refine ⟨?_, ⟨_, h_anti⟩⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : E) → E) x, x⟫‖
h_anti : AntilipschitzWith (α := E) (β := E) c⁻¹ (⇑f : (a : E) → E)
⊢ (↑f : E →ₗ[𝕜] E).range.topologicalClosure = ⊤
have rw : ∀ x ∈ (↑f : E →ₗ[𝕜] E).rangeᗮ, x = 0
Tactic: rw [Submodule.topologicalClosure_eq_top_iff, Submodule.eq_bot_iff]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
f : E →L[𝕜] E
c : ℝ≥0
hc : 0 < c
h : ∀ (x : E), HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) ≤ ‖⟪(f : (a : E) → E) x, x⟫‖
h_anti : AntilipschitzWith (α := E) (β := E) c⁻¹ (⇑f : (a : E) → E)
x : E
hx : x ∈ (↑f : E →ₗ[𝕜] E).rangeᗮ
⊢ x = 0
have this : HPow.hPow (β := ℕ) ‖x‖ 2 * (↑c : ℝ) = 0
Tactic: have : ‖x‖ ^ 2 * c = 0 := le_antisymm (by simpa only [hx (f x) ⟨x, rfl⟩, norm_zero] using h x)
    (by positivity)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
⊢ p.IsPositive ↔ IsSelfAdjoint p
have rw : IsSymmetric.{u_1, u_2} (𝕜 := 𝕜) (E := E) (↑p : E →ₗ[𝕜] E) ↔ IsSelfAdjoint p
Tactic: rw [← isPositive_toLinearMap_iff, IsIdempotentElem.isPositive_iff_isSymmetric hp.toLinearMap]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
⊢ [(↑p : E →ₗ[𝕜] E).rangeᗮ = (↑p : E →ₗ[𝕜] E).ker, IsStarNormal p, IsSelfAdjoint p, p.IsPositive].TFAE
have tfae_2_iff_3 : IsStarNormal p ↔ IsSelfAdjoint p
Tactic: tfae_have 2 ↔ 3 := hp.isSelfAdjoint_iff_isStarNormal.symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
tfae_2_iff_3 : IsStarNormal p ↔ IsSelfAdjoint p
⊢ [(↑p : E →ₗ[𝕜] E).rangeᗮ = (↑p : E →ₗ[𝕜] E).ker, IsStarNormal p, IsSelfAdjoint p, p.IsPositive].TFAE
have tfae_3_iff_4 : IsSelfAdjoint p ↔ p.IsPositive
Tactic: tfae_have 3 ↔ 4 := hp.isPositive_iff_isSelfAdjoint.symm
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : CompleteSpace E
p : E →L[𝕜] E
hp : IsIdempotentElem p
tfae_2_iff_3 : IsStarNormal p ↔ IsSelfAdjoint p
tfae_3_iff_4 : IsSelfAdjoint p ↔ p.IsPositive
⊢ [(↑p : E →ₗ[𝕜] E).rangeᗮ = (↑p : E →ₗ[𝕜] E).ker, IsStarNormal p, IsSelfAdjoint p, p.IsPositive].TFAE
have tfae_3_iff_1 : IsSelfAdjoint p ↔ (↑p : E →ₗ[𝕜] E).rangeᗮ = (↑p : E →ₗ[𝕜] E).ker
Tactic: tfae_have 3 ↔ 1 := p.isSelfAdjoint_iff_isSymmetric.eq ▸
    (LinearMap.IsIdempotentElem.isSymmetric_iff_orthogonal_range hp.toLinearMap)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
inst_4 : V.HasOrthogonalProjection
⊢ U.starProjection ≤ V.starProjection ↔ U ≤ V
have simp_rw : (↑U.starProjection : E →ₗ[𝕜] E) ≤ (↑V.starProjection : E →ₗ[𝕜] E) ↔ U ≤ V
Tactic: simp_rw [← coe_le_coe_iff, isSymmetricProjection_starProjection _
      |>.le_iff_range_le_range <| isSymmetricProjection_starProjection _,
    toLinearMap_starProjection_eq_isComplProjection, range_projection]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
inst_4 : V.HasOrthogonalProjection
simp_rw : (↑U.starProjection : E →ₗ[𝕜] E) ≤ (↑V.starProjection : E →ₗ[𝕜] E) ↔ U ≤ V
⊢ U.starProjection ≤ V.starProjection ↔ U ≤ V
have simp_rw₁ : (↑U.starProjection : E →ₗ[𝕜] E).range ≤ (↑V.starProjection : E →ₗ[𝕜] E).range ↔ U ≤ V
Tactic: simp_rw [← coe_le_coe_iff, isSymmetricProjection_starProjection _
      |>.le_iff_range_le_range <| isSymmetricProjection_starProjection _,
    toLinearMap_starProjection_eq_isComplProjection, range_projection]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
U V : Submodule 𝕜 E
inst_3 : U.HasOrthogonalProjection
inst_4 : V.HasOrthogonalProjection
simp_rw : (↑U.starProjection : E →ₗ[𝕜] E) ≤ (↑V.starProjection : E →ₗ[𝕜] E) ↔ U ≤ V
simp_rw₁ : (↑U.starProjection : E →ₗ[𝕜] E).range ≤ (↑V.starProjection : E →ₗ[𝕜] E).range ↔ U ≤ V
⊢ U.starProjection ≤ V.starProjection ↔ U ≤ V
have simp_rw₂ : (U.projection Uᗮ sorry).range ≤ (V.projection Vᗮ sorry).range ↔ U ≤ V
Tactic: simp_rw [← coe_le_coe_iff, isSymmetricProjection_starProjection _
      |>.le_iff_range_le_range <| isSymmetricProjection_starProjection _,
    toLinearMap_starProjection_eq_isComplProjection, range_projection]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E ≃ₗ[𝕜] E
hT : (↑T : E →ₗ[𝕜] E).IsPositive
⊢ (↑T.symm : E →ₗ[𝕜] E).IsPositive
have refine : ∀ (x : E), LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) x, x⟫ : ℝ)
Tactic: refine ⟨hT.isSymmetric.toLinearMap_symm, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (hypothesis)
Goal:
𝕜 : Type u_1
E : Type u_2
inst : RCLike 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
T : E ≃ₗ[𝕜] E
hT : (↑T : E →ₗ[𝕜] E).IsPositive
x : E
⊢ LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪((↑T.symm : E →ₗ[𝕜] E) : (a : E) → E) x, x⟫ : ℝ)
have this : LE.le (α := ℝ) (0 : ℝ) ((re : (a : 𝕜) → ℝ) ⟪x, (T.symm : (a : E) → E) x⟫ : ℝ)
Tactic: have := by simpa using hT.2 (T.symm.toLinearMap x)