-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
Goal:
R : Type u_1
G : Type u_2
inst : CommRing R
inst_1 : IsDomain R
inst_2 : Group G
inst_3 : Fintype G
f : G →* R
hf : f ≠ 1
obtain :
  ∀ (x : ↥f.toHomUnits.range)
    (hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y),
    Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) 0
obtain₁ obtain₂ :
  ∀ (x : ↥f.toHomUnits.range)
    (hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y)
    (hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0), Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) 0
calc_1 :
  ∀ (x : ↥f.toHomUnits.range)
    (hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y)
    (hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0),
    let c := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)};
    ∀ (u : Rˣ) (hu : Membership.mem (γ := Finset Rˣ) (image.{u_2, u_1} (α := G) (⇑f.toHomUnits : (a : G) → Rˣ) univ) u),
      card.{u_2} (α := G) {g : G | (f.toHomUnits : (a : G) → Rˣ) g = u} = c
calc_2 calc_2₁ :
  ∀ (x : ↥f.toHomUnits.range)
    (hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y)
    (hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0), Eq.{u_1 + 1} (α := R) (∑ b : ↥f.toHomUnits.range, (↑(↑b : Rˣ) : R)) 0
calc_2₂ :
  ∀ (x : ↥f.toHomUnits.range)
    (hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y)
    (hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0), Eq.{u_1 + 1} (α := R) (∑ n ∈ range (orderOf x), (↑(↑x : Rˣ) : R) ^ n) 0
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) 0
have calc_2₃ : ∀ (x : ↥f.toHomUnits.range)
  (hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y)
  (hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0), (↑(↑x : Rˣ) : R) ^ orderOf x - 1 = 0
Tactic: classical
    obtain ⟨x, hx⟩ := IsCyclic.exists_monoid_generator (α := MonoidHom.range f.toHomUnits)
    have hx1 : (x.1 : R) - 1 ≠ 0 := by
      rw [sub_ne_zero]
      contrapose hf
      ext g
      obtain ⟨n, hn⟩ := hx ⟨f.toHomUnits g, g, rfl⟩
      simpa [hf, Subtype.ext_iff, Units.ext_iff] using hn.symm
    let c := #{g | f.toHomUnits g = 1}
    calc
      ∑ g : G, f g = ∑ 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)
      -- remaining goal 1, proven below
      _ = ∑ b : MonoidHom.range f.toHomUnits, c • (b.1 : R) :=
        (Finset.sum_subtype _ (by simp) _)
      _ = c • ∑ b : MonoidHom.range f.toHomUnits, (b.1 : R) := smul_sum.symm
      _ = c • 0 := congr_arg₂ _ rfl ?_
      -- remaining goal 2, proven below
      _ = 0 := smul_zero _
    · -- remaining goal 1
      apply MonoidHom.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
    calc
      (∑ b : MonoidHom.range f.toHomUnits, (b.1 : R))
        = ∑ n ∈ range (orderOf x), (x.1 : R) ^ n :=
        Eq.symm <|
          sum_nbij (x ^ ·) (by simp)
            (by simpa using pow_injOn_Iio_orderOf)
            (fun b _ => let ⟨n, hn⟩ := hx b
              ⟨n % orderOf x, mem_range.2 (Nat.mod_lt _ (orderOf_pos _)), by simp [hn]⟩)
            (by simp)
      _ = 0 := ?_
    rw [← mul_left_inj' hx1, zero_mul, geom_sum_mul]
    norm_cast
    simp [pow_orderOf_eq_one]