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

Goal state before:
pp: F : Type u_1
F' : Type u_2
inst✝⁴ : FunLike F ℍ ℂ
inst✝³ : FunLike F' ℍ ℂ
k : ℤ
g : GL (Fin 2) ℝ
τ : ℍ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.HasDetOne
inst✝¹ : SlashInvariantFormClass F Γ k
f : F
inst✝ : SlashInvariantFormClass F' Γ k
f' : F'
hg : g ∈ Γ
⊢ petersson k (⇑f) (⇑f') (g • τ) = petersson k (⇑f) (⇑f') τ

Tactic:
by
  simpa [SlashInvariantFormClass.slash_action_eq _ _ hg, Subgroup.HasDetOne.det_eq hg, σ]
    using (petersson_slash k f f' g τ).symm

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

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
hS : f ∣[k] S = f
hT : f ∣[k] T = f
γ : SL(2, ℤ)
⊢ f ∣[k] γ = f

Tactic:
have h𝒮ℒ : 𝒮ℒ = Subgroup.closure ({↑S, ↑T} : Set (GL (Fin 2) ℝ)) := by
    rw [MonoidHom.range_eq_map, ← SpecialLinearGroup.SL2Z_generators, MonoidHom.map_closure,
      Set.image_pair]
    rfl

Goal state after:
f : ℍ → ℂ
k : ℤ
hS : f ∣[k] S = f
hT : f ∣[k] T = f
γ : SL(2, ℤ)
h𝒮ℒ :
  (Matrix.SpecialLinearGroup.mapGL ℝ).range =
    Subgroup.closure
      {Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) S),
        Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) T)}
⊢ f ∣[k] γ = f
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: ⊢ I ∈ 𝒟

Tactic:
constructor <;> norm_num

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

Goal state before:
pp: E : Type u_1
inst✝¹ : SeminormedAddCommGroup E
f : ℍ → E
hf_cont : Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
t : ℝ
ht : 0 ≤ t
hf_infinity : ∀ (g : SL(2, ℤ)), (fun τ ↦ f (g • τ)) =O[atImInfty] fun z ↦ z.im ^ t
Γ : Subgroup SL(2, ℤ)
inst✝ : Γ.FiniteIndex
hf_inv : ∀ g ∈ Γ, ∀ (τ : ℍ), f (g • τ) = f τ
f' : ℍ → SL(2, ℤ) ⧸ Γ → E := fun τ ↦ Quotient.lift (fun g ↦ f (g⁻¹ • τ)) ⋯
hf'_cont : ∀ (γ : SL(2, ℤ) ⧸ Γ), Continuous[_, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] fun x ↦ f' x γ
hf'_inv : ∀ (τ : ℍ) (g : SL(2, ℤ)) (γ : SL(2, ℤ) ⧸ Γ), f' (g • τ) (g • γ) = f' τ γ
hf'_infty : ∀ (γ : SL(2, ℤ) ⧸ Γ), (fun x ↦ f' x γ) =O[atImInfty] fun z ↦ z.im ^ t
this : Fintype (SL(2, ℤ) ⧸ Γ)
C : ℝ
hC : ∀ (τ : ℍ), ‖∑ c, ‖f' τ c‖‖ ≤ C * max τ.im (1 / τ.im) ^ t
τ : ℍ
⊢ ‖f τ‖ ≤ ‖∑ c, ‖f' τ c‖‖

Tactic:
simpa [Real.norm_of_nonneg <| show 0 ≤ ∑ γ, ‖f' τ γ‖ by positivity, -sl_moeb, f'] using
    Finset.univ.single_le_sum (fun γ _ ↦ norm_nonneg (f' τ γ)) (Finset.mem_univ ⟦1⟧)

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

Goal state before:
pp: k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
⊢ ∃ C, ∀ (τ : ℍ), ‖‖petersson k (⇑f) (⇑f') τ‖‖ ≤ C

Tactic:
refine ModularGroup.exists_bound_of_subgroup_invariant (by fun_prop) (fun g ↦ ?_)
    fun g hg τ ↦ SlashInvariantFormClass.norm_petersson_smul hg

Goal state after:
k : ℤ
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝⁴ : Γ.IsArithmetic
F : Type u_2
F' : Type u_3
f : F
f' : F'
inst✝³ : FunLike F ℍ ℂ
inst✝² : FunLike F' ℍ ℂ
inst✝¹ : CuspFormClass F Γ k
inst✝ : ModularFormClass F' Γ k
g : SL(2, ℤ)
⊢ IsBoundedAtImInfty fun τ ↦ ‖petersson k (⇑f) (⇑f') (g • τ)‖
Module: Mathlib.NumberTheory.Modular

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

Tactic:
simp [hc]

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h✝ : 0 < ‖↑τ.im ^ ↑k‖
t : NNReal
h : τ.im = ↑t
ht : 0 < ↑t
⊢ max (↑t) (1 / ↑t) ^ ↑k / ‖↑↑t ^ ↑k‖ = max 1 (1 / ↑t ^ ↑k) ^ 2

Tactic:
← coe_nnnorm

Goal state after:
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
F : Type u_2
inst✝¹ : FunLike F ℍ ℂ
f : F
C : ℝ
τ : ℍ
k : ℕ
inst✝ : ModularFormClass F Γ ↑k
hC : ‖f τ‖ ^ 2 ≤ C * (max τ.im (1 / τ.im) ^ ↑k / ‖↑τ.im ^ ↑k‖)
hC' : 0 ≤ C
h✝ : 0 < ‖↑τ.im ^ ↑k‖
t : NNReal
h : τ.im = ↑t
ht : 0 < ↑t
⊢ max (↑t) (1 / ↑t) ^ ↑k / ↑‖↑↑t ^ ↑k‖₊ = max 1 (1 / ↑t ^ ↑k) ^ 2
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ b
hre : (g • z).re = ↑b + z.re
this : |↑b| - |z.re| ≤ 1 / 2
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1

Tactic:
sub_le_iff_le_add,

Goal state after:
g✝ : SL(2, ℤ)
z✝ : ℍ
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg : g • z ∈ 𝒟
hc : ↑g 1 0 = 0
hd' : ↑g 1 1 = 1 ∨ ↑g 1 1 = -1
hd : ↑g 1 1 = 1
ha : ↑g 0 0 = 1
b : ℤ := ↑g 0 1
hgz : g = T ^ b
hre : (g • z).re = ↑b + z.re
this : |↑b| ≤ 1 / 2 + |z.re|
⊢ (g = T ∨ g = -T) ∧ z.re = -1 / 2 ∨ (g = T⁻¹ ∨ g = -T⁻¹) ∧ z.re = 1 / 2 ∨ g = 1 ∨ g = -1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
this✝¹ : ‖↑z + ↑(↑g 1 1)‖ ≤ 1
this✝ : |↑(↑g 1 1) + z.re| ≤ 1
this : |↑(↑g 1 1)| - |z.re| ≤ 1
⊢ |↑g 1 1| ≤ 1

Tactic:
sub_le_iff_le_add,

Goal state after:
g : SL(2, ℤ)
z : ℍ
hz : z ∈ 𝒟
hg' : ‖denom (toGL ((SpecialLinearGroup.map (Int.castRingHom ℝ)) g)) ↑z‖ ≤ 1
hc : ↑g 1 0 = 1
this✝¹ : ‖↑z + ↑(↑g 1 1)‖ ≤ 1
this✝ : |↑(↑g 1 1) + z.re| ≤ 1
this : |↑(↑g 1 1)| ≤ 1 + |z.re|
⊢ |↑g 1 1| ≤ 1
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case inr.inr.inl.inl
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
hzre✝ : |z.re| = 1 / 2
h : ↑g 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ

Tactic:
rw [h, zpow_one] at hg'

Goal state after:
case inr.inr.inl.inl
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 * S
hSre : (S • z).re = -z.re
hzre✝ : |z.re| = 1 / 2
h : ↑g 0 0 = 1
this : |1 + -z.re| ≤ 1 / 2
hzre : z.re = 1 / 2
⊢ g = S ∧ ‖↑z‖ = 1 ∨ g = T⁻¹ * S ∧ z = ρ ∨ g = T * S ∧ z = 1 +ᵥ ρ
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Transform

Goal state before:
pp: z : ℍ
N M : ℤ
⊢ ((↑M * ↑z + ↑N) ^ 2)⁻¹ - ((↑M * ↑z + ↑N)⁻¹ - (↑M * ↑z + ↑N + 1)⁻¹) =
    (↑M * ↑z + ↑N + 1)⁻¹ * ((↑M * ↑z + ↑N) ^ 2)⁻¹ + δ ![M, N]

Tactic:
nth_rw 1 [← aux_identity z M N]

Goal state after:
z : ℍ
N M : ℤ
⊢ (↑M * ↑z + ↑N + 1)⁻¹ * ((↑M * ↑z + ↑N) ^ 2)⁻¹ + δ ![M, N] + ((↑M * ↑z + ↑N)⁻¹ - (↑M * ↑z + ↑N + 1)⁻¹) -
      ((↑M * ↑z + ↑N)⁻¹ - (↑M * ↑z + ↑N + 1)⁻¹) =
    (↑M * ↑z + ↑N + 1)⁻¹ * ((↑M * ↑z + ↑N) ^ 2)⁻¹ + δ ![M, N]
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion

Goal state before:
pp: k l : ℕ
f : ℕ → ℂ
p : ℝ
hp : 0 < p
hf : f =O[atTop] fun n ↦ ↑n ^ l
⊢ SummableLocallyUniformlyOn (fun n ↦ f n • iteratedDerivWithin k (fun z ↦ cexp (2 * ↑π * I * z / ↑p) ^ n) ℍₒ) ℍₒ

Tactic:
apply SummableLocallyUniformlyOn_of_locally_bounded isOpen_upperHalfPlaneSet
  intro K hK hKc
  have : CompactSpace K := isCompact_univ_iff.mp (isCompact_iff_isCompact_univ.mp hKc)
  let c : ContinuousMap K ℂ := ⟨fun r : K ↦ Complex.exp (2 * π * I * r / p), by fun_prop⟩
  let r : ℝ := ‖mkOfCompact c‖
  have hr : ‖r‖ < 1 := by
    simp only [norm_norm, r, norm_lt_iff_of_compact Real.zero_lt_one, mkOfCompact_apply,
      ContinuousMap.coe_mk, c]
    intro x
    have h1 : cexp (2 * π * I * (x / p)) = cexp (2 * π * I * x / p) := by
      ring_nf
    simpa using h1 ▸ norm_exp_two_pi_I_lt_one ⟨((x : ℂ) / p), by aesop⟩
  refine ⟨_, by simpa using (summable_norm_mul_geometric_of_norm_lt_one' hr
    (Asymptotics.isBigO_norm_left.mpr (aux_IsBigO_mul k l p hf))), fun n z hz ↦ ?_⟩
  have h0 := pow_le_pow_left₀ (norm_nonneg _) (norm_coe_le_norm (mkOfCompact c) ⟨z, hz⟩) n
  simp only [norm_mkOfCompact, mkOfCompact_apply, ContinuousMap.coe_mk, ← exp_nsmul', Pi.smul_apply,
    iteratedDerivWithin_cexp_aux k n p isOpen_upperHalfPlaneSet (hK hz), smul_eq_mul,
    norm_mul, norm_pow, Complex.norm_div, norm_ofNat, norm_real, Real.norm_eq_abs, norm_I, mul_one,
    norm_natCast, abs_norm, ge_iff_le, r, c] at *
  rw [← mul_assoc]
  gcongr
  convert! h0
  rw [← norm_pow, ← exp_nsmul']

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ Module.rank ℂ
      (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k ⧸
        cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k) =
    1

Tactic:
apply rank_eq_one (Submodule.Quotient.mk (E hk))

Goal state after:
case n
k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ Submodule.Quotient.mk (E hk) ≠ 0

case h
k : ℕ
hk : 3 ≤ k
hk2 : Even k
⊢ ∀
    (w :
      ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k ⧸
        cuspFormSubmodule (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑k),
    ∃ c, c • Submodule.Quotient.mk (E hk) = w
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case e'_6.e'_6.hfper
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
r : ℝ
hpos : 0 < s.re
hs : r + 1 < s.re
hΛ : Λ hk f s = mellin (fun t ↦ (weakFEPair hk f).f t - (weakFEPair hk f).f₀) s
hcoeff : (fun n ↦ (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f)) =O[atTop] fun n ↦ ↑n ^ r
hh : 0 < h Γ
hΓ : h Γ ∈ Γ.strictPeriods
t : ℝ
ht : 0 < t
this :
  HasSum
    (fun m ↦ (PowerSeries.coeff m) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ m)
    (f (↑ofComplex (I * ↑t)))
⊢ Function.Periodic (⇑f ∘ ↑ofComplex) ↑(h Γ)

Tactic:
· exact SlashInvariantFormClass.periodic_comp_ofComplex f hΓ

Goal state after:
Module: Mathlib.NumberTheory.NumberField.Completion.InfinitePlace

Goal state before:
pp: case ih
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsReal
a : WithAbs ↑v
⊢ ↑((extensionEmbeddingOfIsReal hv) { toCompletion := ↑a }) = (extensionEmbedding v) { toCompletion := ↑a }

Tactic:
| ih a =>

Goal state after:
Module: Mathlib.Topology.Algebra.RestrictedProduct.Units

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
inst✝² : (i : ι) → Monoid (R i)
S : ι → Type u_3
inst✝¹ : (i : ι) → SetLike (S i) (R i)
inst✝ : ∀ (i : ι), SubmonoidClass (S i) (R i)
B : (i : ι) → S i
𝓕 : Filter ι
x b : Πʳ (i : ι), [R i, ↑(B i)]_[𝓕]
hb : ∀ (x_1 : ι), (x * b) x_1 = 1 x_1 ∧ (b * x) x_1 = 1 x_1
⊢ (∀ (i : ι), ∃ b, x i * b = 1 ∧ b * x i = 1) ∧
    ∀ᶠ (i : ι) in 𝓕, ∃ (h : x i ∈ B i), ∃ b, ⟨x i, ⋯⟩ * b = 1 ∧ b * ⟨x i, ⋯⟩ = 1

Tactic:
exact ⟨Classical.skolem.symm.1 ⟨b, hb⟩, by filter_upwards [x.2, b.2] using
    fun i hx hb ↦ ⟨hx, ⟨b i, hb⟩, by simp_all [← SetLike.coe_eq_coe]⟩⟩

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

Goal state before:
pp: case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
this : (2 * ↑n / ↑(h Γ)) ^ s = 2 ^ s * ↑n ^ s / ↑(h Γ) ^ s
⊢ p / ↑n ^ s = (↑π ^ s)⁻¹ * Gamma s * p / (2 ^ s * ↑n ^ s / ↑(h Γ) ^ s) * (2 ^ s * ↑π ^ s / Gamma s * ↑(h Γ) ^ (-s))

Tactic:
cpow_neg

Goal state after:
case e'_5
Γ : Subgroup (GL (Fin 2) ℝ)
inst✝² : Γ.IsArithmetic
k : ℤ
hk : 0 < k
F : Type u_1
inst✝¹ : FunLike F ℍ ℂ
f : F
s : ℂ
inst✝ : ModularFormClass F Γ k
hs : 0 < s.re
hΛ : HasSum (fun n ↦ ↑π ^ (-s) * Gamma s * (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) / ↑(2 * ↑n / h Γ) ^ s) (Λ hk f s)
n : ℕ
p : ℂ
this : (2 * ↑n / ↑(h Γ)) ^ s = 2 ^ s * ↑n ^ s / ↑(h Γ) ^ s
⊢ p / ↑n ^ s = (↑π ^ s)⁻¹ * Gamma s * p / (2 ^ s * ↑n ^ s / ↑(h Γ) ^ s) * (2 ^ s * ↑π ^ s / Gamma s * (↑(h Γ) ^ s)⁻¹)
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝¹ : (i : ι) → TopologicalSpace (R i)
S : Set ι
inst✝ : ∀ (i : ι), WeaklyLocallyCompactSpace (R i)
hS : Sᶜ.Finite
hAcompact : ∀ i ∈ S, IsCompact (A i)
x : Πʳ (i : ι), [R i, A i]_[𝓟 S]
K : (i : ι) → Set (R i)
K_compact : ∀ (i : ι), IsCompact (K i)
hK : ∀ (i : ι), K i ∈ 𝓝 (x i)
Q : Set ((i : ι) → R i) := univ.pi fun i ↦ if i ∈ S then A i else K i
Q_def : Q = univ.pi fun i ↦ if i ∈ S then A i else K i
Q_compact : IsCompact Q
U : Set ((i : ι) → R i) := Sᶜ.pi K
U_nhds : U ∈ 𝓝 ⇑x
y : Πʳ (i : ι), [R i, A i]_[𝓟 S]
H : y ∈ DFunLike.coe ⁻¹' U
i : ι
x✝ : i ∈ univ
⊢ y i ∈ (fun i ↦ if i ∈ S then A i else K i) i

Tactic:
dsimp only
      split_ifs with hi
      · exact y.2 hi
      · exact H i hi

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
this : ∀ (x : ℤ), Odd x → x ^ 2 ^ (i + 1) % 4 = 1
⊢ ¬4 ∣ x ^ 2 ^ (i + 1) + y ^ 2 ^ (i + 1)

Tactic:
Int.dvd_iff_emod_eq_zero,

Goal state after:
x y : ℤ
hx : ¬2 ∣ x
hxy : 4 ∣ x - y
hx_odd : Odd x
hxy_even : Even (x - y)
hy_odd : Odd y
i : ℕ
this : ∀ (x : ℤ), Odd x → x ^ 2 ^ (i + 1) % 4 = 1
⊢ ¬(x ^ 2 ^ (i + 1) + y ^ 2 ^ (i + 1)) % 4 = 0
Module: Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
inst✝ : (i : ι) → TopologicalSpace (R i)
hAopen : ∀ (i : ι), IsOpen[inst✝ i] (A i)
⊢ IsOpen[topologicalSpace R A cofinite] (range (structureMap R A cofinite))

Tactic:
by
    rw [range_structureMap]
    exact isOpen_forall_mem hAopen

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ 4 ∣ x ^ 2 - y ^ 2

Tactic:
Int.dvd_iff_emod_eq_zero,

Goal state after:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ (x ^ 2 - y ^ 2) % 4 = 0
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 (mixedEmbedding.polarCoord K).target,
      (∏ w, (x.2 w).1) • f (↑(mixedEmbedding.polarCoord K).symm x) =
    ∫ (x : realMixedSpace K), f ((mixedSpaceToRealMixedSpace K).symm x) ∂volume

Tactic:
← integral_comp_polarCoordReal_symm,

Goal state after:
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 (mixedEmbedding.polarCoord K).target,
      (∏ w, (x.2 w).1) • f (↑(mixedEmbedding.polarCoord K).symm x) =
    ∫ (x : realMixedSpace K) in (polarCoordReal K).target,
      (∏ w, (x.2 w).1) • f ((mixedSpaceToRealMixedSpace K).symm (↑(polarCoordReal K).symm x))
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
hu : ¬IsMaxRank u
⊢ ¬LinearIndependent ℝ fun i ↦ of (fun i ↦ (logEmbedding K) (Additive.ofMul (u ((equivFinRank K).symm i)))) i

Tactic:
rwa [IsMaxRank, ← linearIndependent_equiv (equivFinRank K).symm] at hu

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

Goal state before:
pp: case refine_2.refine_1.inr
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha₁ : a ∈ A
ha₂ : a ∈ {x | ∀ (w : { w // w.IsReal }), 0 < x.1 w}
w : InfinitePlace K
hw : w.IsComplex
⊢ normAtAllPlaces a w = normAtComplexPlaces a w

Tactic:
rw [normAtAllPlaces_apply, normAtPlace_apply_of_isComplex hw,
          normAtComplexPlaces_apply_isComplex ⟨w, hw⟩]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
⊢ normAtAllPlaces '' A ∩ ⋂ w, {x | x ↑w ≠ 0} = normAtComplexPlaces '' plusPart A

Tactic:
ext x
  refine ⟨?_, ?_⟩
  · rintro ⟨⟨a, ha, rfl⟩, ha₂⟩
    refine ⟨mixedSpaceOfRealSpace (normAtAllPlaces a), ⟨?_, ?_⟩, ?_⟩
    · rw [← hA, Set.mem_preimage, normAtAllPlaces_normAtAllPlaces]
      exact Set.mem_image_of_mem normAtAllPlaces ha
    · intro w
      refine lt_of_le_of_ne' (normAtPlace_nonneg _ _) (Set.mem_iInter.mp ha₂ w)
    · rw [normAtComplexPlaces_normAtAllPlaces]
  · rintro ⟨a, ⟨ha₁, ha₂⟩, rfl⟩
    refine ⟨⟨a, ha₁, funext fun w ↦ ?_⟩, Set.mem_iInter.mpr fun w ↦ ?_⟩
    · obtain hw | hw := isReal_or_isComplex w
      · simpa [normAtComplexPlaces_apply_isReal ⟨w, hw⟩, normAtPlace_apply_of_isReal hw]
          using (ha₂ ⟨w, hw⟩).le
      · rw [normAtAllPlaces_apply, normAtPlace_apply_of_isComplex hw,
          normAtComplexPlaces_apply_isComplex ⟨w, hw⟩]
    · simpa [Set.mem_ofPred_eq, normAtComplexPlaces_apply_isReal] using (ha₂ w).ne'

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

Goal state before:
pp: case refine_1
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
h : L = ⊥
⊢ maximalRealSubfield K ≤ E

Tactic:
← SetLike.coe_set_eq,

Goal state after:
case refine_1
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
h : ↑L = ↑⊥
⊢ maximalRealSubfield K ≤ E
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: case refine_1
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
h : ↑(E ⊔ maximalRealSubfield K) = ↑⊥
⊢ E ⊔ maximalRealSubfield K = E

Tactic:
← SetLike.coe_set_eq,

Goal state after:
case refine_1
K : Type u_2
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : Algebra.IsIntegral ℚ K
inst✝² : IsTotallyComplex K
E : Subfield K
inst✝¹ : IsTotallyReal ↥E
inst✝ : IsQuadraticExtension (↥E) K
L : IntermediateField (↥E) K := (E ⊔ maximalRealSubfield K).toIntermediateField ⋯
h : ↑(E ⊔ maximalRealSubfield K) = ↑⊥
⊢ ↑(E ⊔ maximalRealSubfield K) = ↑E
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) =
    Real.exp (x w₀) •
      Real.exp 0 • fun w ↦
        ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ if ↑i = w₀ then 0 else x ↑i

Tactic:
smul_smul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) =
    (Real.exp (x w₀) * Real.exp 0) • fun w ↦
      ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ if ↑i = w₀ then 0 else x ↑i
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ (Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i) =
    Real.exp (x w₀) • fun w ↦
      ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ if ↑i = w₀ then 0 else x ↑i

Tactic:
conv_rhs =>
    enter [2, w, 2, i]
    rw [if_neg i.prop]

Goal state after:
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, 1 • deriv_expMap_single x_1 ((completeBasis K).equivFun.symm x x_1)) *
        LinearMap.det ↑↑(completeBasis K).equivFunL.symm| =
    Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K

Tactic:
one_smul,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ |(∏ x_1, deriv_expMap_single x_1 ((completeBasis K).equivFun.symm x x_1)) *
        LinearMap.det ↑↑(completeBasis K).equivFunL.symm| =
    Real.exp (x w₀ * ↑(finrank ℚ K)) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : InfinitePlace K
h✝ : x✝ = w₀
⊢ MeasurableSet (Set.Iic 0)

pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : InfinitePlace K
h✝ : ¬x✝ = w₀
⊢ MeasurableSet (Set.Ico 0 1)

Tactic:
· exact measurableSet_Iic

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x✝ : InfinitePlace K
h✝ : ¬x✝ = w₀
⊢ MeasurableSet (Set.Ico 0 1)
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
R : Type u_2
inst✝¹ : CommRing R
inst✝ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
χ : DirichletCharacter R n
H : Subgroup Gal(K/ℚ)
⊢ χ ∈ OrderDual.ofDual ((subgroupGalEquivSubgroupChar n K R) H) ↔ ∀ σ ∈ H, χ ↑((galEquivZMod n K) σ) = 1

Tactic:
simp [subgroupGalEquivSubgroupChar]

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

Goal state before:
pp: n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this✝⁴ : IsAbelianGalois ℚ K
this✝³ : NeZero m
this✝² : NeZero n
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this✝¹ : IsCyclotomicExtension {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left✝ : Pₘ.IsMaximal
right✝¹ : Pₘ.LiesOver 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right✝ : Pₚ.LiesOver 𝒑
this : Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) = 1
⊢ 𝒑.inertiaDegIn (𝓞 K) = orderOf ↑p ∧ 𝒑.ramificationIdxIn (𝓞 K) = p ^ k * (p - 1)

Tactic:
← inertiaDegIn_mul_inertiaDegIn 𝒑 Pₘ Gal(Fₘ/ℚ) _ Gal(K/ℚ) Gal(K/Fₘ),

Goal state after:
n m p k : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : n = p ^ (k + 1) * m
hm : ¬p ∣ m
this✝⁴ : IsAbelianGalois ℚ K
this✝³ : NeZero m
this✝² : NeZero n
ζ : K := zeta n ℚ K
hζ : IsPrimitiveRoot (zeta n ℚ K) n
ζₘ : K := ζ ^ p ^ (k + 1)
hζₘ : IsPrimitiveRoot (zeta n ℚ K ^ p ^ (k + 1)) m
Fₘ : IntermediateField ℚ K := ℚ⟮ζₘ⟯
this✝¹ : IsCyclotomicExtension {m} ℚ ↥Fₘ
Pₘ : Ideal (𝓞 ↥Fₘ)
left✝ : Pₘ.IsMaximal
right✝¹ : Pₘ.LiesOver 𝒑
ζₚ : K := ζ ^ m
hζₚ : IsPrimitiveRoot (zeta n ℚ K ^ m) (p ^ (k + 1))
Fₚ : IntermediateField ℚ K := ℚ⟮ζₚ⟯
this✝ : IsCyclotomicExtension {p ^ (k + 1)} ℚ ↥Fₚ
Pₚ : Ideal (𝓞 ↥Fₚ)
hP₁ : Pₚ.IsMaximal
right✝ : Pₚ.LiesOver 𝒑
this : Pₚ.ramificationIdxIn (𝓞 K) * Pₘ.inertiaDegIn (𝓞 K) = 1
⊢ 𝒑.inertiaDegIn (𝓞 ↥Fₘ) * Pₘ.inertiaDegIn (𝓞 K) = orderOf ↑p ∧ 𝒑.ramificationIdxIn (𝓞 K) = p ^ k * (p - 1)