-- Mathlib/FieldTheory/Finite/Polynomial.lean
theorem map_restrict_dom_evalₗ : (restrictDegree σ K (Fintype.card K - 1)).map (evalₗ K σ) = ⊤

Proof state:
case intro.refine_2.h
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ ∑ x : σ → K, e x • (evalₗ K σ) (indicator x) n = e n

Tactic:
simp only [evalₗ_apply]

Result:
case intro.refine_2.h
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ ∑ x : σ → K, e x • (eval n) (indicator x) = e n

Proof state:
case intro.refine_2.h
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ ∑ x : σ → K, e x • (eval n) (indicator x) = e n

Tactic:
trans

Result:
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ ∑ x : σ → K, e x • (eval n) (indicator x) = ?m.72446

K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ ?m.72446 = e n

K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ K

Proof state:
case intro
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1)) = ⊤

Tactic:
refine top_unique (SetLike.le_def.2 fun e _ => mem_map.2 ?_)

Result:
case intro
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ ∃ y ∈ restrictDegree σ K (Fintype.card K - 1), (evalₗ K σ) y = e

Proof state:
case intro.refine_1
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ ∑ n : σ → K, e n • indicator n ∈ restrictDegree σ K (Fintype.card K - 1)

Tactic:
exact sum_mem fun c _ => smul_mem _ _ (indicator_mem_restrictDegree _)

Result:
no goals

Proof state:
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ e n • (eval n) (indicator n) = e n

Tactic:
rw [eval_indicator_apply_eq_one, smul_eq_mul, mul_one]

Result:
no goals

Proof state:
case intro
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ ∃ y ∈ restrictDegree σ K (Fintype.card K - 1), (evalₗ K σ) y = e

Tactic:
refine ⟨∑ n : σ → K, e n • indicator n, ?_, ?_⟩

Result:
case intro.refine_1
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ ∑ n : σ → K, e n • indicator n ∈ restrictDegree σ K (Fintype.card K - 1)

case intro.refine_2
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ (evalₗ K σ) (∑ n : σ → K, e n • indicator n) = e

Proof state:
case refine_1
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝¹ : e ∈ ⊤
n b : σ → K
x✝ : b ∈ Finset.univ
h : b ≠ n
⊢ e b • (eval n) (indicator b) = 0

Tactic:
rw [eval_indicator_apply_eq_zero _ _ h.symm, smul_zero]

Result:
no goals

Proof state:
case refine_2
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ n ∉ Finset.univ → e n • (eval n) (indicator n) = 0

Tactic:
exact fun h => (h <| Finset.mem_univ n).elim

Result:
no goals

Proof state:
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
⊢ Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1)) = ⊤

Tactic:
cases nonempty_fintype σ

Result:
case intro
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
⊢ Submodule.map (evalₗ K σ) (restrictDegree σ K (Fintype.card K - 1)) = ⊤

Proof state:
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ ∑ x : σ → K, e x • (eval n) (indicator x) = ?m.72446

Tactic:
refine Finset.sum_eq_single n (fun b _ h => ?_) ?_

Result:
case refine_1
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝¹ : e ∈ ⊤
n b : σ → K
x✝ : b ∈ Finset.univ
h : b ≠ n
⊢ e b • (eval n) (indicator b) = 0

case refine_2
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ n ∉ Finset.univ → e n • (eval n) (indicator n) = 0

Proof state:
case intro.refine_2.h
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ (evalₗ K σ) (∑ n : σ → K, e n • indicator n) n = e n

Tactic:
simp only [_root_.map_sum, @Finset.sum_apply (σ → K) (fun _ => K) _ _ _ _ _, Pi.smul_apply,
  map_smul]

Result:
case intro.refine_2.h
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ ∑ x : σ → K, e x • (evalₗ K σ) (indicator x) n = e n

Proof state:
case intro.refine_2
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
⊢ (evalₗ K σ) (∑ n : σ → K, e n • indicator n) = e

Tactic:
ext n

Result:
case intro.refine_2.h
K : Type u_1
σ : Type u_2
inst✝² : Field K
inst✝¹ : Fintype K
inst✝ : Finite σ
val✝ : Fintype σ
e : (σ → K) → K
x✝ : e ∈ ⊤
n : σ → K
⊢ (evalₗ K σ) (∑ n : σ → K, e n • indicator n) n = e n