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

Goal state before:
pp: n : ℕ
B : ℝ≥0
⊢ {p |
        p.natDegree ≤ n ∧
          ∀ (i : Fin (n + 1)), -(↑(n.choose ↑i) * ↑B) ≤ ↑(p.coeff ↑i) ∧ ↑(p.coeff ↑i) ≤ ↑(n.choose ↑i) * ↑B}.ncard =
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)

Tactic:
← boxPoly,

Goal state after:
n : ℕ
B : ℝ≥0
⊢ (boxPoly n (fun i ↦ -(↑(n.choose ↑i) * ↑B)) fun i ↦ ↑(n.choose ↑i) * ↑B).ncard = ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
Module: Mathlib.NumberTheory.MahlerMeasure

Goal state before:
pp: n : ℕ
B : ℝ≥0
h_card :
  {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.ncard =
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
h_subset :
  {p | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B} ⊆
    {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}
⊢ ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1) ≠ 0

Tactic:
Finset.prod_ne_zero_iff

Goal state after:
n : ℕ
B : ℝ≥0
h_card :
  {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}.ncard =
    ∏ i, (2 * ⌊↑(n.choose ↑i) * B⌋₊ + 1)
h_subset :
  {p | p.natDegree ≤ n ∧ (map (castRingHom ℂ) p).mahlerMeasure ≤ ↑B} ⊆
    {p | p.natDegree ≤ n ∧ ∀ (i : Fin (n + 1)), ‖p.coeff ↑i‖ ≤ ↑(n.choose ↑i) * ↑B}
⊢ ∀ a ∈ Finset.univ, 2 * ⌊↑(n.choose ↑a) * B⌋₊ + 1 ≠ 0
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: p : ℕ
hp : Nat.blt 1 p = true
h : Nat.ble 1 (sModNatTR (2 ^ p - 1) (p - 2)) = true
⊢ ¬LucasLehmerTest p

Tactic:
by
  rw [Nat.blt_eq] at hp
  rw [Nat.ble_eq, Nat.succ_le_iff, Nat.pos_iff_ne_zero] at h
  rw [LucasLehmerTest, LucasLehmer.residue_eq_zero_iff_sMod_eq_zero p hp, ← sModNat_eq_sMod p _ hp,
    ← sModNatTR_eq_sModNat]
  simpa using h

Goal state after:
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: n k : ℕ
⊢ 1 * (k / 2 ^ n) + k % 2 ^ n = k / 2 ^ n + k % 2 ^ n

Tactic:
by rw [one_mul]

Goal state after:
Module: Mathlib.Topology.Compactification.OnePoint.ProjectiveLine

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
c : K
g : GL (Fin 2) K
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔
    (if ↑g 1 0 * c + ↑g 1 1 = 0 then ∞ else ↑((↑g 0 0 * c + ↑g 0 1) / (↑g 1 0 * c + ↑g 1 1))) = ↑c

Tactic:
split_ifs with h

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
c : K
g : GL (Fin 2) K
h : ↑g 1 0 * c + ↑g 1 1 = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ∞ = ↑c

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : DecidableEq K
c : K
g : GL (Fin 2) K
h : ¬↑g 1 0 * c + ↑g 1 1 = 0
⊢ ↑g 1 0 * c ^ 2 + (↑g 1 1 - ↑g 0 0) * c - ↑g 0 1 = 0 ↔ ↑((↑g 0 0 * c + ↑g 0 1) / (↑g 1 0 * c + ↑g 1 1)) = ↑c
Module: Mathlib.NumberTheory.ModularForms.BoundedAtCusp

Goal state before:
pp: c : OnePoint ℝ
f : ℍ → ℂ
k : ℤ
g : GL (Fin 2) ℝ
⊢ (g • c).IsBoundedAt f k ↔ c.IsBoundedAt (f ∣[k] g) k

Tactic:
rw [IsBoundedAt, IsBoundedAt, (Equiv.mulLeft g⁻¹).forall_congr_left]
  simp [mul_smul, ← SlashAction.slash_mul]

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

Goal state before:
pp: h : ℝ
f : ℍ → ℂ
hh : 0 < h
hfanalytic : AnalyticAt ℂ (cuspFunction h f) 0
hfper : Periodic (f ∘ ↑ofComplex) ↑h
⊢ (PowerSeries.coeff 0) (qExpansion h f) = valueAtInfty f

Tactic:
by
  simp [qExpansion_coeff, cuspFunction_apply_zero hh hfanalytic hfper]

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

Goal state before:
pp: F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
m : ℕ
⊢ ‖FormalMultilinearSeries.ofScalars ℂ (fun m ↦ (PowerSeries.coeff m) (qExpansion h ⇑f)) m‖ =
    ‖(PowerSeries.coeff m) (qExpansion h ⇑f)‖

Tactic:
← (ContinuousMultilinearMap.piFieldEquiv ℂ (Fin m) ℂ).symm.norm_map

Goal state after:
F : Type u_1
inst✝ : FunLike F ℍ ℂ
h : ℝ
f : F
m : ℕ
⊢ ‖(ContinuousMultilinearMap.piFieldEquiv ℂ (Fin m) ℂ).symm
        (FormalMultilinearSeries.ofScalars ℂ (fun m ↦ (PowerSeries.coeff m) (qExpansion h ⇑f)) m)‖ =
    ‖(PowerSeries.coeff m) (qExpansion h ⇑f)‖
Module: Mathlib.NumberTheory.ModularForms.Petersson

Goal state before:
pp: case right
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
⊢ (fun x ↦ ‖f' x‖ * ‖f x‖ * ‖↑x.im ^ k‖) =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)

Tactic:
norm_zpow,

Goal state after:
case right
F : Type u_1
F' : Type u_2
inst✝⁶ : FunLike F ℍ ℂ
inst✝⁵ : FunLike F' ℍ ℂ
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Fact (IsCusp OnePoint.infty Γ)
inst✝³ : Γ.HasDetPlusMinusOne
inst✝² : DiscreteTopology ↥Γ
inst✝¹ : ModularFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
f : F
h_bd : IsZeroAtImInfty ⇑f
f' : F'
b : ℝ
hb : b > 0
hbf : ⇑f =O[atImInfty] fun τ ↦ Real.exp (-b * τ.im)
a : ℝ
ha : 0 < a
ha' : a < b
⊢ (fun x ↦ ‖f' x‖ * ‖f x‖ * ‖↑x.im‖ ^ k) =O[atImInfty] fun τ ↦ Real.exp (-a * τ.im)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: N r : ℕ
a : Fin 2 → ZMod N
⊢ (y : ℕ) × { x // finGcdMap x = y } ≃ (r : ℕ) × ↑(gammaSet 1 r 0)

Tactic:
refine Equiv.sigmaCongrRight fun b => ?_

Goal state after:
N r : ℕ
a : Fin 2 → ZMod N
b : ℕ
⊢ { x // finGcdMap x = b } ≃ ↑(gammaSet 1 b 0)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case left
⊢ 1 ≤ normSq ↑ρ

Tactic:
norm_num [ρ, ← pow_two, div_pow]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right
⊢ |ρ.re| ≤ 1 / 2

Tactic:
norm_num [ρ, ← pow_two, div_pow]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
⊢ c ≠ 0 → 9 * c ^ 4 ≤ 16

Tactic:
intro hc

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
c' : ℤ := ↑g 1 0
c : ℝ := ↑c'
hc : c ≠ 0
⊢ 9 * c ^ 4 ≤ 16
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ ↑g 0 0 * S
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
have hSre : re (S • z) = -z.re := by
    rw [modular_S_smul, ← coe_re, coe_mk, inv_re, normSq_eq_norm_sq, norm_neg, hz', one_pow,
      div_one, neg_re, coe_re]

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : T ^ ↑g 0 0 • S • z ∈ 𝒟
hg'✝ : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 0
hb : ↑g 0 1 = -1
hz' : ‖↑z‖ = 1
hg' : g = T ^ ↑g 0 0 * S
hSre : (S • z).re = -z.re
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.ModularForms.CuspFormSubmodule

Goal state before:
pp: k : ℤ
f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range k
h : (PowerSeries.coeff 0) (qExpansion 1 ⇑f) = 0
c : OnePoint ℝ
hc : IsCusp c (Matrix.SpecialLinearGroup.mapGL ℝ).range
⊢ c.IsZeroAt (⇑f) k

Tactic:
rw [Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z] at hc
  rw [isZeroAt_iff_forall_SL2Z hc]
  intro γ _
  rw [show (⇑f ∣[k] γ) = ⇑f from f.slash_action_eq' _ ⟨γ, rfl⟩]
  exact isZeroAtImInfty_of_valueAtInfty_eq_zero f <| by
    rwa [← qExpansion_coeff_zero one_pos
      (ModularFormClass.analyticAt_cuspFunction_zero f one_pos one_mem_strictPeriods_SL)
      (periodic_comp_ofComplex f one_mem_strictPeriods_SL)]

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

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormSMulClass ℤ F
f : ℤ → F
hf : Summable f (symmetricIcc ℤ)
hs : Function.Even f
⊢ Tendsto f atTop (𝓝 0)

Tactic:
rw [tendsto_zero_iff_norm_tendsto_zero]
  obtain ⟨L, hL⟩ := hf
  rw [HasSum, symmetricIcc_filter, tendsto_map'_iff, Function.comp_def] at hL
  have := hL.sub (hL.comp (tendsto_atTop_add_const_right _ (-1) tendsto_id))
  simp only [id_eq, Int.reduceNeg, Function.comp_apply, sub_self, ← sub_eq_add_neg] at this
  rw [tendsto_zero_iff_norm_tendsto_zero] at this
  refine (mul_zero (_ : ℝ) ▸ this.const_mul 2⁻¹).congr' ?_
  filter_upwards [eventually_ge_atTop 1] with x hx
  have : Finset.Icc (-x) x = Icc (-(x - 1)) (x - 1) ∪ {-x, x} := by
    lift x to ℕ using by positivity
    convert! Finset.Icc_succ_succ (x - 1) (x - 1) <;> grind
  rw [this, Finset.sum_union, Finset.sum_insert, Finset.sum_singleton,
    hs x, add_comm, add_sub_cancel_right, ← two_zsmul, norm_smul, Int.norm_eq_abs,
    Int.cast_two, abs_two, inv_mul_cancel_left₀ two_ne_zero] <;>
  · simp only [disjoint_iff_ne, mem_insert, mem_singleton, mem_Icc]
    omega

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g = !![1, ↑g 0 0; 0, 1] * !![0, -1; 1, 0] * !![1, 1; 0, 1]

Tactic:
mul_fin_two,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = 1
⊢ ↑g = !![1 * 0 + ↑g 0 0 * 1, 1 * -1 + ↑g 0 0 * 0; 0 * 0 + 1 * 1, 0 * -1 + 1 * 0] * !![1, 1; 0, 1]
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
⊢ ↑g = !![1, ↑g 0 0; 0, 1] * !![0, -1; 1, 0] * !![1, -1; 0, 1]

Tactic:
mul_fin_two,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
hd : ↑g 1 1 = -1
this : ↑g 0 1 = -↑g 0 0 - 1
⊢ ↑g = !![1 * 0 + ↑g 0 0 * 1, 1 * -1 + ↑g 0 0 * 0; 0 * 0 + 1 * 1, 0 * -1 + 1 * 0] * !![1, -1; 0, 1]
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: c : ℂ
F : ℍ → ℂ
hF : MDiff F
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
⊢ D (c • F) z = (c • D F) z

Tactic:
simp only [normalizedDerivOfComplex, Pi.smul_apply, smul_eq_mul]

Goal state after:
c : ℂ
F : ℍ → ℂ
hF : MDiff F
z : ℍ
hFz : DifferentiableAt ℂ (F ∘ ↑ofComplex) ↑z
⊢ (2 * ↑π * I)⁻¹ * deriv ((c • F) ∘ ↑ofComplex) ↑z = c * ((2 * ↑π * I)⁻¹ * deriv (F ∘ ↑ofComplex) ↑z)
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: z : ℍ
N : ℕ
⊢ ∑ m ∈ Icc (-↑N) ↑N, e2Summand m z =
    2 * riemannZeta 2 + ∑ m ∈ range N, -8 * ↑π ^ 2 * ∑' (n : ℕ+), ↑↑n * cexp (2 * ↑π * I * ↑z) ^ ((m + 1) * ↑n)

Tactic:
by
  rw [sum_Icc_of_even_eq_range (e2Summand_even z), Finset.sum_range_succ', smul_add,
    nsmul_eq_mul, Nat.cast_zero, e2Summand_zero_eq_two_riemannZeta_two]
  ring_nf
  simp only [e2Summand, eisSummand, add_comm, Nat.cast_add, Nat.cast_one, Fin.isValue,
    Matrix.cons_val_zero, Int.cast_add, Int.cast_natCast, Int.cast_one, Matrix.cons_val_one,
    Matrix.cons_val_fin_one, Int.reduceNeg, zpow_neg, mul_comm, mul_sum]
  congr with a
  have H2 := qExpansion_identity_pnat (k := 1) (by grind)
    ⟨(a + 1) * z, by simpa [show 0 < ((a + 1) : ℝ) by positivity] using z.2⟩
  simp only [add_comm, Nat.reduceAdd, one_div, mul_comm, mul_neg, even_two,
    Even.neg_pow, Nat.factorial_one, Nat.cast_one, div_one, pow_one] at H2
  simp_rw [zpow_ofNat, H2, ← tsum_mul_left, ← tsum_neg, ← exp_nsmul]
  refine tsum_congr fun b ↦ ?_
  ring_nf
  grind [I_sq, exp_add]

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hg : g • ρ = ρ
⊢ ¬((-↑ρ)⁻¹.re = (↑ρ).re ∧ (-↑ρ)⁻¹.im = (↑ρ).im)

Tactic:
norm_num [ρ, ← pow_two, div_pow]

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
z : ℍ
⊢ ∑' (v : Fin 2 → ℤ), eisSummand (↑k) v z = riemannZeta ↑k * eisensteinSeries 0 (↑k) z

Tactic:
by
  have hk1 : 1 < k := by grind
  have hk2 : 3 ≤ (k : ℤ) := mod_cast hk
  simp_rw [← gammaSetDivGcdSigmaEquiv.symm.tsum_eq, gammaSetDivGcdSigmaEquiv_symm_eq]
  rw [eisensteinSeries, Summable.tsum_sigma ?hsumm, zeta_nat_eq_tsum_of_gt_one hk1,
    tsum_mul_tsum_of_summable_norm (by simp [hk1]) ((summable_norm_eisSummand hk2 z).subtype _)]
  case hsumm =>
    exact gammaSetDivGcdSigmaEquiv.symm.summable_iff.mpr (summable_norm_eisSummand hk2 z).of_norm
      |>.congr <| by simp
  simp_rw [one_div]
  rw [Summable.tsum_prod' ?h₁ fun b ↦ ?h₂]
  case h₁ =>
    exact summable_mul_of_summable_norm (f := fun (n : ℕ) ↦ ((n : ℂ) ^ k)⁻¹)
      (g := fun (v : gammaSet 1 1 0) ↦ eisSummand k v z) (by simp [hk1])
      ((summable_norm_eisSummand hk2 z).subtype _)
  case h₂ =>
    simpa using ((summable_norm_eisSummand hk2 z).subtype _).of_norm.mul_left (a := ((b : ℂ) ^ k)⁻¹)
  refine tsum_congr fun b ↦ ?_
  rcases eq_or_ne b 0 with rfl | hb
  · simp [show ((0 : ℂ) ^ k)⁻¹ = 0 by aesop, eisSummand_of_gammaSet_eq_divIntMap]
  · have : NeZero b := ⟨hb⟩
    simpa [eisSummand_of_gammaSet_eq_divIntMap k z, tsum_mul_left, hb]
      using (gammaSetDivGcdEquiv b).tsum_eq (eisSummand k · z)

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

Goal state before:
pp: z : ℍ
⊢ E₄CubeSubE₆SqForm z = E₄ z ^ 3 - E₆ z ^ 2

Tactic:
by
  simp only [E₄CubeSubE₆SqForm, coe_mcast, coe_pow, sub_apply, Pi.pow_apply]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
n : ℕ
inst✝ : CommRing R
x y p : R
h : x - y ∈ span {p}
⊢ p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * y ^ (n - 1)

Tactic:
← Ideal.Quotient.eq

Goal state after:
R : Type u_1
n : ℕ
inst✝ : CommRing R
x y p : R
h : (Ideal.Quotient.mk (span {p})) x = (Ideal.Quotient.mk (span {p})) y
⊢ p ∣ ∑ i ∈ range n, x ^ i * y ^ (n - 1 - i) ↔ p ∣ ↑n * y ^ (n - 1)
Module: Mathlib.NumberTheory.Multiplicity

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

Tactic:
← Ideal.Quotient.eq

Goal state after:
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)
⊢ (Ideal.Quotient.mk (span {↑p ^ 2})) (∑ i ∈ range p, (a + ↑p * b) ^ i * a ^ (p - 1 - i)) =
    (Ideal.Quotient.mk (span {↑p ^ 2})) (↑p * a ^ (p - 1))
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : ¬p ∣ ↑n
⊢ emultiplicity p ((∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) * (x - y)) = emultiplicity p (x - y)

Tactic:
emultiplicity_mul hp,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
p : R
hp : Prime p
x y : R
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : ¬p ∣ ↑n
⊢ emultiplicity p (∑ i ∈ range n, x ^ i * y ^ (n - 1 - i)) + emultiplicity p (x - y) = emultiplicity p (x - y)
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ emultiplicity (↑p) ((∑ i ∈ range p, x ^ i * y ^ (p - 1 - i)) * (x - y)) = emultiplicity (↑p) (x - y) + 1

Tactic:
emultiplicity_mul hp,

Goal state after:
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
⊢ emultiplicity (↑p) (∑ i ∈ range p, x ^ i * y ^ (p - 1 - i)) + emultiplicity (↑p) (x - y) =
    emultiplicity (↑p) (x - y) + 1
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
a : ℕ
h_ind : emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p) (x - y) + ↑a
⊢ emultiplicity (↑p) (x ^ p ^ (a + 1) - y ^ p ^ (a + 1)) = emultiplicity (↑p) (x - y) + ↑(a + 1)

Tactic:
rw [Nat.cast_add, Nat.cast_one, ← add_assoc, ← h_ind, pow_succ, pow_mul, pow_mul]

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
a : ℕ
h_ind : emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p) (x - y) + ↑a
⊢ emultiplicity (↑p) ((x ^ p ^ a) ^ p - (y ^ p ^ a) ^ p) = emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) + 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (polarCoordReal K).source =ᵐ[volume.prod volume] Set.univ ×ˢ Set.univ

Tactic:
polarCoordReal_source,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Set.univ ×ˢ Set.univ.pi fun x ↦ polarCoord.source) =ᵐ[volume.prod volume] Set.univ ×ˢ Set.univ
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
hx : mixedEmbedding.norm x = 1
w : { w // w ≠ w₀ }
⊢ logMap x w = ↑(↑w).mult * Real.log ((normAtPlace ↑w) x)

Tactic:
by
  rw [logMap_apply, hx, Real.log_one, zero_mul, sub_zero]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
u : (𝓞 K)ˣ
x✝ : ∃ y, (algebraMap (𝓞 ↥K⁺) K) y = (algebraMap (𝓞 K) K) ↑u
y : 𝓞 ↥K⁺
hy : (algebraMap (𝓞 ↥K⁺) K) y = (algebraMap (𝓞 K) K) ↑u
this : IsUnit y
⊢ (algebraMap (𝓞 ↥K⁺) K) ↑this.unit = (algebraMap (𝓞 K) K) ↑u

Tactic:
by simp [hy]

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
x✝ : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
⊢ x ∈ A

Tactic:
rw [← hA, Set.mem_preimage, ← normAtAllPlaces_eq_of_normAtComplexPlaces_eq ha₂]

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
x✝ : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
⊢ normAtAllPlaces a ∈ normAtAllPlaces '' A
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ indexRealUnits K * (unitsMulComplexConjInv K).range.index = 2

Tactic:
rw [indexRealUnits, sup_comm]

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
⊢ (torsion K ⊔ realUnits K).index * (unitsMulComplexConjInv K).range.index = 2
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : IsTotallyReal F
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : Algebra.IsIntegral ℚ K
inst✝³ : IsTotallyComplex K
inst✝² : Algebra F K
inst✝¹ : IsQuadraticExtension F K
inst✝ : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
⊢ IsCMField K

Tactic:
obtain ⟨σ, hσ₁⟩ : ∃ σ : Gal(K/ℚ), ComplexEmbedding.IsConj φ σ :=
    exists_isConj_of_isRamified <|
      isRamified_iff.mpr ⟨IsTotallyComplex.isComplex _, IsTotallyReal.isReal _⟩

Goal state after:
F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : IsTotallyReal F
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : Algebra.IsIntegral ℚ K
inst✝³ : IsTotallyComplex K
inst✝² : Algebra F K
inst✝¹ : IsQuadraticExtension F K
inst✝ : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
⊢ IsCMField K
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: case pos.succ
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
h : p = 2
n : ℕ
hK : IsCyclotomicExtension {2 ^ (n + 2)} ℚ K
hζ✝ : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))
hζ : IsPrimitiveRoot ζ (2 ^ (n + 2))
⊢ Associated ((Algebra.norm ℤ) (hζ✝.toInteger - 1)) ↑p

Tactic:
hζ.norm_toInteger_sub_one_of_eq_two_pow,

Goal state after:
case pos.succ
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
h : p = 2
n : ℕ
hK : IsCyclotomicExtension {2 ^ (n + 2)} ℚ K
hζ✝ : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))
hζ : IsPrimitiveRoot ζ (2 ^ (n + 2))
⊢ Associated 2 ↑p
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
w : InfinitePlace K
⊢ (if w = w₀ then Real.log c else y w) ∈ if w = w₀ then Set.Iic 0 else Set.Icc 0 1

Tactic:
split_ifs with h

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
w : InfinitePlace K
h : w = w₀
⊢ Real.log c ∈ Set.Iic 0

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
w : InfinitePlace K
h : ¬w = w₀
⊢ y w ∈ Set.Icc 0 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p ^ (k + 1)} ℚ K
⊢ 𝒑.ramificationIdxIn (𝓞 K) = p ^ k * (p - 1)

Tactic:
by
  have : IsGalois ℚ K := isGalois {p ^ (k + 1)} ℚ K
  rw [ramificationIdxIn_eq_ramificationIdx 𝒑 (span {hK.zeta_spec.toInteger - 1}) Gal(K/ℚ),
    ramificationIdx_span_zeta_sub_one]

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

Goal state before:
pp: case refine_2.e_a.e_a
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
hc' : 0 < c
w : InfinitePlace K
⊢ (if w = w₀ then 0 else if w = w₀ then Real.log c else y w) = y w

Tactic:
split_ifs with h

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
hc' : 0 < c
w : InfinitePlace K
h : w = w₀
⊢ 0 = y w

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
hc : c ∈ Set.Icc 0 1
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then {0} else Set.Icc 0 1
hx₀ : (fun x1 x2 ↦ x1 • x2) c (↑expMapBasis y) ≠ 0
hc' : 0 < c
w : InfinitePlace K
h : ¬w = w₀
⊢ y w = y w
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1
hx₀ : ↑expMapBasis y ≠ 0
w : InfinitePlace K
⊢ (if w = w₀ then 0 else y w) ∈ if w = w₀ then {0} else Set.Icc 0 1

Tactic:
split_ifs with h

Goal state after:
case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1
hx₀ : ↑expMapBasis y ≠ 0
w : InfinitePlace K
h : w = w₀
⊢ 0 ∈ {0}

case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
y : realSpace K
hy : y ∈ Set.univ.pi fun w ↦ if w = w₀ then Set.Iic 0 else Set.Icc 0 1
hx₀ : ↑expMapBasis y ≠ 0
w : InfinitePlace K
h : ¬w = w₀
⊢ y w ∈ Set.Icc 0 1