awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst_2 : CharP R' p
x : Rˣ
hx : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (-1 : R')
h : HPow.hPow (α := R') (-1) p = -1
⊢ HPow.hPow (α := R') ((χ : (a : R) → R') (↑x : R) : R') p = (χ : (a : R) → R') (↑x : R)

Tactic:
rw [hx]
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst_2 : CharP R' p
x : Rˣ
hx : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (0 : R')
h h₁ : Eq.{u_2 + 1} (α := R') 0 0
⊢ HPow.hPow (α := R') 0 p = 0

Tactic:
rw [zero_pow (@Fact.out p.Prime).ne_zero]

Premises used: Nat.Prime.ne_zero, zero_pow, Fact.out
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst_2 : CharP R' p
x : Rˣ
hx : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (1 : R')
h h₁ : Eq.{u_2 + 1} (α := R') 1 1
⊢ HPow.hPow (α := R') 1 p = 1

Tactic:
rw [one_pow]

Premises used: one_pow
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst_2 : CharP R' p
x : Rˣ
hx : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (-1 : R')
⊢ HPow.hPow (α := R') (-1) p = -1

Tactic:
neg_one_pow_char R' p

Premises used: neg_one_pow_char
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
p : ℕ
hp : Fact (Nat.Prime p)
inst_2 : CharP R' p
x : Rˣ
hx : Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (↑x : R) : R') (-1 : R')
⊢ HPow.hPow (α := R') (-1) p = -1

Tactic:
exact neg_one_pow_char R' p

Premises used: neg_one_pow_char
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
R : Type u_1
inst : CommMonoid R
R' : Type u_2
inst_1 : CommRing R'
χ : MulChar R R'
hχ : χ.IsQuadratic
n : ℕ
hn : Even n
obtain : ∀ (n : ℕ) (hn : Even (2 * n)), χ ^ (2 * n) = 1
⊢ χ ^ n = 1

Tactic:
obtain ⟨n, rfl⟩ := even_iff_two_dvd.mp hn

Premises used: Iff.mp, even_iff_two_dvd, rfl
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
rw₂ rw₃ : Eq (α := MulChar R R') 1 1
⊢ χ ^ (2 * n) = 1

Tactic:
rw [pow_mul, hχ.sq_eq_one, one_pow]

Premises used: one_pow, MulChar.IsQuadratic.sq_eq_one, pow_mul
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
obtain : ∀ (n : ℕ), χ ^ (2 * n + 1) = χ
⊢ χ ^ n = χ

Tactic:
obtain ⟨n, rfl⟩ := hn

Premises used: rfl
-- Module: Mathlib.NumberTheory.MulChar.Basic
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 * χ = χ
rw₃ rw₄ : χ = χ
⊢ χ ^ (2 * n + 1) = χ

Tactic:
rw [pow_add, pow_one, hχ.pow_even (even_two_mul _), one_mul]

Premises used: MulChar.IsQuadratic.pow_even, pow_add, even_two_mul, pow_one, one_mul
-- Module: Mathlib.NumberTheory.MulChar.Basic
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

Tactic:
⟨fun h ↦ ext (fun x ↦ ?_), fun h x ↦ ?_⟩

Premises used: MulChar.ext, Iff.intro
-- Module: Mathlib.NumberTheory.MulChar.Basic
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)
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)
⊢ χ.IsQuadratic ↔ HPow.hPow (β := ℕ) χ 2 = 1

Tactic:
refine ⟨fun h ↦ ext (fun x ↦ ?_), fun h x ↦ ?_⟩
-- Module: Mathlib.NumberTheory.MulChar.Basic
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 : HPow.hPow (α := R) (β := ℕ) ((χ : (a : M) → R) (↑x : M) : R) 2 = 1
⊢ Eq.{u_5 + 1} (α := R) ((HPow.hPow (β := ℕ) χ 2 : (a : M) → R) (↑x : M) : R) ((1 : (a : M) → R) (↑x : M) : R)

Tactic:
rw [one_apply_coe, χ.pow_apply_coe]

Premises used: MulChar.one_apply_coe, MulChar.pow_apply_coe
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
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

Tactic:
rcases h x with H | H | H

Premises used: Units.val
-- Module: Mathlib.NumberTheory.MulChar.Basic
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ˣ
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:
(not_isUnit_zero <| H ▸ IsUnit.map χ <| x.isUnit).elim

Premises used: False.elim, not_isUnit_zero
-- Module: Mathlib.NumberTheory.MulChar.Basic
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ˣ
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:
exact (not_isUnit_zero <| H ▸ IsUnit.map χ <| x.isUnit).elim

Premises used: False.elim, not_isUnit_zero
-- Module: Mathlib.NumberTheory.MulChar.Basic
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ˣ
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:
simp only [H, one_pow]

Premises used: one_pow
-- Module: Mathlib.NumberTheory.MulChar.Basic
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ˣ
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:
simp only [H, even_two, Even.neg_pow, one_pow]

Premises used: one_pow, even_two, Even.neg_pow
-- Module: Mathlib.NumberTheory.MulChar.Basic
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)
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)
⊢ 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

Premises used: IsUnit
-- Module: Mathlib.NumberTheory.MulChar.Basic
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)

Tactic:
.inr <| sq_eq_one_iff.mp ?_

Premises used: sq_eq_one_iff, Iff.mp, Or.inr
-- Module: Mathlib.NumberTheory.MulChar.Basic
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 : HPow.hPow (α := R) (β := ℕ) ((χ : (a : M) → R) x : R) 2 = 1
⊢ 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 .inr <| sq_eq_one_iff.mp ?_

Premises used: sq_eq_one_iff, Iff.mp
-- Module: Mathlib.NumberTheory.MulChar.Basic
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)
pos₂ pos₃ : Eq.{u_5 + 1} (α := R) 1 1
⊢ HPow.hPow (α := R) (β := ℕ) ((χ : (a : M) → R) x : R) 2 = 1

Tactic:
rw [← χ.pow_apply' two_ne_zero, h, MulChar.one_apply hx]

Premises used: MulChar.pow_apply', two_ne_zero, MulChar.one_apply
-- Module: Mathlib.NumberTheory.MulChar.Basic
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)

Tactic:
.inl <| map_nonunit χ hx

Premises used: MulChar.map_nonunit, Or.inl
-- Module: Mathlib.NumberTheory.MulChar.Basic
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)

Tactic:
exact .inl <| map_nonunit χ hx

Premises used: MulChar.map_nonunit
-- Module: Mathlib.NumberTheory.MulChar.Basic
Goal:
M : Type u_1
inst : CommMonoid M
R : Type u_2
inst_1 : CommMonoidWithZero R
inst_2 : Fintype Mˣ
χ : MulChar M R
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)
⊢ χ ^ Fintype.card.{u_1} Mˣ = 1

Tactic:
ext1
-- Module: Mathlib.NumberTheory.MulChar.Basic
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)
h₆ h₇ : Eq.{u_2 + 1} (α := R) 1 1
⊢ Eq.{u_2 + 1} (α := R) ((χ ^ Fintype.card.{u_1} Mˣ : (a : M) → R) (↑a : 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]

Premises used: pow_card_eq_one, Iff.mpr, MulChar.one_apply_coe, MulChar.pow_apply_coe, map_pow, map_one, Units.val_eq_one, Units.val_pow_eq_pow_val, rfl
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
intro : ∀ (val : Fintype Mˣ), 0 < orderOf χ
⊢ 0 < orderOf χ

Tactic:
cases nonempty_fintype Mˣ

Premises used: Units, nonempty_fintype
-- Module: Mathlib.NumberTheory.MulChar.Basic
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ˣ
intro : IsOfFinOrder χ
⊢ 0 < orderOf χ

Tactic:
apply IsOfFinOrder.orderOf_pos

Premises used: IsOfFinOrder.orderOf_pos
-- Module: Mathlib.NumberTheory.MulChar.Basic
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ˣ
⊢ IsOfFinOrder χ

Tactic:
isOfFinOrder_iff_pow_eq_one.2 ⟨_, Fintype.card_pos, χ.pow_card_eq_one⟩

Premises used: Iff.mpr, MulChar.pow_card_eq_one, And.intro, Exists.intro, isOfFinOrder_iff_pow_eq_one, Fintype.card_pos
-- Module: Mathlib.NumberTheory.MulChar.Basic
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ˣ
⊢ IsOfFinOrder χ

Tactic:
exact isOfFinOrder_iff_pow_eq_one.2 ⟨_, Fintype.card_pos, χ.pow_card_eq_one⟩

Premises used: Iff.mpr, MulChar.pow_card_eq_one, And.intro, Exists.intro, isOfFinOrder_iff_pow_eq_one, Fintype.card_pos
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
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
⊢ Eq.{u_2 + 1} (α := R') (∑ a : R, (χ : (a : R) → R') a) 0

Tactic:
rcases ne_one_iff.mp hχ with ⟨b, hb⟩

Premises used: MulChar.ne_one_iff, Iff.mp
-- Module: Mathlib.NumberTheory.MulChar.Basic
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

Tactic:
eq_zero_of_mul_eq_self_left hb ?_

Premises used: eq_zero_of_mul_eq_self_left
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
refine :
  HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (↑b : R) : R') (∑ a : R, (χ : (a : R) → R') a : R') =
    ∑ a : R, (χ : (a : R) → R') a
⊢ Eq.{u_2 + 1} (α := R') (∑ a : R, (χ : (a : R) → R') a) 0

Tactic:
refine eq_zero_of_mul_eq_self_left hb ?_

Premises used: eq_zero_of_mul_eq_self_left
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
⊢ HMul.hMul (α := R') (β := R') ((χ : (a : R) → R') (↑b : R) : R') (∑ a : R, (χ : (a : R) → R') a : R') =
    ∑ a : R, (χ : (a : R) → R') a

Tactic:
simpa only [Finset.mul_sum, ← map_mul] using b.mulLeft_bijective.sum_comp _

Premises used: Finset.mul_sum, Function.Bijective.sum_comp, map_mul, Units.mulLeft_bijective
-- Module: Mathlib.NumberTheory.MulChar.Basic
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) (∑ a : R, if IsUnit a then 1 else 0)

Tactic:
Finset.sum_congr rfl fun a _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.MulChar.Basic
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, if IsUnit a then 1 else 0)
    (↑(Finset.card.{u_1} (α := R) (Finset.filter IsUnit Finset.univ)) : R')

Tactic:
Finset.sum_boole _ _

Premises used: Finset.sum_boole
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')

Tactic:
?_
-- Module: Mathlib.NumberTheory.MulChar.Basic
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.map (α := Rˣ) { toFun := Units.val, inj' := ⋯ } Finset.univ)) : R')
    (↑(Fintype.card.{u_1} Rˣ) : R')

Tactic:
congr_arg _ (Finset.card_map _)

Premises used: Finset.card_map, congr_arg
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
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' := ⋯ } Finset.univ)) : R')
⊢ Eq.{u_2 + 1} (α := R') (∑ a : R, (1 : (a : R) → R') a) (↑(Fintype.card.{u_1} Rˣ) : 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 _)

Premises used: Units.val, Finset.univ, Finset.card_map, IsUnit, Finset.map, Function.Embedding.mk, Units, Fintype.card, congr_arg, Units.val_injective, Finset.card, OfNat.ofNat, Finset.filter, Finset.sum_boole, DFunLike.coe, Finset.sum_congr, Finset.sum, rfl
-- Module: Mathlib.NumberTheory.MulChar.Basic
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')
neg : ∀ (h : ¬IsUnit a), Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') a : R') (0 : R')
⊢ Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') a : R') (if IsUnit a then 1 else 0 : R')

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.MulChar.Basic
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_1 : Membership.mem (γ := Finset R) Finset.univ a
h : IsUnit a
⊢ Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') a : R') (1 : R')

Tactic:
one_apply_coe h.unit

Premises used: MulChar.one_apply_coe, IsUnit.unit
-- Module: Mathlib.NumberTheory.MulChar.Basic
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_1 : Membership.mem (γ := Finset R) Finset.univ a
h : IsUnit a
⊢ Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') a : R') (1 : R')

Tactic:
exact one_apply_coe h.unit

Premises used: MulChar.one_apply_coe, IsUnit.unit
-- Module: Mathlib.NumberTheory.MulChar.Basic
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_1 : Membership.mem (γ := Finset R) Finset.univ a
h : ¬IsUnit a
⊢ Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') a : R') (0 : R')

Tactic:
map_nonunit _ h

Premises used: MulChar.map_nonunit
-- Module: Mathlib.NumberTheory.MulChar.Basic
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_1 : Membership.mem (γ := Finset R) Finset.univ a
h : ¬IsUnit a
⊢ Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') a : R') (0 : R')

Tactic:
exact map_nonunit _ h

Premises used: MulChar.map_nonunit
-- Module: Mathlib.NumberTheory.MulChar.Basic
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_2 :
  Eq.{u_1 + 1} (α := Finset R) (Finset.filter IsUnit Finset.univ)
    (Finset.map (α := Rˣ) { toFun := Units.val, inj' := ⋯ } Finset.univ)
⊢ 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')

Tactic:
congr
-- Module: Mathlib.NumberTheory.MulChar.Basic
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_2 :
  ∀ (a : R),
    Membership.mem (γ := Finset R) (Finset.filter IsUnit Finset.univ) a ↔
      Membership.mem (γ := Finset R) (Finset.map (α := Rˣ) { toFun := Units.val, inj' := ⋯ } Finset.univ) a
⊢ Eq.{u_1 + 1} (α := Finset R) (Finset.filter IsUnit Finset.univ)
    (Finset.map (α := Rˣ) { toFun := Units.val, inj' := ⋯ } Finset.univ)

Tactic:
ext a
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
⊢ Membership.mem (γ := Finset R) (Finset.filter IsUnit Finset.univ) a ↔
    Membership.mem (γ := Finset R) (Finset.map (α := Rˣ) { toFun := Units.val, inj' := ⋯ } Finset.univ) a

Tactic:
simp [IsUnit]

Premises used: IsUnit
-- Module: Mathlib.NumberTheory.MulChar.Basic
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
rw : Eq.{u_2 + 1} (α := R') ((1 : (a : R) → R') (-1) : R') (1 : R')
⊢ Eq.{u_2 + 1} (α := R') ((χ : (a : R) → R') (-1) : R') (1 : R')

Tactic:
rw [← hn.neg_one_pow, map_pow, ← χ.pow_apply' (Nat.ne_of_odd_add hn), hχ]

Premises used: map_pow, MulChar.pow_apply', Nat.ne_of_odd_add, Odd.neg_one_pow
-- Module: Mathlib.NumberTheory.MulChar.Basic
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') ((1 : (a : R) → R') (-1) : R') (1 : R')

Tactic:
MulChar.one_apply_coe (-1)

Premises used: MulChar.one_apply_coe, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.MulChar.Basic
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') ((1 : (a : R) → R') (-1) : R') (1 : R')

Tactic:
exact MulChar.one_apply_coe (-1)

Premises used: MulChar.one_apply_coe, OfNat.ofNat, Neg.neg
-- Module: Mathlib.NumberTheory.MulChar.Duality
Goal:
M : Type u_1
R : Type u_2
inst : CommMonoid M
inst_1 : CommRing R
inst_2 : Finite.{u_1 + 1} Mˣ
inst_3 : IsDomain R
⊢ Finite (MulChar M R)

Tactic:
.of_equiv _ equivToUnitHom.symm

Premises used: Finite.of_equiv, MulChar.equivToUnitHom, Equiv.symm
-- Module: Mathlib.NumberTheory.MulChar.Duality
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ˣ)

Tactic:
⟨fun ⟨χ, hχ⟩ ↦ ⟨χ.toUnitHom, ?_⟩, fun ⟨φ, hφ⟩ ↦ ⟨ofUnitHom φ, ?_⟩⟩

Premises used: _private.0.MulChar.exists_apply_ne_one_iff_exists_monoidHom.match_1, Units.val, _private.0.MulChar.exists_apply_ne_one_iff_exists_monoidHom.match_2, Exists, Ne, MulChar.toUnitHom, Iff.intro, Exists.intro, OfNat.ofNat, MulChar.ofUnitHom, DFunLike.coe