Theorem: ZMod.totalDegree_f₁_add_totalDegree_f₂ (LeanCamCombi/ErdosGinzburgZiv.lean)

State before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ (ZMod.f₁ s).totalDegree + (ZMod.f₂ s).totalDegree < 2 * p - 1
Tactic:
refine (add_le_add (totalDegree_finset_sum _ _) $ (totalDegree_finset_sum _ _).trans $
  Finset.sup_mono_fun fun a _ ↦ totalDegree_smul_le _ _).trans_lt ?_
State after:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ ((s.toEnumFinset.attach.sup fun i => (X i ^ (p - 1)).totalDegree) +
      s.toEnumFinset.attach.sup fun a => (X a ^ (p - 1)).totalDegree) <
    2 * p - 1

State before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ ((s.toEnumFinset.attach.sup fun i => (X i ^ (p - 1)).totalDegree) +
      s.toEnumFinset.attach.sup fun a => (X a ^ (p - 1)).totalDegree) <
    2 * p - 1
Tactic:
simp only [totalDegree_X_pow, ← two_mul]
State after:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ (2 * s.toEnumFinset.attach.sup fun i => p - 1) < 2 * p - 1

State before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ (2 * s.toEnumFinset.attach.sup fun i => p - 1) < 2 * p - 1
Tactic:
refine (mul_le_mul_left' Finset.sup_const_le _).trans_lt ?_
State after:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ 2 * (p - 1) < 2 * p - 1

State before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ 2 * (p - 1) < 2 * p - 1
Tactic:
rw [mul_tsub, mul_one]
State after:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ 2 * p - 2 < 2 * p - 1

State before:
n p : ℕ
inst✝ : Fact p.Prime
s : Multiset (ZMod p)
⊢ 2 * p - 2 < 2 * p - 1
Tactic:
exact tsub_lt_tsub_left_of_le ((Fact.out : p.Prime).two_le.trans $
  le_mul_of_one_le_left' one_le_two) one_lt_two
State after:
no goals