-- Mathlib/RingTheory/IntegralDomain.lean
theorem sum_hom_units_eq_zero (f : G →* R) (hf : f ≠ 1) : ∑ g : G, f g = 0

Proof state:
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 : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #(filter (fun g => f.toHomUnits g = 1) univ)
⊢ ↑↑x ^ orderOf x - 1 = 0

Tactic:
norm_cast

Result:
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 : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #(filter (fun g => f.toHomUnits g = 1) univ)
⊢ ↑↑(x ^ orderOf x) - 1 = 0

Proof state:
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 : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #(filter (fun g => f.toHomUnits g = 1) univ)
⊢ ∀ (x : Rˣ), x ∈ image (⇑f.toHomUnits) univ ↔ x ∈ f.toHomUnits.range

Tactic:
simp

Result:
no goals

Proof state:
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 : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #(filter (fun g => f.toHomUnits g = 1) univ)
⊢ ∑ g : G, f g = 0

Tactic:
calc
  ∑ g : G, f g = ∑ g : G, (f.toHomUnits g : R) := rfl
  _ = ∑ u ∈ univ.image f.toHomUnits, #{g | f.toHomUnits g = u} • (u : R) :=
    sum_comp ((↑) : Rˣ → R) f.toHomUnits
  _ = ∑ u ∈ univ.image f.toHomUnits, c • (u : R) :=
    (sum_congr rfl fun u hu => congr_arg₂ _ ?_ rfl)
  _ = ∑ 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 ?_
  _ = (0 : R) := smul_zero _

Result:
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 : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #(filter (fun g => f.toHomUnits g = 1) univ)
u : Rˣ
hu : u ∈ image (⇑f.toHomUnits) univ
⊢ #(filter (fun g => f.toHomUnits g = u) univ) = c

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 : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #(filter (fun g => f.toHomUnits g = 1) univ)
⊢ ∑ b : ↥f.toHomUnits.range, ↑↑b = 0

Proof state:
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 : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
⊢ x ≠ 1

Tactic:
rintro rfl

Result:
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 : ↥f.toHomUnits.range), y ∈ Submonoid.powers 1
⊢ False

Proof state:
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 : ↥f.toHomUnits.range), y ∈ Submonoid.powers 1
⊢ False

Tactic:
apply hf

Result:
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 : ↥f.toHomUnits.range), y ∈ Submonoid.powers 1
⊢ f = 1

Proof state:
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 : ↥f.toHomUnits.range), y ∈ Submonoid.powers 1
g : G
n : ℕ
hn : (fun x => 1 ^ x) n = ⟨f.toHomUnits g, ⋯⟩
⊢ f g = 1

Tactic:
rwa [Subtype.ext_iff, Units.ext_iff, Subtype.coe_mk, MonoidHom.coe_toHomUnits, one_pow,
  eq_comm] at hn

Result:
no goals

Proof state:
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 : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #(filter (fun g => f.toHomUnits g = 1) univ)
⊢ Set.InjOn (fun x_1 => x ^ x_1) ↑(range (orderOf x))

Tactic:
simpa using pow_injOn_Iio_orderOf

Result:
no goals

Proof state:
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 : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #(filter (fun g => f.toHomUnits g = 1) univ)
⊢ ↑↑(x ^ orderOf x) - 1 = 0

Tactic:
simp [pow_orderOf_eq_one]

Result:
no goals

Proof state:
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 : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #(filter (fun g => f.toHomUnits g = 1) univ)
b : ↥f.toHomUnits.range
x✝ : b ∈ ↑univ
n : ℕ
hn : (fun x_1 => x ^ x_1) n = b
⊢ (fun x_1 => x ^ x_1) (n % orderOf x) = b

Tactic:
dsimp at hn ⊢

Result:
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 : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #(filter (fun g => f.toHomUnits g = 1) univ)
b : ↥f.toHomUnits.range
x✝ : b ∈ ↑univ
n : ℕ
hn : x ^ n = b
⊢ x ^ (n % orderOf x) = b

Proof state:
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 : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), y ∈ Submonoid.powers x
hx1 : ↑↑x - 1 ≠ 0
c : ℕ := #(filter (fun g => f.toHomUnits g = 1) univ)
b : ↥f.toHomUnits.range
x✝ : b ∈ ↑univ
n : ℕ
hn : x ^ n = b
⊢ x ^ (n % orderOf x) = b

Tactic:
rw [pow_mod_orderOf, hn]

Result:
no goals