mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
hp : p ≠ 2
a : ℕ
ha1 : a % 2 = 1
ha0 : ↑a ≠ 0
hp' : Fact (p % 2 = 1)
ha0' : ↑↑a ≠ 0
⊢ (-1) ^ ((∑ x ∈ Ico 1 (p / 2).succ, x * a / p) % 2) = (-1) ^ ((∑ x ∈ Ico 1 (p / 2).succ, x * a / p) % 2)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
hb : b = 0
⊢ 1 ≠ 0

Tactic:
]

Goal state after:
case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
hb : b = 0
⊢ 1 ≠ 0
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x : R
hx : ϖ ^ (n + 1) ∣ x * ϖ ^ n
⊢ x ∈ I

Tactic:
]

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x : R
hx : ϖ ^ (n + 1) ∣ x * ϖ ^ n
⊢ x ∈ I
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inl
a : ℤ
b : ℕ
h : 1 = 0
hb : b = 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1

Tactic:
]

Goal state after:
case inl
a : ℤ
b : ℕ
h : 1 = 0
hb : b = 0
⊢ b ≠ 0 ∧ a.gcd ↑b ≠ 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
x✝ : b ≠ 0 ∧ a.gcd ↑b ≠ 1
hb : NeZero b
h : a.gcd ↑b ≠ 1
⊢ J(a | b) = 0

Tactic:
]

Goal state after:
a : ℤ
b : ℕ
x✝ : b ≠ 0 ∧ a.gcd ↑b ≠ 1
hb : NeZero b
h : a.gcd ↑b ≠ 1
⊢ J(a | b) = 0
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: b : ℕ
hb : 1 < b
⊢ b ≠ 1

Tactic:
]

Goal state after:
b : ℕ
hb : 1 < b
⊢ b ≠ 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
e b : ℕ
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
e b x✝ : ℕ
ih : J(a ^ x✝ | b) = J(a | b) ^ x✝
⊢ J(a | b) ^ x✝ * J(a | b) = J(a | b) ^ x✝ * J(a | b)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case zero
a : ℤ
b : ℕ
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : x = ϖ * y
⊢ x ∈ I

pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : ϖ ^ n * x = ϖ ^ n * (ϖ * y)
⊢ ϖ ≠ 0

Tactic:
]

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : x = ϖ * y
⊢ x ∈ I

R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : ϖ ^ n * x = ϖ ^ n * (ϖ * y)
⊢ ϖ ≠ 0
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ (s - 1) * ε * ∫ (a : ℝ) in Set.Ioi T, a ^ (-s) ≤ (s - 1) * ε * ∫ (t : ℝ) in Set.Ioi 1, t ^ (-s)

Tactic:
]

Goal state after:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ (s - 1) * ε * ∫ (a : ℝ) in Set.Ioi T, a ^ (-s) ≤ (s - 1) * ε * ∫ (t : ℝ) in Set.Ioi 1, t ^ (-s)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case succ.inl
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
hb : b = 0
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.Topology.Algebra.Module.Compact

Goal state before:
pp: R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
this : (Fintype.linearCombination R Subtype.val).range = N
⊢ IsCompact ↑(Fintype.linearCombination R Subtype.val).range

Tactic:
]

Goal state after:
R : Type u_1
M : Type u_2
inst✝⁷ : CommSemiring R
inst✝⁶ : TopologicalSpace R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : TopologicalSpace M
inst✝² : ContinuousAdd M
inst✝¹ : ContinuousSMul R M
inst✝ : CompactSpace R
N : Submodule R M
s : Finset M
hs : span R ↑s = N
this : (Fintype.linearCombination R Subtype.val).range = N
⊢ IsCompact ↑(Fintype.linearCombination R Subtype.val).range
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case succ.inr
a : ℤ
b e : ℕ
ih : J(a | b ^ e) = J(a | b) ^ e
h✝ : NeZero b
⊢ J(a | b) ^ e * J(a | b) = J(a | b) ^ e * J(a | b)

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : x = ϖ * y
⊢ ϖ ∣ x

Tactic:
]

Goal state after:
case mpr
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : x = ϖ * y
⊢ ϖ ∣ x
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = 1
⊢ 1 ^ 2 = 1

Tactic:
]

Goal state after:
case inl
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = 1
⊢ 1 ^ 2 = 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = -1
⊢ (-1) ^ 2 = 1

Tactic:
]

Goal state after:
case inr
a : ℤ
b : ℕ
h : a.gcd ↑b = 1
h₁ : J(a | b) = -1
⊢ (-1) ^ 2 = 1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
h : a.gcd ↑b = 1
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
x y : R
hy : ϖ ^ n * x = ϖ ^ n * (ϖ * y)
h' : ϖ = 0
⊢ 0 = 0

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a₁ a₂ : ℤ
b : ℕ
h : a₁ % ↑b = a₂ % ↑b
⊢ J(a₂ | b) = J(a₂ | b)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : ↑p ∣ x ^ 2 - a * y ^ 2
⊢ ↑p ∣ x ∧ ↑p ∣ y

Tactic:
]

Goal state after:
p : ℕ
inst✝ : Fact (Nat.Prime p)
a : ℤ
h : legendreSym p a = -1
x y : ℤ
hxy : ↑p ∣ x ^ 2 - a * y ^ 2
⊢ ↑p ∣ x ∧ ↑p ∣ y
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ 1 < s

Tactic:
]

Goal state after:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ 1 < s
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case cons
n✝ : ℕ
n : ℤ
l' : List ℤ
ih : J(l'.prod | n✝) = (List.map (fun a ↦ J(a | n✝)) l').prod
⊢ J(n | n✝) * (List.map (fun a ↦ J(a | n✝)) l').prod = J(n | n✝) * (List.map (fun a ↦ J(a | n✝)) l').prod

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ ε * ((s - 1) * (-1 / (-s + 1))) = ε

Tactic:
]

Goal state after:
l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
hT₀ : 0 < T
h : ∀ {t : ℝ}, 0 < t → t ^ (-s) = t * t ^ (-s - 1)
⊢ ε * ((s - 1) * (-1 / (-s + 1))) = ε
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: l : ℂ
s T ε : ℝ
S : ℝ → ℂ
hS : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
hε : 0 < ε
hs : 1 < s
hT₁ : 1 ≤ T
hT : ∀ t ≥ T, ‖S t - l * ↑t‖ ≤ ε * t
⊢ (s - 1) * ∫ (t : ℝ) in Set.Ioi T, ‖S t - l * ↑t‖ * t ^ (-s - 1) ≤ ε

Tactic:
have hT₀ : 0 < T := zero_lt_one.trans_le hT₁
  have h {t : ℝ} (ht : 0 < t) : t ^ (-s) = t * t ^ (-s - 1) := by
    rw [Real.rpow_sub ht, Real.rpow_one, mul_div_cancel₀ _ ht.ne']
  calc
    _ ≤ (s - 1) * ∫ (t : ℝ) in Set.Ioi T, ε * t ^ (-s) := by
      refine mul_le_mul_of_nonneg_left (setIntegral_mono_on ?_ ?_ measurableSet_Ioi fun t ht ↦ ?_)
        (sub_pos_of_lt hs).le
      · exact (lemma₂ hs hS hT).mono_set <| Set.Ioi_subset_Ici_iff.mpr hT₁
      · exact (integrableOn_Ioi_rpow_of_lt (neg_lt_neg_iff.mpr hs) hT₀).const_mul _
      · have ht' : 0 < t := hT₀.trans ht
        rw [h ht', ← mul_assoc]
        exact mul_le_mul_of_nonneg_right (hT t ht.le) (Real.rpow_nonneg ht'.le _)
    _ ≤ ε * ((s - 1) * ∫ (t : ℝ) in Set.Ioi 1, t ^ (-s)) := by
      rw [integral_const_mul, ← mul_assoc, ← mul_assoc, mul_comm ε]
      refine mul_le_mul_of_nonneg_left (setIntegral_mono_set ?_ ?_
        (Set.Ioi_subset_Ioi hT₁).eventuallyLE) (mul_nonneg (sub_pos_of_lt hs).le hε.le)
      · exact integrableOn_Ioi_rpow_of_lt (neg_lt_neg_iff.mpr hs) zero_lt_one
      · exact (ae_restrict_iff' measurableSet_Ioi).mpr <| univ_mem' fun t ht ↦
        Real.rpow_nonneg (zero_le_one.trans ht.le) _
    _ = ε := by
      rw [integral_Ioi_rpow_of_lt (by rwa [neg_lt_neg_iff]) zero_lt_one, Real.one_rpow]
      field [show -s + 1 ≠ 0 by linarith]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case cons
a : ℤ
n : ℕ
l' : List ℕ
ih : (∀ n ∈ l', n ≠ 0) → J(a | l'.prod) = (List.map (fun n ↦ J(a | n)) l').prod
hl : ∀ n_1 ∈ n :: l', n_1 ≠ 0
hn : n ≠ 0
hl' : l'.prod ≠ 0
h : ∀ m ∈ l', m ≠ 0
⊢ J(a | n) * (List.map (fun n ↦ J(a | n)) l').prod = J(a | n) * (List.map (fun n ↦ J(a | n)) l').prod

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
h : 1 = 0
⊢ False

Tactic:
]

Goal state after:
a : ℤ
h : 1 = 0
⊢ False
Module: Mathlib.RingTheory.Ideal.IsPrincipalPowQuotient

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
x : R
hx✝ : x ∈ I ^ n
hx : ϖ ^ n ∣ x
⊢ ∃ a, g a = ⟨x, hx✝⟩

Tactic:
]

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
I : Ideal R
h : Submodule.IsPrincipal I
h' : I ≠ ⊥
n : ℕ
f : ↥(I ^ n) →ₗ[R] ↥(I ^ n) ⧸ I • ⊤ := (I • ⊤).mkQ
ϖ : R := ⋯.choose
hI : I = span {ϖ}
hϖ : ϖ ^ n ∈ I ^ n
g : R →ₗ[R] ↥(I ^ n) := LinearMap.codRestrict (I ^ n) (LinearMap.mulRight R ϖ ^ n) ⋯
this : I = (f ∘ₗ g).ker
e : (R ⧸ I) ≃ₗ[R] R ⧸ (f ∘ₗ g).ker := Submodule.quotEquivOfEq I (f ∘ₗ g).ker this
x : R
hx✝ : x ∈ I ^ n
hx : ϖ ^ n ∣ x
⊢ ∃ a, g a = ⟨x, hx✝⟩
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
n : ℕ
h : (List.map (fun n ↦ J(a | n)) n.primeFactorsList).prod = -1
hn₀ : n ≠ 0
hf₀ : ∀ p ∈ n.primeFactorsList, p ≠ 0
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1

Tactic:
]

Goal state after:
a : ℤ
n : ℕ
h : (List.map (fun n ↦ J(a | n)) n.primeFactorsList).prod = -1
hn₀ : n ≠ 0
hf₀ : ∀ p ∈ n.primeFactorsList, p ≠ 0
⊢ ∃ p, Nat.Prime p ∧ p ∣ n ∧ J(a | p) = -1
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = r.valMinAbs ^ 2 % ↑b
⊢ False

Tactic:
]

Goal state after:
a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = r.valMinAbs ^ 2 % ↑b
⊢ False
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = r.valMinAbs ^ 2 % ↑b
⊢ 0 ≤ J(r.valMinAbs | b) ^ 2

Tactic:
]

Goal state after:
a : ℤ
b : ℕ
h : J(a | b) = -1
x✝ : IsSquare ↑a
r : ZMod b
ha : a % ↑b = r.valMinAbs ^ 2 % ↑b
⊢ 0 ≤ J(r.valMinAbs | b) ^ 2
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ legendreSym p a = -1 ↔ ¬IsSquare ↑a

Tactic:
]

Goal state after:
a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ legendreSym p a = -1 ↔ ¬IsSquare ↑a
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : J(a | p) = 1
⊢ ¬1 = -1

Tactic:
]

Goal state after:
a : ℤ
p : ℕ
inst✝ : Fact (Nat.Prime p)
h : J(a | p) = 1
⊢ ¬1 = -1
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
⊢ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖ ≤ (s - 1) * s * C + s * ε

Tactic:
]

Goal state after:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
⊢ ‖(↑s - 1) * LSeries f ↑s - ↑s * l‖ ≤ (s - 1) * s * C + s * ε
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
R : Type u_1
inst✝ : Semiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ (List.pmap (fun p pp ↦ legendreSym p a) b.primeFactorsList ⋯).prod =
    (List.pmap (fun a x ↦ (⇑χ ∘ Nat.cast) a) b.primeFactorsList ⋯).prod

Tactic:
]

Goal state after:
a : ℤ
R : Type u_1
inst✝ : Semiring R
χ : R →* ℤ
hp : ∀ (p : ℕ) (pp : Nat.Prime p), p ≠ 2 → legendreSym p a = χ ↑p
b : ℕ
hb : Odd b
⊢ (List.pmap (fun p pp ↦ legendreSym p a) b.primeFactorsList ⋯).prod =
    (List.pmap (fun a x ↦ (⇑χ ∘ Nat.cast) a) b.primeFactorsList ⋯).prod
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a : ℤ
b : ℕ
hb : Odd b
⊢ χ₄ ↑b * J(a | b) = χ₄ ↑b * J(a | b)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha4 : 4 * a % 4 = 0
this : (↑2).gcd ↑b = 1
⊢ J(a | b) = J(a | b)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(a | b) else J(a | b)) = (if b % 8 = 1 ∨ b % 8 = 7 then 1 else -1) * J(a | b)

Tactic:
]

Goal state after:
b : ℕ
hb2 : b % 2 = 1
a : ℤ
ha2 : 2 * a % 2 = 0
⊢ (if b % 8 = 3 ∨ b % 8 = 5 then -J(a | b) else J(a | b)) = (if b % 8 = 1 ∨ b % 8 = 7 then 1 else -1) * J(a | b)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: m n : ℕ
hm : Odd m
hn : Odd n
⊢ J(χ₄ ↑m | n) = χ₄ ↑m ^ (n / 2)

Tactic:
]

Goal state after:
m n : ℕ
hm : Odd m
hn : Odd n
⊢ J(χ₄ ↑m | n) = χ₄ ↑m ^ (n / 2)
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inl
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 1
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case inr
m n : ℕ
hm : Odd m
hn : Odd n
h : m % 4 = 3
⊢ χ₄ ↑n = χ₄ ↑n

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: m n : ℕ
hm : Odd m
hn : Odd n
⊢ 1 = 1

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
⊢ 1 < (↑s).re

Tactic:
]

Goal state after:
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
⊢ 1 < (↑s).re
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: m n : ℕ
hm : Odd m
hn : Odd n
⊢ (-1) ^ (n / 2 * (m / 2)) = (-1) ^ (n / 2 * (m / 2))

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case refine_1
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h' : qrSign m n * x = y
h : y = qrSign m n * x := Eq.symm h'
⊢ x = x

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: case refine_2
m n : ℕ
hm : Odd m
hn : Odd n
x y : ℤ
h : x = qrSign m n * y
⊢ y = y

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun a ↦ { toFun := fun x ↦ qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
⊢ J(↑p | a) = qrSign a p * J(↑a | p)

Tactic:
]

Goal state after:
a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun a ↦ { toFun := fun x ↦ qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
⊢ J(↑p | a) = qrSign a p * J(↑a | p)
Module: Mathlib.NumberTheory.LSeries.SumCoeff

Goal state before:
pp: f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
⊢ 1 = 1

pp: case hb
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
⊢ ↑s - 1 ≠ 0

Tactic:
]

Goal state after:
case hb
f : ℕ → ℂ
l : ℂ
hlim : Tendsto (fun n ↦ (∑ k ∈ Icc 1 n, f k) / ↑n) atTop (𝓝 l)
hfS : ∀ (s : ℝ), 1 < s → LSeriesSummable f ↑s
ε : ℝ
hε : ε > 0
T : ℝ
hT₁ : 1 ≤ T
hT : ∀ (y : ℝ), T ≤ y → ‖∑ k ∈ Icc 1 ⌊y⌋₊, f k - l * ↑y‖ < ε * y
S : ℝ → ℂ := fun t ↦ ∑ k ∈ Icc 1 ⌊t⌋₊, f k
C : ℝ := ∫ (t : ℝ) in Set.Ioc 1 T, ‖S t - l * ↑t‖ * t ^ (-1 - 1)
hC : 0 ≤ C
s : ℝ
hs : 1 < s
hs' : 0 ≤ (s - 1) * s
h₀ : LocallyIntegrableOn (fun t ↦ S t - l * ↑t) (Set.Ici 1) volume
h₁ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-s - 1)) (Set.Ici 1) volume
h₂ : IntegrableOn (fun t ↦ ‖S t - l * ↑t‖ * t ^ (-1 - 1)) (Set.Ioc 1 T) volume
⊢ ↑s - 1 ≠ 0
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a b : ℕ
ha : Odd a
hb : Odd b
rhs : ℕ → ℕ →* ℤ := fun a ↦ { toFun := fun x ↦ qrSign x a * J(↑x | a), map_one' := ⋯, map_mul' := ⋯ }
rhs_apply : ∀ (a b : ℕ), (rhs a) b = qrSign b a * J(↑b | a)
p : ℕ
pp : Nat.Prime p
hp : p ≠ 2
hpo : Odd p
q : ℕ
pq : Nat.Prime q
hq : q ≠ 2
hqo : Odd q
⊢ (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q = (-1) ^ (p / 2 * (q / 2)) * legendreSym p ↑q

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a b : ℕ
ha : Odd a
hb : Odd b
⊢ qrSign b a * J(↑b | a) = qrSign b a * J(↑b | a)

Tactic:
]

Goal state after:
Module: Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol

Goal state before:
pp: a b : ℕ
ha : a % 4 = 1
hb : Odd b
⊢ J(↑b | a) = J(↑b | a)

Tactic:
]

Goal state after: