-- Mathlib/Analysis/InnerProductSpace/JointEigenspace.lean
theorem orthogonalFamily_iInf_eigenspaces (hT : ∀ i, (T i).IsSymmetric) :
    OrthogonalFamily 𝕜 (fun γ : n → 𝕜 ↦ (⨅ j, eigenspace (T j) (γ j) : Submodule 𝕜 E))
      fun γ : n → 𝕜 ↦ (⨅ j, eigenspace (T j) (γ j)).subtypeₗᵢ

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H :
  (fun i j =>
      ∀ (v : (fun μ => ↥((T a).eigenspace μ)) i) (w : (fun μ => ↥((T a).eigenspace μ)) j),
        inner (((fun μ => ((T a).eigenspace μ).subtypeₗᵢ) i) v) (((fun μ => ((T a).eigenspace μ).subtypeₗᵢ) j) w) = 0)
    (f a) (g a)
⊢ inner (((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) f) Ef)
      (((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) g) Eg) =
    0

Tactic:
simp only [Submodule.coe_subtypeₗᵢ, Submodule.coe_subtype, Subtype.forall] at H

Result:
case intro
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H : ∀ a_1 ∈ (T a).eigenspace (f a), ∀ a_2 ∈ (T a).eigenspace (g a), inner a_1 a_2 = 0
⊢ inner (((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) f) Ef)
      (((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) g) Eg) =
    0

Proof state:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
⊢ inner (((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) f) Ef)
      (((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) g) Eg) =
    0

Tactic:
obtain ⟨a , ha⟩ := Function.ne_iff.mp hfg

Result:
case intro
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
⊢ inner (((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) f) Ef)
      (((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) g) Eg) =
    0

Proof state:
case intro.b
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H : ∀ a_1 ∈ (T a).eigenspace (f a), ∀ a_2 ∈ (T a).eigenspace (g a), inner a_1 a_2 = 0
⊢ ((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) f) Ef ∈ (T a).eigenspace (f a)

Tactic:
exact (Submodule.mem_iInf <| fun _ ↦ eigenspace (T _) (f _)).mp Ef.2 _

Result:
no goals

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
⊢ inner (((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) f) Ef)
      (((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) g) Eg) =
    0

Tactic:
have H := orthogonalFamily_eigenspaces (hT a) ha

Result:
case intro
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H :
  (fun i j =>
      ∀ (v : (fun μ => ↥((T a).eigenspace μ)) i) (w : (fun μ => ↥((T a).eigenspace μ)) j),
        inner (((fun μ => ((T a).eigenspace μ).subtypeₗᵢ) i) v) (((fun μ => ((T a).eigenspace μ).subtypeₗᵢ) j) w) = 0)
    (f a) (g a)
⊢ inner (((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) f) Ef)
      (((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) g) Eg) =
    0

Proof state:
case intro.b
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H : ∀ a_1 ∈ (T a).eigenspace (f a), ∀ a_2 ∈ (T a).eigenspace (g a), inner a_1 a_2 = 0
⊢ ((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) g) Eg ∈ (T a).eigenspace (g a)

Tactic:
exact (Submodule.mem_iInf <| fun _ ↦ eigenspace (T _) (g _)).mp Eg.2 _

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
⊢ OrthogonalFamily 𝕜 (fun γ => ↥(⨅ j, (T j).eigenspace (γ j))) fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ

Tactic:
intro f g hfg Ef Eg

Result:
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
⊢ inner (((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) f) Ef)
      (((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) g) Eg) =
    0

Proof state:
case intro
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H : ∀ a_1 ∈ (T a).eigenspace (f a), ∀ a_2 ∈ (T a).eigenspace (g a), inner a_1 a_2 = 0
⊢ inner (((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) f) Ef)
      (((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) g) Eg) =
    0

Tactic:
apply H

Result:
case intro.b
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H : ∀ a_1 ∈ (T a).eigenspace (f a), ∀ a_2 ∈ (T a).eigenspace (g a), inner a_1 a_2 = 0
⊢ ((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) f) Ef ∈ (T a).eigenspace (f a)

case intro.b
𝕜 : Type u_1
E : Type u_2
n : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : n → Module.End 𝕜 E
hT : ∀ (i : n), IsSymmetric (T i)
f g : n → 𝕜
hfg : f ≠ g
Ef : ↥(⨅ j, (T j).eigenspace (f j))
Eg : ↥(⨅ j, (T j).eigenspace (g j))
a : n
ha : f a ≠ g a
H : ∀ a_1 ∈ (T a).eigenspace (f a), ∀ a_2 ∈ (T a).eigenspace (g a), inner a_1 a_2 = 0
⊢ ((fun γ => (⨅ j, (T j).eigenspace (γ j)).subtypeₗᵢ) g) Eg ∈ (T a).eigenspace (g a)