awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 = y

Tactic:
replace hc : x = y := by
    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]
-- 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
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
hc : x = y
this : LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
⊢ x = 0

Tactic:
simpa [hc, ← hB.le_zero_iff, B.toQuadraticMap_apply]

Premises used: QuadraticMap.PosDef.le_zero_iff, LinearMap.BilinMap.toQuadraticMap_apply
-- 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
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
hc : x = y
suffices : LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)
⊢ x = 0

Tactic:
suffices B x y ≤ 0 by simpa [hc, ← hB.le_zero_iff, B.toQuadraticMap_apply]
-- 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
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
hc : x = y
this :
  LE.le.{u_5} (α := R) 0
    (∑ x ∈ s with c x < 0,
      ∑ i ∈ s with 0 < c i,
        c x * HMul.hMul (β := R) (c i) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v x) : R))
⊢ LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)

Tactic:
simpa [hx, hy, map_neg, Finset.mul_sum]

Premises used: Finset.mul_sum, map_neg
-- 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
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
hc : x = y
suffices :
  LE.le.{u_5} (α := R) 0
    (∑ x ∈ s with c x < 0,
      ∑ i ∈ s with 0 < c i,
        c x * HMul.hMul (β := R) (c i) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v x) : R))
⊢ LE.le.{u_5} (α := R) ((((B : (a : M) → M →ₗ[R] R) x : M →ₗ[R] R) : (a : M) → R) y : R) (0 : R)

Tactic:
suffices 0 ≤ ∑ x ∈ s with c x < 0, ∑ i ∈ s with 0 < c i, c x * (c i * (B (v i)) (v x)) by
      simpa [hx, hy, map_neg, Finset.mul_sum]
-- 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
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
hc : x = y
⊢ LE.le.{u_5} (α := R) 0
    (∑ x ∈ s with c x < 0,
      ∑ i ∈ s with 0 < c i,
        c x * HMul.hMul (β := R) (c i) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v x) : R))

Tactic:
Finset.sum_nonneg fun i hi ↦ Finset.sum_nonneg fun j hj ↦ ?_

Premises used: Finset.sum_nonneg
-- 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
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
hc : x = y
refine :
  ∀ (i : ι) (hi : i ∈ {x ∈ s | c x < 0}) (j : ι) (hj : j ∈ {i ∈ s | 0 < c i}),
    0 ≤ c i * HMul.hMul (β := R) (c j) ((((B : (a : M) → M →ₗ[R] R) (v j) : M →ₗ[R] R) : (a : M) → R) (v i) : R)
⊢ LE.le.{u_5} (α := R) 0
    (∑ x ∈ s with c x < 0,
      ∑ i ∈ s with 0 < c i,
        c x * HMul.hMul (β := R) (c i) ((((B : (a : M) → M →ₗ[R] R) (v i) : M →ₗ[R] R) : (a : M) → R) (v x) : R))

Tactic:
refine Finset.sum_nonneg fun i hi ↦ Finset.sum_nonneg fun j hj ↦ ?_

Premises used: Finset.sum_nonneg
-- 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
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
hc : x = y
i : ι
hi : i ∈ {x ∈ s | c x < 0}
j : ι
hj : j ∈ {i ∈ s | 0 < c i}
⊢ 0 ≤ c i * HMul.hMul (β := R) (c j) ((((B : (a : M) → M →ₗ[R] R) (v j) : M →ₗ[R] R) : (a : M) → R) (v i) : R)

Tactic:
grind [Pairwise, mul_nonneg_iff, mul_nonpos_iff]

Premises used: mul_nonneg_iff, mul_nonpos_iff, Pairwise
-- 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
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
hc : x = y
⊢ x = 0

Tactic:
have hx₀ : x = 0 := by
    suffices B x y ≤ 0 by simpa [hc, ← hB.le_zero_iff, B.toQuadraticMap_apply]
    suffices 0 ≤ ∑ x ∈ s with c x < 0, ∑ i ∈ s with 0 < c i, c x * (c i * (B (v i)) (v x)) by
      simpa [hx, hy, map_neg, Finset.mul_sum]
    refine Finset.sum_nonneg fun i hi ↦ Finset.sum_nonneg fun j hj ↦ ?_
    grind [Pairwise, mul_nonneg_iff, mul_nonpos_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_1 : ι → R
x : M := ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
hx : x = ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
y : M := ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hy : y = ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hc : x = y
hx₀ : x = 0
c : ι → R
h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0
i : ι
hi : i ∈ s
⊢ Eq.{u_5 + 1} (α := R) (∑ i ∈ s with 0 < c i, HMul.hMul (β := R) (c i) ((f : (a : M) → R) (v i) : R)) 0

Tactic:
simpa using (congr(f $h))

Premises used: congrArg, id, DFunLike.coe
-- 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_1 : ι → R
x : M := ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
hx : x = ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
y : M := ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hy : y = ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hc : x = y
hx₀ : x = 0
c : ι → R
h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0
i : ι
hi : i ∈ s
⊢ Eq.{u_5 + 1} (α := R) (∑ i ∈ s with 0 < c i, HMul.hMul (β := R) (c i) ((f : (a : M) → R) (v i) : R)) 0

Tactic:
have : ∑ i ∈ s with 0 < c i, c i * f (v i) = 0 := by simpa using (congr(f $h))
-- 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_1 : ι → R
x : M := ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
hx : x = ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
y : M := ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hy : y = ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hc : x = y
hx₀ : x = 0
c : ι → R
h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0
i : ι
hi : i ∈ s
this : Eq.{u_5 + 1} (α := R) (∑ i ∈ s with 0 < c i, HMul.hMul (β := R) (c i) ((f : (a : M) → R) (v i) : R)) 0
⊢ ∀ i ∈ {i ∈ s | 0 < c i}, 0 ≤ HMul.hMul (β := R) (c i) ((f : (a : M) → R) (v i) : R)

Tactic:
grind [mul_nonneg]

Premises used: mul_nonneg
-- 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_1 : ι → R
x : M := ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
hx : x = ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
y : M := ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hy : y = ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hc : x = y
hx₀ : x = 0
c : ι → R
h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0
i : ι
hi : i ∈ s
this : Eq.{u_5 + 1} (α := R) (∑ i ∈ s with 0 < c i, HMul.hMul (β := R) (c i) ((f : (a : M) → R) (v i) : R)) 0
⊢ ∀ i ∈ {i ∈ s | 0 < c i}, HMul.hMul (β := R) (c i) ((f : (a : M) → R) (v i) : R) = 0

Tactic:
rw [Finset.sum_eq_zero_iff_of_nonneg (by grind [mul_nonneg])] at this

Premises used: Finset.sum_eq_zero_iff_of_nonneg
-- 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_1 : ι → R
x : M := ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
hx : x = ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
y : M := ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hy : y = ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hc : x = y
hx₀ : x = 0
c : ι → R
h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0
i : ι
hi : i ∈ s
this : ∀ i ∈ {i ∈ s | 0 < c i}, HMul.hMul (β := R) (c i) ((f : (a : M) → R) (v i) : R) = 0
by_contra! : ∀ (hi' : 0 < c i), False
⊢ c i ≤ 0

Tactic:
by_contra! hi'
-- 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_1 : ι → R
x : M := ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
hx : x = ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
y : M := ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hy : y = ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hc : x = y
hx₀ : x = 0
c : ι → R
h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0
i : ι
hi : i ∈ s
this : ∀ i ∈ {i ∈ s | 0 < c i}, HMul.hMul (β := R) (c i) ((f : (a : M) → R) (v i) : R) = 0
hi' : 0 < c i
⊢ 0 < HMul.hMul (β := R) (c i) ((f : (a : M) → R) (v i) : R)

Tactic:
have : 0 < c i * f (v i) := mul_pos hi' (hp i)
-- 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_1 : ι → R
x : M := ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
hx : x = ∑ i ∈ s with 0 < c_1 i, c_1 i • v i
y : M := ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hy : y = ∑ i ∈ s with 0 < -c_1 i, -c_1 i • v i
hc : x = y
hx₀ : x = 0
c : ι → R
h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0
i : ι
hi : i ∈ s
this_1 : ∀ i ∈ {i ∈ s | 0 < c i}, HMul.hMul (β := R) (c i) ((f : (a : M) → R) (v i) : R) = 0
hi' : 0 < c i
this : 0 < HMul.hMul (β := R) (c i) ((f : (a : M) → R) (v i) : R)
⊢ False

Tactic:
grind
-- 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
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
hc : x = y
hx₀ : x = 0
⊢ ∀ (c : ι → R) (h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0) (i : ι) (hi : i ∈ s), c i ≤ 0

Tactic:
have H (c : ι → R) (h : ∑ i ∈ s with 0 < c i, c i • v i = 0) (i : ι) (hi : i ∈ s) : c i ≤ 0 := by
    have : ∑ i ∈ s with 0 < c i, c i * f (v i) = 0 := by simpa using (congr(f $h))
    rw [Finset.sum_eq_zero_iff_of_nonneg (by grind [mul_nonneg])] at this
    by_contra! hi'
    have : 0 < c i * f (v i) := mul_pos hi' (hp i)
    grind
-- 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
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
hc : x = y
hx₀ : x = 0
H : ∀ (c : ι → R) (h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0) (i : ι) (hi : i ∈ s), c i ≤ 0
i : ι
hi : i ∈ s
⊢ Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0

Tactic:
grind
-- 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
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
hc : x = y
hx₀ : x = 0
H : ∀ (c : ι → R) (h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0) (i : ι) (hi : i ∈ s), c i ≤ 0
⊢ ∀ (i : ι) (hi : i ∈ s), c i ≤ 0

Tactic:
replace hx (i : ι) (hi : i ∈ s) : c i ≤ 0 := H _ (by grind) i hi
-- 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
x : M := ∑ 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
hc : x = y
hx₀ : x = 0
H : ∀ (c : ι → R) (h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0) (i : ι) (hi : i ∈ s), c i ≤ 0
hx : ∀ (i : ι) (hi : i ∈ s), c i ≤ 0
i : ι
hi : i ∈ s
⊢ Eq.{u_6 + 1} (α := M)
    (∑ i ∈ s with LT.lt.{u_5} (α := R) 0 ((fun (x : ι) ↦ -c x) i),
      HSMul.hSMul.{u_5, u_6, u_6} (α := R) ((fun (x : ι) ↦ -c x) i) (v i))
    0

Tactic:
grind
-- 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
x : M := ∑ 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
hc : x = y
hx₀ : x = 0
H : ∀ (c : ι → R) (h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0) (i : ι) (hi : i ∈ s), c i ≤ 0
hx : ∀ (i : ι) (hi : i ∈ s), c i ≤ 0
⊢ ∀ (i : ι) (hi : i ∈ s), -c i ≤ 0

Tactic:
replace hy (i : ι) (hi : i ∈ s) : -c i ≤ 0 := H (-c ·) (by grind) i hi
-- 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
x : M := ∑ i ∈ s with 0 < c i, c i • v i
y : M := ∑ i ∈ s with 0 < -c i, -c i • v i
hc : x = y
hx₀ : x = 0
H : ∀ (c : ι → R) (h : Eq.{u_6 + 1} (α := M) (∑ i ∈ s with 0 < c i, c i • v i) 0) (i : ι) (hi : i ∈ s), c i ≤ 0
hx : ∀ (i : ι) (hi : i ∈ s), c i ≤ 0
hy : ∀ (i : ι) (hi : i ∈ s), -c i ≤ 0
⊢ ∀ i ∈ s, c i = 0

Tactic:
grind
-- Module: Mathlib.LinearAlgebra.QuadraticForm.Isometry
Goal:
R : Type u_1
M : Type u_2
M₁ : Type u_3
M₂ : Type u_4
M₃ : Type u_5
M₄ : Type u_6
N : Type u_7
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M₁
inst_3 : AddCommMonoid M₂
inst_4 : AddCommMonoid M₃
inst_5 : AddCommMonoid M₄
inst_6 : AddCommMonoid N
inst_7 : Module R M
inst_8 : Module R M₁
inst_9 : Module R M₂
inst_10 : Module R M₃
inst_11 : Module R M₄
inst_12 : Module R N
Q₁ : QuadraticMap R M₁ N
Q₂ : QuadraticMap R M₂ N
Q₃ : QuadraticMap R M₃ N
Q₄ : QuadraticMap R M₄ N
f g : Q₁ →qᵢ Q₂
h :
  Eq (α := (a : M₁) → M₂) ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂)) f)
    ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂)) g)
mk :
  ∀ (toLinearMap : M₁ →ₗ[R] M₂)
    (map_app' :
      ∀ (m : M₁), Eq.{u_7 + 1} (α := N) ((Q₂ : (a : M₂) → N) (toLinearMap.toFun m) : N) ((Q₁ : (a : M₁) → N) m : N))
    (h :
      Eq (α := (a : M₁) → M₂)
        ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂))
          { toLinearMap := toLinearMap, map_app' := map_app' })
        ((fun (f : Q₁ →qᵢ Q₂) ↦ ((⇑f.toLinearMap : (a : M₁) → M₂) : (a : M₁) → M₂)) g)),
    { toLinearMap := toLinearMap, map_app' := map_app' : Q₁ →qᵢ Q₂ } = g
⊢ f = g

Tactic:
cases f