-- Mathlib/LinearAlgebra/Lagrange.lean
theorem nodal_subgroup_eq_X_pow_card_sub_one [IsDomain R]
  (G : Subgroup Rˣ) [Fintype G] :
  nodal (G : Set Rˣ).toFinset ((↑) : Rˣ → R) = X ^ (Fintype.card G) - 1

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
⊢ nodal (↑G).toFinset Units.val = X ^ Fintype.card ↥G - 1

Tactic:
have h : degree (1 : R[X]) < degree ((X : R[X]) ^ Fintype.card G) := by simp [Fintype.card_pos]

Result:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ nodal (↑G).toFinset Units.val = X ^ Fintype.card ↥G - 1

Proof state:
case hvs
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ Set.InjOn Units.val ↑(↑G).toFinset

Tactic:
exact Set.injOn_of_injective Units.ext

Result:
no goals

Proof state:
case h_eval
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
i : Rˣ
hi : i ∈ G
⊢ 0 = eval (↑i) (X ^ Fintype.card ↥G - 1)

Tactic:
obtain ⟨g, rfl⟩ : ∃ g : G, g.val = i := ⟨⟨i, hi⟩, rfl⟩

Result:
case h_eval.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
g : ↥G
hi : ↑g ∈ G
⊢ 0 = eval (↑↑g) (X ^ Fintype.card ↥G - 1)

Proof state:
case h_deg_eq
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ Fintype.card ↑↑G = Fintype.card ↥G

Tactic:
exact rfl

Result:
no goals

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
⊢ degree 1 < (X ^ Fintype.card ↥G).degree

Tactic:
simp [Fintype.card_pos]

Result:
no goals

Proof state:
case h_deg_le
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).degree ≤ ↑(#(↑G).toFinset)

Tactic:
simp

Result:
no goals

Proof state:
case h_eval
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
i : Rˣ
hi : i ∈ (↑G).toFinset
⊢ eval (↑i) (nodal (↑G).toFinset Units.val) = eval (↑i) (X ^ Fintype.card ↥G - 1)

Tactic:
rw [eval_nodal_at_node hi]

Result:
case h_eval
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
i : Rˣ
hi : i ∈ (↑G).toFinset
⊢ 0 = eval (↑i) (X ^ Fintype.card ↥G - 1)

Proof state:
case h_deg_eq
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).degree = (X ^ Fintype.card ↥G - 1).degree

Tactic:
rw [degree_sub_eq_left_of_degree_lt h, degree_nodal, Set.toFinset_card, degree_pow, degree_X,
  nsmul_eq_mul, mul_one, Nat.cast_inj]

Result:
case h_deg_eq
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ Fintype.card ↑↑G = Fintype.card ↥G

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ nodal (↑G).toFinset Units.val = X ^ Fintype.card ↥G - 1

Tactic:
apply eq_of_degree_le_of_eval_index_eq (v := ((↑) : Rˣ → R)) (G : Set Rˣ).toFinset

Result:
case hvs
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ Set.InjOn Units.val ↑(↑G).toFinset

case h_deg_le
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).degree ≤ ↑(#(↑G).toFinset)

case h_deg_eq
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).degree = (X ^ Fintype.card ↥G - 1).degree

case hlc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).leadingCoeff = (X ^ Fintype.card ↥G - 1).leadingCoeff

case h_eval
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ ∀ i ∈ (↑G).toFinset, eval (↑i) (nodal (↑G).toFinset Units.val) = eval (↑i) (X ^ Fintype.card ↥G - 1)

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
i : Rˣ
hi : i ∈ (↑G).toFinset
⊢ i ∈ G

Tactic:
simpa using hi

Result:
no goals

Proof state:
case hlc
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ (nodal (↑G).toFinset Units.val).leadingCoeff = (X ^ Fintype.card ↥G - 1).leadingCoeff

Tactic:
rw [nodal_monic, leadingCoeff_sub_of_degree_lt h, monic_X_pow]

Result:
no goals

Proof state:
case h_eval
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
⊢ ∀ i ∈ (↑G).toFinset, eval (↑i) (nodal (↑G).toFinset Units.val) = eval (↑i) (X ^ Fintype.card ↥G - 1)

Tactic:
intros i hi

Result:
case h_eval
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
i : Rˣ
hi : i ∈ (↑G).toFinset
⊢ eval (↑i) (nodal (↑G).toFinset Units.val) = eval (↑i) (X ^ Fintype.card ↥G - 1)

Proof state:
case h_eval
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
i : Rˣ
hi : i ∈ (↑G).toFinset
⊢ 0 = eval (↑i) (X ^ Fintype.card ↥G - 1)

Tactic:
replace hi : i ∈ G := by simpa using hi

Result:
case h_eval
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
i : Rˣ
hi : i ∈ G
⊢ 0 = eval (↑i) (X ^ Fintype.card ↥G - 1)

Proof state:
case h_eval.intro
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsDomain R
G : Subgroup Rˣ
inst✝ : Fintype ↥G
h : degree 1 < (X ^ Fintype.card ↥G).degree
g : ↥G
hi : ↑g ∈ G
⊢ 0 = eval (↑↑g) (X ^ Fintype.card ↥G - 1)

Tactic:
simp [← Units.val_pow_eq_pow_val, ← Subgroup.coe_pow G]

Result:
no goals