R : Type ?u.1617651
M : Type ?u.1617654
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1617690
M₁ : Type ?u.1617693
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1618302
M₂ : Type ?u.1618305
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1618492
M₃ : Type ?u.1618495
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1620300
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Subspace K V
b₁ : IsRefl B
⊢ finrank K { x // x ∈ W } +
      finrank K { x // x ∈ Submodule.dualCoannihilator (LinearMap.range (LinearMap.domRestrict (↑toLin B) W)) } =
    finrank K V + finrank K { x // x ∈ LinearMap.ker (LinearMap.domRestrict (↑toLin B) W) }
R : Type ?u.1617651
M : Type ?u.1617654
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1617690
M₁ : Type ?u.1617693
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1618302
M₂ : Type ?u.1618305
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1618492
M₃ : Type ?u.1618495
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1620300
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Subspace K V
b₁ : IsRefl B
⊢ finrank K { x // x ∈ W } + finrank K { x // x ∈ orthogonal B W } =
    finrank K V + finrank K { x // x ∈ W ⊓ orthogonal B ⊤ }
rw [← toLin_restrict_ker_eq_inf_orthogonal _ _ b₁, ←
  toLin_restrict_range_dualCoannihilator_eq_orthogonal _ _, Submodule.finrank_map_subtype_eq]
no goals
R : Type ?u.1617651
M : Type ?u.1617654
inst✝¹⁷ : Semiring R
inst✝¹⁶ : AddCommMonoid M
inst✝¹⁵ : Module R M
R₁ : Type ?u.1617690
M₁ : Type ?u.1617693
inst✝¹⁴ : Ring R₁
inst✝¹³ : AddCommGroup M₁
inst✝¹² : Module R₁ M₁
R₂ : Type ?u.1618302
M₂ : Type ?u.1618305
inst✝¹¹ : CommSemiring R₂
inst✝¹⁰ : AddCommMonoid M₂
inst✝⁹ : Module R₂ M₂
R₃ : Type ?u.1618492
M₃ : Type ?u.1618495
inst✝⁸ : CommRing R₃
inst✝⁷ : AddCommGroup M₃
inst✝⁶ : Module R₃ M₃
V : Type u_2
K : Type u_1
inst✝⁵ : Field K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
B✝ : BilinForm R M
B₁ : BilinForm R₁ M₁
B₂ : BilinForm R₂ M₂
M₂' : Type ?u.1620300
inst✝² : AddCommMonoid M₂'
inst✝¹ : Module R₂ M₂'
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Subspace K V
b₁ : IsRefl B
⊢ finrank K { x // x ∈ W } +
      finrank K { x // x ∈ Submodule.dualCoannihilator (LinearMap.range (LinearMap.domRestrict (↑toLin B) W)) } =
    finrank K V + finrank K { x // x ∈ LinearMap.ker (LinearMap.domRestrict (↑toLin B) W) }
conv_rhs =>
  rw [← @Subspace.finrank_add_finrank_dualCoannihilator_eq K V _ _ _ _
      (LinearMap.range (B.toLin.domRestrict W)),
    add_comm, ← add_assoc, add_comm (finrank K (LinearMap.ker (B.toLin.domRestrict W))),
    LinearMap.finrank_range_add_finrank_ker]