awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u
inst : CommRing R
R' : Type v
inst_1 : CommMonoid R'
inst_2 : Finite R
e : AddChar R R'
r x : R
h : x * r = 0
h' : ¬x = 0
⊢ ¬(e.mulShift r).mulShift x ≠ 1

Tactic:
simp only [mulShift_mulShift, mul_comm r, h, mulShift_zero, not_ne_iff]

Premises used: not_ne_iff, AddChar.mulShift_zero, mul_comm, AddChar.mulShift_mulShift
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u
inst : CommRing R
R' : Type v
inst_1 : CommMonoid R'
inst_2 : Finite R
e : AddChar R R'
r x : R
h : x * r = 0
h' : ¬x = 0
⊢ ∃ (x : R) (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1

Tactic:
exact ⟨x, h', by simp only [mulShift_mulShift, mul_comm r, h, mulShift_zero, not_ne_iff]⟩
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
he : ¬IsPrimitive.{0, u_1} (R := ZMod N) (R' := R) e
⊢ ∃ (x : ZMod N) (_ : x ≠ 0), Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift x) 1

Tactic:
simp_rw [IsPrimitive, not_forall, not_ne_iff] at he

Premises used: AddChar.IsPrimitive, not_ne_iff, Classical.not_forall
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
he : ∃ (x : ZMod N) (_ : x ≠ 0), Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift x) 1
rcases :
  ∀ (b : ZMod N) (hb_ne : b ≠ 0) (hb : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift b) 1),
    ∃ (d : ℕ), d ∣ N ∧ d < N ∧ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
⊢ ∃ (d : ℕ), d ∣ N ∧ d < N ∧ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1

Tactic:
rcases he with ⟨b, hb_ne, hb⟩
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
b : ZMod N
hb_ne : b ≠ 0
hb : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift b) 1
obtain :
  ∀ (d : ℕ) (hd : d ∣ N) (u : ZMod N) (hu : IsUnit u) (hb_ne : u * (↑d : ZMod N) ≠ 0)
    (hb : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (u * (↑d : ZMod N))) 1),
    ∃ (d : ℕ), d ∣ N ∧ d < N ∧ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
⊢ ∃ (d : ℕ), d ∣ N ∧ d < N ∧ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1

Tactic:
obtain ⟨d, hd, u, hu, rfl⟩ := b.eq_unit_mul_divisor

Premises used: ZMod.eq_unit_mul_divisor, rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * (↑d : ZMod N) ≠ 0
hb : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (u * (↑d : ZMod N))) 1
⊢ ∃ (d : ℕ), d ∣ N ∧ d < N ∧ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1

Tactic:
⟨d, hd, lt_of_le_of_ne (Nat.le_of_dvd (NeZero.pos _) hd) ?_, ?_⟩

Premises used: And.intro, Exists.intro, NeZero.pos, Nat.le_of_dvd, lt_of_le_of_ne
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * (↑d : ZMod N) ≠ 0
hb : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (u * (↑d : ZMod N))) 1
refine_1 : d ≠ N
refine_2 : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
⊢ ∃ (d : ℕ), d ∣ N ∧ d < N ∧ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1

Tactic:
refine ⟨d, hd, lt_of_le_of_ne (Nat.le_of_dvd (NeZero.pos _) hd) ?_, ?_⟩
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * (↑d : ZMod N) ≠ 0
hb : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (u * (↑d : ZMod N))) 1
h : d = N
⊢ False

Tactic:
simp only [h, ZMod.natCast_self, mul_zero, ne_eq, not_true_eq_false] at hb_ne

Premises used: ZMod.natCast_self, not_true_eq_false, ne_eq, MulZeroClass.mul_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * (↑d : ZMod N) ≠ 0
hb : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (u * (↑d : ZMod N))) 1
⊢ d ≠ N

Tactic:
exact fun h ↦ by simp only [h, ZMod.natCast_self, mul_zero, ne_eq, not_true_eq_false] at hb_ne
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * (↑d : ZMod N) ≠ 0
hb : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (u * (↑d : ZMod N))) 1
refine_2 :
  Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (mulShift (e.mulShift (↑d : ZMod N)) u) (e.mulShift ((↑d : ZMod N) * u))
⊢ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1

Tactic:
rw [← mulShift_unit_eq_one_iff _ hu, ← hb, mul_comm]

Premises used: AddChar.mulShift_unit_eq_one_iff, mul_comm
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * (↑d : ZMod N) ≠ 0
hb : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (u * (↑d : ZMod N))) 1
refine_2 :
  ∀ (y : ZMod N),
    Eq.{u_1 + 1} (α := R) ((mulShift (e.mulShift (↑d : ZMod N)) u : (a : ZMod N) → R) y : R)
      ((e.mulShift ((↑d : ZMod N) * u) : (a : ZMod N) → R) y : R)
⊢ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (mulShift (e.mulShift (↑d : ZMod N)) u) (e.mulShift ((↑d : ZMod N) * u))

Tactic:
ext1 y
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
N : ℕ
inst : NeZero N
R : Type u_1
inst_1 : CommRing R
e : AddChar (ZMod N) R
d : ℕ
hd : d ∣ N
u : ZMod N
hu : IsUnit u
hb_ne : u * (↑d : ZMod N) ≠ 0
hb : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (u * (↑d : ZMod N))) 1
y : ZMod N
refine_2 :
  Eq.{u_1 + 1} (α := R) ((e.mulShift (↑d : ZMod N) : (a : ZMod N) → R) (u * y) : R)
    ((e.mulShift ((↑d : ZMod N) * u) : (a : ZMod N) → R) y : R)
refine_2₁ :
  Eq (α := R) ((e : (a : ZMod N) → R) ((↑d : ZMod N) * (u * y)) : R)
    ((e.mulShift ((↑d : ZMod N) * u) : (a : ZMod N) → R) y : R)
refine_2₂ :
  Eq (α := R) ((e : (a : ZMod N) → R) ((↑d : ZMod N) * (u * y)) : R)
    ((e : (a : ZMod N) → R) ((↑d : ZMod N) * u * y) : R)
refine_2₃ refine_2₄ :
  Eq (α := R) ((e : (a : ZMod N) → R) ((↑d : ZMod N) * (u * y)) : R)
    ((e : (a : ZMod N) → R) ((↑d : ZMod N) * (u * y)) : R)
⊢ Eq.{u_1 + 1} (α := R) ((mulShift (e.mulShift (↑d : ZMod N)) u : (a : ZMod N) → R) y : R)
    ((e.mulShift ((↑d : ZMod N) * u) : (a : ZMod N) → R) y : R)

Tactic:
rw [mulShift_apply, mulShift_apply, mulShift_apply, mul_assoc]

Premises used: mul_assoc, AddChar.mulShift_apply
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u
inst : CommRing R
R' : Type v
inst_1 : CommMonoid R'
C : Type v
inst_2 : CommMonoid C
n : ℕ
inst_3 : NeZero n
ζ : C
hζ : ζ ^ n = 1
⊢ ζ ^ ZMod.val (n := n) 0 = 1

Tactic:
simp only [ZMod.val_zero, pow_zero]

Premises used: ZMod.val_zero, pow_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u
inst : CommRing R
R' : Type v
inst_1 : CommMonoid R'
C : Type v
inst_2 : CommMonoid C
n : ℕ
inst_3 : NeZero n
ζ : C
hζ : ζ ^ n = 1
x y : ZMod n
⊢ ζ ^ (x + y).val = ζ ^ x.val * ζ ^ y.val

Tactic:
simp only [ZMod.val_add, ← pow_eq_pow_mod _ hζ, ← pow_add]

Premises used: pow_eq_pow_mod, ZMod.val_add, pow_add
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ζ : C
hζ : ζ ^ n = 1
a : ZMod n
⊢ (zmodChar n hζ : (a : ZMod n) → C) a = ζ ^ a.val

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ζ : C
hζ : ζ ^ n = 1
a : ℕ
rw : (zmodChar n hζ : (a : ZMod n) → C) (↑a : ZMod n) = ζ ^ (a % n)
rw₁ : ζ ^ ZMod.val (n := n) (↑a : ZMod n) = ζ ^ (a % n)
rw₂ rw₃ : ζ ^ (a % n) = ζ ^ (a % n)
⊢ (zmodChar n hζ : (a : ZMod n) → C) (↑a : ZMod n) = ζ ^ a

Tactic:
rw [pow_eq_pow_mod a hζ, zmodChar_apply, ZMod.val_natCast]

Premises used: pow_eq_pow_mod, AddChar.zmodChar_apply, ZMod.val_natCast
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ψ : AddChar (ZMod n) C
rw :
  (∃ (x : ZMod n), Ne (α := C) ((ψ : (a : ZMod n) → C) x : C) (1 : C)) ↔
    Ne (α := C) ((ψ : (a : ZMod n) → C) 1 : C) (1 : C)
⊢ ψ ≠ 1 ↔ Ne (α := C) ((ψ : (a : ZMod n) → C) 1 : C) (1 : C)

Tactic:
rw [ne_one_iff]

Premises used: AddChar.ne_one_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ψ : AddChar (ZMod n) C
⊢ (∃ (x : ZMod n), Ne (α := C) ((ψ : (a : ZMod n) → C) x : C) (1 : C)) ↔
    Ne (α := C) ((ψ : (a : ZMod n) → C) 1 : C) (1 : C)

Tactic:
⟨?_, fun h => ⟨_, h⟩⟩

Premises used: Iff.intro, Exists.intro, OfNat.ofNat
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ψ : AddChar (ZMod n) C
refine :
  (∃ (x : ZMod n), Ne (α := C) ((ψ : (a : ZMod n) → C) x : C) (1 : C)) →
    Ne (α := C) ((ψ : (a : ZMod n) → C) 1 : C) (1 : C)
⊢ (∃ (x : ZMod n), Ne (α := C) ((ψ : (a : ZMod n) → C) x : C) (1 : C)) ↔
    Ne (α := C) ((ψ : (a : ZMod n) → C) 1 : C) (1 : C)

Tactic:
refine ⟨?_, fun h => ⟨_, h⟩⟩
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ψ : AddChar (ZMod n) C
contrapose! :
  Eq (α := C) ((ψ : (a : ZMod n) → C) 1 : C) (1 : C) →
    ∀ (x : ZMod n), Eq (α := C) ((ψ : (a : ZMod n) → C) x : C) (1 : C)
⊢ (∃ (x : ZMod n), Ne (α := C) ((ψ : (a : ZMod n) → C) x : C) (1 : C)) →
    Ne (α := C) ((ψ : (a : ZMod n) → C) 1 : C) (1 : C)

Tactic:
contrapose!
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ψ : AddChar (ZMod n) C
h₁ : Eq (α := C) ((ψ : (a : ZMod n) → C) 1 : C) (1 : C)
a : ZMod n
rw : a = (↑a.val : ZMod n)
⊢ a = HSMul.hSMul (β := ZMod n) a.val 1

Tactic:
rw [nsmul_eq_mul, mul_one]

Premises used: nsmul_eq_mul, mul_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ψ : AddChar (ZMod n) C
h₁ : Eq (α := C) ((ψ : (a : ZMod n) → C) 1 : C) (1 : C)
a : ZMod n
⊢ a = (↑a.val : ZMod n)

Tactic:
(ZMod.natCast_zmod_val a).symm

Premises used: ZMod.natCast_zmod_val, Eq.symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ψ : AddChar (ZMod n) C
h₁ : Eq (α := C) ((ψ : (a : ZMod n) → C) 1 : C) (1 : C)
a : ZMod n
⊢ a = (↑a.val : ZMod n)

Tactic:
exact (ZMod.natCast_zmod_val a).symm

Premises used: ZMod.natCast_zmod_val, Eq.symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ψ : AddChar (ZMod n) C
h₁ : Eq (α := C) ((ψ : (a : ZMod n) → C) 1 : C) (1 : C)
a : ZMod n
⊢ a = HSMul.hSMul (β := ZMod n) a.val 1

Tactic:
have ha₁ : a = a.val • (1 : ZMod ↑n) := by
    rw [nsmul_eq_mul, mul_one]; exact (ZMod.natCast_zmod_val a).symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ψ : AddChar (ZMod n) C
h₁ : Eq (α := C) ((ψ : (a : ZMod n) → C) 1 : C) (1 : C)
a : ZMod n
ha₁ : a = HSMul.hSMul (β := ZMod n) a.val 1
rw : Eq (α := C) ((ψ : (a : ZMod n) → C) (HSMul.hSMul (β := ZMod n) a.val 1) : C) (1 : C)
rw₁ : HPow.hPow (α := C) ((ψ : (a : ZMod n) → C) 1 : C) a.val = 1
rw₂ : HPow.hPow (α := C) 1 a.val = 1
rw₃ rw₄ : Eq.{v + 1} (α := C) 1 1
⊢ Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C)

Tactic:
rw [ha₁, map_nsmul_eq_pow, h₁, one_pow]

Premises used: one_pow, AddChar.map_nsmul_eq_pow
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ψ : AddChar (ZMod n) C
hψ : ψ.IsPrimitive
a : ZMod n
ha : a = 0
rw : Eq (α := C) ((ψ : (a : ZMod n) → C) 0 : C) (1 : C)
rw₁ rw₂ : Eq.{v + 1} (α := C) 1 1
⊢ Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C)

Tactic:
rw [ha, map_zero_eq_one]

Premises used: AddChar.map_zero_eq_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ψ : AddChar (ZMod n) C
hψ : ψ.IsPrimitive
a : ZMod n
refine : ∀ (h : Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C)), ¬ψ.mulShift a ≠ 1
⊢ Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C) ↔ a = 0

Tactic:
refine ⟨fun h => not_imp_comm.mp (@hψ a) ?_, fun ha => by rw [ha, map_zero_eq_one]⟩
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ψ : AddChar (ZMod n) C
hψ : ψ.IsPrimitive
a : ZMod n
h : Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C)
rw : ¬Ne (α := C) ((ψ.mulShift a : (a : ZMod n) → C) 1 : C) (1 : C)
rw₁ : ¬Ne (α := C) ((ψ : (a : ZMod n) → C) (a * 1) : C) (1 : C)
rw₂ : ¬Ne (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C)
rw₃ : ¬Ne.{v + 1} (α := C) 1 1
rw₄ rw₅ : Eq.{v + 1} (α := C) 1 1
⊢ ¬ψ.mulShift a ≠ 1

Tactic:
rw [zmod_char_ne_one_iff n (mulShift ψ a), mulShift_apply, mul_one, h, Classical.not_not]

Premises used: Classical.not_not, AddChar.mulShift_apply, AddChar.zmod_char_ne_one_iff, mul_one, AddChar.mulShift
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C) → a = 0
⊢ ψ.IsPrimitive

Tactic:
fun a ha hf => ?_

Premises used: AddChar.IsPrimitive, Not
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C) → a = 0
refine : ∀ (a : ZMod n) (ha : a ≠ 0) (hf : ψ.mulShift a = 1), False
⊢ ψ.IsPrimitive

Tactic:
refine fun a ha hf => ?_
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C) → a = 0
a : ZMod n
ha : a ≠ 0
hf : ψ.mulShift a = 1
⊢ Eq (α := C) ((ψ.mulShift a : (a : ZMod n) → C) 1 : C) ((1 : (a : ZMod n) → C) 1 : C)

Tactic:
have h : mulShift ψ a 1 = (1 : AddChar (ZMod n) C) (1 : ZMod n) :=
    congr_fun (congr_arg (↑) hf) 1
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C) → a = 0
a : ZMod n
ha : a ≠ 0
hf : ψ.mulShift a = 1
h : Eq (α := C) ((ψ.mulShift a : (a : ZMod n) → C) 1 : C) ((1 : (a : ZMod n) → C) 1 : C)
⊢ Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) ((1 : (a : ZMod n) → C) 1 : C)

Tactic:
rw [mulShift_apply, mul_one] at h

Premises used: AddChar.mulShift_apply, mul_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C) → a = 0
a : ZMod n
ha : a ≠ 0
hf : ψ.mulShift a = 1
h : Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) ((1 : (a : ZMod n) → C) 1 : C)
⊢ Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 1 : C)

Tactic:
norm_cast at h
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C) → a = 0
a : ZMod n
ha : a ≠ 0
hf : ψ.mulShift a = 1
h : Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 1 : C)
⊢ False

Tactic:
ha (hψ a h)
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
ψ : AddChar (ZMod n) C
hψ : ∀ (a : ZMod n), Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C) → a = 0
a : ZMod n
ha : a ≠ 0
hf : ψ.mulShift a = 1
h : Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 1 : C)
⊢ False

Tactic:
exact ha (hψ a h)
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
hψ : ∀ (a : ZMod n), Eq (α := C) ((zmodChar n ⋯ : (a : ZMod n) → C) a : C) (1 : C) → a = 0
⊢ (zmodChar n ⋯).IsPrimitive

Tactic:
apply zmod_char_primitive_of_eq_one_only_at_zero

Premises used: AddChar.zmod_char_primitive_of_eq_one_only_at_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
a : ZMod n
ha : Eq (α := C) ((zmodChar n ⋯ : (a : ZMod n) → C) a : C) (1 : C)
⊢ ζ ^ a.val = HPow.hPow (β := ℕ) ζ 0

Tactic:
rw [zmodChar_apply, ← pow_zero ζ] at ha

Premises used: pow_zero, AddChar.zmodChar_apply
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
a : ZMod n
ha : ζ ^ a.val = HPow.hPow (β := ℕ) ζ 0
⊢ a = 0

Tactic:
(ZMod.val_eq_zero a).mp (IsPrimitiveRoot.pow_inj h (ZMod.val_lt a) (NeZero.pos _) ha)

Premises used: IsPrimitiveRoot.pow_inj, Iff.mp, NeZero.pos, ZMod.val_eq_zero, ZMod.val_lt
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
a : ZMod n
ha : ζ ^ a.val = HPow.hPow (β := ℕ) ζ 0
⊢ a = 0

Tactic:
exact (ZMod.val_eq_zero a).mp (IsPrimitiveRoot.pow_inj h (ZMod.val_lt a) (NeZero.pos _) ha)

Premises used: IsPrimitiveRoot.pow_inj, Iff.mp, NeZero.pos, ZMod.val_eq_zero, ZMod.val_lt
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
F : Type u_1
F' : Type u_2
inst : Field F
inst_1 : Finite F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
⊢ Fact (Nat.Prime p)

Tactic:
haveI hp : Fact p.Prime := ⟨CharP.char_is_prime F _⟩
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
F : Type u_1
F' : Type u_2
inst : Field F
inst_1 : Finite F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
inl : ∀ (hq : Nat.Prime (ringChar F')), ¬ringChar F' ∣ p
inr : ∀ (hq : ringChar F' = 0), ¬ringChar F' ∣ p
⊢ ¬ringChar F' ∣ p

Tactic:
rcases CharP.char_is_prime_or_zero F' (ringChar F') with hq | hq

Premises used: CharP.char_is_prime_or_zero, ringChar
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
F : Type u_1
F' : Type u_2
inst : Field F
inst_1 : Finite F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hq : Nat.Prime (ringChar F')
⊢ ¬ringChar F' ∣ p

Tactic:
mt (Nat.Prime.dvd_iff_eq hp.1 (Nat.Prime.ne_one hq)).mp h.symm

Premises used: mt, Nat.Prime.dvd_iff_eq, Ne.symm, Nat.Prime.ne_one, Iff.mp, Fact.out
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
F : Type u_1
F' : Type u_2
inst : Field F
inst_1 : Finite F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hq : Nat.Prime (ringChar F')
⊢ ¬ringChar F' ∣ p

Tactic:
exact mt (Nat.Prime.dvd_iff_eq hp.1 (Nat.Prime.ne_one hq)).mp h.symm

Premises used: mt, Nat.Prime.dvd_iff_eq, Ne.symm, Nat.Prime.ne_one, Iff.mp, Fact.out
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
F : Type u_1
F' : Type u_2
inst : Field F
inst_1 : Finite F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hq : ringChar F' = 0
inr : ¬0 ∣ p
⊢ ¬ringChar F' ∣ p

Tactic:
rw [hq]
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
F : Type u_1
F' : Type u_2
inst : Field F
inst_1 : Finite F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hq : ringChar F' = 0
⊢ ¬0 ∣ p

Tactic:
fun hf => Nat.Prime.ne_zero hp.1 (zero_dvd_iff.mp hf)

Premises used: zero_dvd_iff, Nat.Prime.ne_zero, Iff.mp, Not, Fact.out
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
F : Type u_1
F' : Type u_2
inst : Field F
inst_1 : Finite F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hq : ringChar F' = 0
⊢ ¬0 ∣ p

Tactic:
exact fun hf => Nat.Prime.ne_zero hp.1 (zero_dvd_iff.mp hf)

Premises used: zero_dvd_iff, Nat.Prime.ne_zero, Iff.mp, Fact.out
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
F : Type u_1
F' : Type u_2
inst : Field F
inst_1 : Finite F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
⊢ ¬ringChar F' ∣ p

Tactic:
have hp₂ : ¬ringChar F' ∣ p := by
    rcases CharP.char_is_prime_or_zero F' (ringChar F') with hq | hq
    · exact mt (Nat.Prime.dvd_iff_eq hp.1 (Nat.Prime.ne_one hq)).mp h.symm
    · rw [hq]
      exact fun hf => Nat.Prime.ne_zero hp.1 (zero_dvd_iff.mp hf)
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
F : Type u_1
F' : Type u_2
inst : Field F
inst_1 : Finite F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod (↑pp : ℕ)) F' := primitiveZModChar pp F' ⋯
this : Algebra (ZMod p) F := ZMod.algebra F p
ψ' : AddChar.{u_1, u_2} F (CyclotomicField (↑ψ.n : ℕ) F') :=
  ψ.char.compAddMonoidHom (LinearMap.toAddMonoidHom (modM₁ := Algebra.toModule) (Algebra.trace (ZMod p) F))
obtain :
  ∀ (a : F)
    (ha :
      Ne (α := ZMod (ringChar F))
        (((Algebra.trace (ZMod (ringChar F)) F :
                LinearMap (R := ZMod (ringChar F)) (RingHom.id (ZMod (ringChar F))) F (ZMod (ringChar F))) :
              (a : F) → ZMod (ringChar F))
            (1 * a) :
          ZMod (ringChar F))
        (0 : ZMod (ringChar F))),
    ψ' ≠ 1
⊢ ψ' ≠ 1

Tactic:
obtain ⟨a, ha⟩ := FiniteField.trace_to_zmod_nondegenerate F one_ne_zero

Premises used: one_ne_zero, FiniteField.trace_to_zmod_nondegenerate
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
F : Type u_1
F' : Type u_2
inst : Field F
inst_1 : Finite F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod (↑pp : ℕ)) F' := primitiveZModChar pp F' ⋯
this : Algebra (ZMod p) F := ZMod.algebra F p
ψ' : AddChar.{u_1, u_2} F (CyclotomicField (↑ψ.n : ℕ) F') :=
  ψ.char.compAddMonoidHom (LinearMap.toAddMonoidHom (modM₁ := Algebra.toModule) (Algebra.trace (ZMod p) F))
a : F
ha :
  Ne (α := ZMod (ringChar F))
    (((Algebra.trace (ZMod (ringChar F)) F :
            LinearMap (R := ZMod (ringChar F)) (RingHom.id (ZMod (ringChar F))) F (ZMod (ringChar F))) :
          (a : F) → ZMod (ringChar F))
        (1 * a) :
      ZMod (ringChar F))
    (0 : ZMod (ringChar F))
⊢ Ne (α := ZMod (ringChar F))
    (((Algebra.trace (ZMod (ringChar F)) F :
            LinearMap (R := ZMod (ringChar F)) (RingHom.id (ZMod (ringChar F))) F (ZMod (ringChar F))) :
          (a : F) → ZMod (ringChar F))
        a :
      ZMod (ringChar F))
    (0 : ZMod (ringChar F))

Tactic:
rw [one_mul] at ha

Premises used: one_mul
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
F : Type u_1
F' : Type u_2
inst : Field F
inst_1 : Finite F
inst_2 : Field F'
h : ringChar F' ≠ ringChar F
p : ℕ := ringChar F
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
hp₂ : ¬ringChar F' ∣ p
ψ : PrimitiveAddChar (ZMod (↑pp : ℕ)) F' := primitiveZModChar pp F' ⋯
this : Algebra (ZMod p) F := ZMod.algebra F p
ψ' : AddChar.{u_1, u_2} F (CyclotomicField (↑ψ.n : ℕ) F') :=
  ψ.char.compAddMonoidHom (LinearMap.toAddMonoidHom (modM₁ := Algebra.toModule) (Algebra.trace (ZMod p) F))
a : F
ha :
  Ne (α := ZMod (ringChar F))
    (((Algebra.trace (ZMod (ringChar F)) F :
            LinearMap (R := ZMod (ringChar F)) (RingHom.id (ZMod (ringChar F))) F (ZMod (ringChar F))) :
          (a : F) → ZMod (ringChar F))
        a :
      ZMod (ringChar F))
    (0 : ZMod (ringChar F))
⊢ ψ' ≠ 1

Tactic:
ne_one_iff.2
      ⟨a, fun hf => ha <| (ψ.prim.zmod_char_eq_one_iff pp <| Algebra.trace (ZMod p) F a).mp hf⟩

Premises used: PNat.val, Iff.mpr, AddChar.IsPrimitive.zmod_char_eq_one_iff, AddChar.ne_one_iff, ZMod, AddChar.PrimitiveAddChar.prim, Exists.intro, Iff.mp, Algebra.trace, DFunLike.coe