awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZetaZeros (goal)
Goal:
this : ∀ (x : ℂ), ¬x = 1 → ({1}ᶜ ∩ riemannZetaZeros)ᶜ ∈ nhdsWithin x {x}ᶜ
x : ℂ
inl : Membership.mem (γ := Filter ℂ) (nhdsWithin 1 {1}ᶜ) riemannZetaZerosᶜ
⊢ riemannZetaZerosᶜ ∈ nhdsWithin x {x}ᶜ
have inr : ∀ (hx : x ≠ 1), riemannZetaZerosᶜ ∈ nhdsWithin x {x}ᶜ
Tactic: rcases eq_or_ne x 1 with rfl | hx
-- Lean 4 proof step from Mathlib.NumberTheory.LSeries.ZetaZeros (goal)
Goal:
S : Set ℂ
hS : IsCompact S
⊢ (S ∩ riemannZetaZeros).Finite
have apply : IsDiscrete (S ∩ riemannZetaZeros)
Tactic: apply (hS.inter_right isClosed_riemannZetaZeros).finite
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (hypothesis)
Goal:
R : Type u
inst : CommRing R
R' : Type v
inst_1 : CommMonoid R'
ψ : AddChar R R'
hψ : ψ.IsPrimitive
a b : R
h : ψ.mulShift a = ψ.mulShift b
⊢ a = b
have h₁ : ψ.mulShift a * ψ.mulShift (-b) = ψ.mulShift b * ψ.mulShift (-b)
Tactic: apply_fun fun x => x * mulShift ψ (-b) at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (hypothesis)
Goal:
R : Type u
inst : CommRing R
R' : Type v
inst_1 : CommMonoid R'
ψ : AddChar R R'
hψ : ψ.IsPrimitive
a b : R
h : ψ.mulShift a * ψ.mulShift (-b) = ψ.mulShift b * ψ.mulShift (-b)
⊢ a = b
have h₁ : ψ.mulShift (a + -b) = 1
Tactic: simp only [mulShift_mul, mulShift_zero, add_neg_cancel] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
Goal:
R : Type u
inst : CommRing R
R' : Type v
inst_1 : CommMonoid R'
inst_2 : Finite R
e : AddChar R R'
r : R
hr : ¬IsUnit r
⊢ ¬(e.mulShift r).IsPrimitive
have simp : ∃ (x : R) (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1
Tactic: simp only [IsPrimitive, not_forall]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (hypothesis)
Goal:
R : Type u
inst : CommRing R
R' : Type v
inst_1 : CommMonoid R'
inst_2 : Finite R
e : AddChar R R'
r : R
hr : ¬IsUnit r
⊢ ∃ (x : R) (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1
have hr₁ : ∃ (x : R) (_ : x * r = 0), ¬x = 0
Tactic: simp only [isUnit_iff_mem_nonZeroDivisors_of_finite,
    mem_nonZeroDivisors_iff_right, not_forall] at hr
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
Goal:
R : Type u
inst : CommRing R
R' : Type v
inst_1 : CommMonoid R'
inst_2 : Finite R
e : AddChar R R'
r : R
hr : ∃ (x : R) (_ : x * r = 0), ¬x = 0
⊢ ∃ (x : R) (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1
have rcases : ∀ (x : R) (h : x * r = 0) (h' : ¬x = 0), ∃ (x : R) (_ : x ≠ 0), ¬(e.mulShift r).mulShift x ≠ 1
Tactic: rcases hr with ⟨x, h, h'⟩
Cleared hypotheses: hr
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (hypothesis)
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
⊢ ∃ (d : ℕ), d ∣ N ∧ d < N ∧ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
have he₁ : ∃ (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
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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
⊢ ∃ (d : ℕ), d ∣ N ∧ d < N ∧ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
have 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
Tactic: rcases he with ⟨b, hb_ne, hb⟩
Cleared hypotheses: he
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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
⊢ ∃ (d : ℕ), d ∣ N ∧ d < N ∧ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
have 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
Tactic: obtain ⟨d, hd, u, hu, rfl⟩ := b.eq_unit_mul_divisor
Cleared hypotheses: b, hb_ne, hb
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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
have refine_1 : d ≠ N
Tactic: refine ⟨d, hd, lt_of_le_of_ne (Nat.le_of_dvd (NeZero.pos _) hd) ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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
⊢ ∃ (d : ℕ), d ∣ N ∧ d < N ∧ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
have refine_2 : 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) ?_, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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
⊢ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (e.mulShift (↑d : ZMod N)) 1
have refine_2 : Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (mulShift (e.mulShift (↑d : ZMod N)) u) (e.mulShift ((↑d : ZMod N) * u))
Tactic: rw [← mulShift_unit_eq_one_iff _ hu, ← hb, mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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
⊢ Eq.{u_1 + 1} (α := AddChar (ZMod N) R) (mulShift (e.mulShift (↑d : ZMod N)) u) (e.mulShift ((↑d : ZMod N) * u))
have 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)
Tactic: ext1 y
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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
⊢ 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)
have 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)
Tactic: rw [mulShift_apply, mulShift_apply, mulShift_apply, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mulShift_apply, mulShift_apply, mulShift_apply, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mulShift_apply, mulShift_apply, mulShift_apply, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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)
⊢ 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)
have 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)
Tactic: rw [mulShift_apply, mulShift_apply, mulShift_apply, mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ζ : C
hζ : ζ ^ n = 1
a : ℕ
⊢ (zmodChar n hζ : (a : ZMod n) → C) (↑a : ZMod n) = ζ ^ a
have rw : (zmodChar n hζ : (a : ZMod n) → C) (↑a : ZMod n) = ζ ^ (a % n)
Tactic: rw [pow_eq_pow_mod a hζ, zmodChar_apply, ZMod.val_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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)
⊢ (zmodChar n hζ : (a : ZMod n) → C) (↑a : ZMod n) = ζ ^ a
have rw₁ : ζ ^ ZMod.val (n := n) (↑a : ZMod n) = ζ ^ (a % n)
Tactic: rw [pow_eq_pow_mod a hζ, zmodChar_apply, ZMod.val_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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)
⊢ (zmodChar n hζ : (a : ZMod n) → C) (↑a : ZMod n) = ζ ^ a
have rw₂ : ζ ^ (a % n) = ζ ^ (a % n)
Tactic: rw [pow_eq_pow_mod a hζ, zmodChar_apply, ZMod.val_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ψ : AddChar (ZMod n) C
⊢ ψ ≠ 1 ↔ Ne (α := C) ((ψ : (a : ZMod n) → C) 1 : C) (1 : C)
have rw : (∃ (x : ZMod n), Ne (α := C) ((ψ : (a : ZMod n) → C) x : C) (1 : C)) ↔
  Ne (α := C) ((ψ : (a : ZMod n) → C) 1 : C) (1 : C)
Tactic: rw [ne_one_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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)
have refine : (∃ (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⟩⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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)
have contrapose! : Eq (α := C) ((ψ : (a : ZMod n) → C) 1 : C) (1 : C) → ∀ (x : ZMod n), Eq (α := C) ((ψ : (a : ZMod n) → C) x : C) (1 : C)
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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
have rw : a = (↑a.val : ZMod n)
Tactic: rw [nsmul_eq_mul, mul_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (hypothesis)
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
⊢ Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C)
have ha₁ : 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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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
⊢ Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C)
have rw : Eq (α := C) ((ψ : (a : ZMod n) → C) (HSMul.hSMul (β := ZMod n) a.val 1) : C) (1 : C)
Tactic: rw [ha₁, map_nsmul_eq_pow, h₁, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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)
⊢ Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C)
have rw₁ : HPow.hPow (α := C) ((ψ : (a : ZMod n) → C) 1 : C) a.val = 1
Tactic: rw [ha₁, map_nsmul_eq_pow, h₁, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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
⊢ Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C)
have rw₂ : HPow.hPow (α := C) 1 a.val = 1
Tactic: rw [ha₁, map_nsmul_eq_pow, h₁, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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
⊢ Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C)
have rw₃ : Eq.{v + 1} (α := C) 1 1
Tactic: rw [ha₁, map_nsmul_eq_pow, h₁, one_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ψ : AddChar (ZMod n) C
hψ : ψ.IsPrimitive
a : ZMod n
ha : a = 0
⊢ Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C)
have rw : Eq (α := C) ((ψ : (a : ZMod n) → C) 0 : C) (1 : C)
Tactic: rw [ha, map_zero_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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)
⊢ Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C)
have rw₁ : Eq.{v + 1} (α := C) 1 1
Tactic: rw [ha, map_zero_eq_one]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ψ : AddChar (ZMod n) C
hψ : ψ.IsPrimitive
a : ZMod n
⊢ Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C) ↔ a = 0
have refine : ∀ (h : Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C)), ¬ψ.mulShift a ≠ 1
Tactic: refine ⟨fun h => not_imp_comm.mp (@hψ a) ?_, fun ha => by rw [ha, map_zero_eq_one]⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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)
⊢ ¬ψ.mulShift a ≠ 1
have rw : ¬Ne (α := C) ((ψ.mulShift a : (a : ZMod n) → C) 1 : C) (1 : C)
Tactic: rw [zmod_char_ne_one_iff n (mulShift ψ a), mulShift_apply, mul_one, h, Classical.not_not]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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)
⊢ ¬ψ.mulShift a ≠ 1
have rw₁ : ¬Ne (α := C) ((ψ : (a : ZMod n) → C) (a * 1) : C) (1 : C)
Tactic: rw [zmod_char_ne_one_iff n (mulShift ψ a), mulShift_apply, mul_one, h, Classical.not_not]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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)
⊢ ¬ψ.mulShift a ≠ 1
have rw₂ : ¬Ne (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 : C)
Tactic: rw [zmod_char_ne_one_iff n (mulShift ψ a), mulShift_apply, mul_one, h, Classical.not_not]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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)
⊢ ¬ψ.mulShift a ≠ 1
have rw₃ : ¬Ne.{v + 1} (α := C) 1 1
Tactic: rw [zmod_char_ne_one_iff n (mulShift ψ a), mulShift_apply, mul_one, h, Classical.not_not]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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
⊢ ¬ψ.mulShift a ≠ 1
have rw₄ : Eq.{v + 1} (α := C) 1 1
Tactic: rw [zmod_char_ne_one_iff n (mulShift ψ a), mulShift_apply, mul_one, h, Classical.not_not]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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
have refine : ∀ (a : ZMod n) (ha : a ≠ 0) (hf : ψ.mulShift a = 1), False
Tactic: refine fun a ha hf => ?_
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (hypothesis)
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
⊢ False
have h : 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
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (hypothesis)
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)
⊢ False
have h₁ : Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) ((1 : (a : ZMod n) → C) 1 : C)
Tactic: rw [mulShift_apply, mul_one] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (hypothesis)
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)
⊢ False
have h₁ : Eq (α := C) ((ψ : (a : ZMod n) → C) a : C) (1 1 : C)
Tactic: norm_cast at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
Goal:
C : Type v
inst : CommMonoid C
n : ℕ
inst_1 : NeZero n
ζ : C
h : IsPrimitiveRoot ζ n
⊢ (zmodChar n ⋯).IsPrimitive
have hψ : ∀ (a : ZMod n), Eq (α := C) ((zmodChar n sorry : (a : ZMod n) → C) a : C) (1 : C) → a = 0
Tactic: apply zmod_char_primitive_of_eq_one_only_at_zero
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (hypothesis)
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 = 0
have ha₁ : ζ ^ a.val = HPow.hPow (β := ℕ) ζ 0
Tactic: rw [zmodChar_apply, ← pow_zero ζ] at ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (hypothesis)
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
⊢ PrimitiveAddChar F F'
have hp : Fact (Nat.Prime p)
Tactic: haveI hp : Fact p.Prime := ⟨CharP.char_is_prime F _⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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
have inl : ∀ (hq : Nat.Prime (ringChar F')), ¬ringChar F' ∣ p
Tactic: rcases CharP.char_is_prime_or_zero F' (ringChar F') with hq | hq
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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
⊢ ¬ringChar F' ∣ p
have inr : ∀ (hq : ringChar F' = 0), ¬ringChar F' ∣ p
Tactic: rcases CharP.char_is_prime_or_zero F' (ringChar F') with hq | hq
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
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
⊢ ¬ringChar F' ∣ p
have inr : ¬0 ∣ p
Tactic: rw [hq]