awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hp : Fact (Nat.Prime p)
pp : ℕ+ := p.toPNat ⋯
⊢ PrimitiveAddChar F F'
have hp₂ : ¬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)
-- 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 ⋯
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))
⊢ ψ' ≠ 1
have 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
Tactic: obtain ⟨a, ha⟩ := FiniteField.trace_to_zmod_nondegenerate F one_ne_zero
-- 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
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))
⊢ ψ' ≠ 1
have 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))
Tactic: rw [one_mul] 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
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))
⊢ PrimitiveAddChar F F'
have hψ' : ψ' ≠ 1
Tactic: have hψ' : ψ' ≠ 1 := by
    obtain ⟨a, ha⟩ := FiniteField.trace_to_zmod_nondegenerate F one_ne_zero
    rw [one_mul] at ha
    exact ne_one_iff.2
      ⟨a, fun hf => ha <| (ψ.prim.zmod_char_eq_one_iff pp <| Algebra.trace (ZMod p) F a).mp hf⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
Goal:
R : Type u_1
inst : AddGroup R
inst_1 : Fintype R
R' : Type u_2
inst_2 : CommRing R'
inst_3 : IsDomain R'
ψ : AddChar 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') (1 : R')),
  Eq.{u_2 + 1} (α := R') (∑ a : R, (ψ : (a : R) → R') a) 0
Tactic: rcases ne_one_iff.1 hψ with ⟨b, hb⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (hypothesis)
Goal:
R : Type u_1
inst : AddGroup R
inst_1 : Fintype R
R' : Type u_2
inst_2 : CommRing R'
inst_3 : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : Ne.{u_2 + 1} (α := R') ((ψ : (a : R) → R') b : R') (1 : R')
⊢ Eq.{u_2 + 1} (α := R') (∑ a : R, (ψ : (a : R) → R') a) 0
have h₁ : Eq.{u_2 + 1} (α := R') (∑ a : R, (ψ : (a : R) → R') (b + a)) (∑ a : R, (ψ : (a : R) → R') a)
Tactic: have h₁ : ∑ a : R, ψ (b + a) = ∑ a : R, ψ a :=
    Fintype.sum_bijective _ (AddGroup.addLeft_bijective b) _ _ fun x => rfl
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (hypothesis)
Goal:
R : Type u_1
inst : AddGroup R
inst_1 : Fintype R
R' : Type u_2
inst_2 : CommRing R'
inst_3 : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : Ne.{u_2 + 1} (α := R') ((ψ : (a : R) → R') b : R') (1 : R')
h₁ : Eq.{u_2 + 1} (α := R') (∑ a : R, (ψ : (a : R) → R') (b + a)) (∑ a : R, (ψ : (a : R) → R') a)
⊢ Eq.{u_2 + 1} (α := R') (∑ a : R, (ψ : (a : R) → R') a) 0
have h₂ : Eq.{u_2 + 1} (α := R') (∑ x : R, HMul.hMul (α := R') (β := R') ((ψ : (a : R) → R') b : R') ((ψ : (a : R) → R') x : R'))
  (∑ a : R, (ψ : (a : R) → R') a)
Tactic: simp_rw [map_add_eq_mul] at h₁
Cleared hypotheses: h₁
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (hypothesis)
Goal:
R : Type u_1
inst : AddGroup R
inst_1 : Fintype R
R' : Type u_2
inst_2 : CommRing R'
inst_3 : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : Ne.{u_2 + 1} (α := R') ((ψ : (a : R) → R') b : R') (1 : R')
h₁ :
  Eq.{u_2 + 1} (α := R')
    (∑ x : R, HMul.hMul (α := R') (β := R') ((ψ : (a : R) → R') b : R') ((ψ : (a : R) → R') x : R'))
    (∑ a : R, (ψ : (a : R) → R') a)
⊢ Eq.{u_2 + 1} (α := R') (∑ a : R, (ψ : (a : R) → R') a) 0
have h₂ : Eq.{u_2 + 1} (α := R') (∑ a : R, (ψ : (a : R) → R') a) (Finset.sum.{u_1, u_2} (ι := R) Finset.univ (⇑ψ : (a : R) → R'))
Tactic: have h₂ : ∑ a : R, ψ a = Finset.univ.sum ↑ψ := rfl
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (hypothesis)
Goal:
R : Type u_1
inst : AddGroup R
inst_1 : Fintype R
R' : Type u_2
inst_2 : CommRing R'
inst_3 : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : Ne.{u_2 + 1} (α := R') ((ψ : (a : R) → R') b : R') (1 : R')
h₁ :
  Eq.{u_2 + 1} (α := R')
    (∑ x : R, HMul.hMul (α := R') (β := R') ((ψ : (a : R) → R') b : R') ((ψ : (a : R) → R') x : R'))
    (∑ a : R, (ψ : (a : R) → R') a)
h₂ :
  Eq.{u_2 + 1} (α := R') (∑ a : R, (ψ : (a : R) → R') a)
    (Finset.sum.{u_1, u_2} (ι := R) Finset.univ (⇑ψ : (a : R) → R'))
⊢ Eq.{u_2 + 1} (α := R') (∑ a : R, (ψ : (a : R) → R') a) 0
have h₃ : HMul.hMul (α := R') (β := R') ((ψ : (a : R) → R') b : R')
    (Finset.sum.{u_1, u_2} (ι := R) Finset.univ (⇑ψ : (a : R) → R') : R') =
  Finset.sum.{u_1, u_2} (ι := R) Finset.univ (⇑ψ : (a : R) → R')
Tactic: rw [← Finset.mul_sum, h₂] at h₁
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fintype R
inst_2 : DecidableEq R
R' : Type u_2
inst_3 : CommRing R'
inst_4 : IsDomain R'
ψ : AddChar R R'
b : R
hψ : IsPrimitive.{u_1, u_2} (R := R) (R' := R') ψ
⊢ Eq.{u_2 + 1} (α := R') (∑ x : R, (ψ : (a : R) → R') (x * b)) (↑(if b = 0 then Fintype.card R else 0) : R')
have pos : ∀ (h : b = 0), Eq.{u_2 + 1} (α := R') (∑ x : R, (ψ : (a : R) → R') (x * b)) (↑(Fintype.card R) : R')
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fintype R
inst_2 : DecidableEq R
R' : Type u_2
inst_3 : CommRing R'
inst_4 : IsDomain R'
ψ : AddChar R R'
b : R
hψ : IsPrimitive.{u_1, u_2} (R := R) (R' := R') ψ
pos : ∀ (h : b = 0), Eq.{u_2 + 1} (α := R') (∑ x : R, (ψ : (a : R) → R') (x * b)) (↑(Fintype.card R) : R')
⊢ Eq.{u_2 + 1} (α := R') (∑ x : R, (ψ : (a : R) → R') (x * b)) (↑(if b = 0 then Fintype.card R else 0) : R')
have neg : ∀ (h : ¬b = 0), Eq.{u_2 + 1} (α := R') (∑ x : R, (ψ : (a : R) → R') (x * b)) (↑0 : R')
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fintype R
inst_2 : DecidableEq R
R' : Type u_2
inst_3 : CommRing R'
inst_4 : IsDomain R'
ψ : AddChar R R'
b : R
hψ : IsPrimitive.{u_1, u_2} (R := R) (R' := R') ψ
h : b = 0
⊢ Eq.{u_2 + 1} (α := R') (∑ x : R, (ψ : (a : R) → R') (x * b)) (↑(Fintype.card R) : R')
have pos : Eq.{u_2 + 1} (α := R') (↑(Finset.card.{u_1} (α := R) Finset.univ) : R') (↑(Fintype.card R) : R')
Tactic: simp only [h, mul_zero, map_zero_eq_one, Finset.sum_const, Nat.smul_one_eq_cast]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
Goal:
R : Type u_1
inst : CommRing R
inst_1 : Fintype R
inst_2 : DecidableEq R
R' : Type u_2
inst_3 : CommRing R'
inst_4 : IsDomain R'
ψ : AddChar R R'
b : R
hψ : IsPrimitive.{u_1, u_2} (R := R) (R' := R') ψ
h : ¬b = 0
⊢ Eq.{u_2 + 1} (α := R') (∑ x : R, (ψ : (a : R) → R') (x * b)) (↑0 : R')
have neg : Eq.{u_2 + 1} (α := R') (∑ x : R, (ψ : (a : R) → R') (b * x)) (↑0 : R')
Tactic: simp_rw [mul_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
Goal:
R : Type u_1
inst : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
⊢ MonoidHom.compAddChar (↑(starRingEnd ℂ) : ℂ →* ℂ) φ = φ⁻¹
have h : ∀ (a : R),
  Eq (α := ℂ) ((MonoidHom.compAddChar (↑(starRingEnd ℂ) : ℂ →* ℂ) φ : (a : R) → ℂ) a : ℂ) ((φ⁻¹ : (a : R) → ℂ) a : ℂ)
Tactic: ext1 a
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
Goal:
R : Type u_1
inst : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
⊢ Eq (α := ℂ) ((MonoidHom.compAddChar (↑(starRingEnd ℂ) : ℂ →* ℂ) φ : (a : R) → ℂ) a : ℂ) ((φ⁻¹ : (a : R) → ℂ) a : ℂ)
have h : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : R) → ℂ) a : ℂ) : ℂ) (((φ : (a : R) → ℂ) a)⁻¹ : ℂ)
Tactic: simp only [RingHom.toMonoidHom_eq_coe, MonoidHom.coe_compAddChar, MonoidHom.coe_coe,
    Function.comp_apply, inv_apply']
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (hypothesis)
Goal:
R : Type u_1
inst : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : R) → ℂ) a : ℂ) : ℂ) (((φ : (a : R) → ℂ) a)⁻¹ : ℂ)
have H : norm (E := ℂ) (↑(IsUnit.unit (a := (φ : (a : R) → ℂ) a) sorry) : ℂ) = 1
Tactic: have H := Complex.norm_eq_one_of_mem_rootsOfUnity <| φ.val_mem_rootsOfUnity a hR
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.AddCharacter (goal)
Goal:
R : Type u_1
inst : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : R) → ℂ) a : ℂ) : ℂ) ((φ⁻¹ : (a : R) → ℂ) a : ℂ)
have rw : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : R) → ℂ) a : ℂ) : ℂ)
  ((MonoidHom.compAddChar (↑(starRingEnd ℂ) : ℂ →* ℂ) φ : (a : R) → ℂ) a : ℂ)
Tactic: rw [← starComp_eq_inv hR]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : (ZMod p)ˣ
⊢ (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ x ^ (p / 2) = 1
have pos : ∀ (hc : p = 2), (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ x ^ (p / 2) = 1
Tactic: by_cases hc : p = 2
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : (ZMod p)ˣ
pos : ∀ (hc : p = 2), (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ x ^ (p / 2) = 1
⊢ (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ x ^ (p / 2) = 1
have neg : ∀ (hc : ¬p = 2), (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ x ^ (p / 2) = 1
Tactic: by_cases hc : p = 2
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : p = 2
⊢ (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ x ^ (p / 2) = 1
have pos : ∀ [inst : Fact (Nat.Prime 2)] (x : (ZMod 2)ˣ), (∃ (y : (ZMod 2)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ x ^ (2 / 2) = 1
Tactic: subst hc
Cleared hypotheses: p, inst, x, hc
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
⊢ ringChar (ZMod p) ≠ 2
have rwa : p ≠ 2
Tactic: rwa [ringChar_zmod_n]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
⊢ (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ x ^ (p / 2) = 1
have h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
Tactic: have h₀ := FiniteField.unit_isSquare_iff (by rwa [ringChar_zmod_n]) x
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
⊢ (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ IsSquare x
have rw : (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ ∃ (r : (ZMod p)ˣ), x = HPow.hPow (β := ℕ) r 2
Tactic: rw [isSquare_iff_exists_sq x]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
⊢ (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ x ^ (p / 2) = 1
have hs : (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ IsSquare x
Tactic: have hs : (∃ y : (ZMod p)ˣ, y ^ 2 = x) ↔ IsSquare x := by
      rw [isSquare_iff_exists_sq x]
      simp_rw [eq_comm]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
hs : (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ IsSquare x
⊢ (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ x ^ (p / 2) = 1
have neg : IsSquare x ↔ x ^ (p / 2) = 1
Tactic: rw [hs]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
hs : (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ IsSquare x
⊢ IsSquare x ↔ x ^ (p / 2) = 1
have neg : ∀ (h₀ : IsSquare x ↔ x ^ (p / 2) = 1) (hs : (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ IsSquare x),
  IsSquare x ↔ x ^ (p / 2) = 1
Tactic: rwa [card p] at h₀
Cleared hypotheses: h₀, hs
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ IsSquare a ↔ a ^ (p / 2) = 1
have apply : (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = Units.mk0 a ha) ↔ IsSquare a
Tactic: apply (iff_congr _ (by simp [Units.ext_iff])).mp (euler_criterion_units p (Units.mk0 a ha))
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = Units.mk0 a ha) ↔ IsSquare a
have simp : (∃ (y : (ZMod p)ˣ), (↑y : ZMod p) * (↑y : ZMod p) = a) ↔ IsSquare a
Tactic: simp only [Units.ext_iff, sq, Units.val_mk0, Units.val_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ (∃ (y : (ZMod p)ˣ), (↑y : ZMod p) * (↑y : ZMod p) = a) ↔ IsSquare a
have mp : (∃ (y : (ZMod p)ˣ), (↑y : ZMod p) * (↑y : ZMod p) = a) → IsSquare a
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
mp : (∃ (y : (ZMod p)ˣ), (↑y : ZMod p) * (↑y : ZMod p) = a) → IsSquare a
⊢ (∃ (y : (ZMod p)ˣ), (↑y : ZMod p) * (↑y : ZMod p) = a) ↔ IsSquare a
have mpr : IsSquare a → ∃ (y : (ZMod p)ˣ), (↑y : ZMod p) * (↑y : ZMod p) = a
Tactic: constructor
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
⊢ ∃ (y_1 : (ZMod p)ˣ), (↑y_1 : ZMod p) * (↑y_1 : ZMod p) = y * y
have hy : y ≠ 0
Tactic: have hy : y ≠ 0 := by
      rintro rfl
      simp [mul_zero, ne_eq] at ha
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
hy : y ≠ 0
⊢ ∃ (y_1 : (ZMod p)ˣ), (↑y_1 : ZMod p) * (↑y_1 : ZMod p) = y * y
have mpr : (↑(Units.mk0 y hy : (ZMod p)ˣ) : ZMod p) * (↑(Units.mk0 y hy : (ZMod p)ˣ) : ZMod p) = y * y
Tactic: refine ⟨Units.mk0 y hy, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1
have inl : ∀ [inst : Fact (Nat.Prime 2)] {a : ZMod 2} (ha : a ≠ 0), a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1
Tactic: rcases Prime.eq_two_or_odd (@Fact.out p.Prime _) with rfl | hp_odd
Cleared hypotheses: p, inst, a, ha
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
inl : ∀ [inst : Fact (Nat.Prime 2)] {a : ZMod 2} (ha : a ≠ 0), a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1
⊢ a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1
have inr : ∀ (hp_odd : p % 2 = 1), a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1
Tactic: rcases Prime.eq_two_or_odd (@Fact.out p.Prime _) with rfl | hp_odd
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
inst : Fact (Nat.Prime 2)
a : ZMod 2
ha : a ≠ 0
⊢ a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1
have inl : ∀ {a : ZMod 2} (ha : a ≠ 0), a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1
Tactic: revert a ha
Cleared hypotheses: a, ha
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
inst : Fact (Nat.Prime 2)
a : ZMod 2
⊢ ∀ (ha : a ≠ 0), a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1
have inl : ∀ (ha : Ne (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) ⟨0, sorry⟩) 0),
  HPow.hPow (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) (⟨0, sorry⟩ : Fin (1 + 1))) (2 / 2) = 1 ∨
    HPow.hPow (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) (⟨0, sorry⟩ : Fin (1 + 1))) (2 / 2) = -1
Tactic: fin_cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
inst : Fact (Nat.Prime 2)
a : ZMod 2
inl :
  ∀ (ha : Ne (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) ⟨0, ⋯⟩) 0),
    HPow.hPow (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (1 + 1))) (2 / 2) = 1 ∨
      HPow.hPow (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) (⟨0, ⋯⟩ : Fin (1 + 1))) (2 / 2) = -1
⊢ ∀ (ha : a ≠ 0), a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1
have inl₁ : ∀ (ha : Ne (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) ⟨1, sorry⟩) 0),
  HPow.hPow (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) (⟨1, sorry⟩ : Fin (1 + 1))) (2 / 2) = 1 ∨
    HPow.hPow (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) (⟨1, sorry⟩ : Fin (1 + 1))) (2 / 2) = -1
Tactic: fin_cases a
Cleared hypotheses: a
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp_odd : p % 2 = 1
⊢ a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1
have inr : a ^ (p - 1) = 1
Tactic: rw [← mul_self_eq_one_iff, ← pow_add, ← two_mul, two_mul_odd_div_two hp_odd]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
⊢ (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
have inl : ∀ (hc : ringChar (ZMod p) = 2), (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
Tactic: rcases eq_or_ne (ringChar (ZMod p)) 2 with hc | hc
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
inl : ∀ (hc : ringChar (ZMod p) = 2), (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
⊢ (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
have inr : ∀ (hc : ringChar (ZMod p) ≠ 2), (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
Tactic: rcases eq_or_ne (ringChar (ZMod p)) 2 with hc | hc
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
⊢ (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
have pos : ∀ (ha : Eq (α := ZMod p) (↑a : ZMod p) 0), (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
Tactic: by_cases ha : (a : ZMod p) = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
pos :
  ∀ (ha : Eq (α := ZMod p) (↑a : ZMod p) 0),
    (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
⊢ (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
have neg : ∀ (ha : ¬Eq (α := ZMod p) (↑a : ZMod p) 0),
  (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
Tactic: by_cases ha : (a : ZMod p) = 0
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : Eq (α := ZMod p) (↑a : ZMod p) 0
⊢ (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
have pos : Eq (α := ZMod p) (↑0 : ZMod p) 0
Tactic: rw [legendreSym, ha, quadraticChar_zero,
        zero_pow (Nat.div_pos (@Fact.out p.Prime).two_le (succ_pos 1)).ne']
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : Eq (α := ZMod p) (↑a : ZMod p) 0
⊢ Eq (α := ZMod p) (↑0 : ZMod p) 0
have pos : Eq (α := ZMod p) 0 0
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (hypothesis)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ¬Eq (α := ZMod p) (↑a : ZMod p) 0
⊢ (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
have this : p = 2
Tactic: have := (ringChar_zmod_n p).symm.trans hc
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ℤ
hc : ringChar (ZMod p) = 2
ha : ¬Eq (α := ZMod p) (↑a : ZMod p) 0
this : p = 2
⊢ (↑(legendreSym p a) : ZMod p) = HPow.hPow (α := ZMod p) (↑a : ZMod p) (p / 2)
have neg : ∀ [inst : Fact (Nat.Prime 2)] (hc : ringChar (ZMod 2) = 2) (ha : ¬Eq (α := ZMod 2) (↑a : ZMod 2) 0),
  (↑(legendreSym 2 a) : ZMod 2) = HPow.hPow (α := ZMod 2) (↑a : ZMod 2) (2 / 2)
Tactic: subst p
Cleared hypotheses: p, inst, hc, ha, this
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
a : ℤ
inst : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
ha : ¬Eq (α := ZMod 2) (↑a : ZMod 2) 0
⊢ (↑(legendreSym 2 a) : ZMod 2) = HPow.hPow (α := ZMod 2) (↑a : ZMod 2) (2 / 2)
have neg : (↑1 : ZMod 2) = HPow.hPow (α := ZMod 2) (↑a : ZMod 2) (2 / 2)
Tactic: rw [legendreSym, quadraticChar_eq_one_of_char_two hc ha]
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
a : ℤ
inst : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
ha : ¬Eq (α := ZMod 2) (↑a : ZMod 2) 0
⊢ (↑1 : ZMod 2) = HPow.hPow (α := ZMod 2) (↑a : ZMod 2) (2 / 2)
have neg : ∀ (ha : ¬Eq (α := ZMod 2) (↑a : ZMod 2) 0), (↑1 : ZMod 2) = HPow.hPow (α := ZMod 2) (↑a : ZMod 2) (2 / 2)
Tactic: revert ha
Cleared hypotheses: ha
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
a : ℤ
inst : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
⊢ ∀ (ha : ¬Eq (α := ZMod 2) (↑a : ZMod 2) 0), 1 = HPow.hPow (α := ZMod 2) (β := ℕ) (↑a : ZMod 2) 1
have neg : ∀ (b : ZMod 2) (ha : ¬b = 0), 1 = HPow.hPow (β := ℕ) b 1
Tactic: generalize (a : ZMod 2) = b
-- Lean 4 proof step from Mathlib.NumberTheory.LegendreSymbol.Basic (goal)
Goal:
a : ℤ
inst : Fact (Nat.Prime 2)
hc : ringChar (ZMod 2) = 2
b : ZMod 2
⊢ ∀ (ha : ¬b = 0), 1 = HPow.hPow (β := ℕ) b 1
have neg : ∀ (ha : ¬Eq (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) ⟨0, sorry⟩) 0),
  1 = HPow.hPow (α := ZMod 2) (β := ℕ) ((fun (i : Fin (1 + 1)) ↦ i) (⟨0, sorry⟩ : Fin (1 + 1))) 1
Tactic: fin_cases b
Cleared hypotheses: b