awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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)))
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j_1 i_1 : Fin (d + 1)
i j : Fin d
hij : j.succ ≠ i.succ
⊢ Function.onFun (IsOrtho B)
    (Fin.cons (α := fun (i : Fin (d + 1)) ↦ V) x
      (Function.comp (β := ↥(Submodule.orthogonalBilin B (K ∙ x)))
        (Subtype.val (p := fun (x_1 : V) ↦ x_1 ∈ Submodule.orthogonalBilin B (K ∙ x)))
        (⇑v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x)))))
    j.succ i.succ
have succ : IsOrtho B (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) j) : V)
  (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) i) : V)
Tactic: simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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)))
b : Basis (Fin (d + 1)) K V := Basis.mkFinCons x v' ⋯ ⋯
j_1 i : Fin (d + 1)
j : Fin d
hij : j.succ ≠ 0
⊢ IsOrtho B (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) j) : V) x
have succ : Eq (α := K)
  ((RingHom.id K : (a : K) → K)
      ((((B : (a : V) → V →ₗ[K] K) x : V →ₗ[K] K) : (a : V) → K)
          (↑((v' : (a : Fin d) → ↥(Submodule.orthogonalBilin B (K ∙ x))) j) : V) :
        K) :
    K)
  (0 : K)
Tactic: rw [IsOrtho, ← hB₂.eq]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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
d : ℕ
hd : finrank K V = d
⊢ ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
have zero : ∀ {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 = 0), ∃ (v : Basis (Fin 0) K V), IsOrthoᵢ (n := Fin 0) B (⇑v : (a : Fin 0) → V)
Tactic: induction d generalizing V with
  | zero => exact ⟨basisOfFinrankZero hd, fun _ _ _ => map_zero _⟩
  | succ d ih =>
  -- either the bilinear form is trivial or we can pick a non-null `x`
  obtain rfl | hB₁ := eq_or_ne B 0
  · let b := Module.finBasis K V
    rw [hd] at b
    exact ⟨b, fun i j _ => rfl⟩
  obtain ⟨x, hx⟩ := exists_bilinForm_self_ne_zero hB₁ hB₂
  rw [← Submodule.finrank_add_eq_of_isCompl (isCompl_span_singleton_orthogonal hx).symm,
    finrank_span_singleton (ne_zero_of_map hx)] at hd
  let B' := B.domRestrict₁₂ ((K ∙ x).orthogonalBilin B) ((K ∙ x).orthogonalBilin B)
  obtain ⟨v', hv₁⟩ := ih (hB₂.domRestrict _ : B'.IsSymm) (Nat.succ.inj hd)
  -- concatenate `x` with the basis obtained by induction
  let b :=
    Basis.mkFinCons x v'
      (by
        rintro c y hy hc
        rw [add_eq_zero_iff_neg_eq] at hc
        rw [← hc, Submodule.neg_mem_iff] at hy
        have := (isCompl_span_singleton_orthogonal hx).disjoint
        rw [Submodule.disjoint_def] at this
        have := this (c • x) (Submodule.smul_mem _ _ <| Submodule.mem_span_singleton_self _) hy
        exact (smul_eq_zero.1 this).resolve_right fun h => hx <| h.symm ▸ map_zero _)
      (by
        intro y
        refine ⟨-B x y / B x x, fun z hz => ?_⟩
        obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.1 hz
        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])
  refine ⟨b, ?_⟩
  rw [Basis.coe_mkFinCons]
  intro j i
  refine Fin.cases ?_ (fun i => ?_) i <;> refine Fin.cases ?_ (fun j => ?_) j <;> intro hij <;>
    simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply]
  · exact (hij rfl).elim
  · rw [IsOrtho, ← hB₂.eq]
    exact (v' j).prop _ (Submodule.mem_span_singleton_self x)
  · exact (v' i).prop _ (Submodule.mem_span_singleton_self x)
  · exact hv₁ (ne_of_apply_ne _ hij)
Cleared hypotheses: V, inst_1, inst_2, inst_3, B, hB₂, d, hd
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
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
d : ℕ
hd : finrank K V = d
zero :
  ∀ {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 = 0), ∃ (v : Basis (Fin 0) K V), IsOrthoᵢ (n := Fin 0) B (⇑v : (a : Fin 0) → V)
⊢ ∃ (v : Basis (Fin d) K V), IsOrthoᵢ (n := Fin d) B (⇑v : (a : Fin d) → V)
have succ : ∀ (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_4 : AddCommGroup V] [inst_5 : Module K V] [FiniteDimensional K V] {B : BilinForm K V}
  (hB₂ : IsSymm B) (hd : finrank K V = d + 1),
  ∃ (v : Basis (Fin (d + 1)) K V), IsOrthoᵢ (n := Fin (d + 1)) B (⇑v : (a : Fin (d + 1)) → V)
Tactic: induction d generalizing V with
  | zero => exact ⟨basisOfFinrankZero hd, fun _ _ _ => map_zero _⟩
  | succ d ih =>
  -- either the bilinear form is trivial or we can pick a non-null `x`
  obtain rfl | hB₁ := eq_or_ne B 0
  · let b := Module.finBasis K V
    rw [hd] at b
    exact ⟨b, fun i j _ => rfl⟩
  obtain ⟨x, hx⟩ := exists_bilinForm_self_ne_zero hB₁ hB₂
  rw [← Submodule.finrank_add_eq_of_isCompl (isCompl_span_singleton_orthogonal hx).symm,
    finrank_span_singleton (ne_zero_of_map hx)] at hd
  let B' := B.domRestrict₁₂ ((K ∙ x).orthogonalBilin B) ((K ∙ x).orthogonalBilin B)
  obtain ⟨v', hv₁⟩ := ih (hB₂.domRestrict _ : B'.IsSymm) (Nat.succ.inj hd)
  -- concatenate `x` with the basis obtained by induction
  let b :=
    Basis.mkFinCons x v'
      (by
        rintro c y hy hc
        rw [add_eq_zero_iff_neg_eq] at hc
        rw [← hc, Submodule.neg_mem_iff] at hy
        have := (isCompl_span_singleton_orthogonal hx).disjoint
        rw [Submodule.disjoint_def] at this
        have := this (c • x) (Submodule.smul_mem _ _ <| Submodule.mem_span_singleton_self _) hy
        exact (smul_eq_zero.1 this).resolve_right fun h => hx <| h.symm ▸ map_zero _)
      (by
        intro y
        refine ⟨-B x y / B x x, fun z hz => ?_⟩
        obtain ⟨c, rfl⟩ := Submodule.mem_span_singleton.1 hz
        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])
  refine ⟨b, ?_⟩
  rw [Basis.coe_mkFinCons]
  intro j i
  refine Fin.cases ?_ (fun i => ?_) i <;> refine Fin.cases ?_ (fun j => ?_) j <;> intro hij <;>
    simp only [Function.onFun, Fin.cons_zero, Fin.cons_succ, Function.comp_apply]
  · exact (hij rfl).elim
  · rw [IsOrtho, ← hB₂.eq]
    exact (v' j).prop _ (Submodule.mem_span_singleton_self x)
  · exact (v' i).prop _ (Submodule.mem_span_singleton_self x)
  · exact hv₁ (ne_of_apply_ne _ hij)
Cleared hypotheses: V, inst_1, inst_2, inst_3, B, hB₂, d, hd
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
R : Type u_3
M : Type u_4
N : Type u_5
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_8
inst_5 : Fintype ι
v : Basis ι R M
Q : QuadraticMap R M N
w : ι → R
⊢ Eq.{u_5 + 1} (α := N) ((Q.basisRepr v : (a : ι → R) → N) w : N)
    ((Q : (a : M) → N) (∑ i : ι, HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)) : N)
have rw : Eq.{u_5 + 1} (α := N) ((Q.basisRepr v : (a : ι → R) → N) w : N)
  ((Q : (a : M) → N) ((v.equivFun.symm : (a : ι → R) → M) w : M) : N)
Tactic: rw [← v.equivFun_symm_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
ι : Type u_8
inst : Fintype ι
R : Type u_9
M : Type u_10
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Invertible (α := R) 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ :
  LinearMap.IsOrthoᵢ.{u_9, u_9, u_9, u_10, u_8} (R := R) (R₁ := R) (M := R) (M₁ := M) (n := ι) (I₁ := RingHom.id R)
    (I₁' := RingHom.id R)
    (((associated.{u_9, u_10, u_9} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)
    (⇑v : (a : ι) → M)
⊢ basisRepr Q v = weightedSumSquares (S := R) R fun (i : ι) ↦ (Q : (a : M) → R) ((v : (a : ι) → M) i : M)
have H : ∀ (w : ι → R),
  Eq.{u_9 + 1} (α := R) ((basisRepr Q v : (a : ι → R) → R) w : R)
    ((weightedSumSquares (S := R) R fun (i : ι) ↦ (Q : (a : M) → R) ((v : (a : ι) → M) i : M) : (a : ι → R) → R) w : R)
Tactic: ext w
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
ι : Type u_8
inst : Fintype ι
R : Type u_9
M : Type u_10
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Invertible (α := R) 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ :
  LinearMap.IsOrthoᵢ.{u_9, u_9, u_9, u_10, u_8} (R := R) (R₁ := R) (M := R) (M₁ := M) (n := ι) (I₁ := RingHom.id R)
    (I₁' := RingHom.id R)
    (((associated.{u_9, u_10, u_9} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)
    (⇑v : (a : ι) → M)
w : ι → R
⊢ Eq.{u_9 + 1} (α := R) ((basisRepr Q v : (a : ι → R) → R) w : R)
    ((weightedSumSquares (S := R) R fun (i : ι) ↦ (Q : (a : M) → R) ((v : (a : ι) → M) i : M) : (a : ι → R) → R) w : R)
have H : Eq.{u_9 + 1} (α := R)
  (∑ x : ι,
    (((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                  (a : QuadraticMap R M R) → BilinMap R M R)
                Q :
              BilinMap R M R) :
            (a : M) → M →ₗ[R] R)
          (∑ i : ι, HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)) :
        (a : M) → R)
      (HSMul.hSMul (β := M) (w x) ((v : (a : ι) → M) x : M)))
  (∑ i : ι, HSMul.hSMul (α := R) ((Q : (a : M) → R) ((v : (a : ι) → M) i : M) : R) (w i * w i))
Tactic: rw [basisRepr_apply, ← @associated_eq_self_apply R, map_sum, weightedSumSquares_apply]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
ι : Type u_8
inst : Fintype ι
R : Type u_9
M : Type u_10
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Invertible (α := R) 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ :
  LinearMap.IsOrthoᵢ.{u_9, u_9, u_9, u_10, u_8} (R := R) (R₁ := R) (M := R) (M₁ := M) (n := ι) (I₁ := RingHom.id R)
    (I₁' := RingHom.id R)
    (((associated.{u_9, u_10, u_9} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)
    (⇑v : (a : ι) → M)
w : ι → R
⊢ Eq.{u_9 + 1} (α := R)
    (∑ x : ι,
      (((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                    (a : QuadraticMap R M R) → BilinMap R M R)
                  Q :
                BilinMap R M R) :
              (a : M) → M →ₗ[R] R)
            (∑ i : ι, HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)) :
          (a : M) → R)
        (HSMul.hSMul (β := M) (w x) ((v : (a : ι) → M) x : M)))
    (∑ i : ι, HSMul.hSMul (α := R) ((Q : (a : M) → R) ((v : (a : ι) → M) i : M) : R) (w i * w i))
have H : ∀ (j : ι) (hj : Membership.mem (γ := Finset ι) univ j),
  (((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                  (a : QuadraticMap R M R) → BilinMap R M R)
                Q :
              BilinMap R M R) :
            (a : M) → M →ₗ[R] R)
          (∑ i : ι, HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)) :
        (a : M) → R)
      (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) ((v : (a : ι) → M) j : M) : R) (w j * w j)
Tactic: refine sum_congr rfl fun j hj => ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
ι : Type u_8
inst : Fintype ι
R : Type u_9
M : Type u_10
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Invertible (α := R) 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ :
  LinearMap.IsOrthoᵢ.{u_9, u_9, u_9, u_10, u_8} (R := R) (R₁ := R) (M := R) (M₁ := M) (n := ι) (I₁ := RingHom.id R)
    (I₁' := RingHom.id R)
    (((associated.{u_9, u_10, u_9} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)
    (⇑v : (a : ι) → M)
w : ι → R
j : ι
hj : Membership.mem (γ := Finset ι) univ j
⊢ (((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                  (a : QuadraticMap R M R) → BilinMap R M R)
                Q :
              BilinMap R M R) :
            (a : M) → M →ₗ[R] R)
          (∑ i : ι, HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)) :
        (a : M) → R)
      (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) ((v : (a : ι) → M) j : M) : R) (w j * w j)
have H : ((((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                  (a : QuadraticMap R M R) → BilinMap R M R)
                Q :
              BilinMap R M R) :
            (a : M) → M →ₗ[R] R)
          (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) :
        M →ₗ[R] R) :
      (a : M) → R)
    (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) =
  HSMul.hSMul (α := R)
    (((((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                      (a : QuadraticMap R M R) → BilinMap R M R)
                    Q :
                  BilinMap R M R) :
                (a : M) → M →ₗ[R] R)
              ((v : (a : ι) → M) j) :
            M →ₗ[R] R) :
          (a : M) → R)
        ((v : (a : ι) → M) j : M) :
      R)
    (w j * w j)
Tactic: rw [← @associated_eq_self_apply R, LinearMap.map_sum₂, sum_eq_single_of_mem j hj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
ι : Type u_8
inst : Fintype ι
R : Type u_9
M : Type u_10
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Invertible (α := R) 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ :
  LinearMap.IsOrthoᵢ.{u_9, u_9, u_9, u_10, u_8} (R := R) (R₁ := R) (M := R) (M₁ := M) (n := ι) (I₁ := RingHom.id R)
    (I₁' := RingHom.id R)
    (((associated.{u_9, u_10, u_9} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)
    (⇑v : (a : ι) → M)
w : ι → R
j : ι
hj : Membership.mem (γ := Finset ι) univ j
H :
  ((((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                    (a : QuadraticMap R M R) → BilinMap R M R)
                  Q :
                BilinMap R M R) :
              (a : M) → M →ₗ[R] R)
            (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) :
          M →ₗ[R] R) :
        (a : M) → R)
      (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) =
    HSMul.hSMul (α := R)
      (((((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) :
                          QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                        (a : QuadraticMap R M R) → BilinMap R M R)
                      Q :
                    BilinMap R M R) :
                  (a : M) → M →ₗ[R] R)
                ((v : (a : ι) → M) j) :
              M →ₗ[R] R) :
            (a : M) → R)
          ((v : (a : ι) → M) j : M) :
        R)
      (w j * w j)
⊢ (((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                  (a : QuadraticMap R M R) → BilinMap R M R)
                Q :
              BilinMap R M R) :
            (a : M) → M →ₗ[R] R)
          (∑ i : ι, HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)) :
        (a : M) → R)
      (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) =
    HSMul.hSMul (α := R) ((Q : (a : M) → R) ((v : (a : ι) → M) j : M) : R) (w j * w j)
have H₁ : ∀ (b : ι),
  Membership.mem (γ := Finset ι) univ b →
    b ≠ j →
      Eq.{u_9 + 1} (α := R)
        (((((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) :
                            QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                          (a : QuadraticMap R M R) → BilinMap R M R)
                        Q :
                      BilinMap R M R) :
                    (a : M) → M →ₗ[R] R)
                  (HSMul.hSMul (β := M) (w b) ((v : (a : ι) → M) b : M)) :
                M →ₗ[R] R) :
              (a : M) → R)
            (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) :
          R)
        (0 : R)
Tactic: rw [← @associated_eq_self_apply R, LinearMap.map_sum₂, sum_eq_single_of_mem j hj]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
ι : Type u_8
inst : Fintype ι
R : Type u_9
M : Type u_10
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Invertible (α := R) 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ :
  LinearMap.IsOrthoᵢ.{u_9, u_9, u_9, u_10, u_8} (R := R) (R₁ := R) (M := R) (M₁ := M) (n := ι) (I₁ := RingHom.id R)
    (I₁' := RingHom.id R)
    (((associated.{u_9, u_10, u_9} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)
    (⇑v : (a : ι) → M)
w : ι → R
j : ι
hj : Membership.mem (γ := Finset ι) univ j
⊢ ((((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                    (a : QuadraticMap R M R) → BilinMap R M R)
                  Q :
                BilinMap R M R) :
              (a : M) → M →ₗ[R] R)
            (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) :
          M →ₗ[R] R) :
        (a : M) → R)
      (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) =
    HSMul.hSMul (α := R)
      (((((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) :
                          QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                        (a : QuadraticMap R M R) → BilinMap R M R)
                      Q :
                    BilinMap R M R) :
                  (a : M) → M →ₗ[R] R)
                ((v : (a : ι) → M) j) :
              M →ₗ[R] R) :
            (a : M) → R)
          ((v : (a : ι) → M) j : M) :
        R)
      (w j * w j)
have H : w j *
    (w j *
      HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
        (HSub.hSub (β := R)
          (HSub.hSub (α := R) (β := R)
            ((Q : (a : M) → R) (HAdd.hAdd (α := M) (β := M) ((v : (a : ι) → M) j : M) ((v : (a : ι) → M) j : M)) : R)
            ((Q : (a : M) → R) ((v : (a : ι) → M) j : M) : R))
          ((Q : (a : M) → R) ((v : (a : ι) → M) j : M) : R))) =
  HSMul.hSMul (α := R) (@Invertible.invOf _ Distrib.toMul AddMonoidWithOne.toOne 2 _)
      (HSub.hSub (β := R)
        (HSub.hSub (α := R) (β := R)
          ((Q : (a : M) → R) (HAdd.hAdd (α := M) (β := M) ((v : (a : ι) → M) j : M) ((v : (a : ι) → M) j : M)) : R)
          ((Q : (a : M) → R) ((v : (a : ι) → M) j : M) : R))
        ((Q : (a : M) → R) ((v : (a : ι) → M) j : M) : R)) *
    (w j * w j)
Tactic: rw [map_smul, LinearMap.map_smul₂, smul_eq_mul, associated_apply, smul_eq_mul,
      smul_eq_mul, Module.End.smul_def, half_moduleEnd_apply_eq_half_smul]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basic (goal)
Goal:
ι : Type u_8
inst : Fintype ι
R : Type u_9
M : Type u_10
inst_1 : CommRing R
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Invertible (α := R) 2
Q : QuadraticForm R M
v : Basis ι R M
hv₂ :
  LinearMap.IsOrthoᵢ.{u_9, u_9, u_9, u_10, u_8} (R := R) (R₁ := R) (M := R) (M₁ := M) (n := ι) (I₁ := RingHom.id R)
    (I₁' := RingHom.id R)
    (((associated.{u_9, u_10, u_9} (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
        (a : QuadraticMap R M R) → BilinMap R M R)
      Q)
    (⇑v : (a : ι) → M)
w : ι → R
j : ι
hj : Membership.mem (γ := Finset ι) univ j
i : ι
h : Membership.mem (γ := Finset ι) univ i
hij : i ≠ j
⊢ Eq.{u_9 + 1} (α := R)
    (((((((associatedHom.{u_9, u_9, u_10, u_9} R (R := R) (M := M) (N := R) : QuadraticMap R M R →ₗ[R] BilinMap R M R) :
                      (a : QuadraticMap R M R) → BilinMap R M R)
                    Q :
                  BilinMap R M R) :
                (a : M) → M →ₗ[R] R)
              (HSMul.hSMul (β := M) (w i) ((v : (a : ι) → M) i : M)) :
            M →ₗ[R] R) :
          (a : M) → R)
        (HSMul.hSMul (β := M) (w j) ((v : (a : ι) → M) j : M)) :
      R)
    (0 : R)
have H : w j • HSMul.hSMul (β := R) (w i) 0 = 0
Tactic: rw [map_smul, LinearMap.map_smul₂, hv₂ hij]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Basis (goal)
Goal:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : AddCommGroup N
inst_3 : Module R M
inst_4 : Module R N
Q : QuadraticMap R M N
g : ι → M
l : ι →₀ R
⊢ (Q : (a : M) → N) ((linearCombination R g : (a : ι →₀ R) → M) l : M) =
    HSub.hSub (α := N) (β := N)
      ((linearCombination R (polarSym2 (⇑Q : (a : M) → N) ∘ Sym2.map g) : (a : Sym2 ι →₀ R) → N)
          (l.sym2Mul : Finsupp.{u_1, u_2} (Sym2 ι) R) :
        N)
      ((linearCombination R ((⇑Q : (a : M) → N) ∘ g) : (a : ι →₀ R) → N) (l * l) : N)
have simp_rw : HSub.hSub (α := N)
    (∑ p ∈ l.support.sym2,
      polarSym2.{u_3, u_4} (M := M) (⇑Q : (a : M) → N)
        (Sym2.map (fun (i : ι) ↦ HSMul.hSMul.{u_2, u_3, u_3} (α := R) ((l : (a : ι) → R) i : R) (g i)) p))
    (l.sum fun (i : ι) (a : R) ↦ a • HSMul.hSMul (β := N) a ((Q : (a : M) → N) (g i) : N)) =
  HSub.hSub (α := N)
    (sum (l.sym2Mul : Finsupp.{u_1, u_2} (Sym2 ι) R) fun (i : Sym2 ι) (a : R) ↦
      HSMul.hSMul (β := N) a ((polarSym2 (⇑Q : (a : M) → N) ∘ Sym2.map g) i))
    ((l * l).sum fun (i : ι) (a : R) ↦ HSMul.hSMul (β := N) a (((⇑Q : (a : M) → N) ∘ g) i))
Tactic: simp_rw [linearCombination_apply, map_finsuppSum', Q.map_smul, mul_smul]