R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ↑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
⊢ card (filter (fun g => g ^ n = g₀) univ) ≤ ↑Multiset.card (nthRoots n (↑f g₀))
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ↑f
n : ℕ
hn : 0 < n
g₀ : G
⊢ card (filter (fun g => g ^ n = g₀) univ) ≤ ↑Multiset.card (nthRoots n (↑f g₀))
haveI : DecidableEq R := Classical.decEq _
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ↑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
⊢ card (filter (fun g => g ^ n = g₀) univ) ≤ card (Multiset.toFinset (nthRoots n (↑f g₀)))
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ↑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
⊢ card (filter (fun g => g ^ n = g₀) univ) ≤ ↑Multiset.card (nthRoots n (↑f g₀))
refine' le_trans _ (nthRoots n (f g₀)).toFinset_card_le
case hf
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ↑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
⊢ ∀ (a : G), a ∈ filter (fun g => g ^ n = g₀) univ → ↑f a ∈ Multiset.toFinset (nthRoots n (↑f g₀))

case f_inj
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ↑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
⊢ ∀ (a₁ : G),
    a₁ ∈ filter (fun g => g ^ n = g₀) univ →
      ∀ (a₂ : G), a₂ ∈ filter (fun g => g ^ n = g₀) univ → ↑f a₁ = ↑f a₂ → a₁ = a₂
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ↑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
⊢ card (filter (fun g => g ^ n = g₀) univ) ≤ card (Multiset.toFinset (nthRoots n (↑f g₀)))
apply card_le_card_of_inj_on f
case hf
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ↑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
g : G
hg : g ∈ filter (fun g => g ^ n = g₀) univ
⊢ ↑f g ∈ Multiset.toFinset (nthRoots n (↑f g₀))
case hf
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ↑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
⊢ ∀ (a : G), a ∈ filter (fun g => g ^ n = g₀) univ → ↑f a ∈ Multiset.toFinset (nthRoots n (↑f g₀))
intro g hg
case hf
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ↑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
g : G
hg : g ∈ univ ∧ g ^ n = g₀
⊢ ↑f g ∈ Multiset.toFinset (nthRoots n (↑f g₀))
case hf
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ↑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
g : G
hg : g ∈ filter (fun g => g ^ n = g₀) univ
⊢ ↑f g ∈ Multiset.toFinset (nthRoots n (↑f g₀))
rw [mem_filter] at hg
no goals
case hf
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ↑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
g : G
hg : g ∈ univ ∧ g ^ n = g₀
⊢ ↑f g ∈ Multiset.toFinset (nthRoots n (↑f g₀))
rw [Multiset.mem_toFinset, mem_nthRoots hn, ← f.map_pow, hg.2]
case f_inj
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ↑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
a₁✝ : G
a✝² : a₁✝ ∈ filter (fun g => g ^ n = g₀) univ
a₂✝ : G
a✝¹ : a₂✝ ∈ filter (fun g => g ^ n = g₀) univ
a✝ : ↑f a₁✝ = ↑f a₂✝
⊢ a₁✝ = a₂✝
case f_inj
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ↑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
⊢ ∀ (a₁ : G),
    a₁ ∈ filter (fun g => g ^ n = g₀) univ →
      ∀ (a₂ : G), a₂ ∈ filter (fun g => g ^ n = g₀) univ → ↑f a₁ = ↑f a₂ → a₁ = a₂
intros
case f_inj.a
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ↑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
a₁✝ : G
a✝² : a₁✝ ∈ filter (fun g => g ^ n = g₀) univ
a₂✝ : G
a✝¹ : a₂✝ ∈ filter (fun g => g ^ n = g₀) univ
a✝ : ↑f a₁✝ = ↑f a₂✝
⊢ ↑f a₁✝ = ↑f a₂✝
case f_inj
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ↑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
a₁✝ : G
a✝² : a₁✝ ∈ filter (fun g => g ^ n = g₀) univ
a₂✝ : G
a✝¹ : a₂✝ ∈ filter (fun g => g ^ n = g₀) univ
a✝ : ↑f a₁✝ = ↑f a₂✝
⊢ a₁✝ = a₂✝
apply hf
no goals
case f_inj.a
R : Type u_2
G : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : DecidableEq G
f : G →* R
hf : Injective ↑f
n : ℕ
hn : 0 < n
g₀ : G
this : DecidableEq R
a₁✝ : G
a✝² : a₁✝ ∈ filter (fun g => g ^ n = g₀) univ
a₂✝ : G
a✝¹ : a₂✝ ∈ filter (fun g => g ^ n = g₀) univ
a✝ : ↑f a₁✝ = ↑f a₂✝
⊢ ↑f a₁✝ = ↑f a₂✝
assumption