awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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:
exact 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
-- 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))
⊢ ψ' ≠ 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⟩
-- 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))
hψ' : ψ' ≠ 1
⊢ PrimitiveAddChar F F'

Tactic:
exact ⟨ψ.n, ψ', IsPrimitive.of_ne_one hψ'⟩
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
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
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
⊢ Eq.{u_2 + 1} (α := R') (∑ a : R, (ψ : (a : R) → R') a) 0

Tactic:
rcases ne_one_iff.1 hψ with ⟨b, hb⟩

Premises used: AddChar.ne_one_iff, Iff.mp
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
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') (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
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
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')
    (∑ 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₁

Premises used: AddChar.map_add_eq_mul
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
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)
    (Finset.sum.{u_1, u_2} (ι := R) Finset.univ (⇑ψ : (a : R) → R'))

Tactic:
have h₂ : ∑ a : R, ψ a = Finset.univ.sum ↑ψ := rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
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'))
⊢ 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₁

Premises used: Finset.mul_sum
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
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'))
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')
⊢ Eq.{u_2 + 1} (α := R') (∑ a : R, (ψ : (a : R) → R') a)
    (Finset.sum.{u_1, u_2} (ι := R) Finset.univ (⇑ψ : (a : R) → R'))

Tactic:
rw [← Finset.mul_sum, h₂] at h₁

Premises used: Finset.mul_sum
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
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₁ :
  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')
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

Tactic:
eq_zero_of_mul_eq_self_left hb h₁

Premises used: eq_zero_of_mul_eq_self_left
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
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₁ :
  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')
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

Tactic:
exact eq_zero_of_mul_eq_self_left hb h₁

Premises used: eq_zero_of_mul_eq_self_left
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u_1
inst : AddGroup R
inst_1 : Fintype R
R' : Type u_2
inst_2 : CommRing R'
ψ : AddChar R R'
hψ : ψ = 1
⊢ Eq.{u_2 + 1} (α := R') (∑ a : R, (ψ : (a : R) → R') a) (↑(Fintype.card R) : R')

Tactic:
simp [hψ]
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
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')
neg : ∀ (h : ¬b = 0), Eq.{u_2 + 1} (α := R') (∑ x : R, (ψ : (a : R) → R') (x * b)) (↑0 : R')
⊢ Eq.{u_2 + 1} (α := R') (∑ x : R, (ψ : (a : R) → R') (x * b)) (↑(if b = 0 then Fintype.card R else 0) : R')

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
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
pos : Eq.{u_2 + 1} (α := R') (↑(Finset.card.{u_1} (α := R) Finset.univ) : R') (↑(Fintype.card R) : R')
⊢ Eq.{u_2 + 1} (α := R') (∑ x : R, (ψ : (a : R) → R') (x * b)) (↑(Fintype.card R) : R')

Tactic:
simp only [h, mul_zero, map_zero_eq_one, Finset.sum_const, Nat.smul_one_eq_cast]

Premises used: AddChar.map_zero_eq_one, MulZeroClass.mul_zero, Nat.smul_one_eq_cast, Finset.sum_const
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
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') (↑(Finset.card.{u_1} (α := R) Finset.univ) : R') (↑(Fintype.card R) : R')

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
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
neg : Eq.{u_2 + 1} (α := R') (∑ x : R, (ψ : (a : R) → R') (b * x)) (↑0 : R')
⊢ Eq.{u_2 + 1} (α := R') (∑ x : R, (ψ : (a : R) → R') (x * b)) (↑0 : R')

Tactic:
simp_rw [mul_comm]

Premises used: mul_comm
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
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') (b * x)) (↑0 : R')

Tactic:
mod_cast sum_eq_zero_of_ne_one (hψ h)

Premises used: HMul.hMul, Finset.univ, congrArg, cast, AddChar.sum_eq_zero_of_ne_one, Nat.cast_zero, Eq.symm, Eq, DFunLike.coe, Finset.sum, Eq.trans, AddChar.mulShift
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
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') (b * x)) (↑0 : R')

Tactic:
exact mod_cast sum_eq_zero_of_ne_one (hψ h)

Premises used: AddChar.sum_eq_zero_of_ne_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u_1
inst : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
h :
  ∀ (a : R),
    Eq (α := ℂ) ((MonoidHom.compAddChar (↑(starRingEnd ℂ) : ℂ →* ℂ) φ : (a : R) → ℂ) a : ℂ) ((φ⁻¹ : (a : R) → ℂ) a : ℂ)
⊢ MonoidHom.compAddChar (↑(starRingEnd ℂ) : ℂ →* ℂ) φ = φ⁻¹

Tactic:
ext1 a
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u_1
inst : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
h : Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : R) → ℂ) a : ℂ) : ℂ) (((φ : (a : R) → ℂ) a)⁻¹ : ℂ)
⊢ Eq (α := ℂ) ((MonoidHom.compAddChar (↑(starRingEnd ℂ) : ℂ →* ℂ) φ : (a : R) → ℂ) a : ℂ) ((φ⁻¹ : (a : R) → ℂ) a : ℂ)

Tactic:
simp only [RingHom.toMonoidHom_eq_coe, MonoidHom.coe_compAddChar, MonoidHom.coe_coe,
    Function.comp_apply, inv_apply']

Premises used: RingHom.toMonoidHom_eq_coe, MonoidHom.coe_coe, AddChar.inv_apply', MonoidHom.coe_compAddChar, Function.comp_apply
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u_1
inst : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
⊢ norm (E := ℂ) (↑(IsUnit.unit (a := (φ : (a : R) → ℂ) a) ⋯) : ℂ) = 1

Tactic:
have H := Complex.norm_eq_one_of_mem_rootsOfUnity <| φ.val_mem_rootsOfUnity a hR
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u_1
inst : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
H : norm (E := ℂ) (↑(IsUnit.unit (a := (φ : (a : R) → ℂ) a) ⋯) : ℂ) = 1
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : R) → ℂ) a : ℂ) : ℂ) (((φ : (a : R) → ℂ) a)⁻¹ : ℂ)

Tactic:
(Complex.inv_eq_conj H).symm

Premises used: Complex.inv_eq_conj, Eq.symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u_1
inst : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
H : norm (E := ℂ) (↑(IsUnit.unit (a := (φ : (a : R) → ℂ) a) ⋯) : ℂ) = 1
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : R) → ℂ) a : ℂ) : ℂ) (((φ : (a : R) → ℂ) a)⁻¹ : ℂ)

Tactic:
exact (Complex.inv_eq_conj H).symm

Premises used: Complex.inv_eq_conj, Eq.symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u_1
inst : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
rw :
  Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : R) → ℂ) a : ℂ) : ℂ)
    ((MonoidHom.compAddChar (↑(starRingEnd ℂ) : ℂ →* ℂ) φ : (a : R) → ℂ) a : ℂ)
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : R) → ℂ) a : ℂ) : ℂ) ((φ⁻¹ : (a : R) → ℂ) a : ℂ)

Tactic:
rw [← starComp_eq_inv hR]

Premises used: AddChar.starComp_eq_inv
-- Module: Mathlib.NumberTheory.LegendreSymbol.AddCharacter
Goal:
R : Type u_1
inst : CommRing R
hR : 0 < ringChar R
φ : AddChar R ℂ
a : R
⊢ Eq (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((φ : (a : R) → ℂ) a : ℂ) : ℂ)
    ((MonoidHom.compAddChar (↑(starRingEnd ℂ) : ℂ →* ℂ) φ : (a : R) → ℂ) a : ℂ)

Tactic:
rfl
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
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
neg : ∀ (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

Tactic:
by_cases hc : p = 2
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : p = 2
pos : ∀ [inst : Fact (Nat.Prime 2)] (x : (ZMod 2)ˣ), (∃ (y : (ZMod 2)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ x ^ (2 / 2) = 1
⊢ (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ x ^ (p / 2) = 1

Tactic:
subst hc
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
inst : Fact (Nat.Prime 2)
x : (ZMod 2)ˣ
⊢ (∃ (y : (ZMod 2)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ x ^ (2 / 2) = 1

Tactic:
simp only [eq_iff_true_of_subsingleton, exists_const]

Premises used: exists_const, eq_iff_true_of_subsingleton
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
rwa rwa₁ rwa₂ rwa₃ : p ≠ 2
⊢ ringChar (ZMod p) ≠ 2

Tactic:
rwa [ringChar_zmod_n]

Premises used: ZMod.ringChar_zmod_n
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
⊢ IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1

Tactic:
have h₀ := FiniteField.unit_isSquare_iff (by rwa [ringChar_zmod_n]) x
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
x : (ZMod p)ˣ
hc : ¬p = 2
h₀ : IsSquare x ↔ x ^ (Fintype.card (ZMod p) / 2) = 1
rw : (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ ∃ (r : (ZMod p)ˣ), x = HPow.hPow (β := ℕ) r 2
⊢ (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ IsSquare x

Tactic:
rw [isSquare_iff_exists_sq x]

Premises used: isSquare_iff_exists_sq
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
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) ↔ ∃ (r : (ZMod p)ˣ), x = HPow.hPow (β := ℕ) r 2

Tactic:
simp_rw [eq_comm]

Premises used: eq_comm
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
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

Tactic:
have hs : (∃ y : (ZMod p)ˣ, y ^ 2 = x) ↔ IsSquare x := by
      rw [isSquare_iff_exists_sq x]
      simp_rw [eq_comm]
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
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
neg : IsSquare x ↔ x ^ (p / 2) = 1
⊢ (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = x) ↔ x ^ (p / 2) = 1

Tactic:
rw [hs]
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
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
neg neg₁ neg₂ 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
⊢ IsSquare x ↔ x ^ (p / 2) = 1

Tactic:
rwa [card p] at h₀

Premises used: ZMod.card
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
⊢ HPow.hPow (α := (ZMod p)ˣ) (Units.mk0 a ha : (ZMod p)ˣ) (p / 2) = 1 ↔ a ^ (p / 2) = 1

Tactic:
simp [Units.ext_iff]

Premises used: Units.ext_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
apply : (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = Units.mk0 a ha) ↔ IsSquare a
⊢ IsSquare a ↔ a ^ (p / 2) = 1

Tactic:
apply (iff_congr _ (by simp [Units.ext_iff])).mp (euler_criterion_units p (Units.mk0 a ha))

Premises used: iff_congr, ZMod.euler_criterion_units, Units.mk0, Iff.mp
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
simp : (∃ (y : (ZMod p)ˣ), (↑y : ZMod p) * (↑y : ZMod p) = a) ↔ IsSquare a
⊢ (∃ (y : (ZMod p)ˣ), HPow.hPow (β := ℕ) y 2 = Units.mk0 a ha) ↔ IsSquare a

Tactic:
simp only [Units.ext_iff, sq, Units.val_mk0, Units.val_mul]

Premises used: Units.ext_iff, sq, Units.val_mk0, Units.val_mul
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
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
mpr : IsSquare a → ∃ (y : (ZMod p)ˣ), (↑y : ZMod p) * (↑y : ZMod p) = a
⊢ (∃ (y : (ZMod p)ˣ), (↑y : ZMod p) * (↑y : ZMod p) = a) ↔ IsSquare a

Tactic:
constructor
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
y : (ZMod p)ˣ
hy : (↑y : ZMod p) * (↑y : ZMod p) = a
⊢ IsSquare a

Tactic:
⟨y, hy.symm⟩

Premises used: Units.val, IsSquare, Exists.intro, Eq.symm
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
y : (ZMod p)ˣ
hy : (↑y : ZMod p) * (↑y : ZMod p) = a
⊢ IsSquare a

Tactic:
exact ⟨y, hy.symm⟩
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
ha : HMul.hMul (α := ZMod p) 0 0 ≠ 0
⊢ False

Tactic:
simp [mul_zero, ne_eq] at ha

Premises used: ne_eq, MulZeroClass.mul_zero
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
⊢ y ≠ 0

Tactic:
have hy : y ≠ 0 := by
      rintro rfl
      simp [mul_zero, ne_eq] at ha
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
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

Tactic:
⟨Units.mk0 y hy, ?_⟩

Premises used: Units.mk0, Exists.intro
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
hy : y ≠ 0
mpr : (↑(Units.mk0 y hy : (ZMod p)ˣ) : ZMod p) * (↑(Units.mk0 y hy : (ZMod p)ˣ) : ZMod p) = y * y
⊢ ∃ (y_1 : (ZMod p)ˣ), (↑y_1 : ZMod p) * (↑y_1 : ZMod p) = y * y

Tactic:
refine ⟨Units.mk0 y hy, ?_⟩
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
y : ZMod p
ha : y * y ≠ 0
hy : y ≠ 0
⊢ (↑(Units.mk0 y hy : (ZMod p)ˣ) : ZMod p) * (↑(Units.mk0 y hy : (ZMod p)ˣ) : ZMod p) = y * y

Tactic:
simp
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
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
inr : ∀ (hp_odd : p % 2 = 1), a ^ (p / 2) = 1 ∨ a ^ (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

Premises used: Nat.Prime.eq_two_or_odd, rfl, Fact.out
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
inst : Fact (Nat.Prime 2)
a : ZMod 2
ha : a ≠ 0
inl : ∀ {a : ZMod 2} (ha : a ≠ 0), a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1
⊢ a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1

Tactic:
revert a ha
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
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
inl₁ :
  ∀ (ha : Ne (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) ⟨1, ⋯⟩) 0),
    HPow.hPow (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (1 + 1))) (2 / 2) = 1 ∨
      HPow.hPow (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (1 + 1))) (2 / 2) = -1
⊢ ∀ (ha : a ≠ 0), a ^ (2 / 2) = 1 ∨ a ^ (2 / 2) = -1

Tactic:
fin_cases a
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
inst : Fact (Nat.Prime 2)
inl :
  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 : 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

Tactic:
tauto
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
inst : Fact (Nat.Prime 2)
⊢ ∀ (ha : Ne (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) ⟨1, ⋯⟩) 0),
    HPow.hPow (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (1 + 1))) (2 / 2) = 1 ∨
      HPow.hPow (α := ZMod 2) ((fun (i : Fin (1 + 1)) ↦ i) (⟨1, ⋯⟩ : Fin (1 + 1))) (2 / 2) = -1

Tactic:
simp
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp_odd : p % 2 = 1
inr : a ^ (p - 1) = 1
⊢ a ^ (p / 2) = 1 ∨ a ^ (p / 2) = -1

Tactic:
rw [← mul_self_eq_one_iff, ← pow_add, ← two_mul, two_mul_odd_div_two hp_odd]

Premises used: two_mul, pow_add, Nat.two_mul_odd_div_two, mul_self_eq_one_iff
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp_odd : p % 2 = 1
⊢ a ^ (p - 1) = 1

Tactic:
pow_card_sub_one_eq_one ha

Premises used: ZMod.pow_card_sub_one_eq_one
-- Module: Mathlib.NumberTheory.LegendreSymbol.Basic
Goal:
p : ℕ
inst : Fact (Nat.Prime p)
a : ZMod p
ha : a ≠ 0
hp_odd : p % 2 = 1
⊢ a ^ (p - 1) = 1

Tactic:
exact pow_card_sub_one_eq_one ha

Premises used: ZMod.pow_card_sub_one_eq_one