awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
⊢ Eq.{v + 1} (α := R')
    (∑ i : R,
      ∑ j : R,
        HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') i : R') ((ψ : (a : R) → R') i : R') *
          HMul.hMul (α := R') (β := R') ((φ : (a : R) → R') j : R') ((ψ : (a : R) → R') j : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))
have conv : Eq.{v + 1} (α := R')
  (∑ x : R,
    ∑ x_1 : R,
      HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') x_1 : R') *
        HMul.hMul (α := R') (β := R') ((ψ : (a : R) → R') x : R') ((ψ : (a : R) → R') x_1 : R'))
  (∑ t : R,
    ∑ x : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
        ((ψ : (a : R) → R') t : R'))
Tactic: conv => enter [1, 2, x, 2, x_1]; rw [mul_mul_mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
⊢ Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ x_1 : R,
        HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') x_1 : R') *
          HMul.hMul (α := R') (β := R') ((ψ : (a : R) → R') x : R') ((ψ : (a : R) → R') x_1 : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))
have simp : Eq.{v + 1} (α := R')
  (∑ x : R,
    ∑ x_1 : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') x_1 : R'))
        ((ψ : (a : R) → R') (x + x_1) : R'))
  (∑ t : R,
    ∑ x : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
        ((ψ : (a : R) → R') t : R'))
Tactic: simp only [← ψ.map_add_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
⊢ Eq.{v + 1} (α := R')
    (∑ y : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') y : R'))
        ((ψ : (a : R) → R') (x + y) : R'))
    (∑ y : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (y - x) : R'))
        ((ψ : (a : R) → R') y : R'))
have hi : ∀ (a : R) (ha : Membership.mem (γ := Finset R) univ a), Membership.mem (γ := Finset R) univ (a + x)
Tactic: rw [sum_bij (fun a _ ↦ a + x)]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
hi : ∀ (a : R) (ha : Membership.mem (γ := Finset R) univ a), Membership.mem (γ := Finset R) univ (a + x)
⊢ Eq.{v + 1} (α := R')
    (∑ y : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') y : R'))
        ((ψ : (a : R) → R') (x + y) : R'))
    (∑ y : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (y - x) : R'))
        ((ψ : (a : R) → R') y : R'))
have i_inj : ∀ (a₁ : R) (ha₁ : Membership.mem (γ := Finset R) univ a₁) (a₂ : R) (ha₂ : Membership.mem (γ := Finset R) univ a₂),
  a₁ + x = a₂ + x → a₁ = a₂
Tactic: rw [sum_bij (fun a _ ↦ a + x)]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
hi : ∀ (a : R) (ha : Membership.mem (γ := Finset R) univ a), Membership.mem (γ := Finset R) univ (a + x)
i_inj :
  ∀ (a₁ : R) (ha₁ : Membership.mem (γ := Finset R) univ a₁) (a₂ : R) (ha₂ : Membership.mem (γ := Finset R) univ a₂),
    a₁ + x = a₂ + x → a₁ = a₂
⊢ Eq.{v + 1} (α := R')
    (∑ y : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') y : R'))
        ((ψ : (a : R) → R') (x + y) : R'))
    (∑ y : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (y - x) : R'))
        ((ψ : (a : R) → R') y : R'))
have i_surj : ∀ (b : R), Membership.mem (γ := Finset R) univ b → ∃ (a : R) (_ : Membership.mem (γ := Finset R) univ a), a + x = b
Tactic: rw [sum_bij (fun a _ ↦ a + x)]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x : R
hi : ∀ (a : R) (ha : Membership.mem (γ := Finset R) univ a), Membership.mem (γ := Finset R) univ (a + x)
i_inj :
  ∀ (a₁ : R) (ha₁ : Membership.mem (γ := Finset R) univ a₁) (a₂ : R) (ha₂ : Membership.mem (γ := Finset R) univ a₂),
    a₁ + x = a₂ + x → a₁ = a₂
i_surj :
  ∀ (b : R), Membership.mem (γ := Finset R) univ b → ∃ (a : R) (_ : Membership.mem (γ := Finset R) univ a), a + x = b
⊢ Eq.{v + 1} (α := R')
    (∑ y : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') y : R'))
        ((ψ : (a : R) → R') (x + y) : R'))
    (∑ y : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (y - x) : R'))
        ((ψ : (a : R) → R') y : R'))
have h : ∀ (a : R) (ha : Membership.mem (γ := Finset R) univ a),
  HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') a : R'))
      ((ψ : (a : R) → R') (x + a) : R') =
    HMul.hMul (β := R')
      (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (a + x - x) : R'))
      ((ψ : (a : R) → R') (a + x) : R')
Tactic: rw [sum_bij (fun a _ ↦ a + x)]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x b : R
h : Membership.mem (γ := Finset R) univ b
⊢ b - x + x = b
have rw : b = b
Tactic: rw [sub_add_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x a : R
h : Membership.mem (γ := Finset R) univ a
⊢ HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') a : R'))
      ((ψ : (a : R) → R') (x + a) : R') =
    HMul.hMul (β := R')
      (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (a + x - x) : R'))
      ((ψ : (a : R) → R') (a + x) : R')
have rw : HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') a : R'))
    ((ψ : (a : R) → R') (x + a) : R') =
  HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') a : R'))
    ((ψ : (a : R) → R') (a + x) : R')
Tactic: rw [add_sub_cancel_right, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
x a : R
h : Membership.mem (γ := Finset R) univ a
rw :
  HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') a : R'))
      ((ψ : (a : R) → R') (x + a) : R') =
    HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') a : R'))
      ((ψ : (a : R) → R') (a + x) : R')
⊢ HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') a : R'))
      ((ψ : (a : R) → R') (x + a) : R') =
    HMul.hMul (β := R')
      (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (a + x - x) : R'))
      ((ψ : (a : R) → R') (a + x) : R')
have rw₁ : HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') a : R'))
    ((ψ : (a : R) → R') (a + x) : R') =
  HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') a : R'))
    ((ψ : (a : R) → R') (a + x) : R')
Tactic: rw [add_sub_cancel_right, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (hypothesis)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
⊢ Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ x_1 : R,
        HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') x_1 : R'))
          ((ψ : (a : R) → R') (x + x_1) : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))
have sum_eq : ∀ (x : R),
  Eq.{v + 1} (α := R')
    (∑ y : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') y : R'))
        ((ψ : (a : R) → R') (x + y) : R'))
    (∑ y : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (y - x) : R'))
        ((ψ : (a : R) → R') y : R'))
Tactic: have sum_eq x : ∑ y : R, χ x * φ y * ψ (x + y) = ∑ y : R, χ x * φ (y - x) * ψ y := by
    rw [sum_bij (fun a _ ↦ a + x)]
    · simp only [mem_univ, forall_const]
    · simp only [mem_univ, add_left_inj, imp_self, forall_const]
    · exact fun b _ ↦ ⟨b - x, mem_univ _, by rw [sub_add_cancel]⟩
    · exact fun a _ ↦ by rw [add_sub_cancel_right, add_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
sum_eq :
  ∀ (x : R),
    Eq.{v + 1} (α := R')
      (∑ y : R,
        HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') y : R'))
          ((ψ : (a : R) → R') (x + y) : R'))
      (∑ y : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (y - x) : R'))
          ((ψ : (a : R) → R') y : R'))
⊢ Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ x_1 : R,
        HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') x_1 : R'))
          ((ψ : (a : R) → R') (x + x_1) : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))
have rw : Eq.{v + 1} (α := R')
  (∑ x : R,
    ∑ y : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (y - x) : R'))
        ((ψ : (a : R) → R') y : R'))
  (∑ t : R,
    ∑ x : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
        ((ψ : (a : R) → R') t : R'))
Tactic: rw [sum_congr rfl fun x _ ↦ sum_eq x, sum_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ φ : MulChar R R'
ψ : AddChar R R'
sum_eq :
  ∀ (x : R),
    Eq.{v + 1} (α := R')
      (∑ y : R,
        HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') y : R'))
          ((ψ : (a : R) → R') (x + y) : R'))
      (∑ y : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (y - x) : R'))
          ((ψ : (a : R) → R') y : R'))
rw :
  Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ y : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (y - x) : R'))
          ((ψ : (a : R) → R') y : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))
⊢ Eq.{v + 1} (α := R')
    (∑ x : R,
      ∑ x_1 : R,
        HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') x_1 : R'))
          ((ψ : (a : R) → R') (x + x_1) : R'))
    (∑ t : R,
      ∑ x : R,
        HMul.hMul (β := R')
          (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
          ((ψ : (a : R) → R') t : R'))
have rw₁ : Eq.{v + 1} (α := R')
  (∑ y : R,
    ∑ x : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (y - x) : R'))
        ((ψ : (a : R) → R') y : R'))
  (∑ t : R,
    ∑ x : R,
      HMul.hMul (β := R') (HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((φ : (a : R) → R') (t - x) : R'))
        ((ψ : (a : R) → R') t : R'))
Tactic: rw [sum_congr rfl fun x _ ↦ sum_eq x, sum_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
χ : MulChar R R'
ψ : AddChar R R'
⊢ HMul.hMul (α := R') ((χ : (a : R) → R') (-1) : R') (gaussSum χ ψ⁻¹) = gaussSum χ ψ
have rw : HMul.hMul (α := R') ((χ : (a : R) → R') (↑(-1) : R) : R') (gaussSum χ (ψ.mulShift (↑(-1) : R))) = gaussSum χ ψ
Tactic: rw [ψ.inv_mulShift, ← Units.coe_neg_one]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
⊢ Eq.{v + 1} (α := R')
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (a * b⁻¹) : R') ((ψ : (a : R) → R') (a - b) : R'))
    (∑ c : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') c : R') ((ψ : (a : R) → R') (b * (c - 1)) : R'))
have inl : ∀ (hb : b = 0),
  Eq.{v + 1} (α := R')
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (a * b⁻¹) : R') ((ψ : (a : R) → R') (a - b) : R'))
    (∑ c : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') c : R') ((ψ : (a : R) → R') (b * (c - 1)) : R'))
Tactic: rcases eq_or_ne b 0 with hb | hb
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
inl :
  ∀ (hb : b = 0),
    Eq.{v + 1} (α := R')
      (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (a * b⁻¹) : R') ((ψ : (a : R) → R') (a - b) : R'))
      (∑ c : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') c : R') ((ψ : (a : R) → R') (b * (c - 1)) : R'))
⊢ Eq.{v + 1} (α := R')
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (a * b⁻¹) : R') ((ψ : (a : R) → R') (a - b) : R'))
    (∑ c : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') c : R') ((ψ : (a : R) → R') (b * (c - 1)) : R'))
have inr : ∀ (hb : b ≠ 0),
  Eq.{v + 1} (α := R')
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (a * b⁻¹) : R') ((ψ : (a : R) → R') (a - b) : R'))
    (∑ c : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') c : R') ((ψ : (a : R) → R') (b * (c - 1)) : R'))
Tactic: rcases eq_or_ne b 0 with hb | hb
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
hb : b ≠ 0
⊢ Eq.{v + 1} (α := R')
    (∑ a : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (a * b⁻¹) : R') ((ψ : (a : R) → R') (a - b) : R'))
    (∑ c : R, HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') c : R') ((ψ : (a : R) → R') (b * (c - 1)) : R'))
have inr : ∀ (x : R),
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * x * b⁻¹) : R') ((ψ : (a : R) → R') (b * x - b) : R')
Tactic: refine (Fintype.sum_bijective _ (mulLeft_bijective₀ b hb) _ _ fun x ↦ ?_).symm
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
hb : b ≠ 0
x : R
⊢ HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * x * b⁻¹) : R') ((ψ : (a : R) → R') (b * x - b) : R')
have inr : HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * (x * b⁻¹)) : R') ((ψ : (a : R) → R') (b * x - b) : R')
Tactic: rw [mul_assoc, mul_comm x, ← mul_assoc, mul_inv_cancel₀ hb, one_mul, mul_sub, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
hb : b ≠ 0
x : R
inr :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * (x * b⁻¹)) : R') ((ψ : (a : R) → R') (b * x - b) : R')
⊢ HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * x * b⁻¹) : R') ((ψ : (a : R) → R') (b * x - b) : R')
have inr₁ : HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * (b⁻¹ * x)) : R') ((ψ : (a : R) → R') (b * x - b) : R')
Tactic: rw [mul_assoc, mul_comm x, ← mul_assoc, mul_inv_cancel₀ hb, one_mul, mul_sub, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
hb : b ≠ 0
x : R
inr :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * (x * b⁻¹)) : R') ((ψ : (a : R) → R') (b * x - b) : R')
inr₁ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * (b⁻¹ * x)) : R') ((ψ : (a : R) → R') (b * x - b) : R')
⊢ HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * x * b⁻¹) : R') ((ψ : (a : R) → R') (b * x - b) : R')
have inr₂ : HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * b⁻¹ * x) : R') ((ψ : (a : R) → R') (b * x - b) : R')
Tactic: rw [mul_assoc, mul_comm x, ← mul_assoc, mul_inv_cancel₀ hb, one_mul, mul_sub, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
hb : b ≠ 0
x : R
inr :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * (x * b⁻¹)) : R') ((ψ : (a : R) → R') (b * x - b) : R')
inr₁ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * (b⁻¹ * x)) : R') ((ψ : (a : R) → R') (b * x - b) : R')
inr₂ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * b⁻¹ * x) : R') ((ψ : (a : R) → R') (b * x - b) : R')
⊢ HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * x * b⁻¹) : R') ((ψ : (a : R) → R') (b * x - b) : R')
have inr₃ : HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (1 * x) : R') ((ψ : (a : R) → R') (b * x - b) : R')
Tactic: rw [mul_assoc, mul_comm x, ← mul_assoc, mul_inv_cancel₀ hb, one_mul, mul_sub, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
hb : b ≠ 0
x : R
inr :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * (x * b⁻¹)) : R') ((ψ : (a : R) → R') (b * x - b) : R')
inr₁ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * (b⁻¹ * x)) : R') ((ψ : (a : R) → R') (b * x - b) : R')
inr₂ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * b⁻¹ * x) : R') ((ψ : (a : R) → R') (b * x - b) : R')
inr₃ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (1 * x) : R') ((ψ : (a : R) → R') (b * x - b) : R')
⊢ HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * x * b⁻¹) : R') ((ψ : (a : R) → R') (b * x - b) : R')
have inr₄ : HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * x - b) : R')
Tactic: rw [mul_assoc, mul_comm x, ← mul_assoc, mul_inv_cancel₀ hb, one_mul, mul_sub, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.GaussSum (goal)
Goal:
R : Type u
inst : Field R
inst_1 : Fintype R
R' : Type v
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
ψ : AddChar R R'
b : R
hb : b ≠ 0
x : R
inr :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * (x * b⁻¹)) : R') ((ψ : (a : R) → R') (b * x - b) : R')
inr₁ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * (b⁻¹ * x)) : R') ((ψ : (a : R) → R') (b * x - b) : R')
inr₂ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * b⁻¹ * x) : R') ((ψ : (a : R) → R') (b * x - b) : R')
inr₃ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (1 * x) : R') ((ψ : (a : R) → R') (b * x - b) : R')
inr₄ :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * x - b) : R')
⊢ HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * (x - 1)) : R') =
    HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (b * x * b⁻¹) : R') ((ψ : (a : R) → R') (b * x - b) : R')
have inr₅ : HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * x - b * 1) : R') =
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') x : R') ((ψ : (a : R) → R') (b * x - b) : R')
Tactic: rw [mul_assoc, mul_comm x, ← mul_assoc, mul_inv_cancel₀ hb, one_mul, mul_sub, mul_one]