-- 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)))
y : V
c : K
hz : Membership.mem (γ := Submodule K V) (K ∙ x) (c • x)
rw :
  Eq.{v + 1} (α := K)
    ((((B : (a : V) → V →ₗ[K] K) (c • x) : V →ₗ[K] K) : (a : V) → K)
        (y +
          HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
              ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K) •
            x) :
      K)
    (0 : K)
rw₁ :
  Eq.{v + 1} (α := K)
    ((HSMul.hSMul (β := V →ₗ[K] K) c ((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K)
        (y +
          HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
              ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K) •
            x) :
      K)
    (0 : K)
rw₂ :
  HSMul.hSMul (β := K) c
      ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K)
          (y +
            HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
                ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K) •
              x) :
        K) =
    0
rw₃ :
  c •
      HAdd.hAdd (α := K) (β := K) ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
        ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K)
            (HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
                ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K) •
              x) :
          K) =
    0
rw₄ :
  c •
      HAdd.hAdd (α := K) ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
        (HSMul.hSMul (β := K)
          (HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
            ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K))
          ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K)) =
    0
rw₅ :
  c *
      HAdd.hAdd (α := K) ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
        (HSMul.hSMul (β := K)
          (HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
            ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K))
          ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K)) =
    0
rw₆ :
  c *
      HAdd.hAdd (α := K) ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
        (HMul.hMul (β := K)
          (HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
            ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K))
          ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K)) =
    0
rw₇ :
  c *
      HAdd.hAdd (α := K) (β := K) ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
        (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K) =
    0
rw₈ : c * 0 = 0
rw₉ rw₁₀ : Eq.{v + 1} (α := K) 0 0
⊢ IsOrtho B (c • x)
    (y +
      HDiv.hDiv (α := K) (β := K) (-(((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) y : K)
          ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K) x : K) •
        x)

Tactic:
rw [IsOrtho, map_smul, smul_apply, map_add, map_smul, smul_eq_mul, smul_eq_mul,
          div_mul_cancel₀ _ hx, add_neg_cancel, mul_zero]

Premises used: add_neg_cancel, div_mul_cancel₀, LinearMap.smul_apply, map_add, LinearMap.IsOrtho, MulZeroClass.mul_zero, smul_eq_mul, map_smul