𝕜 : Type u_1
E : Type u_2
F : Type ?u.988806
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 { x // x ∈ K₂ }
h : K₁ ≤ K₂
this : FiniteDimensional 𝕜 { x // x ∈ K₁ }
⊢ finrank 𝕜 { x // x ∈ K₁ } + finrank 𝕜 { x // x ∈ K₁ᗮ ⊓ K₂ } = finrank 𝕜 { x // x ∈ K₂ }
𝕜 : Type u_1
E : Type u_2
F : Type ?u.988806
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 { x // x ∈ K₂ }
h : K₁ ≤ K₂
⊢ finrank 𝕜 { x // x ∈ K₁ } + finrank 𝕜 { x // x ∈ K₁ᗮ ⊓ K₂ } = finrank 𝕜 { x // x ∈ K₂ }
haveI : FiniteDimensional 𝕜 K₁ := Submodule.finiteDimensional_of_le h
𝕜 : Type u_1
E : Type u_2
F : Type ?u.988806
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 { x // x ∈ K₂ }
h : K₁ ≤ K₂
this✝ : FiniteDimensional 𝕜 { x // x ∈ K₁ }
this : ProperSpace { x // x ∈ K₁ }
⊢ finrank 𝕜 { x // x ∈ K₁ } + finrank 𝕜 { x // x ∈ K₁ᗮ ⊓ K₂ } = finrank 𝕜 { x // x ∈ K₂ }
𝕜 : Type u_1
E : Type u_2
F : Type ?u.988806
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 { x // x ∈ K₂ }
h : K₁ ≤ K₂
this : FiniteDimensional 𝕜 { x // x ∈ K₁ }
⊢ finrank 𝕜 { x // x ∈ K₁ } + finrank 𝕜 { x // x ∈ K₁ᗮ ⊓ K₂ } = finrank 𝕜 { x // x ∈ K₂ }
haveI := proper_isROrC 𝕜 K₁
𝕜 : Type u_1
E : Type u_2
F : Type ?u.988806
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 { x // x ∈ K₂ }
h : K₁ ≤ K₂
this✝ : FiniteDimensional 𝕜 { x // x ∈ K₁ }
this : ProperSpace { x // x ∈ K₁ }
hd :
  finrank 𝕜 { x // x ∈ K₁ ⊔ K₁ᗮ ⊓ K₂ } + finrank 𝕜 { x // x ∈ K₁ ⊓ (K₁ᗮ ⊓ K₂) } =
    finrank 𝕜 { x // x ∈ K₁ } + finrank 𝕜 { x // x ∈ K₁ᗮ ⊓ K₂ }
⊢ finrank 𝕜 { x // x ∈ K₁ } + finrank 𝕜 { x // x ∈ K₁ᗮ ⊓ K₂ } = finrank 𝕜 { x // x ∈ K₂ }
𝕜 : Type u_1
E : Type u_2
F : Type ?u.988806
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 { x // x ∈ K₂ }
h : K₁ ≤ K₂
this✝ : FiniteDimensional 𝕜 { x // x ∈ K₁ }
this : ProperSpace { x // x ∈ K₁ }
⊢ finrank 𝕜 { x // x ∈ K₁ } + finrank 𝕜 { x // x ∈ K₁ᗮ ⊓ K₂ } = finrank 𝕜 { x // x ∈ K₂ }
have hd := Submodule.finrank_sup_add_finrank_inf_eq K₁ (K₁ᗮ ⊓ K₂)
𝕜 : Type u_1
E : Type u_2
F : Type ?u.988806
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 { x // x ∈ K₂ }
h : K₁ ≤ K₂
this✝ : FiniteDimensional 𝕜 { x // x ∈ K₁ }
this : ProperSpace { x // x ∈ K₁ }
hd : finrank 𝕜 { x // x ∈ K₂ } + 0 = finrank 𝕜 { x // x ∈ K₁ } + finrank 𝕜 { x // x ∈ K₁ᗮ ⊓ K₂ }
⊢ finrank 𝕜 { x // x ∈ K₁ } + finrank 𝕜 { x // x ∈ K₁ᗮ ⊓ K₂ } = finrank 𝕜 { x // x ∈ K₂ }
𝕜 : Type u_1
E : Type u_2
F : Type ?u.988806
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 { x // x ∈ K₂ }
h : K₁ ≤ K₂
this✝ : FiniteDimensional 𝕜 { x // x ∈ K₁ }
this : ProperSpace { x // x ∈ K₁ }
hd :
  finrank 𝕜 { x // x ∈ K₁ ⊔ K₁ᗮ ⊓ K₂ } + finrank 𝕜 { x // x ∈ K₁ ⊓ (K₁ᗮ ⊓ K₂) } =
    finrank 𝕜 { x // x ∈ K₁ } + finrank 𝕜 { x // x ∈ K₁ᗮ ⊓ K₂ }
⊢ finrank 𝕜 { x // x ∈ K₁ } + finrank 𝕜 { x // x ∈ K₁ᗮ ⊓ K₂ } = finrank 𝕜 { x // x ∈ K₂ }
rw [← inf_assoc, (Submodule.orthogonal_disjoint K₁).eq_bot, bot_inf_eq, finrank_bot,
  Submodule.sup_orthogonal_inf_of_completeSpace h] at hd
𝕜 : Type u_1
E : Type u_2
F : Type ?u.988806
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 { x // x ∈ K₂ }
h : K₁ ≤ K₂
this✝ : FiniteDimensional 𝕜 { x // x ∈ K₁ }
this : ProperSpace { x // x ∈ K₁ }
hd : finrank 𝕜 { x // x ∈ K₂ } = finrank 𝕜 { x // x ∈ K₁ } + finrank 𝕜 { x // x ∈ K₁ᗮ ⊓ K₂ }
⊢ finrank 𝕜 { x // x ∈ K₁ } + finrank 𝕜 { x // x ∈ K₁ᗮ ⊓ K₂ } = finrank 𝕜 { x // x ∈ K₂ }
𝕜 : Type u_1
E : Type u_2
F : Type ?u.988806
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 { x // x ∈ K₂ }
h : K₁ ≤ K₂
this✝ : FiniteDimensional 𝕜 { x // x ∈ K₁ }
this : ProperSpace { x // x ∈ K₁ }
hd : finrank 𝕜 { x // x ∈ K₂ } + 0 = finrank 𝕜 { x // x ∈ K₁ } + finrank 𝕜 { x // x ∈ K₁ᗮ ⊓ K₂ }
⊢ finrank 𝕜 { x // x ∈ K₁ } + finrank 𝕜 { x // x ∈ K₁ᗮ ⊓ K₂ } = finrank 𝕜 { x // x ∈ K₂ }
rw [add_zero] at hd
no goals
𝕜 : Type u_1
E : Type u_2
F : Type ?u.988806
inst✝⁵ : IsROrC 𝕜
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : InnerProductSpace ℝ F
K K₁ K₂ : Submodule 𝕜 E
inst✝ : FiniteDimensional 𝕜 { x // x ∈ K₂ }
h : K₁ ≤ K₂
this✝ : FiniteDimensional 𝕜 { x // x ∈ K₁ }
this : ProperSpace { x // x ∈ K₁ }
hd : finrank 𝕜 { x // x ∈ K₂ } = finrank 𝕜 { x // x ∈ K₁ } + finrank 𝕜 { x // x ∈ K₁ᗮ ⊓ K₂ }
⊢ finrank 𝕜 { x // x ∈ K₁ } + finrank 𝕜 { x // x ∈ K₁ᗮ ⊓ K₂ } = finrank 𝕜 { x // x ∈ K₂ }
exact hd.symm