awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
htwo : Invertible (α := R) 2
B : BilinForm R M
Q : QuadraticMap R M R
hB₁ :
  Ne (α := BilinForm R M)
    (((QuadraticMap.associatedHom.{0, u_3, u_4, u_3} ℕ (R := R) (M := M) (N := R) :
            QuadraticMap R M R →ₗ[ℕ] BilinMap R M R) :
          (a : QuadraticMap R M R) → BilinMap R M R)
        Q :
      BilinMap R M R)
    (0 : BilinForm R M)
obtain :
  ∀ (x : M) (hx : Ne.{u_3 + 1} (α := R) ((Q : (a : M) → R) x : R) (0 : R)),
    ∃ (x : M),
      ¬IsOrtho.{u_3, u_3, u_3, u_3, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := R) (I₁ := RingHom.id R) (I₂ :=
          RingHom.id R)
          (((QuadraticMap.associatedHom.{0, u_3, u_4, u_3} ℕ (R := R) (M := M) (N := R) :
                QuadraticMap R M R →ₗ[ℕ] BilinMap R M R) :
              (a : QuadraticMap R M R) → BilinMap R M R)
            Q)
          x x
⊢ ∃ (x : M),
    ¬IsOrtho.{u_3, u_3, u_3, u_3, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := R) (I₁ := RingHom.id R) (I₂ :=
        RingHom.id R)
        (((QuadraticMap.associatedHom.{0, u_3, u_4, u_3} ℕ (R := R) (M := M) (N := R) :
              QuadraticMap R M R →ₗ[ℕ] BilinMap R M R) :
            (a : QuadraticMap R M R) → BilinMap R M R)
          Q)
        x x

Tactic:
obtain ⟨x, hx⟩ := QuadraticMap.exists_quadraticMap_ne_zero hB₁

Premises used: QuadraticMap.exists_quadraticMap_ne_zero
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
htwo : Invertible (α := R) 2
B : BilinForm R M
Q : QuadraticMap R M R
hB₁ :
  Ne (α := BilinForm R M)
    (((QuadraticMap.associatedHom.{0, u_3, u_4, u_3} ℕ (R := R) (M := M) (N := R) :
            QuadraticMap R M R →ₗ[ℕ] BilinMap R M R) :
          (a : QuadraticMap R M R) → BilinMap R M R)
        Q :
      BilinMap R M R)
    (0 : BilinForm R M)
x : M
hx : Ne.{u_3 + 1} (α := R) ((Q : (a : M) → R) x : R) (0 : R)
⊢ ∃ (x : M),
    ¬IsOrtho.{u_3, u_3, u_3, u_3, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := R) (I₁ := RingHom.id R) (I₂ :=
        RingHom.id R)
        (((QuadraticMap.associatedHom.{0, u_3, u_4, u_3} ℕ (R := R) (M := M) (N := R) :
              QuadraticMap R M R →ₗ[ℕ] BilinMap R M R) :
            (a : QuadraticMap R M R) → BilinMap R M R)
          Q)
        x x

Tactic:
⟨x, fun h => hx (Q.associated_eq_self_apply ℕ x ▸ h)⟩

Premises used: QuadraticMap.associated_eq_self_apply, Eq.rec, Nat, Exists.intro
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
R : Type u_3
M : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
htwo : Invertible (α := R) 2
B : BilinForm R M
Q : QuadraticMap R M R
hB₁ :
  Ne (α := BilinForm R M)
    (((QuadraticMap.associatedHom.{0, u_3, u_4, u_3} ℕ (R := R) (M := M) (N := R) :
            QuadraticMap R M R →ₗ[ℕ] BilinMap R M R) :
          (a : QuadraticMap R M R) → BilinMap R M R)
        Q :
      BilinMap R M R)
    (0 : BilinForm R M)
x : M
hx : Ne.{u_3 + 1} (α := R) ((Q : (a : M) → R) x : R) (0 : R)
⊢ ∃ (x : M),
    ¬IsOrtho.{u_3, u_3, u_3, u_3, u_4, u_4} (R := R) (R₁ := R) (R₂ := R) (M := R) (I₁ := RingHom.id R) (I₂ :=
        RingHom.id R)
        (((QuadraticMap.associatedHom.{0, u_3, u_4, u_3} ℕ (R := R) (M := M) (N := R) :
              QuadraticMap R M R →ₗ[ℕ] BilinMap R M R) :
            (a : QuadraticMap R M R) → BilinMap R M R)
          Q)
        x x

Tactic:
exact ⟨x, fun h => hx (Q.associated_eq_self_apply ℕ x ▸ h)⟩
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
V : Type u
K : Type v
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
hK : Invertible (α := K) 2
B : BilinForm K V
hB₂ : IsSymm B
this : ∀ (d : ℕ), finrank K V = d → ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
⊢ ∃ (v : Basis (Fin (finrank K V)) K V), IsOrthoᵢ (n := Fin (finrank K V)) B (⇑v : (a : Fin (finrank K V)) → V)

Tactic:
this _ rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
V : Type u
K : Type v
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
hK : Invertible (α := K) 2
B : BilinForm K V
hB₂ : IsSymm B
this : ∀ (d : ℕ), finrank K V = d → ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
⊢ ∃ (v : Basis (Fin (finrank K V)) K V), IsOrthoᵢ (n := Fin (finrank K V)) B (⇑v : (a : Fin (finrank K V)) → V)

Tactic:
exact this _ rfl

Premises used: rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
V : Type u
K : Type v
inst : Field K
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
hK : Invertible (α := K) 2
B : BilinForm K V
hB₂ : IsSymm B
suffices : ∀ (d : ℕ), finrank K V = d → ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
⊢ ∃ (v : Basis (Fin (finrank K V)) K V), IsOrthoᵢ (n := Fin (finrank K V)) B (⇑v : (a : Fin (finrank K V)) → V)

Tactic:
suffices ∀ d, finrank K V = d → ∃ v : Basis (Fin d) K V, B.IsOrthoᵢ v by exact this _ rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hd : finrank K V = 0
⊢ ∃ (v : Basis (Fin 0) K V), IsOrthoᵢ (n := Fin 0) B (⇑v : (a : Fin 0) → V)

Tactic:
⟨basisOfFinrankZero hd, fun _ _ _ => map_zero _⟩

Premises used: map_zero, basisOfFinrankZero, Exists.intro, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hd : finrank K V = 0
⊢ ∃ (v : Basis (Fin 0) K V), IsOrthoᵢ (n := Fin 0) B (⇑v : (a : Fin 0) → V)

Tactic:
exact ⟨basisOfFinrankZero hd, fun _ _ _ => map_zero _⟩
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hd : finrank K V = d + 1
succ :
  ∀ (hB₂ : IsSymm.{v, u} (R := K) (M := V) (I := RingHom.id K) 0),
    ∃ (v : Basis (Fin (d + 1)) K V),
      IsOrthoᵢ.{v, v, v, u, 0} (R := K) (R₁ := K) (M := K) (M₁ := V) (n := Fin (d + 1)) (I₁ := RingHom.id K) (I₁' :=
        RingHom.id K) 0 (⇑v : (a : Fin (d + 1)) → V)
succ₁ : ∀ (hB₁ : B ≠ 0), ∃ (v : Basis (Fin (d + 1)) K V), IsOrthoᵢ (n := Fin (d + 1)) B (⇑v : (a : Fin (d + 1)) → V)
⊢ ∃ (v : Basis (Fin (d + 1)) K V), IsOrthoᵢ (n := Fin (d + 1)) B (⇑v : (a : Fin (d + 1)) → V)

Tactic:
obtain rfl | hB₁ := eq_or_ne B 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
hd : finrank K V = d + 1
hB₂ : IsSymm.{v, u} (R := K) (M := V) (I := RingHom.id K) 0
b : Basis (Fin (finrank K V)) K V := finBasis K V
succ :
  ∀ (b : Basis (Fin (d + 1)) K V),
    ∃ (v : Basis (Fin (d + 1)) K V),
      IsOrthoᵢ.{v, v, v, u, 0} (R := K) (R₁ := K) (M := K) (M₁ := V) (n := Fin (d + 1)) (I₁ := RingHom.id K) (I₁' :=
        RingHom.id K) 0 (⇑v : (a : Fin (d + 1)) → V)
⊢ ∃ (v : Basis (Fin (d + 1)) K V),
    IsOrthoᵢ.{v, v, v, u, 0} (R := K) (R₁ := K) (M := K) (M₁ := V) (n := Fin (d + 1)) (I₁ := RingHom.id K) (I₁' :=
      RingHom.id K) 0 (⇑v : (a : Fin (d + 1)) → V)

Tactic:
rw [hd] at b
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
hd : finrank K V = d + 1
hB₂ : IsSymm.{v, u} (R := K) (M := V) (I := RingHom.id K) 0
b : Basis (Fin (d + 1)) K V
⊢ ∃ (v : Basis (Fin (d + 1)) K V),
    IsOrthoᵢ.{v, v, v, u, 0} (R := K) (R₁ := K) (M := K) (M₁ := V) (n := Fin (d + 1)) (I₁ := RingHom.id K) (I₁' :=
      RingHom.id K) 0 (⇑v : (a : Fin (d + 1)) → V)

Tactic:
⟨b, fun i j _ => rfl⟩

Premises used: Exists.intro, rfl
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
hd : finrank K V = d + 1
hB₂ : IsSymm.{v, u} (R := K) (M := V) (I := RingHom.id K) 0
b : Basis (Fin (d + 1)) K V
⊢ ∃ (v : Basis (Fin (d + 1)) K V),
    IsOrthoᵢ.{v, v, v, u, 0} (R := K) (R₁ := K) (M := K) (M₁ := V) (n := Fin (d + 1)) (I₁ := RingHom.id K) (I₁' :=
      RingHom.id K) 0 (⇑v : (a : Fin (d + 1)) → V)

Tactic:
exact ⟨b, fun i j _ => rfl⟩
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hd : finrank K V = d + 1
hB₁ : B ≠ 0
succ :
  ∀ (x : V) (hx : ¬IsOrtho B x x),
    ∃ (v : Basis (Fin (d + 1)) K V), IsOrthoᵢ (n := Fin (d + 1)) B (⇑v : (a : Fin (d + 1)) → V)
⊢ ∃ (v : Basis (Fin (d + 1)) K V), IsOrthoᵢ (n := Fin (d + 1)) B (⇑v : (a : Fin (d + 1)) → V)

Tactic:
obtain ⟨x, hx⟩ := exists_bilinForm_self_ne_zero hB₁ hB₂

Premises used: LinearMap.BilinForm.exists_bilinForm_self_ne_zero
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hd : finrank K V = d + 1
hB₁ : B ≠ 0
x : V
hx : ¬IsOrtho B x x
⊢ finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1

Tactic:
rw [← Submodule.finrank_add_eq_of_isCompl (isCompl_span_singleton_orthogonal hx).symm,
    finrank_span_singleton (ne_zero_of_map hx)] at hd

Premises used: ne_zero_of_map, finrank_span_singleton, LinearMap.isCompl_span_singleton_orthogonal, Submodule.finrank_add_eq_of_isCompl, IsCompl.symm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hd : finrank K V = d + 1
hB₁ : B ≠ 0
x : V
hx : ¬IsOrtho B x x
hd₁ : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
⊢ ¬IsOrtho B x x

Tactic:
rw [← Submodule.finrank_add_eq_of_isCompl (isCompl_span_singleton_orthogonal hx).symm,
    finrank_span_singleton (ne_zero_of_map hx)] at hd

Premises used: ne_zero_of_map, finrank_span_singleton, LinearMap.isCompl_span_singleton_orthogonal, Submodule.finrank_add_eq_of_isCompl, IsCompl.symm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
succ :
  ∀ (v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x)))
    (hv₁ :
      IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
        (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
        (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))),
    ∃ (v : Basis (Fin (d + 1)) K V), IsOrthoᵢ (n := Fin (d + 1)) B (⇑v : (a : Fin (d + 1)) → V)
⊢ ∃ (v : Basis (Fin (d + 1)) K V), IsOrthoᵢ (n := Fin (d + 1)) B (⇑v : (a : Fin (d + 1)) → V)

Tactic:
obtain ⟨v', hv₁⟩ := ih (hB₂.domRestrict _ : B'.IsSymm) (Nat.succ.inj hd)

Premises used: LinearMap.IsSymm.domRestrict, Nat.succ.inj
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ :
  IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
    (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
    (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))
c : K
y : V
hy : y ∈ Submodule.orthogonalBilin B (K ∙ x)
hc : c • x + y = 0
⊢ -(c • x) = y

Tactic:
rw [add_eq_zero_iff_neg_eq] at hc

Premises used: add_eq_zero_iff_neg_eq
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ :
  IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
    (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
    (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))
c : K
y : V
hy : y ∈ Submodule.orthogonalBilin B (K ∙ x)
hc : -(c • x) = y
⊢ c • x ∈ Submodule.orthogonalBilin B (K ∙ x)

Tactic:
rw [← hc, Submodule.neg_mem_iff] at hy

Premises used: Submodule.neg_mem_iff
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ :
  IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
    (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
    (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))
c : K
y : V
hy : y ∈ Submodule.orthogonalBilin B (K ∙ x)
hc : -(c • x) = y
hy₁ : c • x ∈ Submodule.orthogonalBilin B (K ∙ x)
⊢ -(c • x) = y

Tactic:
rw [← hc, Submodule.neg_mem_iff] at hy

Premises used: Submodule.neg_mem_iff
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ :
  IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
    (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
    (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))
c : K
y : V
hy : c • x ∈ Submodule.orthogonalBilin B (K ∙ x)
hc : -(c • x) = y
⊢ Disjoint (K ∙ x) (Submodule.orthogonalBilin B (K ∙ x))

Tactic:
have := (isCompl_span_singleton_orthogonal hx).disjoint
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ :
  IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
    (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
    (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))
c : K
y : V
hy : c • x ∈ Submodule.orthogonalBilin B (K ∙ x)
hc : -(c • x) = y
this : Disjoint (K ∙ x) (Submodule.orthogonalBilin B (K ∙ x))
⊢ ∀ (x_1 : V), Membership.mem (γ := Submodule K V) (K ∙ x) x_1 → x_1 ∈ Submodule.orthogonalBilin B (K ∙ x) → x_1 = 0

Tactic:
rw [Submodule.disjoint_def] at this

Premises used: Submodule.disjoint_def
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ :
  IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
    (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
    (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))
c : K
y : V
hy : c • x ∈ Submodule.orthogonalBilin B (K ∙ x)
hc : -(c • x) = y
this :
  ∀ (x_1 : V), Membership.mem (γ := Submodule K V) (K ∙ x) x_1 → x_1 ∈ Submodule.orthogonalBilin B (K ∙ x) → x_1 = 0
⊢ c • x = 0

Tactic:
have := this (c • x) (Submodule.smul_mem _ _ <| Submodule.mem_span_singleton_self _) hy
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Basic
Goal:
K : Type v
inst : Field K
hK : Invertible (α := K) 2
d : ℕ
ih :
  ∀ {V : Type u} [inst_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
    (hB₂ : IsSymm B) (hd : finrank K V = d), ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
V : Type u
inst_1 : AddCommGroup V
inst_2 : Module K V
inst_3 : FiniteDimensional K V
B : BilinForm K V
hB₂ : IsSymm B
hB₁ : B ≠ 0
x : V
hd : finrank.{v, u} K ↥(Submodule.orthogonalBilin B (K ∙ x)) + 1 = d + 1
hx : ¬IsOrtho B x x
B' : ↥(Submodule.orthogonalBilin B (K ∙ x)) →ₗ[K]
  LinearMap.{v, v, u, v} (RingHom.id K) (↥(Submodule.orthogonalBilin B (K ∙ x))) K :=
  domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x))
v' : Basis.{0, v, u} (Fin d) K ↥(Submodule.orthogonalBilin B (K ∙ x))
hv₁ :
  IsOrthoᵢ (M₁ := ↥(Submodule.orthogonalBilin B (K ∙ x))) (n := Fin d)
    (domRestrict₁₂ B (Submodule.orthogonalBilin B (K ∙ x)) (Submodule.orthogonalBilin B (K ∙ x)))
    (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))
c : K
y : V
hy : c • x ∈ Submodule.orthogonalBilin B (K ∙ x)
hc : -(c • x) = y
this_1 :
  ∀ (x_1 : V), Membership.mem (γ := Submodule K V) (K ∙ x) x_1 → x_1 ∈ Submodule.orthogonalBilin B (K ∙ x) → x_1 = 0
this : c • x = 0
⊢ c = 0

Tactic:
(smul_eq_zero.1 this).resolve_right fun h => hx <| h.symm ▸ map_zero _

Premises used: Eq.rec, map_zero, Iff.mp, Or.resolve_right, OfNat.ofNat, Eq.symm, DFunLike.coe, smul_eq_zero