-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
theorem isCompl_orthogonal_of_restrict_nondegenerate
    (b₁ : B.IsRefl) (b₂ : (B.restrict W).Nondegenerate) : IsCompl W (B.orthogonal W)

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
⊢ W ⊓ B.orthogonal W = ⊥

Tactic:
rw [eq_bot_iff]

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
⊢ W ⊓ B.orthogonal W ≤ ⊥

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
this : W ⊓ B.orthogonal W = ⊥
⊢ finrank K V ≤ finrank K ↥(W ⊔ B.orthogonal W)

Tactic:
conv_rhs => rw [← add_zero (finrank K _)]

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
this : W ⊓ B.orthogonal W = ⊥
⊢ finrank K V ≤ finrank K ↥(W ⊔ B.orthogonal W) + 0

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
⊢ IsCompl W (B.orthogonal W)

Tactic:
have : W ⊓ B.orthogonal W = ⊥ := by
  rw [eq_bot_iff]
  intro x hx
  obtain ⟨hx₁, hx₂⟩ := mem_inf.1 hx
  refine Subtype.mk_eq_mk.1 (b₂ ⟨x, hx₁⟩ ?_)
  rintro ⟨n, hn⟩
  simp only [restrict_apply, domRestrict_apply]
  exact b₁ n x (b₁ x n (b₁ n x (hx₂ n hn)))

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
this : W ⊓ B.orthogonal W = ⊥
⊢ IsCompl W (B.orthogonal W)

Proof state:
case intro
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
x : V
hx : x ∈ W ⊓ B.orthogonal W
hx₁ : x ∈ W
hx₂ : x ∈ B.orthogonal W
⊢ x ∈ ⊥

Tactic:
refine Subtype.mk_eq_mk.1 (b₂ ⟨x, hx₁⟩ ?_)

Result:
case intro
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
x : V
hx : x ∈ W ⊓ B.orthogonal W
hx₁ : x ∈ W
hx₂ : x ∈ B.orthogonal W
⊢ ∀ (n : ↥W), ((B.restrict W) ⟨x, hx₁⟩) n = 0

Proof state:
case intro.mk
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
x : V
hx : x ∈ W ⊓ B.orthogonal W
hx₁ : x ∈ W
hx₂ : x ∈ B.orthogonal W
n : V
hn : n ∈ W
⊢ ((B.restrict W) ⟨x, hx₁⟩) ⟨n, hn⟩ = 0

Tactic:
simp only [restrict_apply, domRestrict_apply]

Result:
case intro.mk
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
x : V
hx : x ∈ W ⊓ B.orthogonal W
hx₁ : x ∈ W
hx₂ : x ∈ B.orthogonal W
n : V
hn : n ∈ W
⊢ (B x) n = 0

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
this : W ⊓ B.orthogonal W = ⊥
⊢ IsCompl W (B.orthogonal W)

Tactic:
refine IsCompl.of_eq this (eq_top_of_finrank_eq <| (finrank_le _).antisymm ?_)

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
this : W ⊓ B.orthogonal W = ⊥
⊢ finrank K V ≤ finrank K ↥(W ⊔ B.orthogonal W)

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
x : V
hx : x ∈ W ⊓ B.orthogonal W
⊢ x ∈ ⊥

Tactic:
obtain ⟨hx₁, hx₂⟩ := mem_inf.1 hx

Result:
case intro
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
x : V
hx : x ∈ W ⊓ B.orthogonal W
hx₁ : x ∈ W
hx₂ : x ∈ B.orthogonal W
⊢ x ∈ ⊥

Proof state:
case intro.mk
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
x : V
hx : x ∈ W ⊓ B.orthogonal W
hx₁ : x ∈ W
hx₂ : x ∈ B.orthogonal W
n : V
hn : n ∈ W
⊢ (B x) n = 0

Tactic:
exact b₁ n x (b₁ x n (b₁ n x (hx₂ n hn)))

Result:
no goals

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
this : W ⊓ B.orthogonal W = ⊥
⊢ finrank K V ≤ finrank K ↥(W ⊔ B.orthogonal W) + 0

Tactic:
rw [← finrank_bot K V, ← this, finrank_sup_add_finrank_inf_eq,
  finrank_add_finrank_orthogonal b₁]

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
this : W ⊓ B.orthogonal W = ⊥
⊢ finrank K V ≤ finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤)

Proof state:
case intro
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
x : V
hx : x ∈ W ⊓ B.orthogonal W
hx₁ : x ∈ W
hx₂ : x ∈ B.orthogonal W
⊢ ∀ (n : ↥W), ((B.restrict W) ⟨x, hx₁⟩) n = 0

Tactic:
rintro ⟨n, hn⟩

Result:
case intro.mk
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
x : V
hx : x ∈ W ⊓ B.orthogonal W
hx₁ : x ∈ W
hx₂ : x ∈ B.orthogonal W
n : V
hn : n ∈ W
⊢ ((B.restrict W) ⟨x, hx₁⟩) ⟨n, hn⟩ = 0

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
this : W ⊓ B.orthogonal W = ⊥
⊢ finrank K V ≤ finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤)

Tactic:
exact le_self_add

Result:
no goals

Proof state:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
⊢ W ⊓ B.orthogonal W ≤ ⊥

Tactic:
intro x hx

Result:
V : Type u_5
K : Type u_6
inst✝³ : Field K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
x : V
hx : x ∈ W ⊓ B.orthogonal W
⊢ x ∈ ⊥