-- Mathlib/FieldTheory/Finite/Polynomial.lean
theorem degrees_indicator (c : σ → K) :
    degrees (indicator c) ≤ ∑ s : σ, (Fintype.card K - 1) • {s}

Proof state:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ (X s).degrees ∪ (C (c s)).degrees ≤ {s}

Tactic:
rw [degrees_C, Multiset.union_zero]

Result:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ (X s).degrees ≤ {s}

Proof state:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ (∏ n : σ, (1 - (X n - C (c n)) ^ (Fintype.card K - 1))).degrees ≤ ∑ s : σ, (Fintype.card K - 1) • {s}

Tactic:
refine degrees_prod_le.trans <| Finset.sum_le_sum fun s _ ↦ degrees_sub_le.trans ?_

Result:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees 1 ∪ ((X s - C (c s)) ^ (Fintype.card K - 1)).degrees ≤ (Fintype.card K - 1) • {s}

Proof state:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ (X s - C (c s)).degrees ≤ {s}

Tactic:
refine degrees_sub_le.trans ?_

Result:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ (X s).degrees ∪ (C (c s)).degrees ≤ {s}

Proof state:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ ((X s - C (c s)) ^ (Fintype.card K - 1)).degrees ≤ (Fintype.card K - 1) • {s}

Tactic:
refine le_trans degrees_pow_le (nsmul_le_nsmul_right ?_ _)

Result:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ (X s - C (c s)).degrees ≤ {s}

Proof state:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ (indicator c).degrees ≤ ∑ s : σ, (Fintype.card K - 1) • {s}

Tactic:
rw [indicator]

Result:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ (∏ n : σ, (1 - (X n - C (c n)) ^ (Fintype.card K - 1))).degrees ≤ ∑ s : σ, (Fintype.card K - 1) • {s}

Proof state:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
⊢ (∏ n : σ, (1 - (X n - C (c n)) ^ (Fintype.card K - 1))).degrees ≤ ∑ s : σ, (Fintype.card K - 1) • {s}

Tactic:
classical
refine degrees_prod_le.trans <| Finset.sum_le_sum fun s _ ↦ degrees_sub_le.trans ?_
rw [degrees_one, Multiset.zero_union]
refine le_trans degrees_pow_le (nsmul_le_nsmul_right ?_ _)
refine degrees_sub_le.trans ?_
rw [degrees_C, Multiset.union_zero]
exact degrees_X' _

Result:
no goals

Proof state:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ degrees 1 ∪ ((X s - C (c s)) ^ (Fintype.card K - 1)).degrees ≤ (Fintype.card K - 1) • {s}

Tactic:
rw [degrees_one, Multiset.zero_union]

Result:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ ((X s - C (c s)) ^ (Fintype.card K - 1)).degrees ≤ (Fintype.card K - 1) • {s}

Proof state:
K : Type u_1
σ : Type u_2
inst✝² : Fintype K
inst✝¹ : Fintype σ
inst✝ : CommRing K
c : σ → K
s : σ
x✝ : s ∈ Finset.univ
⊢ (X s).degrees ≤ {s}

Tactic:
exact degrees_X' _

Result:
no goals