awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) :=
  (↑e.symm : Module.Dual R (Module.Dual R M × M) →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M)) ∘ₗ
    dualProd R M
this : h_d = prodMap id (Module.Dual.eval R M)
⊢ Function.Injective (α := Module.Dual R M) (β := Module.Dual R M) (⇑id : (a : Module.Dual R M) → Module.Dual R M) ∧
      Function.Injective (α := M) (β := Module.Dual R (Module.Dual R M))
        (⇑(Module.Dual.eval R M) : (a : M) → Module.Dual R (Module.Dual R M)) ↔
    Function.Injective (α := M) (β := Module.Dual R (Module.Dual R M))
      (⇑(Module.Dual.eval R M) : (a : M) → Module.Dual R (Module.Dual R M))

Tactic:
and_iff_right Function.injective_id

Premises used: and_iff_right, Function.injective_id
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
e : (Module.Dual R M × Module.Dual R (Module.Dual R M)) ≃ₗ[R] Module.Dual R (Module.Dual R M × M) :=
  LinearEquiv.prodComm R (Module.Dual R M) (Module.Dual R (Module.Dual R M)) ≪≫ₗ
    Module.dualProdDualEquivDual R (Module.Dual R M) M
h_d : Module.Dual R M × M →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M) :=
  (↑e.symm : Module.Dual R (Module.Dual R M × M) →ₗ[R] Module.Dual R M × Module.Dual R (Module.Dual R M)) ∘ₗ
    dualProd R M
this : h_d = prodMap id (Module.Dual.eval R M)
⊢ Function.Injective (α := Module.Dual R M) (β := Module.Dual R M) (⇑id : (a : Module.Dual R M) → Module.Dual R M) ∧
      Function.Injective (α := M) (β := Module.Dual R (Module.Dual R M))
        (⇑(Module.Dual.eval R M) : (a : M) → Module.Dual R (Module.Dual R M)) ↔
    Function.Injective (α := M) (β := Module.Dual R (Module.Dual R M))
      (⇑(Module.Dual.eval R M) : (a : M) → Module.Dual R (Module.Dual R M))

Tactic:
exact and_iff_right Function.injective_id

Premises used: and_iff_right, Function.injective_id
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : Module R M
inst_4 : Module R N
a : R
p : Module.Dual R M × M
rw : (a • p.1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₁ : (a • p.1 : (a : M) → R) (a • p.2) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₂ :
  HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) (a • p.2) : R) =
    HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₃ :
  a • HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₄ :
  a * HSMul.hSMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₅ :
  a * HMul.hMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₆ : a * HMul.hMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = HMul.hMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)
rw₇ rw₈ :
  a * HMul.hMul (β := R) a ((p.1 : (a : M) → R) p.2 : R) = a * HMul.hMul (β := R) a ((p.1 : (a : M) → R) p.2 : R)
⊢ ((a • p).1 : (a : M) → R) (a • p).2 = HSMul.hSMul (β := R) (a * a) ((p.1 : (a : M) → R) p.2 : R)

Tactic:
rw [Prod.smul_fst, Prod.smul_snd, LinearMap.smul_apply, map_smul, smul_eq_mul,
      smul_eq_mul, smul_eq_mul, mul_assoc]

Premises used: LinearMap.smul_apply, mul_assoc, Prod.smul_snd, smul_eq_mul, map_smul, Prod.smul_fst
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
R : Type u_1
M : Type u_2
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
⊢ LinearMap.BilinMap.toQuadraticMap (LinearMap.dualProd R M) =
    HSMul.hSMul (α := ℕ) (β := QuadraticForm R (Module.Dual R M × M)) 2 (dualProd R M)

Tactic:
ext fun _a => (two_nsmul _).symm

Premises used: LinearMap.fst, LinearMap.applyₗ, QuadraticMap.ext, LinearMap.snd, LinearMap.comp, Eq.symm, DFunLike.coe, Module.Dual, LinearMap.compl₂, two_nsmul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
inst_3 : Invertible (α := R) 2
x : M × M
dsimp :
  Eq.{u_1 + 1} (α := R)
    ((dualProd R M : (a : Module.Dual R M × M) → R)
        (((HAdd.hAdd (α := M × M →ₗ[R] M →ₗ[R] R)
                  (({
                          toFun := fun (Q : QuadraticMap R M R) ↦
                            HSMul.hSMul (α := Module.End R R) (β := LinearMap.BilinMap R M R)
                              (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
                              (polarBilin.{u_1, u_2, u_1} (R := R) (M := M) (N := R) Q : LinearMap.BilinMap R M R),
                          map_add' := ⋯, map_smul' := ⋯ : QuadraticMap R M R →ₗ[R] LinearMap.BilinMap R M R } :
                        (a : QuadraticMap R M R) → LinearMap.BilinMap R M R)
                      Q ∘ₗ
                    LinearMap.fst R M M)
                  (({
                          toFun := fun (Q : QuadraticMap R M R) ↦
                            HSMul.hSMul (α := Module.End R R) (β := LinearMap.BilinMap R M R)
                              (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
                              (polarBilin.{u_1, u_2, u_1} (R := R) (M := M) (N := R) Q : LinearMap.BilinMap R M R),
                          map_add' := ⋯, map_smul' := ⋯ : QuadraticMap R M R →ₗ[R] LinearMap.BilinMap R M R } :
                        (a : QuadraticMap R M R) → LinearMap.BilinMap R M R)
                      Q ∘ₗ
                    LinearMap.snd R M M)).prod
              (HSub.hSub (α := M × M →ₗ[R] M) (LinearMap.fst R M M) (LinearMap.snd R M M))).toFun
          x) :
      R)
    ((prod Q (-Q) : (a : M × M) → R) x : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((dualProd R M : (a : Module.Dual R M × M) → R)
        (((HAdd.hAdd (α := M × M →ₗ[R] M →ₗ[R] R)
                  (((associated.{u_1, u_2, u_1} (R := R) (M := M) (N := R) :
                          QuadraticMap R M R →ₗ[R] LinearMap.BilinMap R M R) :
                        (a : QuadraticMap R M R) → LinearMap.BilinMap R M R)
                      Q ∘ₗ
                    LinearMap.fst R M M)
                  (((associated.{u_1, u_2, u_1} (R := R) (M := M) (N := R) :
                          QuadraticMap R M R →ₗ[R] LinearMap.BilinMap R M R) :
                        (a : QuadraticMap R M R) → LinearMap.BilinMap R M R)
                      Q ∘ₗ
                    LinearMap.snd R M M)).prod
              (HSub.hSub (α := M × M →ₗ[R] M) (LinearMap.fst R M M) (LinearMap.snd R M M))).toFun
          x) :
      R)
    ((prod Q (-Q) : (a : M × M) → R) x : R)

Tactic:
dsimp only [QuadraticMap.associated, QuadraticMap.associatedHom]

Premises used: QuadraticMap.associated, QuadraticMap.associatedHom
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
inst_3 : Invertible (α := R) 2
x : M × M
dsimp :
  HSMul.hSMul (α := Module.End R R) (β := R) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
        (polar (⇑Q : (a : M) → R) x.1 (x.1 - x.2)) +
      HSMul.hSMul (α := Module.End R R) (β := R) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
        (polar (⇑Q : (a : M) → R) x.2 (x.1 - x.2)) =
    HAdd.hAdd (α := R) (β := R) ((Q : (a : M) → R) x.1 : R) (-(Q : (a : M) → R) x.2 : R)
⊢ Eq.{u_1 + 1} (α := R)
    ((dualProd R M : (a : Module.Dual R M × M) → R)
        (((HAdd.hAdd (α := M × M →ₗ[R] M →ₗ[R] R)
                  (({
                          toFun := fun (Q : QuadraticMap R M R) ↦
                            HSMul.hSMul (α := Module.End R R) (β := LinearMap.BilinMap R M R)
                              (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
                              (polarBilin.{u_1, u_2, u_1} (R := R) (M := M) (N := R) Q : LinearMap.BilinMap R M R),
                          map_add' := ⋯, map_smul' := ⋯ : QuadraticMap R M R →ₗ[R] LinearMap.BilinMap R M R } :
                        (a : QuadraticMap R M R) → LinearMap.BilinMap R M R)
                      Q ∘ₗ
                    LinearMap.fst R M M)
                  (({
                          toFun := fun (Q : QuadraticMap R M R) ↦
                            HSMul.hSMul (α := Module.End R R) (β := LinearMap.BilinMap R M R)
                              (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
                              (polarBilin.{u_1, u_2, u_1} (R := R) (M := M) (N := R) Q : LinearMap.BilinMap R M R),
                          map_add' := ⋯, map_smul' := ⋯ : QuadraticMap R M R →ₗ[R] LinearMap.BilinMap R M R } :
                        (a : QuadraticMap R M R) → LinearMap.BilinMap R M R)
                      Q ∘ₗ
                    LinearMap.snd R M M)).prod
              (HSub.hSub (α := M × M →ₗ[R] M) (LinearMap.fst R M M) (LinearMap.snd R M M))).toFun
          x) :
      R)
    ((prod Q (-Q) : (a : M × M) → R) x : R)

Tactic:
dsimp only [LinearMap.smul_apply, LinearMap.coe_mk, AddHom.coe_mk, AddHom.toFun_eq_coe,
      LinearMap.coe_toAddHom, LinearMap.prod_apply, Function.prod_apply, LinearMap.add_apply,
      LinearMap.coe_comp, Function.comp_apply, LinearMap.fst_apply, LinearMap.snd_apply,
      LinearMap.sub_apply, dualProd_apply, polarBilin_apply_apply, prod_apply, neg_apply]

Premises used: LinearMap.coe_mk, QuadraticMap.neg_apply, LinearMap.smul_apply, LinearMap.add_apply, QuadraticMap.prod_apply, AddHom.toFun_eq_coe, QuadraticForm.dualProd_apply, LinearMap.fst_apply, LinearMap.coe_comp, LinearMap.coe_toAddHom, LinearMap.sub_apply, Function.prod_apply, Function.comp_apply, LinearMap.prod_apply, AddHom.coe_mk, LinearMap.snd_apply, QuadraticMap.polarBilin_apply_apply
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
inst_3 : Invertible (α := R) 2
x : M × M
simp :
  HSub.hSub (α := R) (β := R)
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : R) → R)
          (HMul.hMul (α := R) (β := R) (2 : R) ((Q : (a : M) → R) x.1 : R)) :
        R)
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : R) → R)
          (HMul.hMul (α := R) (β := R) (2 : R) ((Q : (a : M) → R) x.2 : R)) :
        R) =
    HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) x.1 : R) ((Q : (a : M) → R) x.2 : R)
⊢ HSMul.hSMul (α := Module.End R R) (β := R) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
        (polar (⇑Q : (a : M) → R) x.1 (x.1 - x.2)) +
      HSMul.hSMul (α := Module.End R R) (β := R) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
        (polar (⇑Q : (a : M) → R) x.2 (x.1 - x.2)) =
    HAdd.hAdd (α := R) (β := R) ((Q : (a : M) → R) x.1 : R) (-(Q : (a : M) → R) x.2 : R)

Tactic:
simp only [polar_sub_right, polar_self, nsmul_eq_mul, Nat.cast_ofNat, polar_comm _ x.1 x.2,
      smul_sub, Module.End.smul_def, sub_add_sub_cancel, ← sub_eq_add_neg (Q x.1) (Q x.2)]

Premises used: Nat.cast_ofNat, Module.End.smul_def, sub_add_sub_cancel, sub_eq_add_neg, QuadraticMap.polar_comm, QuadraticMap.polar_self, Prod.fst, smul_sub, QuadraticMap.polar_sub_right, nsmul_eq_mul, Prod.snd, DFunLike.coe
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
inst_3 : Invertible (α := R) 2
x : M × M
rw :
  HSMul.hSMul (α := Module.End R R) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (2 * HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) x.1 : R) ((Q : (a : M) → R) x.2 : R)) =
    HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) x.1 : R) ((Q : (a : M) → R) x.2 : R)
⊢ HSub.hSub (α := R) (β := R)
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : R) → R)
          (HMul.hMul (α := R) (β := R) (2 : R) ((Q : (a : M) → R) x.1 : R)) :
        R)
      ((@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _ : (a : R) → R)
          (HMul.hMul (α := R) (β := R) (2 : R) ((Q : (a : M) → R) x.2 : R)) :
        R) =
    HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) x.1 : R) ((Q : (a : M) → R) x.2 : R)

Tactic:
rw [← map_sub (⅟2 : Module.End R R), ← mul_sub, ← Module.End.smul_def]

Premises used: Module.End.smul_def, map_sub, mul_sub, Invertible.invOf, OfNat.ofNat
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
inst : CommRing R
inst_1 : AddCommGroup M
inst_2 : Module R M
Q : QuadraticForm R M
inst_3 : Invertible (α := R) 2
x : M × M
⊢ HSMul.hSMul (α := Module.End R R) (@Invertible.invOf _ Module.End.instMul Module.End.instOne 2 _)
      (2 * HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) x.1 : R) ((Q : (a : M) → R) x.2 : R)) =
    HSub.hSub (α := R) (β := R) ((Q : (a : M) → R) x.1 : R) ((Q : (a : M) → R) x.2 : R)

Tactic:
simp only [Module.End.smul_def, half_moduleEnd_apply_eq_half_smul, smul_eq_mul,
      invOf_mul_cancel_left']

Premises used: Module.End.smul_def, QuadraticMap.half_moduleEnd_apply_eq_half_smul, invOf_mul_cancel_left', smul_eq_mul
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
⊢ LinearIndependent R v

Tactic:
linearIndependent_iff'.mpr fun s c hc ↦ ?_

Premises used: Iff.mpr, linearIndependent_iff'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
refine : ∀ (s : Finset ι) (c : ι → R) (hc : Eq.{u_6 + 1} (α := M) (∑ i ∈ s, c i • v i) 0), ∀ i ∈ s, c i = 0
⊢ LinearIndependent R v

Tactic:
refine linearIndependent_iff'.mpr fun s c hc ↦ ?_

Premises used: Iff.mpr, linearIndependent_iff'
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c : ι → R
hc : Eq.{u_6 + 1} (α := M) (∑ i ∈ s, c i • v i) 0
⊢ let x : M := ∑ i ∈ s with 0 < c i, c i • v i;
  x = ∑ i ∈ s with 0 < c i, c i • v i

Tactic:
set x := ∑ i ∈ s with 0 < c i, c i • v i with hx
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c : ι → R
hc : Eq.{u_6 + 1} (α := M) (∑ i ∈ s, c i • v i) 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
⊢ let y : M := ∑ i ∈ s with 0 < -c i, -c i • v i;
  y = ∑ i ∈ s with 0 < -c i, -c i • v i

Tactic:
set y := ∑ i ∈ s with 0 < -c i, (-c i) • v i with hy
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c : ι → R
hc : Eq.{u_6 + 1} (α := M) (∑ i ∈ s, c i • v i) 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
simp_rw : HAdd.hAdd (α := M) (∑ i ∈ s with 0 < c i, c i • v i) (∑ x ∈ s with 0 < -c x, c x • v x) = 0
⊢ x = y

Tactic:
simp_rw [hx, hy, neg_smul, Finset.sum_neg_distrib, ← add_eq_zero_iff_eq_neg]

Premises used: neg_smul, add_eq_zero_iff_eq_neg, Finset.sum_neg_distrib
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c : ι → R
hc : Eq.{u_6 + 1} (α := M) (∑ i ∈ s, c i • v i) 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
h : {i ∈ s | 0 < c i} ∪ {i ∈ s | 0 < -c i} ⊆ s
hf : ∀ x ∈ s, x ∉ {i ∈ s | 0 < c i} ∪ {i ∈ s | 0 < -c i} → c x • v x = 0
rw : Disjoint ({i ∈ s | 0 < c i}) ({i ∈ s | 0 < -c i})
⊢ HAdd.hAdd (α := M) (∑ i ∈ s with 0 < c i, c i • v i) (∑ x ∈ s with 0 < -c x, c x • v x) = 0

Tactic:
rw [← hc, ← Finset.sum_union, Finset.sum_subset]

Premises used: Finset.sum_union, Finset.sum_subset
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c : ι → R
hc : Eq.{u_6 + 1} (α := M) (∑ i ∈ s, c i • v i) 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
⊢ {i ∈ s | 0 < c i} ∪ {i ∈ s | 0 < -c i} ⊆ s

Tactic:
grind only [= Finset.subset_iff, = Finset.mem_union, = Finset.mem_filter]

Premises used: Finset.subset_iff, Finset.mem_filter, Finset.mem_union
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c : ι → R
hc : Eq.{u_6 + 1} (α := M) (∑ i ∈ s, c i • v i) 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
⊢ ∀ x ∈ s, x ∉ {i ∈ s | 0 < c i} ∪ {i ∈ s | 0 < -c i} → c x • v x = 0

Tactic:
simp +contextual [eq_comm (a := (0 : R))]

Premises used: eq_comm
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c : ι → R
hc : Eq.{u_6 + 1} (α := M) (∑ i ∈ s, c i • v i) 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
⊢ Disjoint ({i ∈ s | 0 < c i}) ({i ∈ s | 0 < -c i})

Tactic:
grind only [Finset.disjoint_filter]

Premises used: Finset.disjoint_filter
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Dual
Goal:
ι : Type u_4
R : Type u_5
M : Type u_6
inst : CommRing R
inst_1 : LinearOrder R
inst_2 : IsStrictOrderedRing R
inst_3 : AddCommGroup M
inst_4 : Module R M
B : LinearMap.BilinForm R M
hB : (BilinMap.toQuadraticMap B).PosDef
f : Module.Dual R M
v : ι → M
hp : ∀ (i : ι), LT.lt.{u_5} (α := R) (0 : R) ((f : (a : M) → R) (v i) : R)
hn :
  Pairwise fun (i j : ι) ↦
    LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v j) : R) (0 : R)
s : Finset ι
c : ι → R
hc : Eq.{u_6 + 1} (α := M) (∑ i ∈ s, c i • v i) 0
x : M := ∑ i ∈ s with 0 < c i, c i • v i
hx : x = ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hy : y = ∑ i ∈ s with 0 < -c i, -c i • v i
simp_rw : ∑ i ∈ s with 0 < c i, c i • v i = y
simp_rw₁ : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) (∑ i ∈ s with 0 < -c i, -c i • v i)
simp_rw₂ : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) (∑ x ∈ s with 0 < -c x, -(c x • v x))
simp_rw₃ : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) (-∑ x ∈ s with 0 < -c x, c x • v x)
simp_rw₄ : HAdd.hAdd (α := M) (∑ i ∈ s with 0 < c i, c i • v i) (∑ x ∈ s with 0 < -c x, c x • v x) = 0
h : {i ∈ s | 0 < c i} ∪ {i ∈ s | 0 < -c i} ⊆ s
hf : ∀ x ∈ s, x ∉ {i ∈ s | 0 < c i} ∪ {i ∈ s | 0 < -c i} → c x • v x = 0
simp_rw₅ : Disjoint ({i ∈ s | 0 < c i}) ({i ∈ s | 0 < -c i})
hf₁ : ∀ x ∈ s, x ∉ {i ∈ s | 0 < c i} ∪ {i ∈ s | 0 < -c i} → c x • v x = 0
simp_rw₆ simp_rw₇ : Disjoint ({i ∈ s | 0 < c i}) ({i ∈ s | 0 < -c i})
⊢ x = y

Tactic:
classical
    simp_rw [hx, hy, neg_smul, Finset.sum_neg_distrib, ← add_eq_zero_iff_eq_neg]
    rw [← hc, ← Finset.sum_union, Finset.sum_subset]
    · grind only [= Finset.subset_iff, = Finset.mem_union, = Finset.mem_filter]
    · simp +contextual [eq_comm (a := (0 : R))]
    · grind only [Finset.disjoint_filter]

Premises used: neg_smul, Finset.disjoint_filter, add_eq_zero_iff_eq_neg, Finset.sum_union, eq_comm, Finset.subset_iff, Finset.sum_subset, Finset.mem_filter, Finset.mem_union, Finset.sum_neg_distrib