awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
hs : HPow.hPow (β := ℕ) x 2 ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜)) 2
hs' : Ne.{u_3 + 1} (α := 𝕜) (↑(#s) : 𝕜) 0
⊢ (↑(#s) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    (↑(#s) : 𝕜) * HDiv.hDiv (α := 𝕜) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) (↑(#s) : 𝕜)
have hbc : HPow.hPow (β := ℕ) x 2 ≤ HDiv.hDiv (α := 𝕜) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) (↑(#s) : 𝕜)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
hs : HPow.hPow (β := ℕ) x 2 ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜)) 2
hs' : Ne.{u_3 + 1} (α := 𝕜) (↑(#s) : 𝕜) 0
⊢ LE.le.{u_3} (α := 𝕜) (∑ i ∈ s, HPow.hPow (β := ℕ) (f i) 2) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2)
have hf : ∀ i ∈ t, i ∉ s → 0 ≤ HPow.hPow (β := ℕ) (f i) 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
⊢ d + HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)
have inl : ∀ (hscard : Eq.{u_3 + 1} (α := 𝕜) 0 (↑(#s) : 𝕜)),
  d + HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)
Tactic: obtain hscard | hscard := ((#s).cast_nonneg : (0 : 𝕜) ≤ #s).eq_or_lt
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
inl :
  ∀ (hscard : Eq.{u_3 + 1} (α := 𝕜) 0 (↑(#s) : 𝕜)),
    d + HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
      HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)
⊢ d + HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)
have inr : ∀ (hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)),
  d + HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)
Tactic: obtain hscard | hscard := ((#s).cast_nonneg : (0 : 𝕜) ≤ #s).eq_or_lt
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (hypothesis)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
⊢ d + HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)
have htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
Tactic: have htcard : (0 : 𝕜) < #t := hscard.trans_le (Nat.cast_le.2 (card_le_card hst))
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (hypothesis)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
⊢ d + HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)
have h₁ : HPow.hPow (β := ℕ) x 2 ≤
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
Tactic: have h₁ : x ^ 2 ≤ ((∑ i ∈ s, f i) / #s - (∑ i ∈ t, f i) / #t) ^ 2 :=
    sq_le_sq.2 (by rwa [abs_of_nonneg hx])
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
⊢ HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
have apply : HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜)) 2
Tactic: apply h₁.trans
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
have rw : HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
  HPow.hPow (β := ℕ)
    (HSub.hSub (α := 𝕜) (∑ x ∈ s, f x) (∑ x ∈ s, HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) / (↑(#s) : 𝕜)) 2
Tactic: rw [sum_sub_distrib, sum_const, nsmul_eq_mul, sub_div, mul_div_cancel_left₀ _ hscard.ne']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
rw :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ)
      (HSub.hSub (α := 𝕜) (∑ x ∈ s, f x) (∑ x ∈ s, HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) / (↑(#s) : 𝕜)) 2
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
have rw₁ : HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
  HPow.hPow (β := ℕ) ((∑ x ∈ s, f x - #s • HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) / (↑(#s) : 𝕜)) 2
Tactic: rw [sum_sub_distrib, sum_const, nsmul_eq_mul, sub_div, mul_div_cancel_left₀ _ hscard.ne']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
rw :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ)
      (HSub.hSub (α := 𝕜) (∑ x ∈ s, f x) (∑ x ∈ s, HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) / (↑(#s) : 𝕜)) 2
rw₁ :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ) ((∑ x ∈ s, f x - #s • HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) / (↑(#s) : 𝕜)) 2
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
have rw₂ : HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
  HPow.hPow (β := ℕ) ((∑ x ∈ s, f x - (↑(#s) : 𝕜) * HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) / (↑(#s) : 𝕜)) 2
Tactic: rw [sum_sub_distrib, sum_const, nsmul_eq_mul, sub_div, mul_div_cancel_left₀ _ hscard.ne']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
rw :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ)
      (HSub.hSub (α := 𝕜) (∑ x ∈ s, f x) (∑ x ∈ s, HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) / (↑(#s) : 𝕜)) 2
rw₁ :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ) ((∑ x ∈ s, f x - #s • HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) / (↑(#s) : 𝕜)) 2
rw₂ :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ) ((∑ x ∈ s, f x - (↑(#s) : 𝕜) * HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) / (↑(#s) : 𝕜)) 2
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
have rw₃ : HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
  HPow.hPow (β := ℕ)
    (HDiv.hDiv (α := 𝕜) (∑ x ∈ s, f x) (↑(#s) : 𝕜) -
      (↑(#s) : 𝕜) * HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜) / (↑(#s) : 𝕜))
    2
Tactic: rw [sum_sub_distrib, sum_const, nsmul_eq_mul, sub_div, mul_div_cancel_left₀ _ hscard.ne']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
rw :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ)
      (HSub.hSub (α := 𝕜) (∑ x ∈ s, f x) (∑ x ∈ s, HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) / (↑(#s) : 𝕜)) 2
rw₁ :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ) ((∑ x ∈ s, f x - #s • HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) / (↑(#s) : 𝕜)) 2
rw₂ :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ) ((∑ x ∈ s, f x - (↑(#s) : 𝕜) * HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) / (↑(#s) : 𝕜)) 2
rw₃ :
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ)
      (HDiv.hDiv (α := 𝕜) (∑ x ∈ s, f x) (↑(#s) : 𝕜) -
        (↑(#s) : 𝕜) * HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜) / (↑(#s) : 𝕜))
      2
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
have rw₄ : HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 ≤
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
Tactic: rw [sum_sub_distrib, sum_const, nsmul_eq_mul, sub_div, mul_div_cancel_left₀ _ hscard.ne']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (hypothesis)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
⊢ d + HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)
have h₂ : HPow.hPow (β := ℕ) x 2 ≤
  HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜)) 2
Tactic: have h₂ : x ^ 2 ≤ ((∑ i ∈ s, (f i - (∑ j ∈ t, f j) / #t)) / #s) ^ 2 := by
    apply h₁.trans
    rw [sum_sub_distrib, sum_const, nsmul_eq_mul, sub_div, mul_div_cancel_left₀ _ hscard.ne']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
h₂ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
⊢ d + HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)
have inr : HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 +
    HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
  HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)
Tactic: grw [ht]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
h₂ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 +
      HDiv.hDiv (α := 𝕜) (↑(#s) : 𝕜) (↑(#t) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    HDiv.hDiv (α := 𝕜) (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) (↑(#t) : 𝕜)
have inr : HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 * (↑(#t) : 𝕜) +
    (↑(#s) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
  ∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2
Tactic: rw [← mul_div_right_comm, le_div_iff₀ htcard, add_mul, div_mul_cancel₀ _ htcard.ne']
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (hypothesis)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
h₂ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 * (↑(#t) : 𝕜) +
      (↑(#s) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    ∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2
have h₃ : (↑(#s) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
  ∑ i ∈ t, HPow.hPow (α := 𝕜) (β := ℕ) ((fun (i : ι) ↦ f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) i) 2
Tactic: have h₃ := mul_sq_le_sum_sq hst (fun i => (f i - (∑ j ∈ t, f j) / #t)) h₂ hscard.ne'
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
h₂ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
h₃ :
  (↑(#s) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    ∑ i ∈ t, HPow.hPow (α := 𝕜) (β := ℕ) ((fun (i : ι) ↦ f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) i) 2
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 * (↑(#t) : 𝕜) +
      (↑(#s) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    ∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2
have inr : HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 * (↑(#t) : 𝕜) +
    ∑ i ∈ t, HPow.hPow (α := 𝕜) (β := ℕ) ((fun (i : ι) ↦ f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) i) 2 ≤
  ∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2
Tactic: grw [h₃]
-- Lean 4 proof step from Mathlib.Combinatorics.SimpleGraph.Regularity.Bound (goal)
Goal:
ι : Type u_2
𝕜 : Type u_3
inst : Field 𝕜
inst_1 : LinearOrder 𝕜
inst_2 : IsStrictOrderedRing 𝕜
s t : Finset ι
x : 𝕜
hst : s ⊆ t
f : ι → 𝕜
d : 𝕜
hx : 0 ≤ x
hs : x ≤ |HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)|
ht : d ≤ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
hscard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#s) : 𝕜)
htcard : LT.lt.{u_3} (α := 𝕜) 0 (↑(#t) : 𝕜)
h₁ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, f i) (↑(#s) : 𝕜) - HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2
h₂ :
  HPow.hPow (β := ℕ) x 2 ≤
    HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ s, (f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜))) (↑(#s) : 𝕜))
      2
h₃ :
  (↑(#s) : 𝕜) * HPow.hPow (β := ℕ) x 2 ≤
    ∑ i ∈ t, HPow.hPow (α := 𝕜) (β := ℕ) ((fun (i : ι) ↦ f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) i) 2
⊢ HPow.hPow (β := ℕ) (HDiv.hDiv (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) 2 * (↑(#t) : 𝕜) +
      ∑ i ∈ t, HPow.hPow (α := 𝕜) (β := ℕ) ((fun (i : ι) ↦ f i - HDiv.hDiv (α := 𝕜) (∑ j ∈ t, f j) (↑(#t) : 𝕜)) i) 2 ≤
    ∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2
have inr : HPow.hPow (α := 𝕜) (β := ℕ) (∑ i ∈ t, f i) 2 * (↑(#t) : 𝕜) +
    ((∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#t) : 𝕜) 2 -
        (HMul.hMul (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜) + HMul.hMul (α := 𝕜) (∑ i ∈ t, f i) (↑(#t) : 𝕜)) * ∑ i ∈ t, f i +
      (↑(#t) : 𝕜) * HPow.hPow (α := 𝕜) (β := ℕ) (∑ i ∈ t, f i) 2) ≤
  (∑ i ∈ t, HPow.hPow (β := ℕ) (f i) 2) * HPow.hPow (α := 𝕜) (β := ℕ) (↑(#t) : 𝕜) 2
Tactic: simp only [sub_div' htcard.ne', div_pow, ← sum_div, ← mul_div_right_comm _ (#t : 𝕜), ← add_div,
    div_le_iff₀ (sq_pos_of_ne_zero htcard.ne'), sub_sq, sum_add_distrib, sum_const,
    sum_sub_distrib, mul_pow, ← sum_mul, nsmul_eq_mul, two_mul]