awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
z : M
hz : z ∈ p
h :
  Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
    ((B.restrict p : (a : ↥p) → ↥p →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz) :
      LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
    (0 : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
w : M
⊢ Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) w : R) ((0 : (a : M) → R) w : R)
have h₁ : ∀ (x y : M) (hx : x ∈ p) (hy : y ∈ q),
  Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) : (a : M) → R) (x + y) : R)
    ((0 : (a : M) → R) (x + y) : R)
Tactic: obtain ⟨x, y, hx, hy, rfl⟩ := Submodule.codisjoint_iff_exists_add_eq.mp hpq w
Cleared hypotheses: w
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p q : Submodule R M
hpq : Codisjoint p q
B : BilinForm R M
hB : ∀ x ∈ p, ∀ y ∈ q, Eq.{u_1 + 1} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
z : M
hz : z ∈ p
h : Eq (α := M →ₗ[R] R) ((B : (a : M) → M →ₗ[R] R) z : M →ₗ[R] R) (0 : M →ₗ[R] R)
⊢ Eq (α := LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
    ((B.restrict p : (a : ↥p) → ↥p →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz) :
      LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
    (0 : LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R)
have h₁ : ∀ (x : M) (hx : x ∈ p),
  Eq.{u_1 + 1} (α := R)
    ((((B.restrict p : (a : ↥p) → ↥p →ₗ[R] R) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) z hz) :
            LinearMap.{u_1, u_1, u_2, u_1} (RingHom.id R) (↥p) R) :
          (a : ↥p) → R)
        (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) :
      R)
    ((0 : (a : ↥p) → R) (Subtype.mk (p := fun (x : M) ↦ x ∈ p) x hx) : R)
Tactic: ext ⟨x, hx⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ v ∈ Submodule.map W.subtype (ker (B.restrict W))
have simp : 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: simp only [Submodule.mem_map, mem_ker, restrict_apply, Submodule.coe_subtype, Subtype.exists,
    exists_and_left, exists_prop, exists_eq_right_right]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ 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
have 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
Tactic: refine ⟨?_, hv⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ 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
have 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)
Tactic: ext ⟨w, hw⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ 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)
have 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 [← toLin_restrict_ker_eq_inf_ker _ _, ←
    toLin_restrict_range_dualCoannihilator_eq_orthogonal _ _, finrank_map_subtype_eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
| finrank K V + finrank.{u_6, u_5} K ↥(domRestrict B W).ker
have rw : finrank.{u_6, u_5} K ↥W + finrank.{u_6, u_5} K ↥(domRestrict B W).range.dualCoannihilator
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ 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
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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 ⊓ B.orthogonal ⊤)
have 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)
Tactic: rw [orthogonal_top_eq_ker b₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (hypothesis)
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 ↥(B.orthogonal W) = finrank K V - finrank.{u_6, u_5} K ↥W
have 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)
Tactic: have := finrank_add_finrank_orthogonal' (B := B) W
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (hypothesis)
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 ↥(B.orthogonal W) = finrank K V - finrank.{u_6, u_5} K ↥W
have this₁ : 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
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
⊢ B.orthogonal (B.orthogonal W) = W
have apply : finrank.{u_6, u_5} K ↥(B.orthogonal (B.orthogonal W)) ≤ finrank.{u_6, u_5} K ↥W
Tactic: apply (eq_of_le_of_finrank_le (LinearMap.BilinForm.le_orthogonal_orthogonal hB₀) _).symm
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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.{u_6, u_5} K ↥(B.orthogonal (B.orthogonal W)) ≤ finrank.{u_6, u_5} K ↥W
have simp : finrank K V - (finrank K V - finrank.{u_6, u_5} K ↥W) ≤ finrank.{u_6, u_5} K ↥W
Tactic: simp only [finrank_orthogonal hB]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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)
have refine : ∀ (h : Disjoint W (B.orthogonal W)), Codisjoint W (B.orthogonal W)
Tactic: refine ⟨IsCompl.disjoint, fun h ↦ ⟨h, ?_⟩⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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)
⊢ Codisjoint W (B.orthogonal W)
have rw : W ⊔ B.orthogonal W = ⊤
Tactic: rw [codisjoint_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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)
⊢ W ⊔ B.orthogonal W = ⊤
have apply : finrank K V ≤ finrank.{u_6, u_5} K ↥(W ⊔ B.orthogonal W)
Tactic: apply (eq_top_of_finrank_eq <| (finrank_le _).antisymm _)
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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 W)
have finrank : 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: 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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)
have 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)
Tactic: rw [finrank_sup_add_finrank_inf_eq, finrank_add_finrank_orthogonal hB₀ W]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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)
⊢ 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)
have 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 ⊤)
Tactic: rw [finrank_sup_add_finrank_inf_eq, finrank_add_finrank_orthogonal hB₀ W]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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 = ⊥
have rw : W ⊓ B.orthogonal W ≤ ⊥
Tactic: rw [eq_bot_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (hypothesis)
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
⊢ Membership.mem (γ := Submodule K V) ⊥ x
have hx₁ : x ∈ W
Tactic: obtain ⟨hx₁, hx₂⟩ := mem_inf.1 hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (hypothesis)
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
⊢ Membership.mem (γ := Submodule K V) ⊥ x
have hx₂ : x ∈ B.orthogonal W
Tactic: obtain ⟨hx₁, hx₂⟩ := mem_inf.1 hx
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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
have 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)
Tactic: refine Subtype.mk_eq_mk.1 (b₂.1 ⟨x, hx₁⟩ ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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.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)
have simp : Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) n : K) (0 : K)
Tactic: simp only [restrict_apply, domRestrict_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (hypothesis)
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
⊢ IsCompl W (B.orthogonal W)
have this : 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)))
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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)
have refine : finrank K V ≤ finrank.{u_6, u_5} K ↥(W ⊔ B.orthogonal W)
Tactic: refine IsCompl.of_eq this (eq_top_of_finrank_eq <| (finrank_le _).antisymm ?_)
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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.{u_6, u_5} K ↥(W ⊔ B.orthogonal W) + 0
have rw : finrank K V ≤ finrank K V + finrank.{u_6, u_5} K ↥(W ⊓ B.orthogonal ⊤)
Tactic: rw [← finrank_bot K V, ← this, finrank_sup_add_finrank_inf_eq,
    finrank_add_finrank_orthogonal b₁]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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.orthogonal W = ⊤ ↔ W = ⊥
have refine : ∀ (h : B.orthogonal W = ⊤), W = ⊥
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (hypothesis)
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 = ⊥
have this : W ⊓ B.orthogonal W = ⊥
Tactic: have := (B.isCompl_orthogonal_of_restrict_nondegenerate b₁ b₂).inf_eq_bot
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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 = ⊥
⊢ W = ⊥
have rwa : ∀ (this : W ⊓ ⊤ = ⊥), W = ⊥
Tactic: rwa [h, inf_top_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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 = ⊥
⊢ W = ⊥
have rwa₁ : ∀ (this : W = ⊥), W = ⊥
Tactic: rwa [h, inf_top_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (hypothesis)
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 = ⊤
have this : W ⊔ B.orthogonal W = ⊤
Tactic: have := (B.isCompl_orthogonal_of_restrict_nondegenerate b₁ b₂).sup_eq_top
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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 = ⊥
this : W ⊔ B.orthogonal W = ⊤
⊢ W = ⊤
have rwa : ∀ (this : W ⊔ ⊥ = ⊤), W = ⊤
Tactic: rwa [b₃, sup_bot_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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 = ⊥
this : W ⊔ B.orthogonal W = ⊤
rwa : ∀ (this : W ⊔ ⊥ = ⊤), W = ⊤
⊢ W = ⊤
have rwa₁ : ∀ (this : W = ⊤), W = ⊤
Tactic: rwa [b₃, sup_bot_eq] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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.Nondegenerate
⊢ B.orthogonal W = ⊥ ↔ W = ⊤
have refine : ∀ (h : W = ⊤), B.orthogonal W = ⊥
Tactic: refine ⟨eq_top_of_restrict_nondegenerate_of_orthogonal_eq_bot b₁ b₂, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
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.Nondegenerate
h : W = ⊤
⊢ B.orthogonal W = ⊥
have rw : B.orthogonal ⊤ ≤ ⊥
Tactic: rw [h, eq_bot_iff]
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (hypothesis)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
⊢ Nondegenerate (M := ↥(B.orthogonal (K ∙ x))) (B.restrict (B.orthogonal (K ∙ x)))
have this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
Tactic: have (n : V) : n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x) :=
    (span_singleton_sup_orthogonal_eq_top hx).symm ▸ Submodule.mem_top
-- Lean 4 proof step from Mathlib.LinearAlgebra.BilinearForm.Orthogonal (goal)
Goal:
V : Type u_5
K : Type u_6
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
B : BilinForm K V
b₁ : B.Nondegenerate
b₂ : B.IsRefl
x : V
hx : ¬B.IsOrtho x x
this : ∀ (n : V), n ∈ K ∙ x ⊔ B.orthogonal (K ∙ x)
⊢ Nondegenerate (M := ↥(B.orthogonal (K ∙ x))) (B.restrict (B.orthogonal (K ∙ x)))
have refine_1 : ∀ (m : ↥(B.orthogonal (K ∙ x)))
  (hm :
    ∀ (y : ↥(B.orthogonal (K ∙ x))),
      Eq.{u_6 + 1} (α := K)
        ((((B.restrict (B.orthogonal (K ∙ x)) : (a : ↥(B.orthogonal (K ∙ x))) → ↥(B.orthogonal (K ∙ x)) →ₗ[K] K) m :
                LinearMap.{u_6, u_6, u_5, u_6} (RingHom.id K) (↥(B.orthogonal (K ∙ x))) K) :
              (a : ↥(B.orthogonal (K ∙ x))) → K)
            y :
          K)
        (0 : K))
  (n : V), Eq.{u_6 + 1} (α := K) ((((B : (a : V) → V →ₗ[K] K) (↑m : V) : V →ₗ[K] K) : (a : V) → K) n : K) (0 : K)
Tactic: refine ⟨fun m hm => Submodule.coe_eq_zero.1 (b₁.1 m fun n ↦ ?_),
    fun m hm => Submodule.coe_eq_zero.1 (b₁.2 m fun n ↦ ?_)⟩