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

Goal state after:
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
⊢ (if ha4 : a % 4 = 0 then fastJacobiSymAux (a / 4) b flip ⋯
    else
      if ha2 : a % 2 = 0 then fastJacobiSymAux (a / 2) b (decide (b % 8 = 3 ∨ b % 8 = 5) ^^ flip) ⋯
      else
        if ha1 : a = 1 then if flip = true then -1 else 1
        else if hba : b % a = 0 then 0 else fastJacobiSymAux (b % a) a (decide (a % 4 = 3 ∧ b % 4 = 3) ^^ flip) ⋯) =
    if flip = true then -J(↑a | b) else J(↑a | b)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: n : ℕ
odd : Odd n
h : 3 ≤ n
⊢ mersenne n % 3 = 1

Tactic:
obtain ⟨k, rfl⟩ := odd

Goal state after:
k : ℕ
h : 3 ≤ 2 * k + 1
⊢ mersenne (2 * k + 1) % 3 = 1
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case zero
p : ℕ
hp : p ≠ 0
⊢ 0 ≤ sMod p 0

Tactic:
dsimp [sMod]

Goal state after:
case zero
p : ℕ
hp : p ≠ 0
⊢ 0 ≤ 4 % (2 ^ p - 1)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case succ
p : ℕ
hp : p ≠ 0
n✝ : ℕ
⊢ 0 ≤ sMod p (n✝ + 1)

Tactic:
dsimp [sMod]

Goal state after:
case succ
p : ℕ
hp : p ≠ 0
n✝ : ℕ
⊢ 0 ≤ (sMod p n✝ ^ 2 - 2) % (2 ^ p - 1)
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: q : ℕ
inst✝ : Fact (Nat.Prime q)
odd : Odd q
leg3 : legendreSym q 3 = -1
⊢ (1 + α) ^ q = 1 - α

Tactic:
obtain ⟨k, rfl⟩ := odd

Goal state after:
k : ℕ
inst✝ : Fact (Nat.Prime (2 * k + 1))
leg3 : legendreSym (2 * k + 1) 3 = -1
⊢ (1 + α) ^ (2 * k + 1) = 1 - α
Module: Mathlib.NumberTheory.LucasLehmer

Goal state before:
pp: case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
⊢ ¬orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)

Tactic:
intro o

Goal state after:
case h₁
p' : ℕ
h : lucasLehmerResidue (p' + 2) = 0
o : orderOf (ωUnit (p' + 2)) ∣ 2 ^ (p' + 1)
⊢ False
Module: Mathlib.NumberTheory.ModularForms.CongruenceSubgroups

Goal state before:
pp: g : GL (Fin 2) ℚ
t : ConjAct (GL (Fin 2) ℝ) := (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g))⁻¹
N : ℕ
hN : N ≠ 0
hN' : toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) Γ(N) ≤ (mapGL ℝ).range
this : Γ(N) ≤ comap (mapGL ℝ) (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range)
⊢ (t • (mapGL ℝ).range ⊓ (mapGL ℝ).range).relIndex (mapGL ℝ).range ≠ 0

Tactic:
by
    have _ : NeZero N := ⟨hN⟩
    simpa only [index_comap] using! (finiteIndex_of_le this).index_ne_zero

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

Goal state before:
pp: g : GL (Fin 2) ℚ
⊢ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • (mapGL ℝ).range).Commensurable (mapGL ℝ).range

Tactic:
MonoidHom.range_eq_map

Goal state after:
g : GL (Fin 2) ℚ
⊢ (toConjAct ((GeneralLinearGroup.map (Rat.castHom ℝ)) g) • Subgroup.map (mapGL ℝ) ⊤).Commensurable
    (Subgroup.map (mapGL ℝ) ⊤)
Module: Mathlib.NumberTheory.ModularForms.SlashInvariantForms

Goal state before:
pp: case mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
g : SlashInvariantForm Γ k
toFun✝ : ℍ → ℂ
slash_action_eq'✝ : ∀ γ ∈ Γ, toFun✝ ∣[k] γ = toFun✝
h : { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ }.toFun = g.toFun
⊢ { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toFun✝¹ : ℍ → ℂ
slash_action_eq'✝¹ : ∀ γ ∈ Γ, toFun✝¹ ∣[k] γ = toFun✝¹
toFun✝ : ℍ → ℂ
slash_action_eq'✝ : ∀ γ ∈ Γ, toFun✝ ∣[k] γ = toFun✝
h :
  { toFun := toFun✝¹, slash_action_eq' := slash_action_eq'✝¹ }.toFun =
    { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ }.toFun
⊢ { toFun := toFun✝¹, slash_action_eq' := slash_action_eq'✝¹ } =
    { toFun := toFun✝, slash_action_eq' := slash_action_eq'✝ }
Module: Mathlib.NumberTheory.ModularForms.Cusps

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
this : upperRightHom 𝒢.widthInfty ∈ 𝒢.adjoinNegOne
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods

Tactic:
rcases this with (h | h)

Goal state after:
case inl
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : upperRightHom 𝒢.widthInfty ∈ 𝒢
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods

case inr
𝒢 : Subgroup (GL (Fin 2) ℝ)
h : -upperRightHom 𝒢.widthInfty ∈ 𝒢
⊢ 2 * 𝒢.widthInfty ∈ 𝒢.strictPeriods
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: case mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
g : ModularForm Γ k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
bdd_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_cusps' := bdd_at_cusps'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_cusps' := bdd_at_cusps'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDiff ⇑toSlashInvariantForm✝¹
bdd_at_cusps'✝¹ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm✝¹.toFun k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
bdd_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsBoundedAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, bdd_at_cusps' := bdd_at_cusps'✝¹ } =
    (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_cusps' := bdd_at_cusps'✝ }
⊢ { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, bdd_at_cusps' := bdd_at_cusps'✝¹ } =
    { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, bdd_at_cusps' := bdd_at_cusps'✝ }
Module: Mathlib.NumberTheory.ModularForms.Basic

Goal state before:
pp: case mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
g : CuspForm Γ k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
zero_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_cusps' := zero_at_cusps'✝ } =
    (fun f ↦ f.toFun) g
⊢ { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_cusps' := zero_at_cusps'✝ } = g

Tactic:
cases g

Goal state after:
case mk.mk
F : Type u_1
Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
toSlashInvariantForm✝¹ : SlashInvariantForm Γ k
holo'✝¹ : MDiff ⇑toSlashInvariantForm✝¹
zero_at_cusps'✝¹ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm✝¹.toFun k
toSlashInvariantForm✝ : SlashInvariantForm Γ k
holo'✝ : MDiff ⇑toSlashInvariantForm✝
zero_at_cusps'✝ : ∀ {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt toSlashInvariantForm✝.toFun k
h :
  (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, zero_at_cusps' := zero_at_cusps'✝¹ } =
    (fun f ↦ f.toFun)
      { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_cusps' := zero_at_cusps'✝ }
⊢ { toSlashInvariantForm := toSlashInvariantForm✝¹, holo' := holo'✝¹, zero_at_cusps' := zero_at_cusps'✝¹ } =
    { toSlashInvariantForm := toSlashInvariantForm✝, holo' := holo'✝, zero_at_cusps' := zero_at_cusps'✝ }
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: z : ℍ
h : z ∈ 𝒟ᵒ
⊢ |2 * z.re| < 1

Tactic:
by
  rw [abs_mul, abs_two, ← lt_div_iff₀' (zero_lt_two' ℝ)]
  exact h.2

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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
inst✝ : CuspFormClass F Γ k
f : F
⊢ ∃ C, ∀ (τ : ℍ), ‖f τ‖ ≤ C / τ.im ^ (↑k / 2)

Tactic:
obtain ⟨C, hC⟩ := petersson_bounded_left k Γ f f
  refine ⟨C.sqrt, fun τ ↦ ?_⟩
  specialize hC τ
  rw [← sq_le_sq₀ (by positivity) (by positivity), div_pow, Real.sq_sqrt ((norm_nonneg _).trans hC)]
  grw [← hC]
  rw [petersson, ← Real.rpow_mul_natCast τ.im_pos.le]
  simp [abs_of_pos τ.im_pos, field]

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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F✝ : Type u_2
inst✝¹ : FunLike F✝ ℍ ℂ
inst✝ : ModularFormClass F✝ Γ k
f : F✝
e : ℝ
hF : ⇑f =O[comap UpperHalfPlane.im (𝓝 0)] fun τ ↦ τ.im ^ (-e)
h : ℝ := Γ.strictWidthInfty
hh : 0 < h
this : NeZero h
hΓ : h ∈ Γ.strictPeriods
C : ℝ
Cpos : C > 0
hC : ∀ᶠ (b : ℝ) in 𝓝 0, ∀ (a : ℍ), a.im = b → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
n : ℕ
hn : 0 < n
hn' : ∀ (a : ℍ), a.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n → ‖f a‖ ≤ C * ‖a.im ^ (-e)‖
F : ℝ → ℝ := fun x ↦ ‖1 / ↑h * (1 / 𝕢 h (↑x + 1 / ↑n * I) ^ n * f { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ })‖
hne : ‖↑n ^ e‖ = ↑n ^ e
x : ℝ
⊢ { coe := ↑x + 1 / ↑n * I, coe_im_pos := ⋯ }.im = ((fun r ↦ r⁻¹) ∘ Nat.cast) n

Tactic:
simp [← UpperHalfPlane.coe_im]

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

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

Tactic:
rw [← tsum_eq_of_summable_unconditional (L := symmetricIcc ℤ)]

Goal state after:
z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ ∑'[symmetricIcc ℤ] (m : ℤ), e2Summand m z =
    ∑'[symmetricIcc ℤ] (b : ℤ),
      (∑' (n : ℤ), G2Term z ![b, n] + ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑b * ↑z + ↑n) - 1 / (↑b * ↑z + ↑n + 1)))

z : ℍ
t : ℂ := ∑' (m : ℤ) (n : ℤ), G2Term z ![m, n]
⊢ Summable fun b ↦
    ∑' (n : ℤ), G2Term z ![b, n] + ∑'[symmetricIco ℤ] (n : ℤ), (1 / (↑b * ↑z + ↑n) - 1 / (↑b * ↑z + ↑n + 1))
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
N : ℤ
⊢ ∑' (b : ℤ), (1 / (↑b * ↑z + ↑N) ^ 2 - (1 / (↑b * ↑z + ↑N) - 1 / (↑b * ↑z + ↑N + 1))) = ∑' (m : ℤ), G2Term z ![m, N]

Tactic:
apply tsum_congr (fun M ↦ ?_)

Goal state after:
z : ℍ
N M : ℤ
⊢ 1 / (↑M * ↑z + ↑N) ^ 2 - (1 / (↑M * ↑z + ↑N) - 1 / (↑M * ↑z + ↑N + 1)) = G2Term z ![M, N]
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable

Goal state before:
pp: case e'_6
z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
⊢ E2 z - ∑ i ∈ range 1, (if i = 0 then 1 else -24 * ↑((σ 1) i)) • cexp (2 * ↑π * I * ↑z) ^ i =
    ∑' (b : ℕ), -24 * (↑((σ 1) (b + 1)) * cexp (2 * ↑π * I * ↑z) ^ (b + 1))

Tactic:
E2_eq_tsum_cexp,

Goal state after:
case e'_6
z : ℍ
hS : Summable fun n ↦ ↑((σ 1) (n + 1)) * cexp (2 * ↑π * I * ↑z) ^ (n + 1)
⊢ 1 - 24 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n -
      ∑ i ∈ range 1, (if i = 0 then 1 else -24 * ↑((σ 1) i)) • cexp (2 * ↑π * I * ↑z) ^ i =
    ∑' (b : ℕ), -24 * (↑((σ 1) (b + 1)) * cexp (2 * ↑π * I * ↑z) ^ (b + 1))
Module: Mathlib.NumberTheory.ModularForms.NormTrace

Goal state before:
pp: 𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ IsZeroAtImInfty ((ModularForm.trace ℋ f).toFun ∣[k] γ)

Tactic:
ModularForm.toFun_eq_coe,

Goal state after:
𝒢 ℋ : Subgroup (GL (Fin 2) ℝ)
F : Type u_1
f : F
inst✝² : FunLike F ℍ ℂ
k : ℤ
inst✝¹ : 𝒢.IsFiniteRelIndex ℋ
inst✝ : CuspFormClass F 𝒢 k
γ : GL (Fin 2) ℝ
h : IsCusp (γ • OnePoint.infty) ℋ
⊢ IsZeroAtImInfty (⇑(ModularForm.trace ℋ f) ∣[k] γ)
Module: Mathlib.NumberTheory.Multiplicity

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

Tactic:
suffices p ^ 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i) by
      convert! this; abel

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
⊢ p ^ 2 ∣ ∑ i ∈ range n, x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i)
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: case hp
K : Type u_1
inst✝⁶ : Field K
L : Type u_2
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝³ : Algebra v.Completion w.Completion
inst✝² : IsScalarTower K v.Completion w.Completion
inst✝¹ : ContinuousSMul v.Completion w.Completion
inst✝ : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
⊢ IsClosed
    {x | ((conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion)) x = (extensionEmbedding v) x}

pp: case ih
K : Type u_1
inst✝⁶ : Field K
L : Type u_2
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝³ : Algebra v.Completion w.Completion
inst✝² : IsScalarTower K v.Completion w.Completion
inst✝¹ : ContinuousSMul v.Completion w.Completion
inst✝ : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
a✝ : WithAbs ↑v
⊢ ((conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion)) { toCompletion := ↑a✝ } =
    (extensionEmbedding v) { toCompletion := ↑a✝ }

Tactic:
· simpa using! isClosed_eq (.comp (by fun_prop)
          ((isometry_extensionEmbedding w).continuous.comp <|
            continuous_algebraMap v.Completion w.Completion))
        (isometry_extensionEmbedding v).continuous

Goal state after:
case ih
K : Type u_1
inst✝⁶ : Field K
L : Type u_2
inst✝⁵ : Field L
inst✝⁴ : Algebra K L
w : InfinitePlace L
v : InfinitePlace K
inst✝³ : Algebra v.Completion w.Completion
inst✝² : IsScalarTower K v.Completion w.Completion
inst✝¹ : ContinuousSMul v.Completion w.Completion
inst✝ : ComplexEmbedding.LiesOver (conjugate w.embedding) v.embedding
a✝ : WithAbs ↑v
⊢ ((conjugate (extensionEmbedding w)).comp (algebraMap v.Completion w.Completion)) { toCompletion := ↑a✝ } =
    (extensionEmbedding v) { toCompletion := ↑a✝ }
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ rank K = Fintype.card (InfinitePlace K) - 1

Tactic:
rank

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card (InfinitePlace K) - 1 = Fintype.card (InfinitePlace K) - 1
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measurable ↑(polarSpaceCoord K).symm

Tactic:
rw [polarSpaceCoord, OpenPartialHomeomorph.transHomeomorph_symm_apply]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Measurable (↑(mixedEmbedding.polarCoord K).symm ∘ ⇑(homeoRealMixedSpacePolarSpace K).symm)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
a : ↑(integerSet K)
⊢ ↑(intNorm a) = mixedEmbedding.norm ↑a

Tactic:
by
  rw [intNorm, Nat.cast_natAbs, ← Rat.cast_intCast, Int.cast_abs, Algebra.coe_norm_int,
    ← norm_eq_norm, mixedEmbedding_preimageOfMemIntegerSet]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a b : ↑(integerSet K)
x✝ : a ≈ b
u : ↥(torsion K)
hu : (fun m ↦ m • b) u = a
⊢ ↑(intNorm a) = ↑(intNorm b)

Tactic:
intNorm_coe,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a b : ↑(integerSet K)
x✝ : a ≈ b
u : ↥(torsion K)
hu : (fun m ↦ m • b) u = a
⊢ mixedEmbedding.norm ↑a = ↑(intNorm b)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a b : ↑(integerSet K)
x✝ : a ≈ b
u : ↥(torsion K)
hu : (fun m ↦ m • b) u = a
⊢ mixedEmbedding.norm ↑a = ↑(intNorm b)

Tactic:
intNorm_coe,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
a b : ↑(integerSet K)
x✝ : a ≈ b
u : ↥(torsion K)
hu : (fun m ↦ m • b) u = a
⊢ mixedEmbedding.norm ↑a = mixedEmbedding.norm ↑b
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
⊢ ↑(intNorm ↑((idealSetEquiv K J) a)) = mixedEmbedding.norm ↑a

Tactic:
intNorm_coe,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
a : ↑(idealSet K J)
⊢ mixedEmbedding.norm ↑↑((idealSetEquiv K J) a) = mixedEmbedding.norm ↑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
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
⊢ 2 ^ rank ↥K⁺ = 2 ^ Finset.univ.card

Tactic:
rank

Goal state after:
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
W₀ : InfinitePlace K := (equivInfinitePlace K).symm w₀
f : { w // w ≠ W₀ } ≃ { w // w ≠ w₀ } := (equivInfinitePlace K).subtypeEquiv ⋯
g : Fin (rank K) ≃ { w // w ≠ W₀ } := ((finCongr ⋯).trans (equivFinRank ↥K⁺)).trans f.symm
⊢ 2 ^ (Fintype.card (InfinitePlace ↥K⁺) - 1) = 2 ^ Finset.univ.card
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ rank K = Fintype.card (InfinitePlace K) - 1

Tactic:
rank

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Fintype.card (InfinitePlace K) - 1 = Fintype.card (InfinitePlace K) - 1
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: K : Type u_2
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : Algebra.IsIntegral ℚ K
inst✝¹ : IsTotallyComplex K
inst✝ : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card ↥(Subgroup.zpowers σ) = 2
this : Finite ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
W : InfinitePlace K
⊢ ((InfinitePlace.mk W.embedding).comap (algebraMap (↥L) K)).IsReal

Tactic:
comap_mk,

Goal state after:
K : Type u_2
inst✝⁴ : Field K
inst✝³ : CharZero K
inst✝² : Algebra.IsIntegral ℚ K
inst✝¹ : IsTotallyComplex K
inst✝ : IsGalois ℚ K
σ : Gal(K/ℚ)
hσ : ∀ (φ : K →+* ℂ), ComplexEmbedding.IsConj φ σ
φ : K →+* ℂ := Classical.choice ⋯
hσ' : Nat.card ↥(Subgroup.zpowers σ) = 2
this : Finite ↥(Subgroup.zpowers σ)
L : IntermediateField ℚ K := FixedPoints.intermediateField ↥(Subgroup.zpowers σ)
W : InfinitePlace K
⊢ (InfinitePlace.mk (W.embedding.comp (algebraMap (↥L) K))).IsReal
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (∏ x_1, Real.exp (x w₀) ^ x_1.mult) *
      ∏ x_1, (∏ i, x_1 ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) ^ x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K

Tactic:
prod_pow_eq_pow_sum,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (Real.exp (x w₀) ^ ∑ i, i.mult) *
      ∏ x_1, (∏ i, x_1 ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) ^ x_1.mult =
    Real.exp (x w₀) ^ finrank ℚ K
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n i j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ n
hn : 2 ≤ n
hi : i.Coprime n
hj : j.Coprime n
⊢ ζ ^ j - 1 = ↑⋯.unit * ↑⋯.unit⁻¹ * (ζ ^ i - 1)

Tactic:
by
  grind [IsUnit.mul_val_inv, pow_sub_one_mul_geom_sum_eq_pow_sub_one_mul_geom_sum, IsUnit.unit_spec]

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Galois

Goal state before:
pp: n : ℕ
inst✝⁷ : NeZero n
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst✝⁴ : NeZero m
F : Type u_2
inst✝³ : Field F
inst✝² : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst✝¹ : Algebra F K
inst✝ : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
this : (↑((galEquivZMod m F) (σ.restrictNormal F))).cast = (↑((galEquivZMod n K) σ)).cast
⊢ (galEquivZMod m F) (σ.restrictNormal F) = (ZMod.unitsMap h) ((galEquivZMod n K) σ)

Tactic:
ZMod.cast_id

Goal state after:
n : ℕ
inst✝⁷ : NeZero n
K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : NumberField K
hK : IsCyclotomicExtension {n} ℚ K
m : ℕ
inst✝⁴ : NeZero m
F : Type u_2
inst✝³ : Field F
inst✝² : NumberField F
hF : IsCyclotomicExtension {m} ℚ F
inst✝¹ : Algebra F K
inst✝ : IsGalois ℚ F
h : m ∣ n
σ : Gal(K/ℚ)
hζ : IsPrimitiveRoot (zeta m ℚ F) m
ζ : F := zeta m ℚ F
this : ↑((galEquivZMod m F) (σ.restrictNormal F)) = (↑((galEquivZMod n K) σ)).cast
⊢ (galEquivZMod m F) (σ.restrictNormal F) = (ZMod.unitsMap h) ((galEquivZMod n K) σ)
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
e : Fin l.zipIdx.length ≃ Fin l.length := finCongr ⋯
x✝ : Fin l.zipIdx.length
⊢ y ^ l.zipIdx[↑x✝].2 = y ^ ↑(e x✝)

Tactic:
simp [e]

Goal state after:
Module: Mathlib.NumberTheory.Padics.ProperSpace

Goal state before:
pp: case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ dist z ↑(z.appr k) < ε

Tactic:
· exact (((z - z.appr k).norm_le_pow_iff_mem_span_pow k).mpr (z.appr_spec k)).trans_lt hk

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

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

Tactic:
apply (summable_iff_summable_compl_and_tsum_mem f).mpr

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s ↦ ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ Summable (⇑toCompl ∘ f) ∧ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
k : ℕ
hk : 0 < k
this : 0 ≤ logb ↑n₀ ↑n
⊢ (↑n₀ * (↑k * logb ↑n₀ ↑n + ↑k)) ^ (↑k)⁻¹ = (↑n₀ * ((logb ↑n₀ ↑n + 1) * ↑k)) ^ (↑k)⁻¹

Tactic:
add_mul,

Goal state after:
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
k : ℕ
hk : 0 < k
this : 0 ≤ logb ↑n₀ ↑n
⊢ (↑n₀ * (↑k * logb ↑n₀ ↑n + ↑k)) ^ (↑k)⁻¹ = (↑n₀ * (logb ↑n₀ ↑n * ↑k + 1 * ↑k)) ^ (↑k)⁻¹
Module: Mathlib.NumberTheory.Padics.MahlerBasis

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
x✝ : i ∈ range (n + 1)
⊢ ‖((-1) ^ (n - i) * ↑(n.choose i)) • (f (↑i + ↑(p ^ t)) - f ↑i)‖ ≤
    ‖↑(-1) ^ (n - i) * ↑(n.choose i)‖ * ‖f (↑i + ↑(p ^ t)) - f ↑i‖

Tactic:
by
      rw [← Int.cast_smul_eq_zsmul ℤ_[p]]
      exact (norm_smul_le ..).trans (by norm_cast)

Goal state after: