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

Goal state before:
pp: case mp
N : ℕ
A : ↥(Gamma0 N)
⊢ A ∈ Gamma1' N → ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0

pp: case mpr
N : ℕ
A : ↥(Gamma0 N)
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0 → A ∈ Gamma1' N

Tactic:
· intro ha
    have adet : (A.1.1.det : ZMod N) = 1 := by simp only [A.1.property, Int.cast_one]
    rw [Matrix.det_fin_two] at adet
    simp only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk, OneHom.coe_mk, Int.cast_sub,
      Int.cast_mul] at *
    simpa only [Gamma1_mem', Gamma0Map, MonoidHom.coe_mk, OneHom.coe_mk, Int.cast_sub,
      Int.cast_mul, ha, Gamma0_mem.mp A.property, and_self_iff, and_true, mul_one, mul_zero,
      sub_zero] using adet

Goal state after:
case mpr
N : ℕ
A : ↥(Gamma0 N)
⊢ ↑(↑↑A 0 0) = 1 ∧ ↑(↑↑A 1 1) = 1 ∧ ↑(↑↑A 1 0) = 0 → A ∈ Gamma1' N
Module: Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups

Goal state before:
pp: n : Type u_1
inst✝⁶ : Fintype n
inst✝⁵ : DecidableEq n
R : Type u_2
inst✝⁴ : Ring R
inst✝³ : TopologicalSpace R
inst✝² : IsTopologicalRing R
inst✝¹ : T2Space R
𝒢 : Subgroup (GL n R)
inst✝ : DiscreteTopology ↥𝒢
⊢ DiscreteTopology ↥𝒢.adjoinNegOne

Tactic:
rwa [𝒢.commensurable_adjoinNegOne_self.discreteTopology_iff]

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : DecidableEq K
L : Type u_2
inst✝¹ : Field L
inst✝ : DecidableEq L
f : K →+* L
g : GL (Fin 2) K
c : OnePoint K
⊢ OnePoint.map (⇑f) (g • c) = (GeneralLinearGroup.map f) g • OnePoint.map (⇑f) c

Tactic:
cases c with

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : DecidableEq K
g : GL (Fin 2) K
inst✝ : NeZero 2
c : OnePoint K
hg : ↑g ∉ Set.range ⇑(Matrix.scalar (Fin 2))
hdisc : (↑g 0 0 + ↑g 1 1) ^ 2 - 4 * (↑g 0 0 * ↑g 1 1 - ↑g 0 1 * ↑g 1 0) = 0
⊢ g • c = c ↔ c = g.parabolicFixedPoint

Tactic:
cases c with

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

Goal state before:
pp: K : Type u_1
inst✝³ : Field K
inst✝² : DecidableEq K
inst✝¹ : LinearOrder K
inst✝ : IsStrictOrderedRing K
g : GL (Fin 2) K
hg : g.IsElliptic
c : OnePoint K
⊢ g • c ≠ c

Tactic:
cases c with

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

Goal state before:
pp: K : Type u_1
inst✝⁶ : Field K
inst✝⁵ : DecidableEq K
A : Type u_2
inst✝⁴ : CommRing A
inst✝³ : IsDomain A
inst✝² : Algebra A K
inst✝¹ : IsFractionRing A K
inst✝ : IsPrincipalIdealRing A
c : OnePoint K
⊢ ∃ g, (mapGL K) g • ∞ = c

Tactic:
cases c with

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

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
h : ∞.IsBoundedAt f k
⊢ IsBoundedAtImInfty f

Tactic:
by simpa using h 1 (by simp)

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

Goal state before:
pp: f : ℍ → ℂ
k : ℤ
h : ∞.IsZeroAt f k
⊢ IsZeroAtImInfty f

Tactic:
by simpa using h 1 (by simp)

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

Goal state before:
pp: R : Type u_1
inst✝ : Ring R
𝒢 : Subgroup (GL (Fin 2) R)
⊢ 𝒢.strictPeriods ≤ 𝒢.periods

Tactic:
by
  intro k
  simp only [Subgroup.periods, strictPeriods]
  apply 𝒢.le_adjoinNegOne

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

Goal state before:
pp: Γ : Subgroup (GL (Fin 2) ℝ)
k : ℤ
f g : ModularForm Γ k
c✝ : OnePoint ℝ
hc : IsCusp c✝ Γ
⊢ c✝.IsBoundedAt ({ toFun := ⇑f, slash_action_eq' := ⋯ } + { toFun := ⇑g, slash_action_eq' := ⋯ }).toFun k

Tactic:
simpa using (f.bdd_at_cusps' hc).add (g.bdd_at_cusps' hc)

Goal state after:
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: g : SL(2, ℤ)
hc : ↑g 1 0 = 1
hg : 1 = (↑g).det
⊢ ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1

Tactic:
rw [det_fin_two, hc] at hg

Goal state after:
g : SL(2, ℤ)
hc : ↑g 1 0 = 1
hg : 1 = ↑g 0 0 * ↑g 1 1 - ↑g 0 1 * 1
⊢ ↑g 0 1 = ↑g 0 0 * ↑g 1 1 - 1
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: N r : ℕ
a : Fin 2 → ZMod N
inst✝ : NeZero r
γ : SL(2, ℤ)
v : ↑(gammaSet N r (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)))
this :
  ↑v ᵥ* ↑γ⁻¹ ∈
    gammaSet N r
      (a ᵥ*
        (↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ) *
          ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ⁻¹)))
⊢ ↑v ᵥ* ↑γ⁻¹ ∈ gammaSet N r a

Tactic:
← SpecialLinearGroup.coe_mul

Goal state after:
N r : ℕ
a : Fin 2 → ZMod N
inst✝ : NeZero r
γ : SL(2, ℤ)
v : ↑(gammaSet N r (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)))
this :
  ↑v ᵥ* ↑γ⁻¹ ∈
    gammaSet N r
      (a ᵥ*
        ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ *
            (SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ⁻¹))
⊢ ↑v ᵥ* ↑γ⁻¹ ∈ gammaSet N r a
Module: Mathlib.NumberTheory.ModularForms.EisensteinSeries.Defs

Goal state before:
pp: N : ℕ
a : Fin 2 → ZMod N
k : ℤ
γ : SL(2, ℤ)
⊢ eisensteinSeries a k ∣[k] γ = eisensteinSeries (a ᵥ* ↑((SpecialLinearGroup.map (Int.castRingHom (ZMod N))) γ)) k

Tactic:
ext1 z
  simp_rw [SL_slash_apply, zpow_neg,
    mul_inv_eq_iff_eq_mul₀ (zpow_ne_zero _ <| denom_ne_zero _ z),
    eisensteinSeries, eisSummand_SL2_apply, tsum_mul_left, mul_comm (_ ^ k)]
  congr 1
  exact (gammaSetEquiv a γ).tsum_eq (eisSummand k · z)

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

Goal state before:
pp: case hf
z : ℍ
N : ℤ
⊢ Summable fun m ↦ 1 / (↑m * ↑z + ↑N) ^ 2

Tactic:
simpa using! linear_left_summable (ne_zero z) N le_rfl

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

Goal state before:
pp: z : ℍ
⊢ (G2 ∣[2] T) z = G2 z

Tactic:
simp_rw [SL_slash_def, modular_T_smul z]

Goal state after:
z : ℍ
⊢ G2 (1 +ᵥ z) *
      denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) T)) ↑z ^ (-2) =
    G2 z
Module: Mathlib.NumberTheory.ModularForms.Derivative

Goal state before:
pp: F : ℍ → ℂ
hF : DifferentiableOn ℂ (F ∘ ↑ofComplex) {z | 0 < z.im}
c : ℂ := (2 * ↑π * I)⁻¹
⊢ DifferentiableOn ℂ (fun z ↦ c * deriv (F ∘ ↑ofComplex) z) upperHalfPlaneSet

Tactic:
simpa [c] using (hF.deriv isOpen_upperHalfPlaneSet).const_mul ((2 * π * I)⁻¹)

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

Goal state before:
pp: k : ℕ
z : ℍ
⊢ ↑z ∈ ℍₒ

Tactic:
simpa using z.2

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

Goal state before:
pp: k : ℕ
hk : 1 ≤ k
z : ℍ
⊢ ↑z ∈ ℍₒ

Tactic:
simpa using z.2

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

Goal state before:
pp: z : ℍ
⊢ E2 z = 1 - 24 * ∑' (n : ℕ+), ↑((σ 1) ↑n) * cexp (2 * ↑π * I * ↑z) ^ ↑n

Tactic:
simp [E2, G2_eq_tsum_cexp, riemannZeta_two]
  field

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

Goal state before:
pp: k : ℕ
e : ℕ+
z : ℍ
⊢ 0 < (↑↑e * ↑z).im

Tactic:
simpa using z.2

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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
z : ℍ
b : ℕ+
⊢ 0 < (↑↑b * ↑z).im

Tactic:
simpa using z.2

Goal state after:
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ (↑π * I * ↑n ^ 2 * τ).re = -π * τ.im * ↑n ^ 2

Tactic:
(by push_cast; ring : (π * I * n ^ 2 * τ : ℂ) = (π * n ^ 2 : ℝ) * (τ * I)),

Goal state after:
τ : ℂ
hτ : 0 < τ.im
n : ℤ
y : ℝ := rexp (-π * τ.im)
h : y < 1
⊢ (↑(π * ↑n ^ 2) * (τ * I)).re = -π * τ.im * ↑n ^ 2
Module: Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable

Goal state before:
pp: τ : ℂ
hτ : 0 < τ.im
⊢ ‖jacobiTheta τ - 1‖ ≤ 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im)

Tactic:
by
  suffices ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ ≤
      rexp (-π * τ.im) / (1 - rexp (-π * τ.im)) by
    calc
      ‖jacobiTheta τ - 1‖ = ↑2 * ‖∑' n : ℕ, cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ := by
        rw [sub_eq_iff_eq_add'.mpr (jacobiTheta_eq_tsum_nat hτ), norm_mul, Complex.norm_two]
      _ ≤ 2 * (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) := by gcongr
      _ = 2 / (1 - rexp (-π * τ.im)) * rexp (-π * τ.im) := by rw [div_mul_comm, mul_comm]
  have : ∀ n : ℕ, ‖cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ ≤ rexp (-π * τ.im) ^ (n + 1) := by
    intro n
    simpa only [Int.cast_add, Int.cast_one] using! norm_exp_mul_sq_le hτ (n + 1)
  have s : HasSum (fun n : ℕ =>
      rexp (-π * τ.im) ^ (n + 1)) (rexp (-π * τ.im) / (1 - rexp (-π * τ.im))) := by
    simp_rw [pow_succ', div_eq_mul_inv, hasSum_mul_left_iff (Real.exp_ne_zero _)]
    exact hasSum_geometric_of_lt_one (exp_pos (-π * τ.im)).le
      (exp_lt_one_iff.mpr <| mul_neg_of_neg_of_pos (neg_lt_zero.mpr pi_pos) hτ)
  have aux : Summable fun n : ℕ => ‖cexp (π * I * ((n : ℂ) + 1) ^ 2 * τ)‖ :=
    .of_nonneg_of_le (fun n => norm_nonneg _) this s.summable
  exact (norm_tsum_le_tsum_norm aux).trans ((aux.tsum_mono s.summable this).trans_eq s.tsum_eq)

Goal state after:
Module: Mathlib.Topology.Algebra.Group.DiscontinuousSubgroup

Goal state before:
pp: Γ : Type u_1
α : Type u_2
inst✝² : Group Γ
inst✝¹ : TopologicalSpace α
inst✝ : SMul Γ α
S : Subgroup Γ
K L : Set α
hK : IsCompact K
hL : IsCompact L
⊢ {m | (m • K ∩ L).Nonempty}.Finite ↔ {g | g ∈ S ∧ (g • K ∩ L).Nonempty}.Finite

Tactic:
convert! injOn_subtype_val (s := {m : S | (m • K ∩ L).Nonempty}) |>.bijOn_image.finite_iff_finite

Goal state after:
Γ : Type u_1
α : Type u_2
inst✝² : Group Γ
inst✝¹ : TopologicalSpace α
inst✝ : SMul Γ α
S : Subgroup Γ
K L : Set α
hK : IsCompact K
hL : IsCompact L
⊢ {g | g ∈ S ∧ (g • K ∩ L).Nonempty} = Subtype.val '' {m | (m • K ∩ L).Nonempty}
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: 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)

Tactic:
apply Finset.dvd_sum

Goal state after:
case succ
R : Type u_1
inst✝ : CommRing R
p x : R
n : ℕ
⊢ ∀ i ∈ range n, p ^ 2 ∣ x ^ i * p ^ (n + 1 - i) * ↑((n + 1).choose i)
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
this : ∀ x ∈ range p, a ^ (x + (p - 1 - x)) = a ^ (p - 1)
⊢ (Ideal.Quotient.mk (span {s})) (∑ x ∈ range p, a ^ (x + (p - 1 - x))) =
    (Ideal.Quotient.mk (span {s})) (∑ _x ∈ range p, a ^ (p - 1))

Tactic:
rw [Finset.sum_congr rfl this]

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

Goal state before:
pp: case refine_1
Γ : 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 ∈ Set.Ioi 0,
    HasSum
      (fun i ↦
        if 2 * ↑i / h Γ = 0 then 0 else (PowerSeries.coeff i) (qExpansion (h Γ) ⇑f) * ↑(rexp (-π * (2 * ↑i / h Γ) * t)))
      ((weakFEPair hk f).f t - (weakFEPair hk f).f₀)

Tactic:
intro t (ht : 0 < t)
    have := hasSum_qExpansion f hh hΓ (ofComplex (I * t))
    convert! hasSum_ite_sub_hasSum this 0 using 2 with n
    · rcases Nat.eq_zero_or_pos n with rfl | hn
      · simp
      · simp [hn.ne', Function.Periodic.qParam, ofComplex_apply_eq_ite, ht, ← exp_nat_mul]
        grind [I_sq]
    · simp only [weakFEPair]
      rw [qExpansion_coeff_zero hh, pow_zero, mul_one]
      · exact ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ
      · exact SlashInvariantFormClass.periodic_comp_ofComplex f hΓ

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : v.IsReal
x : v.Completion
⊢ ↑((extensionEmbeddingOfIsReal hv) x) = (extensionEmbedding v) x

Tactic:
by
  induction x using induction_on with
  | hp =>
    exact isClosed_eq
      (Complex.continuous_ofReal.comp (isometry_extensionEmbeddingOfIsReal hv).continuous)
      (isometry_extensionEmbedding v).continuous
  | ih a => simp

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ emultiplicity p (x ^ n - y ^ n) = emultiplicity p (x - y) + emultiplicity p n

pp: x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ n ≠ 0

pp: x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ x - y ≠ 0

pp: x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ x ^ n - y ^ n ≠ 0

Tactic:
· exact Nat.emultiplicity_pow_sub_pow hp.out hp1 hxy hx n

Goal state after:
x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ n ≠ 0

x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ x - y ≠ 0

x y p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hyx : y < x
hxy : p ∣ x - y
hx : ¬p ∣ x
n : ℕ
hn : n ≠ 0
⊢ x ^ n - y ^ n ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x✝ : { w // w ≠ w₀ }
⊢ logMap (c • 1) x✝ = 0 x✝

Tactic:
rw [logMap_apply, normAtPlace_smul, norm_smul, map_one, map_one, mul_one, mul_one, Real.log_pow,
    mul_comm (finrank ℚ K : ℝ) _, mul_assoc, mul_inv_cancel₀ (Nat.cast_ne_zero.mpr finrank_pos.ne'),
    mul_one, sub_self, mul_zero, Pi.zero_apply]

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
φ ψ : K →+* ℂ
σ τ : Gal(K/↥K⁺)
hφ : ComplexEmbedding.IsConj φ σ
hψ : ComplexEmbedding.IsConj ψ τ
⊢ σ = τ

Tactic:
have : Nat.card (K ≃ₐ[K⁺] K) = 2 :=
    (IsQuadraticExtension.finrank_eq_two K⁺ K) ▸ IsGalois.card_aut_eq_finrank K⁺ K
  rw [Nat.card_eq_two_iff' 1] at this
  exact ExistsUnique.unique this
    ((isConj_ne_one_iff hφ).mpr <| IsTotallyComplex.complexEmbedding_not_isReal φ)
    ((isConj_ne_one_iff hψ).mpr <| IsTotallyComplex.complexEmbedding_not_isReal ψ)

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

Goal state before:
pp: case refine_1
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : ↑x ∈ K⁺
this : IsIntegral ℤ ⟨↑x, h⟩
⊢ (algebraMap (𝓞 ↥K⁺) K) ⟨⟨↑x, h⟩, this⟩ = ↑x

Tactic:
IsScalarTower.algebraMap_apply (𝓞 K⁺) K⁺,

Goal state after:
case refine_1
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : Algebra.IsIntegral ℚ K
x : 𝓞 K
h : ↑x ∈ K⁺
this : IsIntegral ℤ ⟨↑x, h⟩
⊢ (algebraMap (↥K⁺) K) ((algebraMap (𝓞 ↥K⁺) ↥K⁺) ⟨⟨↑x, h⟩, this⟩) = ↑x
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 : ℝ
x✝ : ↑(integerSet K)
⊢ 1 • x✝ = x✝

Tactic:
by
    rw [Subtype.mk_eq_mk, integerSetTorsionSMul_smul_coe, OneMemClass.coe_one, one_smul]

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

Goal state before:
pp: case e'_2.e'_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
c : ℝ
J : ↥(Ideal (𝓞 K))⁰
n : ℕ
e_1✝ : { a // ↑(preimageOfMemIntegerSet a) ∈ ↑J } = ↑{a | ↑(preimageOfMemIntegerSet a) ∈ ↑↑J}
x✝ : { a // ↑(preimageOfMemIntegerSet a) ∈ ↑J }
⊢ mixedEmbedding.norm ↑↑x✝ = ↑n ↔ mixedEmbedding.norm ↑((idealSetEquiv K J).symm x✝) = ↑n

Tactic:
rw [idealSetEquiv_symm_apply]

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

Goal state before:
pp: case mem
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x x✝ : realSpace K
h : x✝ ∈ Set.range fun w ↦ completeFamily K ↑w
⊢ ∑ w, x✝ w = 0

Tactic:
obtain ⟨w, rfl⟩ := h
      simp_rw [completeFamily, dif_neg w.prop, sum_expMap_symm_apply (coe_ne_zero _),
        Units.norm, Rat.cast_one, Real.log_one]

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
⊢ |Real.exp (x w₀)| ^ finrank ℚ K * |(∏ w, ↑expMapBasis x ↑w)⁻¹| * |2⁻¹| ^ nrComplexPlaces K *
      (↑(finrank ℚ K) * regulator K) =
    Real.exp (x w₀) ^ ↑(finrank ℚ K) * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) *
      regulator K

Tactic:
Real.rpow_natCast,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ |Real.exp (x w₀)| ^ finrank ℚ K * |(∏ w, ↑expMapBasis x ↑w)⁻¹| * |2⁻¹| ^ nrComplexPlaces K *
      (↑(finrank ℚ K) * regulator K) =
    Real.exp (x w₀) ^ finrank ℚ K * (∏ w, ↑expMapBasis x ↑w)⁻¹ * 2⁻¹ ^ nrComplexPlaces K * ↑(finrank ℚ K) * regulator K
Module: Mathlib.NumberTheory.NumberField.Ideal.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
I : Ideal (𝓞 K)
inst✝ : NumberField K
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime (torsionOrder K)
⊢ Function.Injective ⇑I.torsionMapQuot

Tactic:
intro ⟨x, hx⟩

Goal state after:
K : Type u_1
inst✝¹ : Field K
I : Ideal (𝓞 K)
inst✝ : NumberField K
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime (torsionOrder K)
x : (𝓞 K)ˣ
hx : x ∈ torsion K
⊢ ∀ ⦃a₂ : ↥(torsion K)⦄, I.torsionMapQuot ⟨x, hx⟩ = I.torsionMapQuot a₂ → ⟨x, hx⟩ = a₂
Module: Mathlib.NumberTheory.NumberField.Ideal.Basic

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
I : Ideal (𝓞 K)
inst✝ : NumberField K
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime (torsionOrder K)
x : (𝓞 K)ˣ
hx : x ∈ torsion K
y : (𝓞 K)ˣ
hy : y ∈ torsion K
h : I.torsionMapQuot ⟨x, hx⟩ = I.torsionMapQuot ⟨y, hy⟩
⊢ ⟨x, hx⟩ = ⟨y, hy⟩

Tactic:
rw [← rootsOfUnity_eq_torsion] at hx hy

Goal state after:
K : Type u_1
inst✝¹ : Field K
I : Ideal (𝓞 K)
inst✝ : NumberField K
hI₁ : absNorm I ≠ 1
hI₂ : (absNorm I).Coprime (torsionOrder K)
x : (𝓞 K)ˣ
hx✝ : x ∈ torsion K
hx : x ∈ rootsOfUnity (torsionOrder K) (𝓞 K)
y : (𝓞 K)ˣ
hy✝ : y ∈ torsion K
hy : y ∈ rootsOfUnity (torsionOrder K) (𝓞 K)
h : I.torsionMapQuot ⟨x, hx✝⟩ = I.torsionMapQuot ⟨y, hy✝⟩
⊢ ⟨x, hx✝⟩ = ⟨y, hy✝⟩
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
x : 𝓞 K
hx : ¬hζ.toInteger - 1 ∣ x
⊢ IsCoprime (span {↑p}) (span {x})

Tactic:
← span_singleton_eq_span_singleton.mpr
    (associated_zeta_sub_one_pow_prime p hζ),

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
hK : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ p
x : 𝓞 K
hx : ¬hζ.toInteger - 1 ∣ x
⊢ IsCoprime (span {(hζ.toInteger - 1) ^ (p - 1)}) (span {x})
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Ideal

Goal state before:
pp: m p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
P : Ideal (𝓞 K)
hP₁ : P.IsPrime
hP₂ : P.LiesOver 𝒑
inst✝ : NeZero m
hK : IsCyclotomicExtension {m} ℚ K
hm : ¬p ∣ m
⊢ P.inertiaDeg ℤ = orderOf ↑p

Tactic:
replace hm : p.Coprime m := hp.out.coprime_iff_not_dvd.mpr hm
  let ζ := (zeta_spec m ℚ K).toInteger
  have h₁ : ¬ p ∣ exponent ζ := by
    rw [exponent_eq_one_iff.mpr <| adjoin_singleton_eq_top (zeta_spec m ℚ K)]
    exact hp.out.not_dvd_one
  have h₂ := (primesOverSpanEquivMonicFactorsMod h₁ ⟨P, ⟨inferInstance, inferInstance⟩⟩).2
  have h₃ := inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply' h₁ h₂
  simp only [Subtype.coe_eta, Equiv.symm_apply_apply] at h₃
  rw [Multiset.mem_toFinset, Polynomial.mem_normalizedFactors_iff
    (map_monic_ne_zero (minpoly.monic ζ.isIntegral))] at h₂
  have : P.IsMaximal := .of_liesOver_isMaximal P 𝒑
  rw [h₃, natDegree_of_dvd_cyclotomic_of_irreducible (by simp) hm (f := 1) _ h₂.1]
  · simpa using (orderOf_injective _ Units.coeHom_injective (ZMod.unitOfCoprime p hm)).symm
  · refine dvd_trans h₂.2.2 ?_
    rw [← map_cyclotomic_int, cyclotomic_eq_minpoly (zeta_spec m ℚ K) (NeZero.pos _),
      ← (zeta_spec m ℚ K).coe_toInteger, ← RingOfIntegers.minpoly_coe ζ]
    simp [ζ]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
⊢ ↑({x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} ∩
        ⇑↑↑(toMixed K) ⁻¹' ↑(idealLattice K ((FractionalIdeal.mk0 K) J))) ≃
    { a // mixedEmbedding.norm ↑a ≤ s }

Tactic:
refine (((toMixed K).toEquiv.image _).trans (Equiv.subtypeEquivProp ?_)).trans
    (Equiv.subtypeSubtypeEquivSubtypeInter _ (mixedEmbedding.norm · ≤ s)).symm

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
⊢ (fun x ↦
      x ∈
        ⇑(↑(toMixed K)).toEquiv ''
          ({x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} ∩
            ⇑↑↑(toMixed K) ⁻¹' ↑(idealLattice K ((FractionalIdeal.mk0 K) J)))) =
    fun x ↦ x ∈ idealSet K J ∧ mixedEmbedding.norm x ≤ s
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Tendsto (fun s ↦ ↑(Nat.card { I // ↑(absNorm I) ≤ s }) / s) atTop
    (𝓝
      (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * ↑(classNumber K) /
        (↑(torsionOrder K) * √|↑(discr K)|)))

Tactic:
have := (tendsto_norm_le_div_atTop₀ K).add tendsto_inv_atTop_zero

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this :
  Tendsto (fun x ↦ ↑(Nat.card { I // ↑(absNorm ↑I) ≤ x }) / x + x⁻¹) atTop
    (𝓝
      (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * ↑(classNumber K) /
          (↑(torsionOrder K) * √|↑(discr K)|) +
        0))
⊢ Tendsto (fun s ↦ ↑(Nat.card { I // ↑(absNorm I) ≤ s }) / s) atTop
    (𝓝
      (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * ↑(classNumber K) /
        (↑(torsionOrder K) * √|↑(discr K)|)))
Module: Mathlib.NumberTheory.PrimesCongruentOne

Goal state before:
pp: case inl
n : ℕ
hk0 : 1 ≠ 0
p : ℕ
hnp : n + 1 ≤ p
hp : Prime p
⊢ ∃ p, Prime p ∧ n < p ∧ p ≡ 1 [MOD 1]

Tactic:
exact ⟨p, hp, hnp, modEq_one⟩

Goal state after:
Module: Mathlib.NumberTheory.RatFunc.Ostrowski

Goal state before:
pp: case refine_1
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
a : K
hπᵥ : v (C a) < 1 ∧ Polynomial.C a ≠ 0
ha0 : a ≠ 0
ha : Polynomial.C a = πᵥ
⊢ False

Tactic:
← algebraMap_eq_C

Goal state after:
case refine_1
K : Type u_1
Γ : Type u_2
inst✝² : Field K
inst✝¹ : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝ : IsTrivialOn K v
hne : {p | v ↑p < 1 ∧ p ≠ 0}.Nonempty
πᵥ : K[X] := ⋯.min {p | v ↑p < 1 ∧ p ≠ 0} hne
a : K
hπᵥ : v ((algebraMap K K⟮X⟯) a) < 1 ∧ Polynomial.C a ≠ 0
ha0 : a ≠ 0
ha : Polynomial.C a = πᵥ
⊢ False