awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
W : Submodule R M
b₁ : B.IsRefl
v : M
hv : v ∈ W
hv' : v ∈ B.orthogonal W
refine : Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥W) R) (domRestrict ((B : (a : M) → M →ₗ[R] R) v) W) 0
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥W) R) (domRestrict ((B : (a : M) → M →ₗ[R] R) v) W) 0 ∧ v ∈ W

Tactic:
refine ⟨?_, hv⟩
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
W : Submodule R M
b₁ : B.IsRefl
v : M
hv : v ∈ W
hv' : v ∈ B.orthogonal W
h :
  ∀ (w : M) (hw : w ∈ W),
    Eq.{u_1 + 1} (α := R)
      ((domRestrict ((B : (a : M) → M →ₗ[R] R) v) W : (a : ↥W) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) w hw) : R)
      ((0 : (a : ↥W) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) w hw) : R)
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥W) R) (domRestrict ((B : (a : M) → M →ₗ[R] R) v) W) 0

Tactic:
ext ⟨w, hw⟩
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
W : Submodule R M
b₁ : B.IsRefl
v : M
hv : v ∈ W
hv' : v ∈ B.orthogonal W
w : M
hw : w ∈ W
⊢ Eq.{u_1 + 1} (α := R)
    ((domRestrict ((B : (a : M) → M →ₗ[R] R) v) W : (a : ↥W) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) w hw) : R)
    ((0 : (a : ↥W) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) w hw) : R)

Tactic:
b₁ w v <| hv' w hw
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
B : BilinForm R M
W : Submodule R M
b₁ : B.IsRefl
v : M
hv : v ∈ W
hv' : v ∈ B.orthogonal W
w : M
hw : w ∈ W
⊢ Eq.{u_1 + 1} (α := R)
    ((domRestrict ((B : (a : M) → M →ₗ[R] R) v) W : (a : ↥W) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) w hw) : R)
    ((0 : (a : ↥W) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ W) w hw) : R)

Tactic:
exact b₁ w v <| hv' w hw
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
rw :
  finrank.{u_6, u_5} K ↥W + finrank.{u_6, u_5} K ↥(domRestrict B W).range.dualCoannihilator =
    finrank K V + finrank.{u_6, u_5} K ↥(domRestrict B W).ker
⊢ finrank.{u_6, u_5} K ↥W + finrank.{u_6, u_5} K ↥(B.orthogonal W) = finrank K V + finrank.{u_6, u_5} K ↥(W ⊓ ker B)

Tactic:
rw [← toLin_restrict_ker_eq_inf_ker _ _, ←
    toLin_restrict_range_dualCoannihilator_eq_orthogonal _ _, finrank_map_subtype_eq]

Premises used: LinearMap.BilinForm.toLin_restrict_ker_eq_inf_ker, Submodule.finrank_map_subtype_eq, LinearMap.BilinForm.toLin_restrict_range_dualCoannihilator_eq_orthogonal
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
rw : finrank.{u_6, u_5} K ↥W + finrank.{u_6, u_5} K ↥(domRestrict B W).range.dualCoannihilator
| finrank K V + finrank.{u_6, u_5} K ↥(domRestrict B W).ker

Tactic:
rw [← @Subspace.finrank_add_finrank_dualCoannihilator_eq K V _ _ _ _
        (LinearMap.range (B.domRestrict W)),
      add_comm, ← add_assoc, add_comm (finrank K (LinearMap.ker (B.domRestrict W))),
      LinearMap.finrank_range_add_finrank_ker]

Premises used: add_assoc, LinearMap.ker, Membership.mem, LinearMap.range, Subtype, add_comm, Subspace.finrank_add_finrank_dualCoannihilator_eq, LinearMap.domRestrict, LinearMap.finrank_range_add_finrank_ker, Module.finrank
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
conv_rhs :
  finrank.{u_6, u_5} K ↥W + finrank.{u_6, u_5} K ↥(domRestrict B W).range.dualCoannihilator =
    finrank K V + finrank.{u_6, u_5} K ↥(domRestrict B W).ker
conv_rhs₁ :
  finrank.{u_6, u_5} K ↥W + finrank.{u_6, u_5} K ↥(domRestrict B W).range.dualCoannihilator =
    finrank.{u_6, u_5} K ↥W + finrank.{u_6, u_5} K ↥(domRestrict B W).range.dualCoannihilator
⊢ finrank.{u_6, u_5} K ↥W + finrank.{u_6, u_5} K ↥(domRestrict B W).range.dualCoannihilator =
    finrank K V + finrank.{u_6, u_5} K ↥(domRestrict B W).ker

Tactic:
conv_rhs =>
    rw [← @Subspace.finrank_add_finrank_dualCoannihilator_eq K V _ _ _ _
        (LinearMap.range (B.domRestrict W)),
      add_comm, ← add_assoc, add_comm (finrank K (LinearMap.ker (B.domRestrict W))),
      LinearMap.finrank_range_add_finrank_ker]

Premises used: add_assoc, LinearMap.ker, Membership.mem, LinearMap.range, Subtype, add_comm, Subspace.finrank_add_finrank_dualCoannihilator_eq, LinearMap.domRestrict, LinearMap.finrank_range_add_finrank_ker, Module.finrank
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
b₁ : B.IsRefl
W : Submodule K V
rw : finrank.{u_6, u_5} K ↥W + finrank.{u_6, u_5} K ↥(B.orthogonal W) = finrank K V + finrank.{u_6, u_5} K ↥(W ⊓ ker B)
⊢ finrank.{u_6, u_5} K ↥W + finrank.{u_6, u_5} K ↥(B.orthogonal W) =
    finrank K V + finrank.{u_6, u_5} K ↥(W ⊓ B.orthogonal ⊤)

Tactic:
rw [orthogonal_top_eq_ker b₁]

Premises used: LinearMap.BilinForm.orthogonal_top_eq_ker
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
b₁ : B.IsRefl
W : Submodule K V
⊢ finrank.{u_6, u_5} K ↥W + finrank.{u_6, u_5} K ↥(B.orthogonal W) = finrank K V + finrank.{u_6, u_5} K ↥(W ⊓ ker B)

Tactic:
finrank_add_finrank_orthogonal' _

Premises used: Set.Mem, LinearMap.BilinForm.finrank_add_finrank_orthogonal'
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
b₁ : B.IsRefl
W : Submodule K V
⊢ finrank.{u_6, u_5} K ↥W + finrank.{u_6, u_5} K ↥(B.orthogonal W) = finrank K V + finrank.{u_6, u_5} K ↥(W ⊓ ker B)

Tactic:
exact finrank_add_finrank_orthogonal' _

Premises used: LinearMap.BilinForm.finrank_add_finrank_orthogonal'
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
W : Submodule K V
⊢ finrank.{u_6, u_5} K ↥W + finrank.{u_6, u_5} K ↥(B.orthogonal W) = finrank K V + finrank.{u_6, u_5} K ↥(W ⊓ ker B)

Tactic:
have := finrank_add_finrank_orthogonal' (B := B) W
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
W : Submodule K V
this :
  finrank.{u_6, u_5} K ↥W + finrank.{u_6, u_5} K ↥(B.orthogonal W) = finrank K V + finrank.{u_6, u_5} K ↥(W ⊓ ker B)
⊢ finrank.{u_6, u_5} K ↥W + finrank.{u_6, u_5} K ↥(B.orthogonal W) = finrank K V

Tactic:
rw [hB.ker_eq_bot, inf_bot_eq, finrank_bot, add_zero] at this

Premises used: inf_bot_eq, LinearMap.BilinForm.Nondegenerate.ker_eq_bot, finrank_bot, add_zero
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
W : Submodule K V
this : finrank.{u_6, u_5} K ↥W + finrank.{u_6, u_5} K ↥(B.orthogonal W) = finrank K V
⊢ finrank.{u_6, u_5} K ↥(B.orthogonal W) = finrank K V - finrank.{u_6, u_5} K ↥W

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
hB₀ : B.IsRefl
W : Submodule K V
apply : finrank.{u_6, u_5} K ↥(B.orthogonal (B.orthogonal W)) ≤ finrank.{u_6, u_5} K ↥W
⊢ B.orthogonal (B.orthogonal W) = W

Tactic:
apply (eq_of_le_of_finrank_le (LinearMap.BilinForm.le_orthogonal_orthogonal hB₀) _).symm

Premises used: Submodule.eq_of_le_of_finrank_le, LinearMap.BilinForm.le_orthogonal_orthogonal, Eq.symm
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
hB₀ : B.IsRefl
W : Submodule K V
simp : finrank K V - (finrank K V - finrank.{u_6, u_5} K ↥W) ≤ finrank.{u_6, u_5} K ↥W
⊢ finrank.{u_6, u_5} K ↥(B.orthogonal (B.orthogonal W)) ≤ finrank.{u_6, u_5} K ↥W

Tactic:
simp only [finrank_orthogonal hB]

Premises used: LinearMap.BilinForm.finrank_orthogonal
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB : B.Nondegenerate
hB₀ : B.IsRefl
W : Submodule K V
⊢ finrank K V - (finrank K V - finrank.{u_6, u_5} K ↥W) ≤ finrank.{u_6, u_5} K ↥W

Tactic:
lia
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
hB₀ : B.IsRefl
⊢ IsCompl W (B.orthogonal W) ↔ Disjoint W (B.orthogonal W)

Tactic:
⟨IsCompl.disjoint, fun h ↦ ⟨h, ?_⟩⟩

Premises used: Iff.intro, IsCompl.mk, IsCompl.disjoint
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
hB₀ : B.IsRefl
refine : ∀ (h : Disjoint W (B.orthogonal W)), Codisjoint W (B.orthogonal W)
⊢ IsCompl W (B.orthogonal W) ↔ Disjoint W (B.orthogonal W)

Tactic:
refine ⟨IsCompl.disjoint, fun h ↦ ⟨h, ?_⟩⟩
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
hB₀ : B.IsRefl
h : Disjoint W (B.orthogonal W)
rw : W ⊔ B.orthogonal W = ⊤
⊢ Codisjoint W (B.orthogonal W)

Tactic:
rw [codisjoint_iff]

Premises used: codisjoint_iff
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
hB₀ : B.IsRefl
h : Disjoint W (B.orthogonal W)
apply : finrank K V ≤ finrank.{u_6, u_5} K ↥(W ⊔ B.orthogonal W)
⊢ W ⊔ B.orthogonal W = ⊤

Tactic:
apply (eq_top_of_finrank_eq <| (finrank_le _).antisymm _)

Premises used: LE.le.antisymm, Submodule.finrank_le, Submodule.eq_top_of_finrank_eq
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
hB₀ : B.IsRefl
h : Disjoint W (B.orthogonal W)
⊢ finrank K V ≤ finrank K V + finrank.{u_6, u_5} K ↥(W ⊓ B.orthogonal ⊤)

Tactic:
le_self_add

Premises used: le_self_add
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
hB₀ : B.IsRefl
h : Disjoint W (B.orthogonal W)
⊢ finrank K V + finrank.{u_6, u_5} K ↥(W ⊓ B.orthogonal ⊤) ≤
    finrank.{u_6, u_5} K ↥(W ⊔ B.orthogonal W) + finrank.{u_6, u_5} K ↥(W ⊓ B.orthogonal W)

Tactic:
?_
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
hB₀ : B.IsRefl
h : Disjoint W (B.orthogonal W)
⊢ finrank.{u_6, u_5} K ↥(W ⊔ B.orthogonal W) + finrank.{u_6, u_5} K ↥(W ⊓ B.orthogonal W) ≤
    finrank.{u_6, u_5} K ↥(W ⊔ B.orthogonal W)

Tactic:
simp [h.eq_bot]

Premises used: Disjoint.eq_bot
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
hB₀ : B.IsRefl
h : Disjoint W (B.orthogonal W)
finrank :
  Module.finrank K V + Module.finrank.{u_6, u_5} K ↥(W ⊓ B.orthogonal ⊤) ≤
    Module.finrank.{u_6, u_5} K ↥(W ⊔ B.orthogonal W) + Module.finrank.{u_6, u_5} K ↥(W ⊓ B.orthogonal W)
⊢ Module.finrank K V ≤ Module.finrank.{u_6, u_5} K ↥(W ⊔ B.orthogonal W)

Tactic:
calc
    finrank K V ≤ finrank K V + finrank K ↥(W ⊓ B.orthogonal ⊤) := le_self_add
    _ ≤ finrank K ↥(W ⊔ B.orthogonal W) + finrank K ↥(W ⊓ B.orthogonal W) := ?_
    _ ≤ finrank K ↥(W ⊔ B.orthogonal W) := by simp [h.eq_bot]

Premises used: Membership.mem, Subtype, Max.max, LinearMap.BilinForm.orthogonal, Top.top, le_self_add, Min.min, Module.finrank
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
hB₀ : B.IsRefl
h : Disjoint W (B.orthogonal W)
rw :
  finrank K V + finrank.{u_6, u_5} K ↥(W ⊓ B.orthogonal ⊤) ≤
    finrank.{u_6, u_5} K ↥W + finrank.{u_6, u_5} K ↥(B.orthogonal W)
rw₁ rw₂ :
  finrank K V + finrank.{u_6, u_5} K ↥(W ⊓ B.orthogonal ⊤) ≤ finrank K V + finrank.{u_6, u_5} K ↥(W ⊓ B.orthogonal ⊤)
⊢ finrank K V + finrank.{u_6, u_5} K ↥(W ⊓ B.orthogonal ⊤) ≤
    finrank.{u_6, u_5} K ↥(W ⊔ B.orthogonal W) + finrank.{u_6, u_5} K ↥(W ⊓ B.orthogonal W)

Tactic:
rw [finrank_sup_add_finrank_inf_eq, finrank_add_finrank_orthogonal hB₀ W]

Premises used: Submodule.finrank_sup_add_finrank_inf_eq, LinearMap.BilinForm.finrank_add_finrank_orthogonal
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
rw : W ⊓ B.orthogonal W ≤ ⊥
⊢ W ⊓ B.orthogonal W = ⊥

Tactic:
rw [eq_bot_iff]

Premises used: eq_bot_iff
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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 ∈ W

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

Premises used: Submodule.mem_inf, Iff.mp
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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
⊢ x ∈ B.orthogonal W

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

Premises used: Submodule.mem_inf, Iff.mp
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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
⊢ Membership.mem (γ := Submodule K V) ⊥ x

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

Premises used: Set.Mem, setOf, Subtype.mk, And.left, Set.singleton, Subtype.mk_eq_mk, Iff.mp
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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
refine :
  ∀ (y : ↥W),
    Eq.{u_6 + 1} (α := K)
      ((((B.restrict W : (a : ↥W) → ↥W →ₗ[K] K) (Subtype.mk (p := fun (x : V) ↦ x ∈ W) x hx₁) :
              LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥W) K) :
            (a : ↥W) → K)
          y :
        K)
      (0 : K)
⊢ Membership.mem (γ := Submodule K V) ⊥ x

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

Premises used: Subtype.mk, And.left, Subtype.mk_eq_mk, Iff.mp
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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
simp : Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) n : K) (0 : K)
⊢ Eq.{u_6 + 1} (α := K)
    ((((B.restrict W : (a : ↥W) → ↥W →ₗ[K] K) (Subtype.mk (p := fun (x : V) ↦ x ∈ W) x hx₁) :
            LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥W) K) :
          (a : ↥W) → K)
        (Subtype.mk (p := fun (x : V) ↦ x ∈ W) n hn) :
      K)
    (0 : K)

Tactic:
simp only [restrict_apply, domRestrict_apply]

Premises used: LinearMap.domRestrict_apply, LinearMap.BilinForm.restrict_apply
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) n : K) (0 : K)

Tactic:
b₁ n x (b₁ x n (b₁ n x (hx₂ n hn)))
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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
⊢ Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) n : K) (0 : K)

Tactic:
exact b₁ n x (b₁ x n (b₁ n x (hx₂ n hn)))
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
⊢ 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₂.1 ⟨x, hx₁⟩ ?_)
    rintro ⟨n, hn⟩
    simp only [restrict_apply, domRestrict_apply]
    exact b₁ n x (b₁ x n (b₁ n x (hx₂ n hn)))
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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:
IsCompl.of_eq this (eq_top_of_finrank_eq <| (finrank_le _).antisymm ?_)

Premises used: LE.le.antisymm, IsCompl.of_eq, Submodule.finrank_le, Submodule.eq_top_of_finrank_eq
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
this : W ⊓ B.orthogonal W = ⊥
refine : finrank K V ≤ finrank.{u_6, u_5} K ↥(W ⊔ B.orthogonal W)
⊢ IsCompl W (B.orthogonal W)

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

Premises used: LE.le.antisymm, IsCompl.of_eq, Submodule.finrank_le, Submodule.eq_top_of_finrank_eq
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
this : W ⊓ B.orthogonal W = ⊥
rw : finrank K V ≤ finrank K V + finrank.{u_6, u_5} K ↥(W ⊓ B.orthogonal ⊤)
⊢ finrank K V ≤ finrank.{u_6, u_5} K ↥(W ⊔ B.orthogonal W) + 0

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

Premises used: Submodule.finrank_sup_add_finrank_inf_eq, finrank_bot, LinearMap.BilinForm.finrank_add_finrank_orthogonal
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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.{u_6, u_5} K ↥(W ⊓ B.orthogonal ⊤)

Tactic:
le_self_add

Premises used: le_self_add
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : 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.{u_6, u_5} K ↥(W ⊓ B.orthogonal ⊤)

Tactic:
exact le_self_add

Premises used: le_self_add
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
⊢ (B.restrict W).Nondegenerate ↔ IsCompl W (B.orthogonal W)

Tactic:
⟨fun b₂ => isCompl_orthogonal_of_restrict_nondegenerate b₁ b₂, fun h =>
    B.nondegenerate_restrict_of_disjoint_orthogonal b₁ h.1⟩

Premises used: Iff.intro, IsCompl.disjoint, LinearMap.BilinForm.isCompl_orthogonal_of_restrict_nondegenerate, LinearMap.BilinForm.nondegenerate_restrict_of_disjoint_orthogonal
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
h : W = ⊥
⊢ B.orthogonal W = ⊤

Tactic:
simp [h]
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
refine : ∀ (h : B.orthogonal W = ⊤), W = ⊥
⊢ B.orthogonal W = ⊤ ↔ W = ⊥

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
h : B.orthogonal W = ⊤
⊢ W ⊓ B.orthogonal W = ⊥

Tactic:
have := (B.isCompl_orthogonal_of_restrict_nondegenerate b₁ b₂).inf_eq_bot
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
h : B.orthogonal W = ⊤
this : W ⊓ B.orthogonal W = ⊥
rwa : ∀ (this : W ⊓ ⊤ = ⊥), W = ⊥
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (this : W = ⊥), W = ⊥
⊢ W = ⊥

Tactic:
rwa [h, inf_top_eq] at this

Premises used: inf_top_eq
-- Module: Mathlib.LinearAlgebra.BilinearForm.Orthogonal
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
W : Submodule K V
b₁ : B.IsRefl
b₂ : (B.restrict W).Nondegenerate
b₃ : B.orthogonal W = ⊥
⊢ W ⊔ B.orthogonal W = ⊤

Tactic:
have := (B.isCompl_orthogonal_of_restrict_nondegenerate b₁ b₂).sup_eq_top