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

Goal state before:
pp: case ind
a : ℕ
IH :
  ∀ m < a,
    ∀ {b : ℕ} {flip : Bool} {ha0 : m > 0},
      b % 2 = 1 → b > 1 → fastJacobiSymAux m b flip ha0 = if flip = true then -J(↑m | b) else J(↑m | b)
b : ℕ
flip : Bool
ha0 : a > 0
hb2 : b % 2 = 1
hb1 : b > 1
⊢ fastJacobiSymAux a b flip ha0 = if flip = true then -J(↑a | b) else J(↑a | b)

Tactic:
unfold fastJacobiSymAux
  split <;> rename_i ha4
  · rw [IH (a / 4) (a.div_lt_self ha0 (by decide)) hb2 hb1]
    simp only [Int.natCast_ediv, Nat.cast_ofNat, div_four_left (a := a) (mod_cast ha4) hb2]
  split <;> rename_i ha2
  · rw [IH (a / 2) (a.div_lt_self ha0 (by decide)) hb2 hb1]
    simp only [Int.natCast_ediv, Nat.cast_ofNat, ← even_odd (a := a) (mod_cast ha2) hb2]
    by_cases h : b % 8 = 3 ∨ b % 8 = 5 <;> simp [h]; cases flip <;> simp
  split <;> rename_i ha1
  · subst ha1; simp
  split <;> rename_i hba
  · suffices J(a | b) = 0 by simp [this]
    refine eq_zero_iff.mpr ⟨fun h ↦ absurd (h ▸ hb1) (by decide), ?_⟩
    rwa [Int.gcd_natCast_natCast, Nat.gcd_eq_left (Nat.dvd_of_mod_eq_zero hba)]
  rw [IH (b % a) (b.mod_lt ha0) (Nat.mod_two_ne_zero.mp ha2) (lt_of_le_of_ne ha0 (Ne.symm ha1))]
  simp only [Int.natCast_mod, ← mod_left]
  rw [← quadratic_reciprocity_if (Nat.mod_two_ne_zero.mp ha2) hb2]
  by_cases h : a % 4 = 3 ∧ b % 4 = 3 <;> simp [h]; cases flip <;> simp

Goal state after:
Module: Mathlib.Topology.Algebra.Valued.LocallyCompact

Goal state before:
pp: case right
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc✝ : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := ⋯
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
c : K
hc : v c = ↑↑i
hzi : z ≤ i
hi1 : i ≤ 1
j : K
hj : j ∈ t
hj' : c ∈ if v j ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v j}
⊢ (if hi' : v j ≤ ↑↑z then z else Units.mk0 ⟨v j, ⋯⟩ ⋯) = i

Tactic:
split_ifs at hj' with hcj

Goal state after:
case pos
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc✝ : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
c : K
hc : v c = ↑↑i
hzi : z ≤ i
hi1 : i ≤ 1
j : K
hj : j ∈ t
hcj : v j ≤ ↑↑z
hj' : c ∈ {w | v w ≤ ↑↑z}
⊢ (if hi' : v j ≤ ↑↑z then z else Units.mk0 ⟨v j, ⋯⟩ ⋯) = i

case neg
K : Type u_1
Γ₀ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ₀
inst✝ : Valued K Γ₀
hc✝ : IsCompact ↑𝒪[K]
z : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
a : K
ha : (MonoidWithZeroHom.ofClass v) a = ↑↑z
hz1 : z ≤ 1
z0' : 0 < ↑z
z0 : 0 < ↑↑z
a0 : 0 < v a
U : K → Set K := fun y ↦ if v y ≤ ↑↑z then {w | v w ≤ ↑↑z} else {w | v w = v y}
t : Finset K
ht : ↑𝒪[K] ⊆ ⋃ i ∈ t, U i
i : (↥(MonoidHom.mrange (MonoidWithZeroHom.ofClass v)))ˣ
c : K
hc : v c = ↑↑i
hzi : z ≤ i
hi1 : i ≤ 1
j : K
hj : j ∈ t
hcj : ¬v j ≤ ↑↑z
hj' : c ∈ {w | v w = v j}
⊢ (if hi' : v j ≤ ↑↑z then z else Units.mk0 ⟨v j, ⋯⟩ ⋯) = i
Module: Mathlib.RingTheory.SimpleRing.Field

Goal state before:
pp: A : Type u_1
inst✝¹ : Ring A
inst✝ : IsSimpleRing A
⊢ ∀ {a : ↥(Subring.center A)}, a ≠ 0 → ∃ b, a * b = 1

Tactic:
by
    rintro ⟨x, hx1⟩ hx2
    rw [Subring.mem_center_iff] at hx1
    replace hx2 : x ≠ 0 := by simpa [Subtype.ext_iff] using hx2
    -- Todo: golf the following `let` once `TwoSidedIdeal.span` is defined
    let I := TwoSidedIdeal.mk' (Set.range (x * ·)) ⟨0, by simp⟩
      (by rintro _ _ ⟨x, rfl⟩ ⟨y, rfl⟩; exact ⟨x + y, mul_add _ _ _⟩)
      (by rintro _ ⟨x, rfl⟩; exact ⟨-x, by simp⟩)
      (by rintro a _ ⟨c, rfl⟩; exact ⟨a * c, by dsimp; rw [← mul_assoc, ← hx1, mul_assoc]⟩)
      (by rintro _ b ⟨a, rfl⟩; exact ⟨a * b, by dsimp; rw [← mul_assoc, ← hx1, mul_assoc]⟩)
    have mem : 1 ∈ I := one_mem_of_ne_zero_mem I hx2 (by simpa [I, mem_mk'] using ⟨1, by simp⟩)
    simp only [TwoSidedIdeal.mem_mk', Set.mem_range, I] at mem
    obtain ⟨y, hy⟩ := mem
    refine ⟨⟨y, Subring.mem_center_iff.2 fun a ↦ ?_⟩, by ext; exact hy⟩
    calc a * y
      _ = (x * y) * a * y := by rw [hy, one_mul]
      _ = (y * x) * a * y := by rw [hx1]
      _ = y * (x * a) * y := by rw [mul_assoc y x a]
      _ = y * (a * x) * y := by rw [hx1]
      _ = y * ((a * x) * y) := by rw [mul_assoc]
      _ = y * (a * (x * y)) := by rw [mul_assoc a x y]
      _ = y * a := by rw [hy, mul_one]

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime (mersenne p))
hp : 3 ≤ p
⊢ legendreSym (mersenne p) 2 = 1

Tactic:
have := mersenne_mod_eight hp
  rw [legendreSym.at_two (by lia), ZMod.χ₈_nat_eq_if_mod_eight]
  lia

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: N : ℕ
inst✝ : NeZero N
A : SL(2, ℤ)
hA : A ∈ Γ(N)
⊢ A ∈ Gamma1 N

Tactic:
simp_all [Gamma1_mem, Gamma_mem]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: g : ConjAct SL(2, ℤ)
Γ : Subgroup SL(2, ℤ)
h : IsCongruenceSubgroup Γ
⊢ IsCongruenceSubgroup (g • Γ)

Tactic:
obtain ⟨N, HN⟩ := h
  refine ⟨N, ?_⟩
  rw [← Gamma_cong_eq_self N g, Subgroup.pointwise_smul_le_pointwise_smul_iff]
  exact HN

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.SlashActions

Goal state before:
pp: k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
τ : ℍ
⊢ (σ B) ((σ A) (f (A • B • τ))) *
        (↑|↑(Matrix.GeneralLinearGroup.det A)| ^ (k - 1) * ↑|↑(Matrix.GeneralLinearGroup.det B)| ^ (k - 1)) *
      ((σ B) (denom A ↑(B • τ)) ^ (-k) * denom B ↑τ ^ (-k)) =
    (σ B) ((σ A) (f (A • B • τ))) * (σ B) ↑|↑(Matrix.GeneralLinearGroup.det A)| ^ (k - 1) *
          (σ B) (denom A ↑(B • τ)) ^ (-k) *
        ↑|↑(Matrix.GeneralLinearGroup.det B)| ^ (k - 1) *
      denom B ↑τ ^ (-k)

Tactic:
σ_ofReal

Goal state after:
k : ℤ
A B : GL (Fin 2) ℝ
f : ℍ → ℂ
τ : ℍ
⊢ (σ B) ((σ A) (f (A • B • τ))) *
        (↑|↑(Matrix.GeneralLinearGroup.det A)| ^ (k - 1) * ↑|↑(Matrix.GeneralLinearGroup.det B)| ^ (k - 1)) *
      ((σ B) (denom A ↑(B • τ)) ^ (-k) * denom B ↑τ ^ (-k)) =
    (σ B) ((σ A) (f (A • B • τ))) * ↑|↑(Matrix.GeneralLinearGroup.det A)| ^ (k - 1) * (σ B) (denom A ↑(B • τ)) ^ (-k) *
        ↑|↑(Matrix.GeneralLinearGroup.det B)| ^ (k - 1) *
      denom B ↑τ ^ (-k)
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: k : ℤ
f f' : ℍ → ℂ
hf : Continuous f
hf' : Continuous f'
⊢ Continuous (petersson k f f')

Tactic:
unfold petersson

Goal state after:
k : ℤ
f f' : ℍ → ℂ
hf : Continuous f
hf' : Continuous f'
⊢ Continuous fun τ ↦ (starRingEnd ℂ) (f τ) * f' τ * ↑τ.im ^ k
Module: Mathlib.NumberTheory.ModularForms.QExpansion

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfper : Periodic (f ∘ ↑ofComplex) ↑h
hfhol : MDiff f
hfbdd : IsBoundedAtImInfty f
n : ℕ
R : ℝ
hR : 0 < R
hR' : R < 1
this :
  (∮ (z : ℂ) in C(0, R), (1 / (z - 0) ^ (n + 1)) • cuspFunction h f z) / (2 * ↑π * Complex.I) =
    (↑n.factorial)⁻¹ * iteratedDeriv n (cuspFunction h f) 0
⊢ (PowerSeries.coeff n) (qExpansion h f) =
    (2 * ↑π * Complex.I)⁻¹ * ∮ (z : ℂ) in C(0, R), cuspFunction h f z / z ^ (n + 1)

Tactic:
simp_rw [qExpansion, PowerSeries.coeff_mk, ← this, sub_zero, smul_eq_mul, one_div_mul_eq_div,
    div_eq_inv_mul]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
⊢ v = r • divIntMap (↑r) v

Tactic:
by_cases hr : r = 0

Goal state after:
case pos
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hr : r = 0
⊢ v = r • divIntMap (↑r) v

case neg
r : ℕ
v : Fin 2 → ℤ
hv : v ∈ gammaSet 1 r 0
hr : ¬r = 0
⊢ v = r • divIntMap (↑r) v
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: r : ℕ
inst✝ : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
i : Fin 2
⊢ v i = (r • (v / ↑r)) i

Tactic:
refine Eq.symm (Int.mul_ediv_cancel' ?_)

Goal state after:
r : ℕ
inst✝ : NeZero r
v : Fin 2 → ℤ
hab : finGcdMap v = r
A : SL(2, ℤ)
i : Fin 2
⊢ ↑r ∣ v i
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: N r : ℕ
a : Fin 2 → ZMod N
inst✝ : NeZero r
v : Fin 2 → ℤ
hv : v ∈ gammaSet N r a
γ : SL(2, ℤ)
this :
  ∀ (i : Fin 2),
    (Int.castRingHom (ZMod N)) ((v ᵥ* ↑γ) i) =
      (⇑(Int.castRingHom (ZMod N)) ∘ v ᵥ* (↑γ).map ⇑(Int.castRingHom (ZMod N))) i
⊢ Int.cast ∘ (v ᵥ* ↑γ) = a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)

Tactic:
simp only [eq_intCast, Int.coe_castRingHom] at this

Goal state after:
N r : ℕ
a : Fin 2 → ZMod N
inst✝ : NeZero r
v : Fin 2 → ℤ
hv : v ∈ gammaSet N r a
γ : SL(2, ℤ)
this : ∀ (i : Fin 2), ↑((v ᵥ* ↑γ) i) = ((fun x ↦ ↑x) ∘ v ᵥ* (↑γ).map fun x ↦ ↑x) i
⊢ Int.cast ∘ (v ᵥ* ↑γ) = a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
⊢ |↑n| < 1

Tactic:
have h₁ := hz.2

Goal state after:
z : ℍ
n : ℤ
hz : z ∈ 𝒟ᵒ
hg : T ^ n • z ∈ 𝒟ᵒ
h₁ : |z.re| < 1 / 2
⊢ |↑n| < 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case e_f
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
a : ℤ
⊢ e2Summand a z =
    ∑' (n : ℤ), G2Term z ![a, n] + ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑a * ↑z + ↑n) - 1 / (↑a * ↑z + ↑n + 1))

Tactic:
rw [e2Summand, tsum_eq_of_summable_unconditional
        (summable_right_one_div_linear_sub_one_div_linear_succ z a), ← Summable.tsum_add
        ((G2Term_prod_summable z).prod_factor _)
        (summable_right_one_div_linear_sub_one_div_linear_succ z a)]

Goal state after:
case e_f
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
a : ℤ
⊢ ∑' (n : ℤ), eisSummand 2 ![a, n] z =
    ∑' (b : ℤ), (G2Term z ![(a, b).1, (a, b).2] + (1 / (↑a * ↑z + ↑b) - 1 / (↑a * ↑z + ↑b + 1)))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: case h₂
z : ℍ
⊢ ∀ (c : ℤ), Summable fun b ↦ G2Term z ![b, c]

Tactic:
have H := G2Term_summable z

Goal state after:
case h₂
z : ℍ
H : Summable (G2Term z)
⊢ ∀ (c : ℤ), Summable fun b ↦ G2Term z ![b, c]
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
this : ∀ {g : SL(2, ℤ)} {z : ℍ}, z ∈ 𝒟 → g • z ∈ 𝒟 → z.im ≤ (g • z).im → (g • z).im = z.im
hden : ¬z.im ≤ (g • z).im
⊢ (g • z).im ≤ (g⁻¹ • g • z).im

Tactic:
by simpa using le_of_not_ge hden

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula

Goal state before:
pp: f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
⊢ c4 • qExpansion 1 ⇑E₄ = qExpansion 1 ⇑(f.mul f)

Tactic:
← ModularForm.qExpansion_smul one_pos one_mem_strictPeriods_SL c4 E₄,

Goal state after:
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 2
c4 : ℂ
hc4 : c4 • E₄ = f.mul f
c6 : ℂ
hc6 : c6 • E₆ = (f.mul f).mul f
⊢ qExpansion 1 (c4 • ⇑E₄) = qExpansion 1 ⇑(f.mul f)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟
⊢ g = 1 ∨ g = -1

Tactic:
have : ρ ∉ 𝒟ᵒ := by
    intro h
    grind [norm_ρ, one_lt_normSq_iff.mp h.1]

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟ᵒ
hg : g • z ∈ 𝒟
this : ρ ∉ 𝒟ᵒ
⊢ g = 1 ∨ g = -1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
⊢ Tendsto (fun n ↦ 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑n / ↑z - ↑↑m) + 1 / (-↑n / ↑z + ↑↑m))) atTop (𝓝 (-2 * ↑π * I / ↑z))

Tactic:
by
  rw [← PNat.tendsto_comp_val_iff]
  have H0 : (fun n : ℕ+ ↦ (2 / z * ∑' (m : ℕ+), (1 / (-(n : ℂ) / z - m) + 1 / (-n / z + m)))) =
      (fun n : ℕ+ ↦ (-2 * π * I / z) - (2 / z * (2 * π * I)) *
      (∑' m : ℕ+, cexp (2 * π * I * (-n / z)) ^ (m : ℕ)) + 2 / n) := by
    ext N
    have h2 := cot_series_rep <| coe_mem_integerComplement ⟨-N / z, im_pnat_div_pos N z⟩
    rw [pi_mul_cot_pi_q_exp, ← sub_eq_iff_eq_add', one_div, inv_div, neg_mul, ← h2,
      ← tsum_zero_pnat_eq_tsum_nat
      (by simpa using norm_exp_two_pi_I_lt_one ⟨-N / z, im_pnat_div_pos N z⟩)] at *
    field [ne_zero z]
  rw [H0]
  nth_rw 2 [show -2 * π * I / z = (-2 * π * I / z) - (2 / z * (2 * π * I)) * 0 + 2 * 0 by ring]
  refine aux_tendsto_tsum_cexp_pnat z |>.const_mul _ |>.const_sub _ |>.add (.const_mul _ ?_)
  exact PNat.tendsto_comp_val_iff.mpr tendsto_inv_atTop_nhds_zero_nat

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing

Goal state before:
pp: z : ℍ
g : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12
hg : CuspForm.toModularFormₗ g = E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : ⇑g = ⇑E₄CubeSubE₆SqForm
hc_eq : c = 1728
⊢ E₄CubeSubE₆SqForm z = E₄ z ^ 3 - E₆ z ^ 2

Tactic:
E₄CubeSubE₆SqForm_apply

Goal state after:
z : ℍ
g : CuspForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 12
hg : CuspForm.toModularFormₗ g = E₄CubeSubE₆SqForm
c : ℂ
hc : c • CuspForm.discriminant = g
hgE : ⇑g = ⇑E₄CubeSubE₆SqForm
hc_eq : c = 1728
⊢ E₄ z ^ 3 - E₆ z ^ 2 = E₄ z ^ 3 - E₆ z ^ 2
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
p x : R
n y : ℕ
hy : y ∈ range n
⊢ p ^ 2 ∣ x ^ y * p ^ (n + 1 - y) * ↑((n + 1).choose y)

Tactic:
calc
      p ^ 2 ∣ p ^ (n + 1 - y) :=
        pow_dvd_pow p (le_tsub_of_add_le_left (by linarith [Finset.mem_range.mp hy]))
      _ ∣ x ^ y * p ^ (n + 1 - y) * ↑((n + 1).choose y) :=
        dvd_mul_of_dvd_left (dvd_mul_left _ _) _

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝ : CommRing R
a b : R
p : ℕ
hp : Odd p
h1 :
  ∀ (i : ℕ),
    (Ideal.Quotient.mk (span {↑p ^ 2})) ((a + ↑p * b) ^ i) =
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (i - 1) * (↑p * b) * ↑i + a ^ i)
s : R := ↑p ^ 2
⊢ ∑ x ∈ range p,
      (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (x - 1) * (↑p * b) * ↑x + a ^ x) *
        (Ideal.Quotient.mk (span {↑p ^ 2})) (a ^ (p - 1 - x)) =
    ∑ x ∈ range p, (Ideal.Quotient.mk (span {↑p ^ 2})) ((a ^ (x - 1) * (↑p * b) * ↑x + a ^ x) * a ^ (p - 1 - x))

Tactic:
← map_mul

Goal state after:
Module: Mathlib.NumberTheory.NumberField.InfiniteAdeleRing

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
⊢ ‖(algebraMap K K∞) x‖ = ↑|(Algebra.norm ℚ) x|

Tactic:
simpa [-Rat.cast_abs, norm_def] using! InfinitePlace.prod_eq_abs_norm x

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
R : Type u_1
inst✝ : CommRing R
x y : R
d : ℕ
hd : x ^ 2 ^ d - y ^ 2 ^ d = (∏ i ∈ range d, (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)
⊢ x ^ 2 ^ (d + 1) - y ^ 2 ^ (d + 1) = (∏ i ∈ range (d + 1), (x ^ 2 ^ i + y ^ 2 ^ i)) * (x - y)

Tactic:
| succ d hd =>

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ padicValNat 2 ((x + 1) * (x - 1)) ≥ 3

Tactic:
refine (padicValNat_dvd_iff_le (by grind [mul_ne_zero])).mp ?_

Goal state after:
n x : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ 2 ^ 3 ∣ (x + 1) * (x - 1)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : NumberField K
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : mixedSpace K → E
⊢ ∫ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ((homeoRealMixedSpacePolarSpace K) x).1 ↑w) •
        f (↑(polarSpaceCoord K).symm ((homeoRealMixedSpacePolarSpace K) x)) ∂volume =
    ∫ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, (x.2 w).1) • f (↑(mixedEmbedding.polarCoord K).symm x)

Tactic:
simp_rw [polarSpaceCoord_symm_apply, mixedEmbedding.polarCoord_symm_apply,
    homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal,
    homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex, homeoRealMixedSpacePolarSpace_apply_snd]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
f : mixedSpace K → ℝ≥0∞
⊢ ∫⁻ (a : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ENNReal.ofReal (((homeoRealMixedSpacePolarSpace K) a).1 ↑w)) *
        f (↑(polarSpaceCoord K).symm ((homeoRealMixedSpacePolarSpace K) a)) ∂volume =
    ∫⁻ (x : realMixedSpace K) in Set.univ ×ˢ Set.univ.pi fun i ↦ Complex.polarCoord.target,
      (∏ w, ENNReal.ofReal (x.2 w).1) * f (↑(mixedEmbedding.polarCoord K).symm x)

Tactic:
simp_rw [polarSpaceCoord_symm_apply, mixedEmbedding.polarCoord_symm_apply,
    homeoRealMixedSpacePolarSpace_apply_fst_ofIsReal,
    homeoRealMixedSpacePolarSpace_apply_fst_ofIsComplex, homeoRealMixedSpacePolarSpace_apply_snd]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : x ∈ fundamentalCone K
u : (𝓞 K)ˣ
⊢ u • x ∈ fundamentalCone K ↔ u ∈ torsion K

Tactic:
by
  classical
  refine ⟨fun h ↦ ?_, fun h ↦ torsion_smul_mem_of_mem hx h⟩
  rw [← logEmbedding_eq_zero_iff]
  let B := (basisUnitLattice K).ofZLatticeBasis ℝ
  refine (Subtype.mk_eq_mk (h := ?_) (h' := Submodule.zero_mem _)).mp <|
    (ZSpan.exist_unique_vadd_mem_fundamentalDomain B (logMap x)).unique ?_ ?_
  · rw [Module.Basis.ofZLatticeBasis_span ℝ (unitLattice K)]
    exact ⟨u, trivial, rfl⟩
  · rw [AddSubmonoid.mk_vadd, vadd_eq_add, ← logMap_unit_smul _ hx.2]
    exact h.1
  · rw [AddSubmonoid.mk_vadd, vadd_eq_add, zero_add]
    exact hx.1

Goal state after:
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : (𝓞 K)ˣ
x : 𝓞 K
hx : mixedEmbedding.norm ((mixedEmbedding K) ((algebraMap (𝓞 K) K) x)) ≠ 0
hu : u • (mixedEmbedding K) ((algebraMap (𝓞 K) K) x) ∈ fundamentalCone K
⊢ (mixedEmbedding K) ↑(↑u * x) =
    (mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑u) * (mixedEmbedding K) ((algebraMap (𝓞 K) K) x)

Tactic:
← map_mul

Goal state after:
Module: Mathlib.NumberTheory.NumberField.DirichletDensity

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
δ : ℝ
h : HasDirichletDensity S δ
s : ℝ
⊢ primeIdealZetaSum S s / primeIdealZetaSum univ s ≤ 1

Tactic:
rw [primeIdealZetaSum_def, primeIdealZetaSum_def,
    tsum_univ fun 𝔭 : HeightOneSpectrum (𝓞 K) ↦ (𝔭.asIdeal.absNorm : ℝ) ^ (-s)]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
S : Set (HeightOneSpectrum (𝓞 K))
δ : ℝ
h : HasDirichletDensity S δ
s : ℝ
⊢ (∑' (𝔭 : ↑S), ↑(Ideal.absNorm (↑𝔭).asIdeal) ^ (-s)) /
      ∑' (x : HeightOneSpectrum (𝓞 K)), ↑(Ideal.absNorm x.asIdeal) ^ (-s) ≤
    1
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: T : Type u_1
F : Type u_2
inst✝ : DivisionRing F
l : List T
y : F
hy : y ≠ 1
⊢ (List.mapIdx (fun i x ↦ y ^ i) l).sum = (y ^ l.length - 1) / (y - 1)

Tactic:
rw [← geom_sum_eq hy l.length, List.mapIdx_eq_zipIdx_map, Finset.sum_range,
    ← Fin.sum_univ_fun_getElem]
  simp only
  let e : Fin l.zipIdx.length ≃ Fin l.length := finCongr List.length_zipIdx
  exact Fintype.sum_bijective e e.bijective _ _ fun _ ↦ by simp [e]

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
⊢ ↑(#S) = ∏ i, (P i - N i + 1)

Tactic:
by
  rw [Pi.card_Icc N P, Nat.cast_prod]
  congr
  ext i
  rw [Int.card_Icc_of_le (N i) (P i) (N_le_P_add_one A i)]
  exact add_sub_right_comm (P i) 1 (N i)

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion

Goal state before:
pp: case mp
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformAddGroup α
f : β → α
a : α
ha : HasSum f a
⊢ (CauchySeq fun s ↦ ∑ b ∈ s, f b) ∧ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl

Tactic:
exact ⟨ha.cauchySeq, ((summable_iff_summable_compl_and_tsum_mem f).mp ⟨a, ha⟩).2⟩

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
⊢ ∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑n * max 1 ‖A‖) ^ e

Tactic:
rcases Finset.exists_ne_map_eq_of_card_lt_of_maps_to
    (card_S_lt_card_T A hn hm) (image_T_subset_S A)
    with ⟨x, hxT, y, hyT, hneq, hfeq⟩

Goal state after:
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
⊢ ∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑n * max 1 ‖A‖) ^ e
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case right
α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : 0 ≤ x ∧ x ≤ B'
y : β → ℤ
hyT : 0 ≤ y ∧ y ≤ B'
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
n_mul_norm_A_pow_e_nonneg : 0 ≤ (↑n * max 1 ‖A‖) ^ e
i : β
j : Unit
⊢ x i - y i ≤ ↑⌊(↑n * max 1 ‖A‖) ^ ↑(Rat.divInt (↑m) (subNatNat n m))⌋₊

Tactic:
· simp only [tsub_le_iff_right]
    apply le_trans (hxT.2 i)
    norm_cast
    simp only [le_add_iff_nonneg_right]
    exact hyT.1 i

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
⊢ ∃ t, t ≠ 0 ∧ A *ᵥ t = 0 ∧ ‖t‖ ≤ (↑n * max 1 ‖A‖) ^ e

Tactic:
by
  classical
  -- Pigeonhole
  rcases Finset.exists_ne_map_eq_of_card_lt_of_maps_to
    (card_S_lt_card_T A hn hm) (image_T_subset_S A)
    with ⟨x, hxT, y, hyT, hneq, hfeq⟩
  -- Proofs that x - y ≠ 0 and x - y is a solution
  refine ⟨x - y, sub_ne_zero.mpr hneq, by simp only [mulVec_sub, sub_eq_zero, hfeq], ?_⟩
  -- Inequality
  have n_mul_norm_A_pow_e_nonneg : 0 ≤ (n * max 1 ‖A‖) ^ e := by positivity
  rw [← norm_replicateCol (ι := Unit), norm_le_iff n_mul_norm_A_pow_e_nonneg]
  intro i j
  simp only [replicateCol_apply, Pi.sub_apply]
  rw [Int.norm_eq_abs, ← Int.cast_abs]
  refine le_trans ?_ (Nat.floor_le n_mul_norm_A_pow_e_nonneg)
  norm_cast
  rw [abs_le]
  rw [Finset.mem_Icc] at hxT hyT
  constructor
  · simp only [neg_le_sub_iff_le_add]
    apply le_trans (hyT.2 i)
    norm_cast
    simp only [le_add_iff_nonneg_left]
    exact hxT.1 i
  · simp only [tsub_le_iff_right]
    apply le_trans (hxT.2 i)
    norm_cast
    simp only [le_add_iff_nonneg_right]
    exact hyT.1 i

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
k : ℕ
hk : k ≠ 0
h_ineq1 : ∀ {m n : ℕ}, 1 < m → 1 < n → f ↑n ≤ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ logb ↑m ↑n
he : 0 < ↑m * f ↑m / (f ↑m - 1)
⊢ f ↑n ^ k ≤ (↑m * f ↑m / (f ↑m - 1)) ^ ((↑k)⁻¹ * ↑k) * f ↑m ^ (logb ↑m ↑n * ↑k)

Tactic:
inv_mul_cancel₀ (mod_cast hk),

Goal state after:
f : AbsoluteValue ℚ ℝ
m n : ℕ
hm : 1 < m
hn : 1 < n
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
k : ℕ
hk : k ≠ 0
h_ineq1 : ∀ {m n : ℕ}, 1 < m → 1 < n → f ↑n ≤ ↑m * f ↑m / (f ↑m - 1) * f ↑m ^ logb ↑m ↑n
he : 0 < ↑m * f ↑m / (f ↑m - 1)
⊢ f ↑n ^ k ≤ (↑m * f ↑m / (f ↑m - 1)) ^ 1 * f ↑m ^ (logb ↑m ↑n * ↑k)