awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
⊢ CompleteSpace.{u_7} ↥S

Tactic:
haveI : CompleteSpace S := FiniteDimensional.complete 𝕜 S
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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 : CompleteSpace.{u_7} ↥S
⊢ CompleteSpace V

Tactic:
haveI : CompleteSpace V := FiniteDimensional.complete 𝕜 V
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
⊢ (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)

Tactic:
simp only [M, LinearMap.add_apply, LinearMap.comp_apply, LinearMap.comp_apply,
        LinearIsometry.coe_toLinearMap]

Premises used: LinearIsometry.coe_toLinearMap, LinearMap.add_apply, LinearMap.comp_apply
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
⊢ (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)

Tactic:
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]
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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)
⊢ 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)
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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)
simp : Membership.mem (α := V) L.rangeᗮ.subtype.range ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)
⊢ Membership.mem (α := V) L.rangeᗮ ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)

Tactic:
simp only [LS,
          ← Submodule.range_subtype LSᗮ]

Premises used: Submodule.orthogonal, Submodule.range_subtype
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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ᗮ.subtype.range ((L3 : (a : ↥Sᗮ) → V) ((p2 : (a : V) → ↥Sᗮ) x : ↥Sᗮ) : V)

Tactic:
apply LinearMap.mem_range_self

Premises used: LinearMap.mem_range_self
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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)

Tactic:
have Lp2x : L3 (p2 x) ∈ (LinearMap.range L.toLinearMap)ᗮ := by
        simp only [LS,
          ← Submodule.range_subtype LSᗮ]
        apply LinearMap.mem_range_self
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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)
Lp2x : Membership.mem (α := V) L.rangeᗮ ((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

Tactic:
apply Submodule.inner_right_of_mem_orthogonal Lp1x Lp2x

Premises used: Submodule.inner_right_of_mem_orthogonal
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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

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
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
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
⊢ Norm.norm (E := V) ((M : (a : V) → V) x : V) = ‖x‖

Tactic:
rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _), norm_sq_eq_add_norm_sq_projection x S]

Premises used: Submodule.norm_sq_eq_add_norm_sq_projection, sq_eq_sq₀, norm_nonneg
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
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ᗮ)
⊢ 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:
simp only [sq, Mx_decomp]

Premises used: sq
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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
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ᗮ)
⊢ ‖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:
rw [norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero (L (p1 x)) (L3 (p2 x)) Mx_orth]

Premises used: DFunLike.coe, norm_add_sq_eq_norm_sq_add_norm_sq_of_inner_eq_zero
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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) ((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:
simp only [p1, p2, LinearIsometry.norm_map,
      ContinuousLinearMap.coe_coe, Submodule.coe_norm]

Premises used: LinearIsometry.norm_map, ContinuousLinearMap.coe_coe, Submodule.coe_norm
-- Module: Mathlib.Analysis.InnerProductSpace.PiL2
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), 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]