[GOAL]
M✝ : Type u_1
inst✝⁵ : CancelMonoidWithZero M✝
inst✝⁴ : Finite M✝
M : Type u_2
inst✝³ : CancelMonoidWithZero M
inst✝² : DecidableEq M
inst✝¹ : Fintype M
inst✝ : Nontrivial M
src✝¹ : Nontrivial M := inst✝
src✝ : CancelMonoidWithZero M := inst✝³
⊢ 0⁻¹ = 0
[PROOFSTEP]
simp [Inv.inv, dif_pos rfl]
[GOAL]
M✝ : Type u_1
inst✝⁵ : CancelMonoidWithZero M✝
inst✝⁴ : Finite M✝
M : Type u_2
inst✝³ : CancelMonoidWithZero M
inst✝² : DecidableEq M
inst✝¹ : Fintype M
inst✝ : Nontrivial M
src✝¹ : Nontrivial M := inst✝
src✝ : CancelMonoidWithZero M := inst✝³
a : M
ha : a ≠ 0
⊢ a * a⁻¹ = 1
[PROOFSTEP]
simp [Inv.inv, dif_neg ha]
[GOAL]
M✝ : Type u_1
inst✝⁵ : CancelMonoidWithZero M✝
inst✝⁴ : Finite M✝
M : Type u_2
inst✝³ : CancelMonoidWithZero M
inst✝² : DecidableEq M
inst✝¹ : Fintype M
inst✝ : Nontrivial M
src✝¹ : Nontrivial M := inst✝
src✝ : CancelMonoidWithZero M := inst✝³
a : M
ha : a ≠ 0
⊢ a * bijInv (_ : Bijective fun b => a * b) 1 = 1
[PROOFSTEP]
exact Fintype.rightInverse_bijInv _ _
[GOAL]
M : Type u_1
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
a b c : R
n : ℕ
cp : IsCoprime a b
h : a * b = c ^ n
⊢ ∃ d, a = d ^ n
[PROOFSTEP]
refine' exists_eq_pow_of_mul_eq_pow (isUnit_of_dvd_one _) h
[GOAL]
M : Type u_1
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
a b c : R
n : ℕ
cp : IsCoprime a b
h : a * b = c ^ n
⊢ GCDMonoid.gcd a b ∣ 1
[PROOFSTEP]
obtain ⟨x, y, hxy⟩ := cp
[GOAL]
case intro.intro
M : Type u_1
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ GCDMonoid.gcd a b ∣ 1
[PROOFSTEP]
rw [← hxy]
[GOAL]
case intro.intro
M : Type u_1
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
R : Type u_2
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
a b c : R
n : ℕ
h : a * b = c ^ n
x y : R
hxy : x * a + y * b = 1
⊢ GCDMonoid.gcd a b ∣ x * a + y * b
[PROOFSTEP]
exact
  -- porting note: added `GCDMonoid.` twicedvd_add (dvd_mul_of_dvd_right (GCDMonoid.gcd_dvd_left _ _) _)
    (dvd_mul_of_dvd_right (GCDMonoid.gcd_dvd_right _ _) _)
[GOAL]
M : Type u_1
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
ι : Type u_2
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → IsCoprime (f i) (f j)
hprod : ∏ i in s, f i = c ^ n
⊢ ∀ (i : ι), i ∈ s → ∃ d, f i = d ^ n
[PROOFSTEP]
classical
intro i hi
rw [← insert_erase hi, prod_insert (not_mem_erase i s)] at hprod
refine'
  exists_eq_pow_of_mul_eq_pow_of_coprime (IsCoprime.prod_right fun j hj => h i hi j (erase_subset i s hj) fun hij => _)
    hprod
rw [hij] at hj
exact (s.not_mem_erase _) hj
[GOAL]
M : Type u_1
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
ι : Type u_2
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → IsCoprime (f i) (f j)
hprod : ∏ i in s, f i = c ^ n
⊢ ∀ (i : ι), i ∈ s → ∃ d, f i = d ^ n
[PROOFSTEP]
intro i hi
[GOAL]
M : Type u_1
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
ι : Type u_2
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → IsCoprime (f i) (f j)
hprod : ∏ i in s, f i = c ^ n
i : ι
hi : i ∈ s
⊢ ∃ d, f i = d ^ n
[PROOFSTEP]
rw [← insert_erase hi, prod_insert (not_mem_erase i s)] at hprod
[GOAL]
M : Type u_1
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
ι : Type u_2
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x in erase s i, f x = c ^ n
hi : i ∈ s
⊢ ∃ d, f i = d ^ n
[PROOFSTEP]
refine'
  exists_eq_pow_of_mul_eq_pow_of_coprime (IsCoprime.prod_right fun j hj => h i hi j (erase_subset i s hj) fun hij => _)
    hprod
[GOAL]
M : Type u_1
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
ι : Type u_2
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x in erase s i, f x = c ^ n
hi : i ∈ s
j : ι
hj : j ∈ erase s i
hij : i = j
⊢ False
[PROOFSTEP]
rw [hij] at hj
[GOAL]
M : Type u_1
inst✝⁵ : CancelMonoidWithZero M
inst✝⁴ : Finite M
ι : Type u_2
R : Type u_3
inst✝³ : CommSemiring R
inst✝² : IsDomain R
inst✝¹ : GCDMonoid R
inst✝ : Unique Rˣ
n : ℕ
c : R
s : Finset ι
f : ι → R
h : ∀ (i : ι), i ∈ s → ∀ (j : ι), j ∈ s → i ≠ j → IsCoprime (f i) (f j)
i : ι
hprod : f i * ∏ x in erase s i, f x = c ^ n
hi : i ∈ s
j : ι
hj : j ∈ erase s j
hij : i = j
⊢ False
[PROOFSTEP]
exact (s.not_mem_erase _) hj
[GOAL]
R✝ : Type u_1
G : Type u_2
inst✝⁵ : Ring R✝
inst✝⁴ : IsDomain R✝
inst✝³ : Fintype R✝
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Finite R
⊢ IsField R
[PROOFSTEP]
cases nonempty_fintype R
[GOAL]
case intro
R✝ : Type u_1
G : Type u_2
inst✝⁵ : Ring R✝
inst✝⁴ : IsDomain R✝
inst✝³ : Fintype R✝
R : Type u_3
inst✝² : CommRing R
inst✝¹ : IsDomain R
inst✝ : Finite R
val✝ : Fintype R
⊢ IsField R
[PROOFSTEP]
exact @Field.toIsField R (@Fintype.fieldOfDomain R _ _ (Classical.decEq R) _)
[GOAL]
R : Type u_1
G : Type u_2
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₀))
[PROOFSTEP]
haveI : DecidableEq R := Classical.decEq _
[GOAL]
R : Type u_1
G : Type u_2
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₀))
[PROOFSTEP]
refine' le_trans _ (nthRoots n (f g₀)).toFinset_card_le
[GOAL]
R : Type u_1
G : Type u_2
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₀)))
[PROOFSTEP]
apply card_le_card_of_inj_on f
[GOAL]
case hf
R : Type u_1
G : Type u_2
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₀))
[PROOFSTEP]
intro g hg
[GOAL]
case hf
R : Type u_1
G : Type u_2
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₀))
[PROOFSTEP]
rw [mem_filter] at hg
[GOAL]
case hf
R : Type u_1
G : Type u_2
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₀))
[PROOFSTEP]
rw [Multiset.mem_toFinset, mem_nthRoots hn, ← f.map_pow, hg.2]
[GOAL]
case f_inj
R : Type u_1
G : Type u_2
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₂
[PROOFSTEP]
intros
[GOAL]
case f_inj
R : Type u_1
G : Type u_2
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₂✝
[PROOFSTEP]
apply hf
[GOAL]
case f_inj.a
R : Type u_1
G : Type u_2
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₂✝
[PROOFSTEP]
assumption
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ↑f
⊢ IsCyclic G
[PROOFSTEP]
classical
cases nonempty_fintype G
apply isCyclic_of_card_pow_eq_one_le
intro n hn
exact le_trans (card_nthRoots_subgroup_units f hf hn 1) (card_nthRoots n (f 1))
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ↑f
⊢ IsCyclic G
[PROOFSTEP]
cases nonempty_fintype G
[GOAL]
case intro
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ↑f
val✝ : Fintype G
⊢ IsCyclic G
[PROOFSTEP]
apply isCyclic_of_card_pow_eq_one_le
[GOAL]
case intro.hn
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ↑f
val✝ : Fintype G
⊢ ∀ (n : ℕ), 0 < n → card (filter (fun a => a ^ n = 1) univ) ≤ n
[PROOFSTEP]
intro n hn
[GOAL]
case intro.hn
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Finite G
f : G →* R
hf : Injective ↑f
val✝ : Fintype G
n : ℕ
hn : 0 < n
⊢ card (filter (fun a => a ^ n = 1) univ) ≤ n
[PROOFSTEP]
exact le_trans (card_nthRoots_subgroup_units f hf hn 1) (card_nthRoots n (f 1))
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
S : Subgroup Rˣ
inst✝ : Finite { x // x ∈ S }
⊢ IsCyclic { x // x ∈ S }
[PROOFSTEP]
apply isCyclic_of_subgroup_isDomain (R := R) (G := S) _ _
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
S : Subgroup Rˣ
inst✝ : Finite { x // x ∈ S }
⊢ { x // x ∈ S } →* R
[PROOFSTEP]
exact MonoidHom.mk (OneHom.mk (fun s => ↑s.val) rfl) (by simp)
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
S : Subgroup Rˣ
inst✝ : Finite { x // x ∈ S }
⊢ ∀ (x y : { x // x ∈ S }),
    OneHom.toFun { toFun := fun s => ↑↑s, map_one' := (_ : (fun s => ↑↑s) 1 = (fun s => ↑↑s) 1) } (x * y) =
      OneHom.toFun { toFun := fun s => ↑↑s, map_one' := (_ : (fun s => ↑↑s) 1 = (fun s => ↑↑s) 1) } x *
        OneHom.toFun { toFun := fun s => ↑↑s, map_one' := (_ : (fun s => ↑↑s) 1 = (fun s => ↑↑s) 1) } y
[PROOFSTEP]
simp
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
S : Subgroup Rˣ
inst✝ : Finite { x // x ∈ S }
⊢ Injective
    ↑{ toOneHom := { toFun := fun s => ↑↑s, map_one' := (_ : (fun s => ↑↑s) 1 = (fun s => ↑↑s) 1) },
        map_mul' := (_ : ∀ (a a_1 : { x // x ∈ S }), ↑↑a * ↑↑a_1 = ↑↑a * ↑↑a_1) }
[PROOFSTEP]
exact Units.ext.comp Subtype.val_injective
[GOAL]
R : Type u_1
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : Monic g
⊢ ∃ q r,
    degree r < degree g ∧
      ↑(algebraMap R[X] K) f / ↑(algebraMap R[X] K) g =
        ↑(algebraMap R[X] K) q + ↑(algebraMap R[X] K) r / ↑(algebraMap R[X] K) g
[PROOFSTEP]
refine' ⟨f /ₘ g, f %ₘ g, _, _⟩
[GOAL]
case refine'_1
R : Type u_1
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : Monic g
⊢ degree (f %ₘ g) < degree g
[PROOFSTEP]
exact degree_modByMonic_lt _ hg
[GOAL]
case refine'_2
R : Type u_1
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : Monic g
⊢ ↑(algebraMap R[X] K) f / ↑(algebraMap R[X] K) g =
    ↑(algebraMap R[X] K) (f /ₘ g) + ↑(algebraMap R[X] K) (f %ₘ g) / ↑(algebraMap R[X] K) g
[PROOFSTEP]
have hg' : algebraMap R[X] K g ≠ 0 :=
  -- porting note: the proof was `by exact_mod_cast Monic.ne_zero hg`(map_ne_zero_iff _
        (IsFractionRing.injective R[X] K)).mpr
    (Monic.ne_zero hg)
[GOAL]
case refine'_2
R : Type u_1
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : Monic g
hg' : ↑(algebraMap R[X] K) g ≠ 0
⊢ ↑(algebraMap R[X] K) f / ↑(algebraMap R[X] K) g =
    ↑(algebraMap R[X] K) (f /ₘ g) + ↑(algebraMap R[X] K) (f %ₘ g) / ↑(algebraMap R[X] K) g
[PROOFSTEP]
field_simp [hg']
  -- porting note: `norm_cast` was here, but does nothing.
[GOAL]
case refine'_2
R : Type u_1
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
K : Type
inst✝² : Field K
inst✝¹ : Algebra R[X] K
inst✝ : IsFractionRing R[X] K
f g : R[X]
hg : Monic g
hg' : ↑(algebraMap R[X] K) g ≠ 0
⊢ ↑(algebraMap R[X] K) f = ↑(algebraMap R[X] K) (f /ₘ g) * ↑(algebraMap R[X] K) g + ↑(algebraMap R[X] K) (f %ₘ g)
[PROOFSTEP]
rw [add_comm, mul_comm, ← map_mul, ← map_add, modByMonic_add_div f hg]
[GOAL]
R : Type u_1
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_3
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y : H
hx : x ∈ Set.range ↑f
hy : y ∈ Set.range ↑f
⊢ card (filter (fun g => ↑f g = x) univ) = card (filter (fun g => ↑f g = y) univ)
[PROOFSTEP]
rcases hx with ⟨x, rfl⟩
[GOAL]
case intro
R : Type u_1
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_3
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
y : H
hy : y ∈ Set.range ↑f
x : G
⊢ card (filter (fun g => ↑f g = ↑f x) univ) = card (filter (fun g => ↑f g = y) univ)
[PROOFSTEP]
rcases hy with ⟨y, rfl⟩
[GOAL]
case intro.intro
R : Type u_1
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_3
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y : G
⊢ card (filter (fun g => ↑f g = ↑f x) univ) = card (filter (fun g => ↑f g = ↑f y) univ)
[PROOFSTEP]
refine' card_congr (fun g _ => g * x⁻¹ * y) _ _ fun g hg => ⟨g * y⁻¹ * x, _⟩
[GOAL]
case intro.intro.refine'_1
R : Type u_1
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_3
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y : G
⊢ ∀ (a : G) (ha : a ∈ filter (fun g => ↑f g = ↑f x) univ),
    (fun g x_1 => g * x⁻¹ * y) a ha ∈ filter (fun g => ↑f g = ↑f y) univ
[PROOFSTEP]
simp (config := { contextual := true }) only [*, mem_filter, one_mul, MonoidHom.map_mul, mem_univ, mul_right_inv,
  eq_self_iff_true, MonoidHom.map_mul_inv, and_self_iff, forall_true_iff]
  -- porting note: added the following `simp`
[GOAL]
case intro.intro.refine'_1
R : Type u_1
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_3
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y : G
⊢ ∀ (a : G), True ∧ ↑f a = ↑f x → True ∧ ↑f x * ↑f x⁻¹ * ↑f y = ↑f y
[PROOFSTEP]
simp only [true_and, map_inv, mul_right_inv, one_mul, and_self, implies_true, forall_const]
[GOAL]
case intro.intro.refine'_2
R : Type u_1
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_3
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y : G
⊢ ∀ (a b : G) (ha : a ∈ filter (fun g => ↑f g = ↑f x) univ) (hb : b ∈ filter (fun g => ↑f g = ↑f x) univ),
    (fun g x_1 => g * x⁻¹ * y) a ha = (fun g x_1 => g * x⁻¹ * y) b hb → a = b
[PROOFSTEP]
simp only [mul_left_inj, imp_self, forall₂_true_iff]
[GOAL]
case intro.intro.refine'_3
R : Type u_1
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_3
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y g : G
hg : g ∈ filter (fun g => ↑f g = ↑f y) univ
⊢ ∃ ha, (fun g x_1 => g * x⁻¹ * y) (g * y⁻¹ * x) ha = g
[PROOFSTEP]
simp only [true_and_iff, mem_filter, mem_univ] at hg
[GOAL]
case intro.intro.refine'_3
R : Type u_1
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_3
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y g : G
hg : ↑f g = ↑f y
⊢ ∃ ha, (fun g x_1 => g * x⁻¹ * y) (g * y⁻¹ * x) ha = g
[PROOFSTEP]
simp only [hg, mem_filter, one_mul, MonoidHom.map_mul, mem_univ, mul_right_inv, eq_self_iff_true, exists_prop_of_true,
  MonoidHom.map_mul_inv, and_self_iff, mul_inv_cancel_right, inv_mul_cancel_right]
  -- porting note: added the next line.  It is weird!
[GOAL]
case intro.intro.refine'_3
R : Type u_1
G : Type u_2
inst✝⁵ : CommRing R
inst✝⁴ : IsDomain R
inst✝³ : Group G
inst✝² : Fintype G
H : Type u_3
inst✝¹ : Group H
inst✝ : DecidableEq H
f : G →* H
x y g : G
hg : ↑f g = ↑f y
⊢ ∃ h, True
[PROOFSTEP]
simp only [map_inv, mul_right_inv, one_mul, and_self, exists_prop]
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
⊢ ∑ g : G, ↑f g = 0
[PROOFSTEP]
classical
obtain ⟨x, hx⟩ : ∃ x : MonoidHom.range f.toHomUnits, ∀ y : MonoidHom.range f.toHomUnits, y ∈ Submonoid.powers x
exact IsCyclic.exists_monoid_generator
have hx1 : x ≠ 1 := by
  rintro rfl
  apply hf
  ext g
  rw [MonoidHom.one_apply]
  cases' hx ⟨f.toHomUnits g, g, rfl⟩ with n hn
  rwa [Subtype.ext_iff, Units.ext_iff, Subtype.coe_mk, MonoidHom.coe_toHomUnits, one_pow, eq_comm] at hn
replace hx1 :
  (x.val : R) - 1 ≠
    0
      -- porting note: was `(x : R)`
exact fun h => hx1 (Subtype.eq (Units.ext (sub_eq_zero.1 h)))
let c := (univ.filter fun g => f.toHomUnits g = 1).card
calc
  ∑ g : G, f g = ∑ g : G, (f.toHomUnits g : R) := rfl
  _ = ∑ u : Rˣ in univ.image f.toHomUnits, (univ.filter fun g => f.toHomUnits g = u).card • (u : R) :=
    (sum_comp ((↑) : Rˣ → R) f.toHomUnits)
  _ = ∑ u : Rˣ in univ.image f.toHomUnits, c • (u : R) :=
    (sum_congr rfl fun u hu => congr_arg₂ _ ?_ rfl)
      -- remaining goal 1, proven below
            -- Porting note: have to change `(b : R)` into `((b : Rˣ) : R)`
  _ = ∑ b : MonoidHom.range f.toHomUnits, c • ((b : Rˣ) : R) := (Finset.sum_subtype _ (by simp) _)
  _ = c • ∑ b : MonoidHom.range f.toHomUnits, ((b : Rˣ) : R) := smul_sum.symm
  _ = c • (0 : R) :=
    (congr_arg₂ _ rfl ?_)
      -- remaining goal 2, proven below
  _ = (0 : R) := smul_zero _
·
  -- remaining goal 1
  show (univ.filter fun g : G => f.toHomUnits g = u).card = c
  apply card_fiber_eq_of_mem_range f.toHomUnits
  · simpa only [mem_image, mem_univ, true_and, Set.mem_range] using hu
  ·
    exact
      ⟨1, f.toHomUnits.map_one⟩
        -- remaining goal 2
show (∑ b : MonoidHom.range f.toHomUnits, ((b : Rˣ) : R)) = 0
calc
  (∑ b : MonoidHom.range f.toHomUnits, ((b : Rˣ) : R)) = ∑ n in range (orderOf x), ((x : Rˣ) : R) ^ n :=
    Eq.symm <|
      sum_bij (fun n _ => x ^ n) (by simp only [mem_univ, forall_true_iff])
        (by simp only [imp_true_iff, eq_self_iff_true, Subgroup.coe_pow, Units.val_pow_eq_pow_val])
        (fun m n hm hn =>
          pow_injective_of_lt_orderOf _ (by simpa only [mem_range] using hm) (by simpa only [mem_range] using hn))
        (fun b _ =>
          let ⟨n, hn⟩ := hx b
          ⟨n % orderOf x, mem_range.2 (Nat.mod_lt _ (orderOf_pos _)),
            -- Porting note: have to use `dsimp` to apply the functionby dsimp at hn ⊢; rw [← pow_eq_mod_orderOf, hn]⟩)
  _ = 0 := ?_
rw [← mul_left_inj' hx1, zero_mul, geom_sum_mul]
norm_cast
simp [pow_orderOf_eq_one]
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
⊢ ∑ g : G, ↑f g = 0
[PROOFSTEP]
obtain ⟨x, hx⟩ : ∃ x : MonoidHom.range f.toHomUnits, ∀ y : MonoidHom.range f.toHomUnits, y ∈ Submonoid.powers x
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
⊢ ∃ x, ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
case intro
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
⊢ ∑ g : G, ↑f g = 0
[PROOFSTEP]
exact IsCyclic.exists_monoid_generator
[GOAL]
case intro
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
⊢ ∑ g : G, ↑f g = 0
[PROOFSTEP]
have hx1 : x ≠ 1 := by
  rintro rfl
  apply hf
  ext g
  rw [MonoidHom.one_apply]
  cases' hx ⟨f.toHomUnits g, g, rfl⟩ with n hn
  rwa [Subtype.ext_iff, Units.ext_iff, Subtype.coe_mk, MonoidHom.coe_toHomUnits, one_pow, eq_comm] at hn
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
⊢ x ≠ 1
[PROOFSTEP]
rintro rfl
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers 1
⊢ False
[PROOFSTEP]
apply hf
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers 1
⊢ f = 1
[PROOFSTEP]
ext g
[GOAL]
case h
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers 1
g : G
⊢ ↑f g = ↑1 g
[PROOFSTEP]
rw [MonoidHom.one_apply]
[GOAL]
case h
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers 1
g : G
⊢ ↑f g = 1
[PROOFSTEP]
cases' hx ⟨f.toHomUnits g, g, rfl⟩ with n hn
[GOAL]
case h.intro
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers 1
g : G
n : ℕ
hn :
  (fun x x_1 => x ^ x_1) 1 n =
    { val := ↑(MonoidHom.toHomUnits f) g,
      property := (_ : ∃ y, ↑(MonoidHom.toHomUnits f) y = ↑(MonoidHom.toHomUnits f) g) }
⊢ ↑f g = 1
[PROOFSTEP]
rwa [Subtype.ext_iff, Units.ext_iff, Subtype.coe_mk, MonoidHom.coe_toHomUnits, one_pow, eq_comm] at hn
[GOAL]
case intro
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : x ≠ 1
⊢ ∑ g : G, ↑f g = 0
[PROOFSTEP]
replace hx1 :
  (x.val : R) - 1 ≠
    0
      -- porting note: was `(x : R)`
[GOAL]
case hx1
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : x ≠ 1
⊢ ↑↑x - 1 ≠ 0
case intro
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
⊢ ∑ g : G, ↑f g = 0
[PROOFSTEP]
exact fun h => hx1 (Subtype.eq (Units.ext (sub_eq_zero.1 h)))
[GOAL]
case intro
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
⊢ ∑ g : G, ↑f g = 0
[PROOFSTEP]
let c := (univ.filter fun g => f.toHomUnits g = 1).card
[GOAL]
case intro
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = 1) univ)
⊢ ∑ g : G, ↑f g = 0
[PROOFSTEP]
calc
  ∑ g : G, f g = ∑ g : G, (f.toHomUnits g : R) := rfl
  _ = ∑ u : Rˣ in univ.image f.toHomUnits, (univ.filter fun g => f.toHomUnits g = u).card • (u : R) :=
    (sum_comp ((↑) : Rˣ → R) f.toHomUnits)
  _ = ∑ u : Rˣ in univ.image f.toHomUnits, c • (u : R) :=
    (sum_congr rfl fun u hu => congr_arg₂ _ ?_ rfl)
      -- remaining goal 1, proven below
            -- Porting note: have to change `(b : R)` into `((b : Rˣ) : R)`
  _ = ∑ b : MonoidHom.range f.toHomUnits, c • ((b : Rˣ) : R) := (Finset.sum_subtype _ (by simp) _)
  _ = c • ∑ b : MonoidHom.range f.toHomUnits, ((b : Rˣ) : R) := smul_sum.symm
  _ = c • (0 : R) :=
    (congr_arg₂ _ rfl ?_)
      -- remaining goal 2, proven below
  _ = (0 : R) := smul_zero _
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = 1) univ)
⊢ ∀ (x : Rˣ), x ∈ image (↑(MonoidHom.toHomUnits f)) univ ↔ x ∈ MonoidHom.range (MonoidHom.toHomUnits f)
[PROOFSTEP]
simp
[GOAL]
case intro.calc_1
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = 1) univ)
u : Rˣ
hu : u ∈ image (↑(MonoidHom.toHomUnits f)) univ
⊢ card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = u) univ) = c
[PROOFSTEP]
show (univ.filter fun g : G => f.toHomUnits g = u).card = c
[GOAL]
case intro.calc_1
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = 1) univ)
u : Rˣ
hu : u ∈ image (↑(MonoidHom.toHomUnits f)) univ
⊢ card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = u) univ) = c
[PROOFSTEP]
apply card_fiber_eq_of_mem_range f.toHomUnits
[GOAL]
case intro.calc_1.hx
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = 1) univ)
u : Rˣ
hu : u ∈ image (↑(MonoidHom.toHomUnits f)) univ
⊢ u ∈ Set.range ↑(MonoidHom.toHomUnits f)
[PROOFSTEP]
simpa only [mem_image, mem_univ, true_and, Set.mem_range] using hu
[GOAL]
case intro.calc_1.hy
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = 1) univ)
u : Rˣ
hu : u ∈ image (↑(MonoidHom.toHomUnits f)) univ
⊢ 1 ∈ Set.range ↑(MonoidHom.toHomUnits f)
[PROOFSTEP]
exact
  ⟨1, f.toHomUnits.map_one⟩
    -- remaining goal 2
[GOAL]
case intro.calc_2
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = 1) univ)
⊢ ∑ b : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }, ↑↑b = 0
[PROOFSTEP]
show (∑ b : MonoidHom.range f.toHomUnits, ((b : Rˣ) : R)) = 0
[GOAL]
case intro.calc_2
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = 1) univ)
⊢ ∑ b : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }, ↑↑b = 0
[PROOFSTEP]
calc
  (∑ b : MonoidHom.range f.toHomUnits, ((b : Rˣ) : R)) = ∑ n in range (orderOf x), ((x : Rˣ) : R) ^ n :=
    Eq.symm <|
      sum_bij (fun n _ => x ^ n) (by simp only [mem_univ, forall_true_iff])
        (by simp only [imp_true_iff, eq_self_iff_true, Subgroup.coe_pow, Units.val_pow_eq_pow_val])
        (fun m n hm hn =>
          pow_injective_of_lt_orderOf _ (by simpa only [mem_range] using hm) (by simpa only [mem_range] using hn))
        (fun b _ =>
          let ⟨n, hn⟩ := hx b
          ⟨n % orderOf x, mem_range.2 (Nat.mod_lt _ (orderOf_pos _)),
            -- Porting note: have to use `dsimp` to apply the functionby dsimp at hn ⊢; rw [← pow_eq_mod_orderOf, hn]⟩)
  _ = 0 := ?_
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = 1) univ)
⊢ ∀ (a : ℕ) (ha : a ∈ range (orderOf x)), (fun n x_1 => x ^ n) a ha ∈ univ
[PROOFSTEP]
simp only [mem_univ, forall_true_iff]
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = 1) univ)
⊢ ∀ (a : ℕ) (ha : a ∈ range (orderOf x)), ↑↑x ^ a = ↑↑((fun n x_1 => x ^ n) a ha)
[PROOFSTEP]
simp only [imp_true_iff, eq_self_iff_true, Subgroup.coe_pow, Units.val_pow_eq_pow_val]
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = 1) univ)
m n : ℕ
hm : m ∈ range (orderOf x)
hn : n ∈ range (orderOf x)
⊢ m < orderOf x
[PROOFSTEP]
simpa only [mem_range] using hm
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = 1) univ)
m n : ℕ
hm : m ∈ range (orderOf x)
hn : n ∈ range (orderOf x)
⊢ n < orderOf x
[PROOFSTEP]
simpa only [mem_range] using hn
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = 1) univ)
b : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
x✝ : b ∈ univ
n : ℕ
hn : (fun x x_1 => x ^ x_1) x n = b
⊢ b = (fun n x_1 => x ^ n) (n % orderOf x) (_ : n % orderOf x ∈ range (orderOf x))
[PROOFSTEP]
dsimp at hn ⊢
[GOAL]
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = 1) univ)
b : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
x✝ : b ∈ univ
n : ℕ
hn : x ^ n = b
⊢ b = x ^ (n % orderOf x)
[PROOFSTEP]
rw [← pow_eq_mod_orderOf, hn]
[GOAL]
case intro.calc_2
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = 1) univ)
⊢ ∑ n in range (orderOf x), ↑↑x ^ n = 0
[PROOFSTEP]
rw [← mul_left_inj' hx1, zero_mul, geom_sum_mul]
[GOAL]
case intro.calc_2
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = 1) univ)
⊢ ↑↑x ^ orderOf x - 1 = 0
[PROOFSTEP]
norm_cast
[GOAL]
case intro.calc_2
R : Type u_1
G : Type u_2
inst✝³ : CommRing R
inst✝² : IsDomain R
inst✝¹ : Group G
inst✝ : Fintype G
f : G →* R
hf : f ≠ 1
x : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }
hx : ∀ (y : { x // x ∈ MonoidHom.range (MonoidHom.toHomUnits f) }), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := card (filter (fun g => ↑(MonoidHom.toHomUnits f) g = 1) univ)
⊢ ↑↑(x ^ orderOf x) - 1 = 0
[PROOFSTEP]
simp [pow_orderOf_eq_one]
[GOAL]
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
⊢ ∑ g : G, ↑f g = ↑(if f = 1 then Fintype.card G else 0)
[PROOFSTEP]
split_ifs with h
[GOAL]
case pos
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : f = 1
⊢ ∑ g : G, ↑f g = ↑(Fintype.card G)
[PROOFSTEP]
simp [h, card_univ]
[GOAL]
case neg
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : ¬f = 1
⊢ ∑ g : G, ↑f g = ↑0
[PROOFSTEP]
rw [cast_zero]
  -- porting note: added
[GOAL]
case neg
R : Type u_1
G : Type u_2
inst✝⁴ : CommRing R
inst✝³ : IsDomain R
inst✝² : Group G
inst✝¹ : Fintype G
f : G →* R
inst✝ : Decidable (f = 1)
h : ¬f = 1
⊢ ∑ g : G, ↑f g = 0
[PROOFSTEP]
exact sum_hom_units_eq_zero f h


[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
⊢ N = J • N
[PROOFSTEP]
refine' le_antisymm _ (Submodule.smul_le.2 fun _ _ _ => Submodule.smul_mem _ _)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
⊢ N ≤ J • N
[PROOFSTEP]
intro n hn
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
n : M
hn : n ∈ N
⊢ n ∈ J • N
[PROOFSTEP]
cases' Submodule.exists_sub_one_mem_and_smul_eq_zero_of_fg_of_le_smul I N hN hIN with r hr
[GOAL]
case intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
⊢ n ∈ J • N
[PROOFSTEP]
cases' exists_mul_sub_mem_of_sub_one_mem_jacobson r (hIjac hr.1) with s hs
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
s : R
hs : s * r - 1 ∈ J
⊢ n ∈ J • N
[PROOFSTEP]
have : n = -(s * r - 1) • n := by rw [neg_sub, sub_smul, mul_smul, hr.2 n hn, one_smul, smul_zero, sub_zero]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
s : R
hs : s * r - 1 ∈ J
⊢ n = -(s * r - 1) • n
[PROOFSTEP]
rw [neg_sub, sub_smul, mul_smul, hr.2 n hn, one_smul, smul_zero, sub_zero]
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
s : R
hs : s * r - 1 ∈ J
this : n = -(s * r - 1) • n
⊢ n ∈ J • N
[PROOFSTEP]
rw [this]
[GOAL]
case intro.intro
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson J
n : M
hn : n ∈ N
r : R
hr : r - 1 ∈ I ∧ ∀ (n : M), n ∈ N → r • n = 0
s : R
hs : s * r - 1 ∈ J
this : n = -(s * r - 1) • n
⊢ -(s * r - 1) • n ∈ J • N
[PROOFSTEP]
exact Submodule.smul_mem_smul (Submodule.neg_mem _ hs) hn
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N : Submodule R M
hN : FG N
hIN : N ≤ I • N
hIjac : I ≤ jacobson ⊥
⊢ N = ⊥
[PROOFSTEP]
rw [eq_smul_of_le_smul_of_le_jacobson hN hIN hIjac, Submodule.bot_smul]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
⊢ N ⊔ I • N' = N ⊔ J • N'
[PROOFSTEP]
have hNN' : N ⊔ N' = N ⊔ I • N' :=
  le_antisymm hNN (sup_le_sup_left (Submodule.smul_le.2 fun _ _ _ => Submodule.smul_mem _ _) _)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
⊢ N ⊔ I • N' = N ⊔ J • N'
[PROOFSTEP]
have h_comap := Submodule.comap_injective_of_surjective (LinearMap.range_eq_top.1 N.range_mkQ)
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap (mkQ N))
⊢ N ⊔ I • N' = N ⊔ J • N'
[PROOFSTEP]
have : (I • N').map N.mkQ = N'.map N.mkQ := by
  rw [← h_comap.eq_iff]
  simpa [comap_map_eq, sup_comm, eq_comm] using hNN'
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap (mkQ N))
⊢ map (mkQ N) (I • N') = map (mkQ N) N'
[PROOFSTEP]
rw [← h_comap.eq_iff]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap (mkQ N))
⊢ comap (mkQ N) (map (mkQ N) (I • N')) = comap (mkQ N) (map (mkQ N) N')
[PROOFSTEP]
simpa [comap_map_eq, sup_comm, eq_comm] using hNN'
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap (mkQ N))
this : map (mkQ N) (I • N') = map (mkQ N) N'
⊢ N ⊔ I • N' = N ⊔ J • N'
[PROOFSTEP]
have :=
  @Submodule.eq_smul_of_le_smul_of_le_jacobson _ _ _ _ _ I J (N'.map N.mkQ) (hN'.map _) (by rw [← map_smul'', this]) hIJ
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap (mkQ N))
this : map (mkQ N) (I • N') = map (mkQ N) N'
⊢ map (mkQ N) N' ≤ I • map (mkQ N) N'
[PROOFSTEP]
rw [← map_smul'', this]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap (mkQ N))
this✝ : map (mkQ N) (I • N') = map (mkQ N) N'
this : map (mkQ N) N' = J • map (mkQ N) N'
⊢ N ⊔ I • N' = N ⊔ J • N'
[PROOFSTEP]
rw [← map_smul'', ← h_comap.eq_iff, comap_map_eq, comap_map_eq, Submodule.ker_mkQ, sup_comm, hNN'] at this
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I J : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson J
hNN : N ⊔ N' ≤ N ⊔ I • N'
hNN' : N ⊔ N' = N ⊔ I • N'
h_comap : Function.Injective (comap (mkQ N))
this✝ : map (mkQ N) (I • N') = map (mkQ N) N'
this : N ⊔ I • N' = J • N' ⊔ N
⊢ N ⊔ I • N' = N ⊔ J • N'
[PROOFSTEP]
rw [this, sup_comm]
[GOAL]
R : Type u_1
M : Type u_2
inst✝² : CommRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
I : Ideal R
N N' : Submodule R M
hN' : FG N'
hIJ : I ≤ jacobson ⊥
hNN : N ⊔ N' ≤ N ⊔ I • N'
⊢ I • N' ≤ N
[PROOFSTEP]
rw [← sup_eq_left, smul_sup_eq_smul_sup_of_le_smul_of_le_jacobson hN' hIJ hNN, bot_smul, sup_bot_eq]