K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K { x // x ∈ s } + finrank K { x // x ∈ t } = finrank K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank K { x // x ∈ s ⊓ t } = 0
⊢ s ⊔ t = ⊤
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K { x // x ∈ s } + finrank K { x // x ∈ t } = finrank K V
hdisjoint : Disjoint s t
⊢ s ⊔ t = ⊤
have h_finrank_inf : finrank K ↑(s ⊓ t) = 0 := by
  rw [disjoint_iff_inf_le, le_bot_iff] at hdisjoint
  rw [hdisjoint, finrank_bot]
case h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K { x // x ∈ s } + finrank K { x // x ∈ t } = finrank K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank K { x // x ∈ s ⊓ t } = 0
⊢ finrank K { x // x ∈ s ⊔ t } = finrank K V
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K { x // x ∈ s } + finrank K { x // x ∈ t } = finrank K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank K { x // x ∈ s ⊓ t } = 0
⊢ s ⊔ t = ⊤
apply eq_top_of_finrank_eq
case h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K { x // x ∈ s } + finrank K { x // x ∈ t } = finrank K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank K { x // x ∈ s ⊓ t } = 0
⊢ finrank K { x // x ∈ s ⊔ t } = finrank K { x // x ∈ s } + finrank K { x // x ∈ t }
case h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K { x // x ∈ s } + finrank K { x // x ∈ t } = finrank K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank K { x // x ∈ s ⊓ t } = 0
⊢ finrank K { x // x ∈ s ⊔ t } = finrank K V
rw [← hdim]
case h.e'_2
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K { x // x ∈ s } + finrank K { x // x ∈ t } = finrank K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank K { x // x ∈ s ⊓ t } = 0
⊢ finrank K { x // x ∈ s ⊔ t } = finrank K { x // x ∈ s ⊔ t } + finrank K { x // x ∈ s ⊓ t }
case h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K { x // x ∈ s } + finrank K { x // x ∈ t } = finrank K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank K { x // x ∈ s ⊓ t } = 0
⊢ finrank K { x // x ∈ s ⊔ t } = finrank K { x // x ∈ s } + finrank K { x // x ∈ t }
convert s.finrank_sup_add_finrank_inf_eq t
case h.e'_2
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K { x // x ∈ s } + finrank K { x // x ∈ t } = finrank K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank K { x // x ∈ s ⊓ t } = 0
⊢ finrank K { x // x ∈ s ⊔ t } = finrank K { x // x ∈ s ⊔ t } + 0
case h.e'_2
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K { x // x ∈ s } + finrank K { x // x ∈ t } = finrank K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank K { x // x ∈ s ⊓ t } = 0
⊢ finrank K { x // x ∈ s ⊔ t } = finrank K { x // x ∈ s ⊔ t } + finrank K { x // x ∈ s ⊓ t }
rw [h_finrank_inf]
no goals
case h.e'_2
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K { x // x ∈ s } + finrank K { x // x ∈ t } = finrank K V
hdisjoint : Disjoint s t
h_finrank_inf : finrank K { x // x ∈ s ⊓ t } = 0
⊢ finrank K { x // x ∈ s ⊔ t } = finrank K { x // x ∈ s ⊔ t } + 0
rfl
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K { x // x ∈ s } + finrank K { x // x ∈ t } = finrank K V
hdisjoint : s ⊓ t = ⊥
⊢ finrank K { x // x ∈ s ⊓ t } = 0
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K { x // x ∈ s } + finrank K { x // x ∈ t } = finrank K V
hdisjoint : Disjoint s t
⊢ finrank K { x // x ∈ s ⊓ t } = 0
rw [disjoint_iff_inf_le, le_bot_iff] at hdisjoint
no goals
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
s t : Submodule K V
hdim : finrank K { x // x ∈ s } + finrank K { x // x ∈ t } = finrank K V
hdisjoint : s ⊓ t = ⊥
⊢ finrank K { x // x ∈ s ⊓ t } = 0
rw [hdisjoint, finrank_bot]