-- Mathlib/Analysis/InnerProductSpace/Semisimple.lean
theorem isFinitelySemisimple :
    T.IsFinitelySemisimple

Proof state:
case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ Disjoint q (qᗮ ⊓ p)

Tactic:
simp [disjoint_iff, ← inf_assoc, Submodule.inf_orthogonal_eq_bot q]

Result:
no goals

Proof state:
case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ q ⊔ qᗮ = ⊤

Tactic:
replace hp₂ : Module.Finite 𝕜 q := Submodule.finiteDimensional_of_le hq₂

Result:
case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
hp₂ : Module.Finite 𝕜 ↥q
⊢ q ⊔ qᗮ = ⊤

Proof state:
case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
hp₂ : Module.Finite 𝕜 ↥q
⊢ q ⊔ qᗮ = ⊤

Tactic:
exact Submodule.sup_orthogonal_of_completeSpace

Result:
no goals

Proof state:
case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ q ⊔ qᗮ ⊓ p = p

Tactic:
suffices q ⊔ qᗮ = ⊤ by rw [← sup_inf_assoc_of_le _ hq₂, this, top_inf_eq p]

Result:
case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ q ⊔ qᗮ = ⊤

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
⊢ T.IsFinitelySemisimple

Tactic:
refine Module.End.isFinitelySemisimple_iff.mpr fun p hp₁ hp₂ q hq₁ hq₂ ↦
  ⟨qᗮ ⊓ p, inf_le_right, Module.End.invtSubmodule.inf_mem ?_ hp₁, ?_, ?_⟩

Result:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ qᗮ ∈ T.invtSubmodule

case refine_2
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ Disjoint q (qᗮ ⊓ p)

case refine_3
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ q ⊔ qᗮ ⊓ p = p

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
this : q ⊔ qᗮ = ⊤
⊢ q ⊔ qᗮ ⊓ p = p

Tactic:
rw [← sup_inf_assoc_of_le _ hq₂, this, top_inf_eq p]

Result:
no goals

Proof state:
case refine_1
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
T : Module.End 𝕜 E
hT : IsSymmetric T
p : Submodule 𝕜 E
hp₁ : p ∈ T.invtSubmodule
hp₂ : Module.Finite 𝕜 ↥p
q : Submodule 𝕜 E
hq₁ : q ∈ T.invtSubmodule
hq₂ : q ≤ p
⊢ qᗮ ∈ T.invtSubmodule

Tactic:
exact orthogonalComplement_mem_invtSubmodule hT hq₁

Result:
no goals