awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
hn : Even (2 * n)
⊢ χ ^ (2 * n) = 1
have rw : HPow.hPow (β := ℕ) χ 2 ^ n = 1
Tactic: rw [pow_mul, hχ.sq_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
hn : Even (2 * n)
rw : HPow.hPow (β := ℕ) χ 2 ^ n = 1
⊢ χ ^ (2 * n) = 1
have rw₁ : HPow.hPow (α := MulChar R R') 1 n = 1
Tactic: rw [pow_mul, hχ.sq_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
hn : Even (2 * n)
rw : HPow.hPow (β := ℕ) χ 2 ^ n = 1
rw₁ : HPow.hPow (α := MulChar R R') 1 n = 1
⊢ χ ^ (2 * n) = 1
have rw₂ : Eq (α := MulChar R R') 1 1
Tactic: rw [pow_mul, hχ.sq_eq_one, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
hn : Odd n
⊢ χ ^ n = χ
have obtain : ∀ (n : ℕ), χ ^ (2 * n + 1) = χ
Tactic: obtain ⟨n, rfl⟩ := hn
Cleared hypotheses: n, hn
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
⊢ χ ^ (2 * n + 1) = χ
have rw : χ ^ (2 * n) * HPow.hPow (β := ℕ) χ 1 = χ
Tactic: rw [pow_add, pow_one, hχ.pow_even (even_two_mul _), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
rw : χ ^ (2 * n) * HPow.hPow (β := ℕ) χ 1 = χ
⊢ χ ^ (2 * n + 1) = χ
have rw₁ : χ ^ (2 * n) * χ = χ
Tactic: rw [pow_add, pow_one, hχ.pow_even (even_two_mul _), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
rw : χ ^ (2 * n) * HPow.hPow (β := ℕ) χ 1 = χ
rw₁ : χ ^ (2 * n) * χ = χ
⊢ χ ^ (2 * n + 1) = χ
have rw₂ : 1 * χ = χ
Tactic: rw [pow_add, pow_one, hχ.pow_even (even_two_mul _), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
rw : χ ^ (2 * n) * HPow.hPow (β := ℕ) χ 1 = χ
rw₁ : χ ^ (2 * n) * χ = χ
rw₂ : 1 * χ = χ
⊢ χ ^ (2 * n + 1) = χ
have rw₃ : χ = χ
Tactic: rw [pow_add, pow_one, hχ.pow_even (even_two_mul _), one_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_4
R : Type u_5
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
χ : MulChar M R
⊢ χ.IsQuadratic ↔ HPow.hPow (β := ℕ) χ 2 = 1
have refine_1 : ∀ (h : χ.IsQuadratic) (x : Mˣ),
  Eq.{u_5 + 1} (α := R) ((HPow.hPow (β := ℕ) χ 2 : (a : M) → R) (↑x : M) : R) ((1 : (a : M) → R) (↑x : M) : R)
Tactic: refine ⟨fun h ↦ ext (fun x ↦ ?_), fun h x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_4
R : Type u_5
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
χ : MulChar M R
refine_1 :
  ∀ (h : χ.IsQuadratic) (x : Mˣ),
    Eq.{u_5 + 1} (α := R) ((HPow.hPow (β := ℕ) χ 2 : (a : M) → R) (↑x : M) : R) ((1 : (a : M) → R) (↑x : M) : R)
⊢ χ.IsQuadratic ↔ HPow.hPow (β := ℕ) χ 2 = 1
have refine_2 : ∀ (h : HPow.hPow (β := ℕ) χ 2 = 1) (x : M),
  Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (0 : R) ∨
    Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (1 : R) ∨ Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (-1 : R)
Tactic: refine ⟨fun h ↦ ext (fun x ↦ ?_), fun h x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_4
R : Type u_5
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
⊢ Eq.{u_5 + 1} (α := R) ((HPow.hPow (β := ℕ) χ 2 : (a : M) → R) (↑x : M) : R) ((1 : (a : M) → R) (↑x : M) : R)
have refine_1 : HPow.hPow (α := R) (β := ℕ) ((χ : (a : M) → R) (↑x : M) : R) 2 = 1
Tactic: rw [one_apply_coe, χ.pow_apply_coe]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_4
R : Type u_5
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
⊢ HPow.hPow (α := R) (β := ℕ) ((χ : (a : M) → R) (↑x : M) : R) 2 = 1
have refine_1 : ∀ (H : Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) (↑x : M) : R) (0 : R)),
  HPow.hPow (α := R) (β := ℕ) ((χ : (a : M) → R) (↑x : M) : R) 2 = 1
Tactic: rcases h x with H | H | H
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_4
R : Type u_5
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
refine_1 :
  ∀ (H : Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) (↑x : M) : R) (0 : R)),
    HPow.hPow (α := R) (β := ℕ) ((χ : (a : M) → R) (↑x : M) : R) 2 = 1
⊢ HPow.hPow (α := R) (β := ℕ) ((χ : (a : M) → R) (↑x : M) : R) 2 = 1
have refine_1₁ : ∀ (H : Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) (↑x : M) : R) (1 : R)),
  HPow.hPow (α := R) (β := ℕ) ((χ : (a : M) → R) (↑x : M) : R) 2 = 1
Tactic: rcases h x with H | H | H
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_4
R : Type u_5
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
χ : MulChar M R
h : χ.IsQuadratic
x : Mˣ
refine_1 :
  ∀ (H : Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) (↑x : M) : R) (0 : R)),
    HPow.hPow (α := R) (β := ℕ) ((χ : (a : M) → R) (↑x : M) : R) 2 = 1
refine_1₁ :
  ∀ (H : Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) (↑x : M) : R) (1 : R)),
    HPow.hPow (α := R) (β := ℕ) ((χ : (a : M) → R) (↑x : M) : R) 2 = 1
⊢ HPow.hPow (α := R) (β := ℕ) ((χ : (a : M) → R) (↑x : M) : R) 2 = 1
have refine_1₂ : ∀ (H : Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) (↑x : M) : R) (-1 : R)),
  HPow.hPow (α := R) (β := ℕ) ((χ : (a : M) → R) (↑x : M) : R) 2 = 1
Tactic: rcases h x with H | H | H
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_4
R : Type u_5
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
χ : MulChar M R
h : HPow.hPow (β := ℕ) χ 2 = 1
x : M
⊢ Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (0 : R) ∨
    Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (1 : R) ∨ Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (-1 : R)
have pos : ∀ (hx : IsUnit x),
  Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (0 : R) ∨
    Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (1 : R) ∨ Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (-1 : R)
Tactic: by_cases hx : IsUnit x
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_4
R : Type u_5
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
χ : MulChar M R
h : HPow.hPow (β := ℕ) χ 2 = 1
x : M
pos :
  ∀ (hx : IsUnit x),
    Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (0 : R) ∨
      Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (1 : R) ∨ Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (-1 : R)
⊢ Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (0 : R) ∨
    Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (1 : R) ∨ Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (-1 : R)
have neg : ∀ (hx : ¬IsUnit x),
  Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (0 : R) ∨
    Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (1 : R) ∨ Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (-1 : R)
Tactic: by_cases hx : IsUnit x
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_4
R : Type u_5
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
χ : MulChar M R
h : HPow.hPow (β := ℕ) χ 2 = 1
x : M
hx : IsUnit x
⊢ Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (0 : R) ∨
    Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (1 : R) ∨ Eq.{u_5 + 1} (α := R) ((χ : (a : M) → R) x : R) (-1 : R)
have pos : HPow.hPow (α := R) (β := ℕ) ((χ : (a : M) → R) x : R) 2 = 1
Tactic: refine .inr <| sq_eq_one_iff.mp ?_
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_4
R : Type u_5
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
χ : MulChar M R
h : HPow.hPow (β := ℕ) χ 2 = 1
x : M
hx : IsUnit x
⊢ HPow.hPow (α := R) (β := ℕ) ((χ : (a : M) → R) x : R) 2 = 1
have pos : Eq.{u_5 + 1} (α := R) ((HPow.hPow (β := ℕ) χ 2 : (a : M) → R) x : R) (1 : R)
Tactic: rw [← χ.pow_apply' two_ne_zero, h, MulChar.one_apply hx]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_4
R : Type u_5
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
χ : MulChar M R
h : HPow.hPow (β := ℕ) χ 2 = 1
x : M
hx : IsUnit x
pos : Eq.{u_5 + 1} (α := R) ((HPow.hPow (β := ℕ) χ 2 : (a : M) → R) x : R) (1 : R)
⊢ HPow.hPow (α := R) (β := ℕ) ((χ : (a : M) → R) x : R) 2 = 1
have pos₁ : Eq.{u_5 + 1} (α := R) ((1 : (a : M) → R) x : R) (1 : R)
Tactic: rw [← χ.pow_apply' two_ne_zero, h, MulChar.one_apply hx]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_4
R : Type u_5
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : NoZeroDivisors R
inst_3 : Nontrivial R
χ : MulChar M R
h : HPow.hPow (β := ℕ) χ 2 = 1
x : M
hx : IsUnit x
pos : Eq.{u_5 + 1} (α := R) ((HPow.hPow (β := ℕ) χ 2 : (a : M) → R) x : R) (1 : R)
pos₁ : Eq.{u_5 + 1} (α := R) ((1 : (a : M) → R) x : R) (1 : R)
⊢ HPow.hPow (α := R) (β := ℕ) ((χ : (a : M) → R) x : R) 2 = 1
have pos₂ : Eq.{u_5 + 1} (α := R) 1 1
Tactic: rw [← χ.pow_apply' two_ne_zero, h, MulChar.one_apply hx]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
R : Type u_2
inst_1 : CommMonoidWithZero R
inst_2 : Fintype Mˣ
χ : MulChar M R
⊢ χ ^ Fintype.card.{u_1} Mˣ = 1
have h : ∀ (a : Mˣ),
  Eq.{u_2 + 1} (α := R) ((χ ^ Fintype.card.{u_1} Mˣ : (a : M) → R) (↑a : M) : R) ((1 : (a : M) → R) (↑a : M) : R)
Tactic: ext1
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
R : Type u_2
inst_1 : CommMonoidWithZero R
inst_2 : Fintype Mˣ
χ : MulChar M R
a : Mˣ
⊢ Eq.{u_2 + 1} (α := R) ((χ ^ Fintype.card.{u_1} Mˣ : (a : M) → R) (↑a : M) : R) ((1 : (a : M) → R) (↑a : M) : R)
have h : HPow.hPow (α := R) ((χ : (a : M) → R) (↑a : M) : R) (Fintype.card.{u_1} Mˣ) = (1 : (a : M) → R) (↑a : M)
Tactic: rw [pow_apply_coe, ← map_pow, one_apply_coe, ← Units.val_pow_eq_pow_val, pow_card_eq_one,
    Units.val_eq_one.mpr rfl, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
R : Type u_2
inst_1 : CommMonoidWithZero R
inst_2 : Fintype Mˣ
χ : MulChar M R
a : Mˣ
h : HPow.hPow (α := R) ((χ : (a : M) → R) (↑a : M) : R) (Fintype.card.{u_1} Mˣ) = (1 : (a : M) → R) (↑a : M)
⊢ Eq.{u_2 + 1} (α := R) ((χ ^ Fintype.card.{u_1} Mˣ : (a : M) → R) (↑a : M) : R) ((1 : (a : M) → R) (↑a : M) : R)
have h₁ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) ((↑a : M) ^ Fintype.card.{u_1} Mˣ) : R) ((1 : (a : M) → R) (↑a : M) : R)
Tactic: rw [pow_apply_coe, ← map_pow, one_apply_coe, ← Units.val_pow_eq_pow_val, pow_card_eq_one,
    Units.val_eq_one.mpr rfl, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
R : Type u_2
inst_1 : CommMonoidWithZero R
inst_2 : Fintype Mˣ
χ : MulChar M R
a : Mˣ
h : HPow.hPow (α := R) ((χ : (a : M) → R) (↑a : M) : R) (Fintype.card.{u_1} Mˣ) = (1 : (a : M) → R) (↑a : M)
h₁ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) ((↑a : M) ^ Fintype.card.{u_1} Mˣ) : R) ((1 : (a : M) → R) (↑a : M) : R)
⊢ Eq.{u_2 + 1} (α := R) ((χ ^ Fintype.card.{u_1} Mˣ : (a : M) → R) (↑a : M) : R) ((1 : (a : M) → R) (↑a : M) : R)
have h₂ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) ((↑a : M) ^ Fintype.card.{u_1} Mˣ) : R) (1 : R)
Tactic: rw [pow_apply_coe, ← map_pow, one_apply_coe, ← Units.val_pow_eq_pow_val, pow_card_eq_one,
    Units.val_eq_one.mpr rfl, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
R : Type u_2
inst_1 : CommMonoidWithZero R
inst_2 : Fintype Mˣ
χ : MulChar M R
a : Mˣ
h : HPow.hPow (α := R) ((χ : (a : M) → R) (↑a : M) : R) (Fintype.card.{u_1} Mˣ) = (1 : (a : M) → R) (↑a : M)
h₁ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) ((↑a : M) ^ Fintype.card.{u_1} Mˣ) : R) ((1 : (a : M) → R) (↑a : M) : R)
h₂ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) ((↑a : M) ^ Fintype.card.{u_1} Mˣ) : R) (1 : R)
⊢ Eq.{u_2 + 1} (α := R) ((χ ^ Fintype.card.{u_1} Mˣ : (a : M) → R) (↑a : M) : R) ((1 : (a : M) → R) (↑a : M) : R)
have h₃ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑(a ^ Fintype.card.{u_1} Mˣ) : M) : R) (1 : R)
Tactic: rw [pow_apply_coe, ← map_pow, one_apply_coe, ← Units.val_pow_eq_pow_val, pow_card_eq_one,
    Units.val_eq_one.mpr rfl, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
R : Type u_2
inst_1 : CommMonoidWithZero R
inst_2 : Fintype Mˣ
χ : MulChar M R
a : Mˣ
h : HPow.hPow (α := R) ((χ : (a : M) → R) (↑a : M) : R) (Fintype.card.{u_1} Mˣ) = (1 : (a : M) → R) (↑a : M)
h₁ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) ((↑a : M) ^ Fintype.card.{u_1} Mˣ) : R) ((1 : (a : M) → R) (↑a : M) : R)
h₂ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) ((↑a : M) ^ Fintype.card.{u_1} Mˣ) : R) (1 : R)
h₃ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑(a ^ Fintype.card.{u_1} Mˣ) : M) : R) (1 : R)
⊢ Eq.{u_2 + 1} (α := R) ((χ ^ Fintype.card.{u_1} Mˣ : (a : M) → R) (↑a : M) : R) ((1 : (a : M) → R) (↑a : M) : R)
have h₄ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑1 : M) : R) (1 : R)
Tactic: rw [pow_apply_coe, ← map_pow, one_apply_coe, ← Units.val_pow_eq_pow_val, pow_card_eq_one,
    Units.val_eq_one.mpr rfl, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
R : Type u_2
inst_1 : CommMonoidWithZero R
inst_2 : Fintype Mˣ
χ : MulChar M R
a : Mˣ
h : HPow.hPow (α := R) ((χ : (a : M) → R) (↑a : M) : R) (Fintype.card.{u_1} Mˣ) = (1 : (a : M) → R) (↑a : M)
h₁ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) ((↑a : M) ^ Fintype.card.{u_1} Mˣ) : R) ((1 : (a : M) → R) (↑a : M) : R)
h₂ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) ((↑a : M) ^ Fintype.card.{u_1} Mˣ) : R) (1 : R)
h₃ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑(a ^ Fintype.card.{u_1} Mˣ) : M) : R) (1 : R)
h₄ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑1 : M) : R) (1 : R)
⊢ Eq.{u_2 + 1} (α := R) ((χ ^ Fintype.card.{u_1} Mˣ : (a : M) → R) (↑a : M) : R) ((1 : (a : M) → R) (↑a : M) : R)
have h₅ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) 1 : R) (1 : R)
Tactic: rw [pow_apply_coe, ← map_pow, one_apply_coe, ← Units.val_pow_eq_pow_val, pow_card_eq_one,
    Units.val_eq_one.mpr rfl, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
R : Type u_2
inst_1 : CommMonoidWithZero R
inst_2 : Fintype Mˣ
χ : MulChar M R
a : Mˣ
h : HPow.hPow (α := R) ((χ : (a : M) → R) (↑a : M) : R) (Fintype.card.{u_1} Mˣ) = (1 : (a : M) → R) (↑a : M)
h₁ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) ((↑a : M) ^ Fintype.card.{u_1} Mˣ) : R) ((1 : (a : M) → R) (↑a : M) : R)
h₂ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) ((↑a : M) ^ Fintype.card.{u_1} Mˣ) : R) (1 : R)
h₃ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑(a ^ Fintype.card.{u_1} Mˣ) : M) : R) (1 : R)
h₄ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑1 : M) : R) (1 : R)
h₅ : Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) 1 : R) (1 : R)
⊢ Eq.{u_2 + 1} (α := R) ((χ ^ Fintype.card.{u_1} Mˣ : (a : M) → R) (↑a : M) : R) ((1 : (a : M) → R) (↑a : M) : R)
have h₆ : Eq.{u_2 + 1} (α := R) 1 1
Tactic: rw [pow_apply_coe, ← map_pow, one_apply_coe, ← Units.val_pow_eq_pow_val, pow_card_eq_one,
    Units.val_eq_one.mpr rfl, map_one]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
R : Type u_2
inst_1 : CommMonoidWithZero R
inst_2 : Finite.{u_1 + 1} Mˣ
χ : MulChar M R
⊢ 0 < orderOf χ
have intro : ∀ (val : Fintype Mˣ), 0 < orderOf χ
Tactic: cases nonempty_fintype Mˣ
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
M : Type u_1
inst : CommMonoid M
R : Type u_2
inst_1 : CommMonoidWithZero R
inst_2 : Finite.{u_1 + 1} Mˣ
χ : MulChar M R
val : Fintype Mˣ
⊢ 0 < orderOf χ
have intro : IsOfFinOrder χ
Tactic: apply IsOfFinOrder.orderOf_pos
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
inst_1 : Fintype R
R' : Type u_2
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
⊢ Eq.{u_2 + 1} (α := R') (∑ a : R, (χ : (a : R) → R') a) 0
have rcases : ∀ (b : Rˣ) (hb : Ne.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑b : R) : R') (1 : R')),
  Eq.{u_2 + 1} (α := R') (∑ a : R, (χ : (a : R) → R') a) 0
Tactic: rcases ne_one_iff.mp hχ with ⟨b, hb⟩
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
inst_1 : Fintype R
R' : Type u_2
inst_2 : CommRing R'
inst_3 : IsDomain R'
χ : MulChar R R'
hχ : χ ≠ 1
b : Rˣ
hb : Ne.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑b : R) : R') (1 : R')
⊢ Eq.{u_2 + 1} (α := R') (∑ a : R, (χ : (a : R) → R') a) 0
have refine : HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (↑b : R) : R') (∑ a : R, (χ : (a : R) → R') a : R') =
  ∑ a : R, (χ : (a : R) → R') a
Tactic: refine eq_zero_of_mul_eq_self_left hb ?_
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
inst_1 : Fintype R
R' : Type u_2
inst_2 : CommRing R'
inst_3 : DecidableEq R
⊢ Eq.{u_2 + 1} (α := R') (∑ a : R, (1 : (a : R) → R') a) (↑(Fintype.card.{u_1} Rˣ) : R')
have calc_1 : ∀ (a : R),
  Membership.mem (γ := Finset R) Finset.univ a →
    Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') a : R') (if IsUnit a then 1 else 0 : R')
Tactic: calc
    (∑ a, (1 : MulChar R R') a) = ∑ a : R, if IsUnit a then 1 else 0 :=
      Finset.sum_congr rfl fun a _ => ?_
    _ = ((Finset.univ : Finset R).filter IsUnit).card := Finset.sum_boole _ _
    _ = (Finset.univ.map ⟨((↑) : Rˣ → R), Units.val_injective⟩).card := ?_
    _ = Fintype.card Rˣ := congr_arg _ (Finset.card_map _)
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
inst_1 : Fintype R
R' : Type u_2
inst_2 : CommRing R'
inst_3 : DecidableEq R
calc_1 :
  ∀ (a : R),
    Membership.mem (γ := Finset R) Finset.univ a →
      Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') a : R') (if IsUnit a then 1 else 0 : R')
⊢ Eq.{u_2 + 1} (α := R') (∑ a : R, (1 : (a : R) → R') a) (↑(Fintype.card.{u_1} Rˣ) : R')
have calc_2 : Eq.{u_2 + 1} (α := R') (↑(Finset.card.{u_1} (α := R) (Finset.filter IsUnit Finset.univ)) : R')
  (↑(Finset.card.{u_1} (α := R) (Finset.map (α := Rˣ) { toFun := Units.val, inj' := sorry } Finset.univ)) : R')
Tactic: calc
    (∑ a, (1 : MulChar R R') a) = ∑ a : R, if IsUnit a then 1 else 0 :=
      Finset.sum_congr rfl fun a _ => ?_
    _ = ((Finset.univ : Finset R).filter IsUnit).card := Finset.sum_boole _ _
    _ = (Finset.univ.map ⟨((↑) : Rˣ → R), Units.val_injective⟩).card := ?_
    _ = Fintype.card Rˣ := congr_arg _ (Finset.card_map _)
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
inst_1 : Fintype R
R' : Type u_2
inst_2 : CommRing R'
inst_3 : DecidableEq R
a : R
h : Membership.mem (γ := Finset R) Finset.univ a
⊢ Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') a : R') (if IsUnit a then 1 else 0 : R')
have pos : ∀ (h : IsUnit a), Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') a : R') (1 : R')
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
inst_1 : Fintype R
R' : Type u_2
inst_2 : CommRing R'
inst_3 : DecidableEq R
a : R
h : Membership.mem (γ := Finset R) Finset.univ a
pos : ∀ (h : IsUnit a), Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') a : R') (1 : R')
⊢ Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') a : R') (if IsUnit a then 1 else 0 : R')
have neg : ∀ (h : ¬IsUnit a), Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') a : R') (0 : R')
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
inst_1 : Fintype R
R' : Type u_2
inst_2 : CommRing R'
inst_3 : DecidableEq R
⊢ Eq.{u_2 + 1} (α := R') (↑(Finset.card.{u_1} (α := R) (Finset.filter IsUnit Finset.univ)) : R')
    (↑(Finset.card.{u_1} (α := R) (Finset.map (α := Rˣ) { toFun := Units.val, inj' := ⋯ } Finset.univ)) : R')
have calc_2 : Eq.{u_1 + 1} (α := Finset R) (Finset.filter IsUnit Finset.univ)
  (Finset.map (α := Rˣ) { toFun := Units.val, inj' := sorry } Finset.univ)
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
inst : CommMonoid R
inst_1 : Fintype R
R' : Type u_2
inst_2 : CommRing R'
inst_3 : DecidableEq R
⊢ Eq.{u_1 + 1} (α := Finset R) (Finset.filter IsUnit Finset.univ)
    (Finset.map (α := Rˣ) { toFun := Units.val, inj' := ⋯ } Finset.univ)
have calc_2 : ∀ (a : R),
  Membership.mem (γ := Finset R) (Finset.filter IsUnit Finset.univ) a ↔
    Membership.mem (γ := Finset R) (Finset.map (α := Rˣ) { toFun := Units.val, inj' := sorry } Finset.univ) a
Tactic: ext a
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Basic (goal)
Goal:
R : Type u_1
R' : Type u_2
inst : CommRing R
inst_1 : CommMonoidWithZero R'
χ : MulChar R R'
n : ℕ
hn : Odd n
hχ : χ ^ n = 1
⊢ Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (-1) : R') (1 : R')
have rw : Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') (-1) : R') (1 : R')
Tactic: rw [← hn.neg_one_pow, map_pow, ← χ.pow_apply' (Nat.ne_of_odd_add hn), hχ]
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
a : Mˣ
⊢ (∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)) ↔
    ∃ (φ : MonoidHom.{u_1, u_2} Mˣ Rˣ), Ne.{u_2 + 1} (α := Rˣ) ((φ : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)
have refine_1 : (∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)) →
  ∀ (χ : MulChar M R) (hχ : Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)),
    Ne.{u_2 + 1} (α := Rˣ) ((χ.toUnitHom : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)
Tactic: refine ⟨fun ⟨χ, hχ⟩ ↦ ⟨χ.toUnitHom, ?_⟩, fun ⟨φ, hφ⟩ ↦ ⟨ofUnitHom φ, ?_⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
a : Mˣ
refine_1 :
  (∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)) →
    ∀ (χ : MulChar M R) (hχ : Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)),
      Ne.{u_2 + 1} (α := Rˣ) ((χ.toUnitHom : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)
⊢ (∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)) ↔
    ∃ (φ : MonoidHom.{u_1, u_2} Mˣ Rˣ), Ne.{u_2 + 1} (α := Rˣ) ((φ : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)
have refine_2 : (∃ (φ : MonoidHom.{u_1, u_2} Mˣ Rˣ), Ne.{u_2 + 1} (α := Rˣ) ((φ : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)) →
  ∀ (φ : MonoidHom.{u_1, u_2} Mˣ Rˣ) (hφ : Ne.{u_2 + 1} (α := Rˣ) ((φ : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)),
    Ne.{u_2 + 1} (α := R) ((ofUnitHom φ : (a : M) → R) (↑a : M) : R) (1 : R)
Tactic: refine ⟨fun ⟨χ, hχ⟩ ↦ ⟨χ.toUnitHom, ?_⟩, fun ⟨φ, hφ⟩ ↦ ⟨ofUnitHom φ, ?_⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.MulChar.Duality (goal)
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
a : Mˣ
h : ∃ (χ : MulChar M R), Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)
χ : MulChar M R
hχ : Ne.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)
⊢ Ne.{u_2 + 1} (α := Rˣ) ((χ.toUnitHom : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)
have refine_1 : ∀ (hχ : Eq.{u_2 + 1} (α := Rˣ) ((χ.toUnitHom : (a : Mˣ) → Rˣ) a : Rˣ) (1 : Rˣ)),
  Eq.{u_2 + 1} (α := R) ((χ : (a : M) → R) (↑a : M) : R) (1 : R)
Tactic: contrapose hχ
Cleared hypotheses: hχ