-- Mathlib/RingTheory/IntegralDomain.lean
theorem sum_hom_units_eq_zero (f : G →* R) (hf : f ≠ 1) : ∑ g : G, f g = 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)
⊢ ∀ a ∈ range (orderOf x), (fun x_1 => x ^ x_1) a ∈ univ

Tactic:
simp only [mem_univ, forall_true_iff]

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

Tactic:
ext g

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

Proof state:
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 : ↥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
⊢ 1 ∈ Set.range ⇑f.toHomUnits

Tactic:
exact ⟨1, f.toHomUnits.map_one⟩

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)
⊢ ∑ n ∈ range (orderOf x), ↑↑x ^ n = 0

Tactic:
rw [← mul_left_inj' hx1, zero_mul, geom_sum_mul]

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:
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
⊢ ∑ g : G, f g = 0

Tactic:
replace hx1 : (x.val : R) - 1 ≠ 0 := fun h => hx1 (Subtype.eq (Units.ext (sub_eq_zero.1 h)))

Result:
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
⊢ ∑ g : G, f g = 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
⊢ ∑ g : G, f g = 0

Tactic:
obtain ⟨x, hx⟩ : ∃ x : MonoidHom.range f.toHomUnits,
    ∀ y : MonoidHom.range f.toHomUnits, y ∈ Submonoid.powers x :=
  IsCyclic.exists_monoid_generator

Result:
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
⊢ ∑ g : G, f g = 0

Proof state:
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

Tactic:
apply MonoidHom.card_fiber_eq_of_mem_range f.toHomUnits

Result:
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 : ↥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
⊢ u ∈ Set.range ⇑f.toHomUnits

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 : ↥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
⊢ 1 ∈ Set.range ⇑f.toHomUnits

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
⊢ ∑ g : G, f g = 0

Tactic:
let c := #{g | f.toHomUnits g = 1}

Result:
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

Proof state:
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 : ↥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
⊢ u ∈ Set.range ⇑f.toHomUnits

Tactic:
simpa only [mem_image, mem_univ, true_and, Set.mem_range] using hu

Result:
no goals

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

Tactic:
rw [MonoidHom.one_apply]

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

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

Tactic:
obtain ⟨n, hn⟩ := hx ⟨f.toHomUnits g, g, rfl⟩

Result:
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

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)
⊢ ∀ a ∈ range (orderOf x), ↑↑x ^ a = ↑↑((fun x_1 => x ^ x_1) a)

Tactic:
simp only [imp_true_iff, eq_self_iff_true, Subgroup.coe_pow,
Units.val_pow_eq_pow_val]

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
⊢ ∑ g : G, f g = 0

Tactic:
have hx1 : x ≠ 1 := by
  rintro rfl
  apply hf
  ext g
  rw [MonoidHom.one_apply]
  obtain ⟨n, hn⟩ := hx ⟨f.toHomUnits g, g, rfl⟩
  rwa [Subtype.ext_iff, Units.ext_iff, Subtype.coe_mk, MonoidHom.coe_toHomUnits, one_pow,
    eq_comm] at hn

Result:
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
⊢ ∑ g : G, f g = 0