awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
K : Type u_3
inst_2 : Field K
inst_3 : Algebra.{u_1, u_3} R[X] K
inst_4 : IsFractionRing.{u_1, u_3} R[X] K
f g : R[X]
hg : g.Monic
hg' : Ne.{u_3 + 1} (α := K) ((algebraMap R[X] K : (a : R[X]) → K) g : K) (0 : K)
refine_2 :
  (algebraMap R[X] K : (a : R[X]) → K) f =
    HAdd.hAdd (α := K) ((algebraMap R[X] K : (a : R[X]) → K) (f %ₘ g) : K)
      (HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) g : K)
        ((algebraMap R[X] K : (a : R[X]) → K) (f /ₘ g) : K))
refine_2₁ :
  (algebraMap R[X] K : (a : R[X]) → K) f =
    HAdd.hAdd (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) (f %ₘ g) : K)
      ((algebraMap R[X] K : (a : R[X]) → K) (g * (f /ₘ g)) : K)
refine_2₂ :
  Eq.{u_3 + 1} (α := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K)
    ((algebraMap R[X] K : (a : R[X]) → K) (f %ₘ g + g * (f /ₘ g)) : K)
⊢ (algebraMap R[X] K : (a : R[X]) → K) f =
    HAdd.hAdd (β := K)
      (HMul.hMul (α := K) (β := K) ((algebraMap R[X] K : (a : R[X]) → K) g : K)
        ((algebraMap R[X] K : (a : R[X]) → K) (f /ₘ g) : K))
      ((algebraMap R[X] K : (a : R[X]) → K) (f %ₘ g) : K)
have refine_2₃ : Eq.{u_3 + 1} (α := K) ((algebraMap R[X] K : (a : R[X]) → K) f : K) ((algebraMap R[X] K : (a : R[X]) → K) f : K)
Tactic: rw [add_comm, ← map_mul, ← map_add, modByMonic_add_div]
-- 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
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) 0
have 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
Tactic: obtain ⟨x, hx⟩ := IsCyclic.exists_monoid_generator (α := MonoidHom.range f.toHomUnits)
-- 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
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
⊢ (↑(↑x : Rˣ) : R) - 1 ≠ 0
have rw : (↑(↑x : Rˣ) : R) ≠ 1
Tactic: rw [sub_ne_zero]
-- 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
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
⊢ (↑(↑x : Rˣ) : R) ≠ 1
have contrapose : ∀ (hf : (↑(↑x : Rˣ) : R) = 1), f = 1
Tactic: contrapose hf
Cleared hypotheses: hf
-- 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
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hf : (↑(↑x : Rˣ) : R) = 1
⊢ f = 1
have h : ∀ (g : G), Eq.{u_1 + 1} (α := R) ((f : (a : G) → R) g : R) ((1 : (a : G) → R) g : R)
Tactic: ext g
-- 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
x : ↥f.toHomUnits.range
hx : ∀ (y : ↥f.toHomUnits.range), Membership.mem (γ := Submonoid ↥f.toHomUnits.range) (Submonoid.powers x) y
hf : (↑(↑x : Rˣ) : R) = 1
g : G
⊢ Eq.{u_1 + 1} (α := R) ((f : (a : G) → R) g : R) ((1 : (a : G) → R) g : R)
have h : ∀ (n : ℕ)
  (hn :
    Eq.{u_1 + 1} (α := ↥f.toHomUnits.range) ((fun (x_1 : ℕ) ↦ x ^ x_1) n : ↥f.toHomUnits.range)
      (Subtype.mk (p := fun (x : Rˣ) ↦ x ∈ f.toHomUnits.range) ((f.toHomUnits : (a : G) → Rˣ) g) sorry :
        ↥f.toHomUnits.range)),
  Eq.{u_1 + 1} (α := R) ((f : (a : G) → R) g : R) ((1 : (a : G) → R) g : R)
Tactic: obtain ⟨n, hn⟩ := hx ⟨f.toHomUnits g, g, rfl⟩
-- Lean 4 proof step from Mathlib.RingTheory.IntegralDomain (hypothesis)
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
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
have hx1 : (↑(↑x : Rˣ) : R) - 1 ≠ 0
Tactic: 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
-- 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
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
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) 0
have calc_1 : ∀ (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
Tactic: 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 _
-- 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
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
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
calc_1 :
  ∀ (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
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) 0
have calc_2 : Eq.{u_1 + 1} (α := R) (∑ b : ↥f.toHomUnits.range, (↑(↑b : Rˣ) : R)) 0
Tactic: 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 _
-- 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
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
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
have calc_1 : Membership.mem (γ := Set Rˣ) (Set.range.{u_1, u_2 + 1} (ι := G) (⇑f.toHomUnits : (a : G) → Rˣ)) u
Tactic: apply MonoidHom.card_fiber_eq_of_mem_range f.toHomUnits
-- 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
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
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
calc_1 : Membership.mem (γ := Set Rˣ) (Set.range.{u_1, u_2 + 1} (ι := G) (⇑f.toHomUnits : (a : G) → Rˣ)) u
⊢ card.{u_2} (α := G) {g : G | (f.toHomUnits : (a : G) → Rˣ) g = u} = c
have calc_1₁ : Membership.mem (γ := Set Rˣ) (Set.range.{u_1, u_2 + 1} (ι := G) (⇑f.toHomUnits : (a : G) → Rˣ)) 1
Tactic: apply MonoidHom.card_fiber_eq_of_mem_range f.toHomUnits
-- 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
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
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
⊢ Eq.{u_1 + 1} (α := R) (∑ b : ↥f.toHomUnits.range, (↑(↑b : Rˣ) : R)) 0
have calc_2 : Eq.{u_1 + 1} (α := R) (∑ n ∈ range (orderOf x), (↑(↑x : Rˣ) : R) ^ n) 0
Tactic: 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 := ?_
-- 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
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
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
⊢ Eq.{u_1 + 1} (α := R) (∑ n ∈ range (orderOf x), (↑(↑x : Rˣ) : R) ^ n) 0
have calc_2 : (↑(↑x : Rˣ) : R) ^ orderOf x - 1 = 0
Tactic: rw [← mul_left_inj' hx1, zero_mul, geom_sum_mul]
-- 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
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
c : ℕ := card.{u_2} (α := G) {g : G | Eq.{u_1 + 1} (α := Rˣ) ((f.toHomUnits : (a : G) → Rˣ) g : Rˣ) (1 : Rˣ)}
⊢ (↑(↑x : Rˣ) : R) ^ orderOf x - 1 = 0
have calc_2 : (↑(↑(x ^ orderOf x) : Rˣ) : R) - 1 = 0
Tactic: norm_cast
-- 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
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) 0
have 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
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]
-- 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
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) 0
have 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
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]
-- 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
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) 0
have 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
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]
-- 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
⊢ 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), Eq.{u_1 + 1} (α := R) (∑ b : ↥f.toHomUnits.range, (↑(↑b : Rˣ) : R)) 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]
-- 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
inst_4 : Decidable (f = 1)
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) (↑(if f = 1 then Fintype.card G else 0) : R)
have pos : ∀ (h : f = 1), Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) (↑(Fintype.card G) : R)
Tactic: split_ifs with h
-- 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
inst_4 : Decidable (f = 1)
pos : ∀ (h : f = 1), Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) (↑(Fintype.card G) : R)
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) (↑(if f = 1 then Fintype.card G else 0) : R)
have neg : ∀ (h : ¬f = 1), Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) (↑0 : R)
Tactic: split_ifs with h
-- 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
inst_4 : Decidable (f = 1)
h : ¬f = 1
⊢ Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) (↑0 : R)
have neg : Eq.{u_1 + 1} (α := R) (∑ g : G, (f : (a : G) → R) g) 0
Tactic: rw [Nat.cast_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Invariant.Basic (goal)
Goal:
A : Type u_1
K : Type u_2
L : Type u_3
B : Type u_4
inst : CommRing A
inst_1 : CommRing B
inst_2 : Field K
inst_3 : Field L
inst_4 : Algebra A K
inst_5 : Algebra B L
inst_6 : IsFractionRing A K
inst_7 : IsFractionRing B L
inst_8 : Algebra A B
inst_9 : Algebra K L
inst_10 : Algebra A L
inst_11 : IsScalarTower A K L
inst_12 : IsScalarTower A B L
inst_13 : IsIntegrallyClosed A
inst_14 : IsIntegralClosure B A L
inst_15 : Algebra.IsAlgebraic K L
this : MulSemiringAction.{u_3, u_4} Gal(L/K) B := IsIntegralClosure.MulSemiringAction A K L B
g : Gal(L/K)
b : B
l : L
⊢ g • b • l = (g • b) • g • l
have simp : HSMul.hSMul (β := L) g ((algebraMap B L : (a : B) → L) b : L) = (algebraMap B L : (a : B) → L) (g • b) ∨ g • l = 0
Tactic: simp only [Algebra.smul_def, smul_mul', mul_eq_mul_right_iff]