awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
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
⊢ 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)
have 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' := sorry, map_smul' := sorry : 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' := sorry, map_smul' := sorry : 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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
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
⊢ 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)
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
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) (β := 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)
have 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)
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)]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
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
⊢ 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)
have 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)
Tactic: rw [← map_sub (⅟2 : Module.End R R), ← mul_sub, ← Module.End.smul_def]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
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
have refine : ∀ (s : Finset ι) (c : ι → R) (hc : Eq.{u_6 + 1} (α := M) (∑ i ∈ s, c i • v i) 0), ∀ i ∈ s, c i = 0
Tactic: refine linearIndependent_iff'.mpr fun s c hc ↦ ?_
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (hypothesis)
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
⊢ ∀ i ∈ s, c i = 0
have hx : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (hypothesis)
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
⊢ ∀ i ∈ s, c i = 0
have hy : 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
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
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 = y
have 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
Tactic: simp_rw [hx, hy, neg_smul, Finset.sum_neg_distrib, ← add_eq_zero_iff_eq_neg]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
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
⊢ HAdd.hAdd (α := M) (∑ i ∈ s with 0 < c i, c i • v i) (∑ x ∈ s with 0 < -c x, c x • v x) = 0
have h : {i ∈ s | 0 < c i} ∪ {i ∈ s | 0 < -c i} ⊆ s
Tactic: rw [← hc, ← Finset.sum_union, Finset.sum_subset]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
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
⊢ HAdd.hAdd (α := M) (∑ i ∈ s with 0 < c i, c i • v i) (∑ x ∈ s with 0 < -c x, c x • v x) = 0
have hf : ∀ x ∈ s, x ∉ {i ∈ s | 0 < c i} ∪ {i ∈ s | 0 < -c i} → c x • v x = 0
Tactic: rw [← hc, ← Finset.sum_union, Finset.sum_subset]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
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
⊢ HAdd.hAdd (α := M) (∑ i ∈ s with 0 < c i, c i • v i) (∑ x ∈ s with 0 < -c x, c x • v x) = 0
have rw : Disjoint ({i ∈ s | 0 < c i}) ({i ∈ s | 0 < -c i})
Tactic: rw [← hc, ← Finset.sum_union, Finset.sum_subset]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
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)
⊢ x = y
have 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))
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
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))
⊢ x = y
have 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)
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
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)
⊢ x = y
have 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
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
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
⊢ x = y
have h : {i ∈ s | 0 < c i} ∪ {i ∈ s | 0 < -c i} ⊆ s
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
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
⊢ x = y
have hf : ∀ x ∈ s, x ∉ {i ∈ s | 0 < c i} ∪ {i ∈ s | 0 < -c i} → c x • v x = 0
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]
-- Lean 4 proof step from Mathlib.LinearAlgebra.QuadraticForm.Dual (goal)
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
⊢ x = y
have simp_rw₅ : Disjoint ({i ∈ s | 0 < c i}) ({i ∈ s | 0 < -c i})
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]