awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E_1 : Type u_4
inst_1 : NormedAddCommGroup E_1
inst_2 : InnerProductSpace 𝕜 E_1
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this_1 : CompleteSpace.{u_7} ↥S
this : CompleteSpace V
p1 : V →ₗ[𝕜] ↥S := (↑S.orthogonalProjection : V →ₗ[𝕜] ↥S)
p2 : V →ₗ[𝕜] ↥Sᗮ := (↑Sᗮ.orthogonalProjection : V →ₗ[𝕜] ↥Sᗮ)
M : V →ₗ[𝕜] V := L.toLinearMap ∘ₗ p1 + L3.toLinearMap ∘ₗ p2
x : V
Mx_decomp :
  (M : (a : V) → V) x =
    HAdd.hAdd (α := V) (β := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
      ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)
⊢ inner 𝕜 (E := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
      ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V) =
    0
have Lp1x : Membership.mem (α := V) L.range ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
Tactic: have Lp1x : L (p1 x) ∈ LinearMap.range L.toLinearMap :=
        LinearMap.mem_range_self L.toLinearMap (p1 x)
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E_1 : Type u_4
inst_1 : NormedAddCommGroup E_1
inst_2 : InnerProductSpace 𝕜 E_1
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this_1 : CompleteSpace.{u_7} ↥S
this : CompleteSpace V
p1 : V →ₗ[𝕜] ↥S := (↑S.orthogonalProjection : V →ₗ[𝕜] ↥S)
p2 : V →ₗ[𝕜] ↥Sᗮ := (↑Sᗮ.orthogonalProjection : V →ₗ[𝕜] ↥Sᗮ)
M : V →ₗ[𝕜] V := L.toLinearMap ∘ₗ p1 + L3.toLinearMap ∘ₗ p2
x : V
Mx_decomp :
  (M : (a : V) → V) x =
    HAdd.hAdd (α := V) (β := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
      ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)
Lp1x : Membership.mem (α := V) L.range ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
⊢ Membership.mem (α := V) L.rangeᗮ ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)
have simp : Membership.mem (α := V) L.rangeᗮ.subtype.range ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)
Tactic: simp only [LS,
          ← Submodule.range_subtype LSᗮ]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E_1 : Type u_4
inst_1 : NormedAddCommGroup E_1
inst_2 : InnerProductSpace 𝕜 E_1
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this_1 : CompleteSpace.{u_7} ↥S
this : CompleteSpace V
p1 : V →ₗ[𝕜] ↥S := (↑S.orthogonalProjection : V →ₗ[𝕜] ↥S)
p2 : V →ₗ[𝕜] ↥Sᗮ := (↑Sᗮ.orthogonalProjection : V →ₗ[𝕜] ↥Sᗮ)
M : V →ₗ[𝕜] V := L.toLinearMap ∘ₗ p1 + L3.toLinearMap ∘ₗ p2
x : V
Mx_decomp :
  (M : (a : V) → V) x =
    HAdd.hAdd (α := V) (β := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
      ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)
Lp1x : Membership.mem (α := V) L.range ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
⊢ inner 𝕜 (E := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
      ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V) =
    0
have Lp2x : Membership.mem (α := V) L.rangeᗮ ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)
Tactic: have Lp2x : L3 (p2 x) ∈ (LinearMap.range L.toLinearMap)ᗮ := by
        simp only [LS,
          ← Submodule.range_subtype LSᗮ]
        apply LinearMap.mem_range_self
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E_1 : Type u_4
inst_1 : NormedAddCommGroup E_1
inst_2 : InnerProductSpace 𝕜 E_1
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this_1 : CompleteSpace.{u_7} ↥S
this : CompleteSpace V
p1 : V →ₗ[𝕜] ↥S := (↑S.orthogonalProjection : V →ₗ[𝕜] ↥S)
p2 : V →ₗ[𝕜] ↥Sᗮ := (↑Sᗮ.orthogonalProjection : V →ₗ[𝕜] ↥Sᗮ)
M : V →ₗ[𝕜] V := L.toLinearMap ∘ₗ p1 + L3.toLinearMap ∘ₗ p2
x : V
Mx_decomp :
  (M : (a : V) → V) x =
    HAdd.hAdd (α := V) (β := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
      ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)
⊢ Norm.norm (E := V) ((M : (a : V) → V) x : V) = ‖x‖
have Mx_orth : inner 𝕜 (E := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
    ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V) =
  0
Tactic: have Mx_orth : ⟪L (p1 x), L3 (p2 x)⟫ = 0 := by
      have Lp1x : L (p1 x) ∈ LinearMap.range L.toLinearMap :=
        LinearMap.mem_range_self L.toLinearMap (p1 x)
      have Lp2x : L3 (p2 x) ∈ (LinearMap.range L.toLinearMap)ᗮ := by
        simp only [LS,
          ← Submodule.range_subtype LSᗮ]
        apply LinearMap.mem_range_self
      apply Submodule.inner_right_of_mem_orthogonal Lp1x Lp2x
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E_1 : Type u_4
inst_1 : NormedAddCommGroup E_1
inst_2 : InnerProductSpace 𝕜 E_1
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this_1 : CompleteSpace.{u_7} ↥S
this : CompleteSpace V
p1 : V →ₗ[𝕜] ↥S := (↑S.orthogonalProjection : V →ₗ[𝕜] ↥S)
p2 : V →ₗ[𝕜] ↥Sᗮ := (↑Sᗮ.orthogonalProjection : V →ₗ[𝕜] ↥Sᗮ)
M : V →ₗ[𝕜] V := L.toLinearMap ∘ₗ p1 + L3.toLinearMap ∘ₗ p2
x : V
Mx_decomp :
  (M : (a : V) → V) x =
    HAdd.hAdd (α := V) (β := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
      ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)
Mx_orth :
  inner 𝕜 (E := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
      ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V) =
    0
⊢ Norm.norm (E := V) ((M : (a : V) → V) x : V) = ‖x‖
have rw : HPow.hPow (β := ℕ) (Norm.norm (E := V) ((M : (a : V) → V) x : V)) 2 =
  HPow.hPow (β := ℕ) (Norm.norm (E := ↥S) ((S.orthogonalProjection : (a : V) → ↥S) x : ↥S)) 2 +
    HPow.hPow (β := ℕ) (Norm.norm (E := ↥Sᗮ) ((Sᗮ.orthogonalProjection : (a : V) → ↥Sᗮ) x : ↥Sᗮ)) 2
Tactic: rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _), norm_sq_eq_add_norm_sq_projection x S]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E_1 : Type u_4
inst_1 : NormedAddCommGroup E_1
inst_2 : InnerProductSpace 𝕜 E_1
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this_1 : CompleteSpace.{u_7} ↥S
this : CompleteSpace V
p1 : V →ₗ[𝕜] ↥S := (↑S.orthogonalProjection : V →ₗ[𝕜] ↥S)
p2 : V →ₗ[𝕜] ↥Sᗮ := (↑Sᗮ.orthogonalProjection : V →ₗ[𝕜] ↥Sᗮ)
M : V →ₗ[𝕜] V := L.toLinearMap ∘ₗ p1 + L3.toLinearMap ∘ₗ p2
x : V
Mx_decomp :
  (M : (a : V) → V) x =
    HAdd.hAdd (α := V) (β := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
      ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)
Mx_orth :
  inner 𝕜 (E := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
      ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V) =
    0
⊢ HPow.hPow (β := ℕ) (Norm.norm (E := V) ((M : (a : V) → V) x : V)) 2 =
    HPow.hPow (β := ℕ) (Norm.norm (E := ↥S) ((S.orthogonalProjection : (a : V) → ↥S) x : ↥S)) 2 +
      HPow.hPow (β := ℕ) (Norm.norm (E := ↥Sᗮ) ((Sᗮ.orthogonalProjection : (a : V) → ↥Sᗮ) x : ↥Sᗮ)) 2
have simp : ‖HAdd.hAdd (α := V) (β := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
        ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)‖ *
    ‖HAdd.hAdd (α := V) (β := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
        ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)‖ =
  Norm.norm (E := ↥S) ((S.orthogonalProjection : (a : V) → ↥S) x : ↥S) *
      Norm.norm (E := ↥S) ((S.orthogonalProjection : (a : V) → ↥S) x : ↥S) +
    Norm.norm (E := ↥Sᗮ) ((Sᗮ.orthogonalProjection : (a : V) → ↥Sᗮ) x : ↥Sᗮ) *
      Norm.norm (E := ↥Sᗮ) ((Sᗮ.orthogonalProjection : (a : V) → ↥Sᗮ) x : ↥Sᗮ)
Tactic: simp only [sq, Mx_decomp]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E_1 : Type u_4
inst_1 : NormedAddCommGroup E_1
inst_2 : InnerProductSpace 𝕜 E_1
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this_1 : CompleteSpace.{u_7} ↥S
this : CompleteSpace V
p1 : V →ₗ[𝕜] ↥S := (↑S.orthogonalProjection : V →ₗ[𝕜] ↥S)
p2 : V →ₗ[𝕜] ↥Sᗮ := (↑Sᗮ.orthogonalProjection : V →ₗ[𝕜] ↥Sᗮ)
M : V →ₗ[𝕜] V := L.toLinearMap ∘ₗ p1 + L3.toLinearMap ∘ₗ p2
x : V
Mx_decomp :
  (M : (a : V) → V) x =
    HAdd.hAdd (α := V) (β := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
      ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)
Mx_orth :
  inner 𝕜 (E := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
      ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V) =
    0
⊢ ‖HAdd.hAdd (α := V) (β := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
          ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)‖ *
      ‖HAdd.hAdd (α := V) (β := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V)
          ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)‖ =
    Norm.norm (E := ↥S) ((S.orthogonalProjection : (a : V) → ↥S) x : ↥S) *
        Norm.norm (E := ↥S) ((S.orthogonalProjection : (a : V) → ↥S) x : ↥S) +
      Norm.norm (E := ↥Sᗮ) ((Sᗮ.orthogonalProjection : (a : V) → ↥Sᗮ) x : ↥Sᗮ) *
        Norm.norm (E := ↥Sᗮ) ((Sᗮ.orthogonalProjection : (a : V) → ↥Sᗮ) x : ↥Sᗮ)
have rw : Norm.norm (E := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V) *
      Norm.norm (E := V) ((L : (a : ↥S) → V) ((p1 : (a : V) → ↥S) x : ↥S) : V) +
    Norm.norm (E := V) ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V) *
      Norm.norm (E := V) ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V) =
  Norm.norm (E := ↥S) ((S.orthogonalProjection : (a : V) → ↥S) x : ↥S) *
      Norm.norm (E := ↥S) ((S.orthogonalProjection : (a : V) → ↥S) x : ↥S) +
    Norm.norm (E := ↥Sᗮ) ((Sᗮ.orthogonalProjection : (a : V) → ↥Sᗮ) x : ↥Sᗮ) *
      Norm.norm (E := ↥Sᗮ) ((Sᗮ.orthogonalProjection : (a : V) → ↥Sᗮ) x : ↥Sᗮ)
Tactic: rw [norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (L (p1 x)) (L3 (p2 x)) Mx_orth]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (hypothesis)
Goal:
ι : Type u_1
ι' : Type u_2
𝕜 : Type u_3
inst : RCLike 𝕜
E_1 : Type u_4
inst_1 : NormedAddCommGroup E_1
inst_2 : InnerProductSpace 𝕜 E_1
F : Type u_5
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace ℝ F
F' : Type u_6
inst_5 : NormedAddCommGroup F'
inst_6 : InnerProductSpace ℝ F'
inst_7 : Fintype ι
V : Type u_7
inst_8 : NormedAddCommGroup V
inst_9 : InnerProductSpace 𝕜 V
inst_10 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L_1 L : ↥S →ₗᵢ[𝕜] V
d : ℕ := finrank.{u_3, u_7} 𝕜 ↥Sᗮ
LS : Submodule 𝕜 V := L.range
E : ↥Sᗮ ≃ₗᵢ[𝕜] ↥LSᗮ
L3 : ↥Sᗮ →ₗᵢ[𝕜] V := LSᗮ.subtypeₗᵢ.comp E.toLinearIsometry
this_1 : CompleteSpace.{u_7} ↥S
this : CompleteSpace V
p1 : V →ₗ[𝕜] ↥S := (↑S.orthogonalProjection : V →ₗ[𝕜] ↥S)
p2 : V →ₗ[𝕜] ↥Sᗮ := (↑Sᗮ.orthogonalProjection : V →ₗ[𝕜] ↥Sᗮ)
M : V →ₗ[𝕜] V := L.toLinearMap ∘ₗ p1 + L3.toLinearMap ∘ₗ p2
⊢ V →ₗᵢ[𝕜] V
have M_norm_map : ∀ (x : V), Norm.norm (E := V) ((M : (a : V) → V) x : V) = ‖x‖
Tactic: have M_norm_map : ∀ x : V, ‖M x‖ = ‖x‖ := by
    intro x
    -- Apply M to the orthogonal decomposition of x
    have Mx_decomp : M x = L (p1 x) + L3 (p2 x) := by
      simp only [M, LinearMap.add_apply, LinearMap.comp_apply, LinearMap.comp_apply,
        LinearIsometry.coe_toLinearMap]
    -- Mx_decomp is the orthogonal decomposition of M x
    have Mx_orth : ⟪L (p1 x), L3 (p2 x)⟫ = 0 := by
      have Lp1x : L (p1 x) ∈ LinearMap.range L.toLinearMap :=
        LinearMap.mem_range_self L.toLinearMap (p1 x)
      have Lp2x : L3 (p2 x) ∈ (LinearMap.range L.toLinearMap)ᗮ := by
        simp only [LS,
          ← Submodule.range_subtype LSᗮ]
        apply LinearMap.mem_range_self
      apply Submodule.inner_right_of_mem_orthogonal Lp1x Lp2x
    -- Apply the Pythagorean theorem and simplify
    rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _), norm_sq_eq_add_norm_sq_projection x S]
    simp only [sq, Mx_decomp]
    rw [norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (L (p1 x)) (L3 (p2 x)) Mx_orth]
    simp only [p1, p2, LinearIsometry.norm_map,
      ContinuousLinearMap.coe_coe, Submodule.coe_norm]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
V : Type u_7
inst_1 : NormedAddCommGroup V
inst_2 : InnerProductSpace 𝕜 V
inst_3 : FiniteDimensional 𝕜 V
S : Submodule 𝕜 V
L : ↥S →ₗᵢ[𝕜] V
s : ↥S
⊢ Eq (α := V) ((L.extend : (a : V) → V) (↑s : V) : V) ((L : (a : ↥S) → V) s : V)
have simp : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
Tactic: simp only [LinearIsometry.extend, ← LinearIsometry.coe_toLinearMap]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
m : Type u_7
n : Type u_8
inst_3 : Fintype n
inst_4 : DecidableEq n
inst_5 : Fintype m
b : OrthonormalBasis n 𝕜 E
b₂ : OrthonormalBasis m 𝕜 𝕜
x : E
⊢ Eq (α := Matrix m n 𝕜)
    ((toMatrix b.toBasis b₂.toBasis : (a : E →ₗ[𝕜] 𝕜) → Matrix m n 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x) :
      Matrix m n 𝕜)
    (vecMulVec (star (⇑b₂ : (a : m) → 𝕜)) (star (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 n) x))) :
      Matrix m n 𝕜)
have a : ∀ (i : m) (j : n),
  Eq.{u_3 + 1} (α := 𝕜)
    ((toMatrix b.toBasis b₂.toBasis : (a : E →ₗ[𝕜] 𝕜) → Matrix m n 𝕜) ((innerₛₗ 𝕜 : (a : E) → E →ₗ[𝕜] 𝕜) x) i j : 𝕜)
    (vecMulVec (star (⇑b₂ : (a : m) → 𝕜)) (star (ofLp (p := 2) ((b.repr : (a : E) → EuclideanSpace 𝕜 n) x))) i j : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
𝕜 : Type u_7
E : Type u_8
F : Type u_9
ι : Type u_10
ι' : Type u_11
inst : RCLike 𝕜
inst_1 : SeminormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : InnerProductSpace 𝕜 F
inst_5 : Finite ι
inst_6 : Fintype ι'
inst_7 : DecidableEq ι'
x : E
y : F
b : Basis ι 𝕜 E
b' : OrthonormalBasis ι' 𝕜 F
⊢ Eq (α := Matrix ι ι' 𝕜)
    ((toMatrix b'.toBasis b : (a : F →ₗ[𝕜] E) → Matrix ι ι' 𝕜)
        (↑((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y) : F →ₗ[𝕜] E) :
      Matrix ι ι' 𝕜)
    (Matrix.vecMulVec (⇑((b.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : (a : ι) → 𝕜)
        (star (ofLp (p := 2) ((b'.repr : (a : F) → EuclideanSpace 𝕜 ι') y))) :
      Matrix ι ι' 𝕜)
have have : ∀ (this : Fintype ι),
  Eq (α := Matrix ι ι' 𝕜)
    ((toMatrix b'.toBasis b : (a : F →ₗ[𝕜] E) → Matrix ι ι' 𝕜)
        (↑((((rankOne 𝕜 : (a : E) → F →L⋆[𝕜] F →L[𝕜] E) x : F →L⋆[𝕜] F →L[𝕜] E) : (a : F) → F →L[𝕜] E) y) : F →ₗ[𝕜] E) :
      Matrix ι ι' 𝕜)
    (Matrix.vecMulVec (⇑((b.repr : (a : E) → ι →₀ 𝕜) x : ι →₀ 𝕜) : (a : ι) → 𝕜)
        (star (ofLp (p := 2) ((b'.repr : (a : F) → EuclideanSpace 𝕜 ι') y))) :
      Matrix ι ι' 𝕜)
Tactic: have := Fintype.ofFinite ι
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.PiL2 (goal)
Goal:
ι : Type u_1
𝕜 : Type u_3
inst : RCLike 𝕜
E : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : InnerProductSpace 𝕜 E
inst_3 : Fintype ι
inst_4 : Unique ι
h : finrank 𝕜 E = 1
v : E
hv : ‖v‖ = 1
w : E
⊢ Eq (α := EuclideanSpace 𝕜 ι)
    ((OrthonormalBasis.repr (orthonormalBasisSingleton ι 𝕜 h v hv) : (a : E) → EuclideanSpace 𝕜 ι) w :
      EuclideanSpace 𝕜 ι)
    (EuclideanSpace.single default ⟪v, w⟫ : EuclideanSpace 𝕜 ι)
have h₁ : ∀ (i : ι),
  Eq.{u_3 + 1} (α := 𝕜)
    (ofLp (p := 2) ((OrthonormalBasis.repr (orthonormalBasisSingleton ι 𝕜 h v hv) : (a : E) → EuclideanSpace 𝕜 ι) w) i :
      𝕜)
    (ofLp (EuclideanSpace.single default ⟪v, w⟫) i : 𝕜)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
E' : Type u_4
inst : NormedAddCommGroup E'
inst_1 : InnerProductSpace ℂ E'
T : E' →ₗ[ℂ] E'
⊢ T.IsPositive ↔
    ∀ (x : E'),
      (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ ∧
        LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
have simp_rw : (IsSymmetric.{0, u_4} (𝕜 := ℂ) (E := E') T ∧
    ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)) ↔
  ∀ (x : E'),
    (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ ∧
      LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
Tactic: simp_rw [IsPositive, forall_and, isSymmetric_iff_inner_map_self_real,
    conj_eq_iff_re, re_to_complex, Complex.coe_algebraMap]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
E' : Type u_4
inst : NormedAddCommGroup E'
inst_1 : InnerProductSpace ℂ E'
T : E' →ₗ[ℂ] E'
simp_rw :
  (IsSymmetric.{0, u_4} (𝕜 := ℂ) (E := E') T ∧
      ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)) ↔
    ∀ (x : E'),
      (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ ∧
        LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
⊢ T.IsPositive ↔
    ∀ (x : E'),
      (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ ∧
        LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
have simp_rw₁ : (IsSymmetric.{0, u_4} (𝕜 := ℂ) (E := E') T ∧
    ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)) ↔
  (∀ (x : E'), (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ) ∧
    ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
Tactic: simp_rw [IsPositive, forall_and, isSymmetric_iff_inner_map_self_real,
    conj_eq_iff_re, re_to_complex, Complex.coe_algebraMap]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
E' : Type u_4
inst : NormedAddCommGroup E'
inst_1 : InnerProductSpace ℂ E'
T : E' →ₗ[ℂ] E'
simp_rw :
  (IsSymmetric.{0, u_4} (𝕜 := ℂ) (E := E') T ∧
      ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)) ↔
    ∀ (x : E'),
      (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ ∧
        LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
simp_rw₁ :
  (IsSymmetric.{0, u_4} (𝕜 := ℂ) (E := E') T ∧
      ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)) ↔
    (∀ (x : E'), (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ) ∧
      ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
⊢ T.IsPositive ↔
    ∀ (x : E'),
      (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ ∧
        LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
have simp_rw₂ : ((∀ (v : E'), (starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : E') → E') v, v⟫_ℂ = ⟪(T : (a : E') → E') v, v⟫_ℂ) ∧
    ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)) ↔
  (∀ (x : E'), (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ) ∧
    ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
Tactic: simp_rw [IsPositive, forall_and, isSymmetric_iff_inner_map_self_real,
    conj_eq_iff_re, re_to_complex, Complex.coe_algebraMap]
-- Lean 4 proof step from Mathlib.Analysis.InnerProductSpace.Positive (goal)
Goal:
E' : Type u_4
inst : NormedAddCommGroup E'
inst_1 : InnerProductSpace ℂ E'
T : E' →ₗ[ℂ] E'
simp_rw :
  (IsSymmetric.{0, u_4} (𝕜 := ℂ) (E := E') T ∧
      ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)) ↔
    ∀ (x : E'),
      (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ ∧
        LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
simp_rw₁ :
  (IsSymmetric.{0, u_4} (𝕜 := ℂ) (E := E') T ∧
      ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)) ↔
    (∀ (x : E'), (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ) ∧
      ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
simp_rw₂ :
  ((∀ (v : E'), (starRingEnd ℂ : (a : ℂ) → ℂ) ⟪(T : (a : E') → E') v, v⟫_ℂ = ⟪(T : (a : E') → E') v, v⟫_ℂ) ∧
      ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)) ↔
    (∀ (x : E'), (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ) ∧
      ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
⊢ T.IsPositive ↔
    ∀ (x : E'),
      (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ ∧
        LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
have simp_rw₃ : ((∀ (v : E'), (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') v, v⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') v, v⟫_ℂ) ∧
    ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)) ↔
  (∀ (x : E'), (↑((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ) : ℂ) = ⟪(T : (a : E') → E') x, x⟫_ℂ) ∧
    ∀ (x : E'), LE.le (α := ℝ) (0 : ℝ) ((re : (a : ℂ) → ℝ) ⟪(T : (a : E') → E') x, x⟫_ℂ : ℝ)
Tactic: simp_rw [IsPositive, forall_and, isSymmetric_iff_inner_map_self_real,
    conj_eq_iff_re, re_to_complex, Complex.coe_algebraMap]