-- Mathlib/LinearAlgebra/FiniteDimensional.lean
theorem eq_top_of_disjoint [FiniteDimensional K V] (s t : Submodule K V)
    (hdim : finrank K V ≤ finrank K s + finrank K t) (hdisjoint : Disjoint s t) : s ⊔ t = ⊤

Proof state:
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 V ≤ finrank K ↥s + finrank K ↥t
hdisjoint : Disjoint s t
h_finrank_inf : finrank K ↥(s ⊓ t) = 0
⊢ finrank K ↥(s ⊔ t) = finrank K V

Tactic:
replace hdim : finrank K V = finrank K s + finrank K t :=
  le_antisymm hdim (finrank_add_finrank_le_of_disjoint hdisjoint)

Result:
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
hdisjoint : Disjoint s t
h_finrank_inf : finrank K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank K ↥s + finrank K ↥t
⊢ finrank K ↥(s ⊔ t) = finrank K V

Proof state:
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
hdisjoint : Disjoint s t
h_finrank_inf : finrank K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank K ↥s + finrank K ↥t
⊢ finrank K ↥(s ⊔ t) = finrank K V

Tactic:
rw [hdim]

Result:
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
hdisjoint : Disjoint s t
h_finrank_inf : finrank K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank K ↥s + finrank K ↥t
⊢ finrank K ↥(s ⊔ t) = finrank K ↥s + finrank K ↥t

Proof state:
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
hdisjoint : Disjoint s t
h_finrank_inf : finrank K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank K ↥s + finrank K ↥t
⊢ finrank K ↥(s ⊔ t) = finrank K ↥(s ⊔ t) + 0

Tactic:
rfl

Result:
no goals

Proof state:
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 V ≤ finrank K ↥s + finrank K ↥t
hdisjoint : Disjoint s t
⊢ s ⊔ t = ⊤

Tactic:
have h_finrank_inf : finrank K ↑(s ⊓ t) = 0 := by
  rw [disjoint_iff_inf_le, le_bot_iff] at hdisjoint
  rw [hdisjoint, finrank_bot]

Result:
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 V ≤ finrank K ↥s + finrank K ↥t
hdisjoint : Disjoint s t
h_finrank_inf : finrank K ↥(s ⊓ t) = 0
⊢ s ⊔ t = ⊤

Proof state:
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 V ≤ finrank K ↥s + finrank K ↥t
hdisjoint : Disjoint s t
h_finrank_inf : finrank K ↥(s ⊓ t) = 0
⊢ s ⊔ t = ⊤

Tactic:
apply eq_top_of_finrank_eq

Result:
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 V ≤ finrank K ↥s + finrank K ↥t
hdisjoint : Disjoint s t
h_finrank_inf : finrank K ↥(s ⊓ t) = 0
⊢ finrank K ↥(s ⊔ t) = finrank K V

Proof state:
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 V ≤ finrank K ↥s + finrank K ↥t
hdisjoint : Disjoint s t
⊢ finrank K ↥(s ⊓ t) = 0

Tactic:
rw [disjoint_iff_inf_le, le_bot_iff] at hdisjoint

Result:
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 V ≤ finrank K ↥s + finrank K ↥t
hdisjoint : s ⊓ t = ⊥
⊢ finrank K ↥(s ⊓ t) = 0

Proof state:
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
hdisjoint : Disjoint s t
h_finrank_inf : finrank K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank K ↥s + finrank K ↥t
⊢ finrank K ↥(s ⊔ t) = finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t)

Tactic:
rw [h_finrank_inf]

Result:
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
hdisjoint : Disjoint s t
h_finrank_inf : finrank K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank K ↥s + finrank K ↥t
⊢ finrank K ↥(s ⊔ t) = finrank K ↥(s ⊔ t) + 0

Proof state:
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
hdisjoint : Disjoint s t
h_finrank_inf : finrank K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank K ↥s + finrank K ↥t
⊢ finrank K ↥(s ⊔ t) = finrank K ↥s + finrank K ↥t

Tactic:
convert s.finrank_sup_add_finrank_inf_eq t

Result:
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
hdisjoint : Disjoint s t
h_finrank_inf : finrank K ↥(s ⊓ t) = 0
hdim : finrank K V = finrank K ↥s + finrank K ↥t
⊢ finrank K ↥(s ⊔ t) = finrank K ↥(s ⊔ t) + finrank K ↥(s ⊓ t)

Proof state:
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 V ≤ finrank K ↥s + finrank K ↥t
hdisjoint : s ⊓ t = ⊥
⊢ finrank K ↥(s ⊓ t) = 0

Tactic:
rw [hdisjoint, finrank_bot]

Result:
no goals