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

Goal state before:
pp: k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(2 * ↑k / ↑(bernoulli k))
c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑((σ (k - 1)) m)
τ : ℍ
hS : Summable fun n ↦ ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
⊢ HasSum (fun n ↦ β * ↑((σ (k - 1)) (n + 1)) * 𝕢 1 ↑τ ^ (n + 1)) ((E hk) τ - 1)

Tactic:
have hval : E hk τ - 1 = β * ∑' n : ℕ, (σ (k - 1) (n + 1)) * cexp (2 * π * I * τ) ^ (n + 1) := by
    have := q_expansion_bernoulli hk hk2 τ
    simp_rw [zpow_natCast] at this
    rw [this, ← tsum_pnat_eq_tsum_succ (f := fun n ↦ (σ (k - 1) n : ℂ) * cexp (2 * π * I * τ) ^ n)]
    ring

Goal state after:
k : ℕ
hk : 3 ≤ k
hk2 : Even k
m : ℕ
β : ℂ := -(2 * ↑k / ↑(bernoulli k))
c : ℕ → ℂ := fun m ↦ if m = 0 then 1 else β * ↑((σ (k - 1)) m)
τ : ℍ
hS : Summable fun n ↦ ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
hval : (E hk) τ - 1 = β * ∑' (n : ℕ), ↑((σ (k - 1)) (n + 1)) * cexp (2 * ↑π * I * ↑τ) ^ (n + 1)
⊢ HasSum (fun n ↦ β * ↑((σ (k - 1)) (n + 1)) * 𝕢 1 ↑τ ^ (n + 1)) ((E hk) τ - 1)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case mpr
y : ℝ
z : ℂ
⊢ z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖} → z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y

Tactic:
rintro ⟨hz, h1, h2, h3⟩

Goal state after:
case mpr
y : ℝ
z : ℂ
hz : 0 ≤ z.im
h1 : z.im ≤ y
h2 : |z.re| ≤ 1 / 2
h3 : 1 ≤ ‖z‖
⊢ z ∈ UpperHalfPlane.coe '' truncatedFundamentalDomain y
Module: Mathlib.NumberTheory.ModularForms.LevelOne.GradedRing

Goal state before:
pp: ⊢ (PowerSeries.coeff 1) (qExpansion 1 ⇑E₄CubeSubE₆SqForm) = 1728

Tactic:
E₄CubeSubE₆SqForm_qExpansion_eq

Goal state after:
⊢ (PowerSeries.coeff 1) (qExpansion 1 ⇑E₄ * qExpansion 1 ⇑E₄ * qExpansion 1 ⇑E₄ - qExpansion 1 ⇑E₆ * qExpansion 1 ⇑E₆) =
    1728
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case h₂
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ z.im ^ 2 ≤ y ^ 2

Tactic:
rw [sq_le_sq₀ hz.1 (hz.1.trans hz.2.1)]

Goal state after:
case h₂
y : ℝ
z : ℂ
hz : z ∈ {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
⊢ z.im ≤ y
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: case e'_6.e'_6.hfanalytic
Γ : 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)))
⊢ AnalyticAt ℂ (cuspFunction (h Γ) ⇑f) 0

Tactic:
exact ModularFormClass.analyticAt_cuspFunction_zero f hh hΓ

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

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

Tactic:
simp only [pow_zero, pow_one, range_zero, prod_empty, one_mul]

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

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

Tactic:
refine hasSum_Λ_of_qExpansion_isBigO hk f (r := k / 2)
    (by linarith [show (0 : ℝ) < k from mod_cast hk]) hs ?_ ?_
  · simp [Λ_eq_mellin, (CuspFormClass.zero_at_infty f).valueAtInfty_eq_zero]
  · simpa using CuspFormClass.qExpansion_isBigO f

Goal state after:
Module: Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing

Goal state before:
pp: R : Type u_1
inst✝⁴ : CommRing R
inst✝³ : IsDedekindDomain R
K : Type u_2
inst✝² : Field K
inst✝¹ : Algebra R K
inst✝ : IsFractionRing R K
k : K
⊢ ∀ᶠ (i : HeightOneSpectrum R) in Filter.cofinite,
    (fun i ↦ { toCompletion := ↑((WithVal.equiv (valuation K i)).symm k) }) i ∈
      (fun v ↦ ↑(adicCompletionIntegers K v)) i

Tactic:
by
    simp only [Filter.eventually_cofinite, SetLike.mem_coe, mem_adicCompletionIntegers R K,
     valuedAdicCompletion_eq_valuation', not_le]
    exact HeightOneSpectrum.Support.finite R k

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

Goal state before:
pp: ι : Type u_1
R : ι → Type u_2
A : (i : ι) → Set (R i)
𝓕✝ 𝓖 : Filter ι
S : ι → Type u_3
inst✝⁴ : (i : ι) → SetLike (S i) (R i)
B : (i : ι) → S i
T : Set ι
𝓕 : Filter ι
inst✝³ : (i : ι) → TopologicalSpace (R i)
hBopen : Fact (∀ (i : ι), IsOpen[inst✝³ i] ↑(B i))
inst✝² : (i : ι) → Mul (R i)
inst✝¹ : ∀ (i : ι), MulMemClass (S i) (R i)
inst✝ : ∀ (i : ι), ContinuousMul (R i)
⊢ Continuous[instTopologicalSpaceProd, topologicalSpace R (fun i ↦ ↑(B i)) cofinite] fun p ↦ p.1 * p.2

Tactic:
rw [continuous_dom_prod hBopen.out hBopen.out]
    exact fun S hS ↦ (continuous_inclusion hS).comp continuous_mul

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
hx : x ∈ fundamentalCone K
hy : ∀ (w : InfinitePlace K), (normAtPlace w) y = (normAtPlace w) x
⊢ logMap y ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))

Tactic:
logMap_eq_of_normAtPlace_eq hy

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : mixedSpace K
hx : x ∈ fundamentalCone K
hy : ∀ (w : InfinitePlace K), (normAtPlace w) y = (normAtPlace w) x
⊢ logMap x ∈ ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K))
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
⊢ ∀ (x y : (𝓞 K)ˣ),
    ⟨x * y * ((unitsComplexConj K) (x * y))⁻¹, ⋯⟩ =
      ⟨x * ((unitsComplexConj K) x)⁻¹, ⋯⟩ * ⟨y * ((unitsComplexConj K) y)⁻¹, ⋯⟩

Tactic:
intro _ _
    rw [MulMemClass.mk_mul_mk, Subtype.mk_eq_mk]
    apply coe_injective
    simp only [map_mul, mul_inv_rev, Units.val_mul, map_units_inv]
    ring

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x y : realSpace K
⊢ ↑expMap (x + y) = ↑expMap x * ↑expMap y

Tactic:
by
  ext
  simp [mul_add, Real.exp_add]

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
w : InfinitePlace K
hw : w ≠ w₀
⊢ ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr
          (logMap (Real.exp (x w₀) • mixedSpaceOfRealSpace (↑expMapBasis fun i ↦ if i = w₀ then 0 else x i))))
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1

Tactic:
logMap_real_smul (norm_expMapBasis_ne_zero _)
    (Real.exp_ne_zero _),

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
w : InfinitePlace K
hw : w ≠ w₀
⊢ ((Basis.ofZLatticeBasis ℝ (unitLattice K) (basisUnitLattice K)).repr
          (logMap (mixedSpaceOfRealSpace (↑expMapBasis fun i ↦ if i = w₀ then 0 else x i))))
        (equivFinRank.symm ⟨w, hw⟩) ∈
      Set.Ico 0 1 ↔
    x w ∈ Set.Ico 0 1
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: n✝ j : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
n : ℕ
hζ : IsPrimitiveRoot ζ (n + 2)
hj : j.Coprime (n + 2)
⊢ ζ ^ j - 1 ∣ ζ - 1

Tactic:
obtain ⟨m, -, hm⟩ := exists_mul_mod_eq_one_of_coprime hj (by lia)
      use ∑ i ∈ range m, (ζ ^ j) ^ i
      rw [mul_geom_sum, ← pow_mul, ← pow_mod_orderOf, ← hζ.eq_orderOf, hm, pow_one]

Goal state after:
Module: Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits

Goal state before:
pp: p✝ : ℕ
A✝ : Type u_1
ζ✝ : A✝
inst✝³ : CommRing A✝
inst✝² : IsDomain A✝
p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ ↑(nthRootsFinset p 1)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ ↑(nthRootsFinset p 1)
e : ζ ^ i ≠ ζ ^ j
hij : j ≤ i
H : (i - j).Coprime p
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)

Tactic:
obtain ⟨u, h⟩ := hζ.associated_pow_add_sub_sub_one hp.two_le j H

Goal state after:
p✝ : ℕ
A✝ : Type u_1
ζ✝ : A✝
inst✝³ : CommRing A✝
inst✝² : IsDomain A✝
p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
this : NeZero p
i : ℕ
hi : i < p
hη₁ : ζ ^ i ∈ ↑(nthRootsFinset p 1)
j : ℕ
hj : j < p
hη₂ : ζ ^ j ∈ ↑(nthRootsFinset p 1)
e : ζ ^ i ≠ ζ ^ j
hij : j ≤ i
H : (i - j).Coprime p
u : Aˣ
h : (ζ - 1) * ↑u = ζ ^ (j + (i - j)) - ζ ^ j
⊢ Associated (ζ - 1) (ζ ^ i - ζ ^ j)
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
this : IsBounded (↑expMapBasis '' paramSet K)
⊢ IsBounded (normAtAllPlaces ⁻¹' ↑expMapBasis '' paramSet K)

Tactic:
obtain ⟨C, hC⟩ := isBounded_iff_forall_norm_le.mp this
    refine isBounded_iff_forall_norm_le.mpr ⟨C, fun x hx ↦ ?_⟩
    rw [norm_eq_sup'_normAtPlace]
    refine sup'_le _ _ fun w _ ↦ ?_
    simpa [normAtAllPlaces_apply, Real.norm_of_nonneg (normAtPlace_nonneg w x)]
      using (pi_norm_le_iff_of_nonempty _).mp (hC _ hx) w

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
h : m = 0
⊢ False

Tactic:
simp [h] at hm

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
R : Type u_2
inst✝² : CommRing R
inst✝¹ : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)
inst✝ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
⊢ Nat.card
      ↥(OrderDual.ofDual
          (OrderDual.ofDual
            (OrderDual.toDual
              ((subgroupGalEquivSubgroupChar n K R) (OrderDual.ofDual (OrderDual.toDual F.fixingSubgroup)))))) =
    Module.finrank ℚ ↥F

Tactic:
OrderDual.ofDual_toDual,

Goal state after:
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)ˣ)
inst✝ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
⊢ Nat.card
      ↥(OrderDual.ofDual
          ((subgroupGalEquivSubgroupChar n K R) (OrderDual.ofDual (OrderDual.toDual F.fixingSubgroup)))) =
    Module.finrank ℚ ↥F
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)ˣ)
inst✝ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
⊢ Nat.card
      ↥(OrderDual.ofDual
          ((subgroupGalEquivSubgroupChar n K R) (OrderDual.ofDual (OrderDual.toDual F.fixingSubgroup)))) =
    Module.finrank ℚ ↥F

Tactic:
OrderDual.ofDual_toDual,

Goal state after:
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)ˣ)
inst✝ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
⊢ Nat.card ↥(OrderDual.ofDual ((subgroupGalEquivSubgroupChar n K R) F.fixingSubgroup)) = Module.finrank ℚ ↥F
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)ˣ)
inst✝³ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
m : ℕ
inst✝² : NeZero m
inst✝¹ : IsGalois ℚ ↥F
inst✝ : IsCyclotomicExtension {m} ℚ ↥F
hdiv : m ∣ n
χ : DirichletCharacter R n
⊢ (∀ (σ : Gal(K/ℚ)), (∀ x ∈ F, σ x = x) → χ ↑((galEquivZMod n K) σ) = 1) ↔
    ∀ (a : Gal(K/ℚ)), (∀ x ∈ F, a x = x) → ↑((equivToUnitHom χ) ((galEquivZMod n K) a)) = ↑1

Tactic:
coe_equivToUnitHom,

Goal state after:
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)ˣ)
inst✝³ : IsAbelianGalois ℚ K
F : IntermediateField ℚ K
m : ℕ
inst✝² : NeZero m
inst✝¹ : IsGalois ℚ ↥F
inst✝ : IsCyclotomicExtension {m} ℚ ↥F
hdiv : m ∣ n
χ : DirichletCharacter R n
⊢ (∀ (σ : Gal(K/ℚ)), (∀ x ∈ F, σ x = x) → χ ↑((galEquivZMod n K) σ) = 1) ↔
    ∀ (a : Gal(K/ℚ)), (∀ x ∈ F, a x = x) → χ ↑((galEquivZMod n K) a) = ↑1
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α β : K
⊢ house (α * β) ≤ house α * house β

Tactic:
simp only [house, map_mul]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α β : K
⊢ ‖(canonicalEmbedding K) α * (canonicalEmbedding K) β‖ ≤ ‖(canonicalEmbedding K) α‖ * ‖(canonicalEmbedding K) β‖
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
α : K
σ : K →+* ℂ
⊢ ‖(Algebra.norm ℚ) α‖ ≤ ‖σ α‖ * house α ^ (finrank ℚ K - 1)

Tactic:
set σ' := σ.toRatAlgHom
  calc _ = ‖∏ τ : K →ₐ[ℚ] ℂ, τ α‖ := ?_
       _ = ‖(σ' α) * ∏ τ ∈ univ.erase σ', τ α‖ := by rw [mul_prod_erase univ (· α) (mem_univ σ')]
       _ ≤ ‖σ' α‖ * ∏ τ ∈ univ.erase σ', ‖τ α‖ := ?_
       _ ≤ ‖σ' α‖ * ∏ τ ∈ univ.erase σ', house α := by gcongr; apply norm_embedding_le_house
       _ = ‖σ' α‖ * house α ^ (Module.finrank ℚ K - 1) := by simp
  · rw [← Algebra.norm_eq_prod_embeddings, ← Rat.norm_cast_real,
      Real.norm_eq_abs, eq_ratCast, Complex.norm_ratCast]
  · rw [Complex.norm_mul]
    gcongr
    exact norm_prod_le (univ.erase σ') (· α)

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

Goal state before:
pp: K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
h0ph : 0 < p * h
hfinp : Fintype.card (α × (K →+* ℂ)) = p * h
hfinq : Fintype.card (β × (K →+* ℂ)) = q * h
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
hmulvec0 : asiegel K a *ᵥ x = 0
hxbound : ‖x‖ ≤ (↑q * ↑h * ‖asiegel K a‖) ^ (↑p * ↑h / (↑q * ↑h - ↑p * ↑h))
⊢ ∃ ξ, ξ ≠ 0 ∧ a *ᵥ ξ = 0 ∧ ∀ (l : β), house ↑(ξ l) ≤ c₁ K * (c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))

Tactic:
← sub_mul,

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
ha : a ≠ 0
p q : ℕ
h0p : 0 < p
hpq : p < q
inst✝² : Fintype β
cardβ : Fintype.card β = q
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
cardα : Fintype.card α = p
h : ℕ := finrank ℚ K
hphqh : p * h < q * h
h0ph : 0 < p * h
hfinp : Fintype.card (α × (K →+* ℂ)) = p * h
hfinq : Fintype.card (β × (K →+* ℂ)) = q * h
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
hmulvec0 : asiegel K a *ᵥ x = 0
hxbound : ‖x‖ ≤ (↑q * ↑h * ‖asiegel K a‖) ^ (↑p * ↑h / ((↑q - ↑p) * ↑h))
⊢ ∃ ξ, ξ ≠ 0 ∧ a *ᵥ ξ = 0 ∧ ∀ (l : β), house ↑(ξ l) ≤ c₁ K * (c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))
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
inst✝ : CompleteSpace E
a : ℕ → E
ha : Tendsto a atTop (𝓝 0)
n : ℕ
⊢ Δ_[1]^[n] (⇑(mahlerSeries a)) 0 = Δ_[1]^[n] (fun k ↦ ∑ j ∈ range (n + 1), k.choose j • a j) 0

Tactic:
simp only [fwdDiff_iter_eq_sum_shift, zero_add]
    refine Finset.sum_congr rfl fun j hj ↦ ?_
    rw [nsmul_one, nsmul_one,
      mahlerSeries_apply_nat ha (Nat.lt_succ_iff.mp <| Finset.mem_range.mp hj), Nat.cast_id]

Goal state after:
Module: Mathlib.Topology.UniformSpace.ProdApproximation

Goal state before:
pp: X : Type u_1
Y : Type u_2
R : Type u_3
V : Type u_4
inst✝¹¹ : TopologicalSpace X
inst✝¹⁰ : TotallyDisconnectedSpace X
inst✝⁹ : T2Space X
inst✝⁸ : CompactSpace X
inst✝⁷ : TopologicalSpace Y
inst✝⁶ : CompactSpace Y
inst✝⁵ : AddCommGroup V
inst✝⁴ : UniformSpace V
inst✝³ : IsUniformAddGroup V
S : Set (V × V)
inst✝² : TopologicalSpace R
inst✝¹ : MonoidWithZero R
inst✝ : MulActionWithZero R V
f : C(X × Y, V)
hS : S ∈ 𝓤 V
⊢ ∃ n g h, ∀ (x : X) (y : Y), (f (x, y), ∑ i, (g i) x • (h i) y) ∈ S

Tactic:
by
  have hS' : {(f, g) | ∀ y, (f y, g y) ∈ S} ∈ 𝓤 C(Y, V) :=
    (mem_compactConvergence_entourage_iff _).mpr
      ⟨_, _, isCompact_univ, hS, by simp only [Set.mem_univ, true_implies, subset_refl]⟩
  obtain ⟨n, U, v, hv⟩ := exists_finite_sum_const_indicator_approximation_of_mem_nhds_diagonal
    f.curry (nhdsSet_diagonal_le_uniformity hS')
  refine ⟨n, fun i ↦ ⟨_, (U i).isClopen.continuous_indicator <| continuous_const (y := 1)⟩,
    v, fun x y ↦ ?_⟩
  convert! hv x y using 2
  simp only [sum_apply]
  congr 1 with i
  by_cases hi : x ∈ U i <;> simp [hi]

Goal state after:
Module: Mathlib.NumberTheory.PowModTotient

Goal state before:
pp: case succ
x k n : ℕ
hn : 1 < n
h : x.Coprime n
l : ℕ
ih : x ^ (k + l * φ n) % n = x ^ k % n
⊢ x ^ (k + l * φ n) % n = x ^ k % n

Tactic:
ih

Goal state after:
case succ
x k n : ℕ
hn : 1 < n
h : x.Coprime n
l : ℕ
ih : x ^ (k + l * φ n) % n = x ^ k % n
⊢ x ^ k % n = x ^ k % n
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : a.x = 1
⊢ a = 1

Tactic:
have prop := a.prop_y

Goal state after:
d : ℤ
h₀ : d ≠ 0
a : Solution₁ d
ha : a.x = 1
prop : d * a.y ^ 2 = a.x ^ 2 - 1
⊢ a = 1
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
ncs : CauSeq ℤ_[p] norm
F : Polynomial R
⊢ Tendsto (fun i ↦ ‖(Polynomial.aeval (↑ncs i)) (Polynomial.derivative F)‖) atTop
    (𝓝 ‖(Polynomial.aeval ncs.lim) (Polynomial.derivative F)‖)

Tactic:
by
  refine Tendsto.comp (continuous_iff_continuousAt.1 continuous_norm _) ?_
  rw [← Polynomial.eval_map_algebraMap]
  refine (comp_tendsto_lim ncs).congr ?_
  simp

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inl
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : a₁ = (a₁ ^ n₂) ^ n₁ ∨ a₁ = -(a₁ ^ n₂) ^ n₁
⊢ a₁ ^ n₂ = a₁

Tactic:
← zpow_mul,

Goal state after:
case inl
d : ℤ
h₀ : 0 < d
hd : ¬IsSquare d
a₁ : Solution₁ d
ha₁ : IsFundamental a₁
n₁ n₂ : ℤ
Hx : 1 < (a₁ ^ n₂).x
Hy : 0 < (a₁ ^ n₂).y
H : ∀ (a : Solution₁ d), ∃ n, a = (a₁ ^ n₂) ^ n ∨ a = -(a₁ ^ n₂) ^ n
hn₁ : a₁ = a₁ ^ (n₂ * n₁) ∨ a₁ = -a₁ ^ (n₂ * n₁)
⊢ a₁ ^ n₂ = a₁
Module: Mathlib.NumberTheory.Padics.Hensel

Goal state before:
pp: p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
F : Polynomial R
a : ℤ_[p]
hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
hnsol : (Polynomial.aeval a) F ≠ 0
n : ℕ
this : 2 ≤ 2 ^ (n + 1)
⊢ ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ * T_gen p F a ^ 1 =
    ‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖

Tactic:
by
      rw [T_gen, sq, pow_one, norm_div, ← mul_div_assoc, PadicInt.padic_norm_e_of_padicInt,
        PadicInt.coe_mul, norm_mul]
      apply mul_div_mul_left
      apply deriv_norm_ne_zero; assumption

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

Goal state before:
pp: K : Type u_1
Γ : Type u_2
inst✝³ : Field K
inst✝² : LinearOrderedCommGroupWithZero Γ
v : Valuation K⟮X⟯ Γ
inst✝¹ : v.IsNontrivial
inst✝ : IsTrivialOn K v
hle : v X ≤ 1
f : K⟮X⟯
hf : f ≠ 0
h0 : v ↑πᵥ ≠ 0
⊢ ∃ z, v f = v ↑πᵥ ^ z

Tactic:
induction f using RatFunc.induction_on with
  | f p q hq =>
    use (Associates.mk (Pᵥ).asIdeal).count (Associates.mk (Ideal.span {p})).factors -
      (Associates.mk (Pᵥ).asIdeal).count (Associates.mk (Ideal.span {q})).factors
    simp only [map_div₀, map_pow, zpow_sub₀ h0, zpow_natCast,
      valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle hq,
      valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one hle
        (p := p) (by aesop)]

Goal state after:
Module: Mathlib.NumberTheory.SelbergSieve

Goal state before:
pp: s : BoundingSieve
⊢ (s.nu.pmul (prodPrimeFactors fun p ↦ (1 - s.nu p)⁻¹)).IsMultiplicative

Tactic:
arith_mult

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

Goal state before:
pp: R : Type u
inst✝¹⁵ : CommRing R
S : Type v
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker f ≠ ⊤
F : V'' →ₗ[R] V
hf : Function.Injective ⇑F
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : ∑ i ∈ s, g i • (⇑F ∘ b) i = 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI✝ : a * g j ∉ ↑(RingHom.ker f)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : ι → R := fun i ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K) (g' i) = a * g i
hgI : f (g' j) ≠ 0
i : ι
hi : i ∈ s
⊢ (a * g i) • F (b i) = a • g i • (⇑F ∘ b) i

Tactic:
← smul_assoc,

Goal state after:
R : Type u
inst✝¹⁵ : CommRing R
S : Type v
inst✝¹⁴ : CommRing S
inst✝¹³ : Algebra R S
K : Type u_1
inst✝¹² : Field K
inst✝¹¹ : Algebra R K
V : Type u_3
V' : Type u_4
V'' : Type u_5
inst✝¹⁰ : AddCommGroup V
inst✝⁹ : Module R V
inst✝⁸ : Module K V
inst✝⁷ : IsScalarTower R K V
inst✝⁶ : AddCommGroup V'
inst✝⁵ : Module R V'
inst✝⁴ : Module S V'
inst✝³ : IsScalarTower R S V'
inst✝² : AddCommGroup V''
inst✝¹ : Module R V''
hRK : IsFractionRing R K
inst✝ : IsDedekindDomain R
hRS : RingHom.ker f ≠ ⊤
F : V'' →ₗ[R] V
hf : Function.Injective ⇑F
f' : V'' →ₗ[R] V'
ι : Type u_6
b : ι → V''
s : Finset ι
g : ι → K
eq : ∑ i ∈ s, g i • (⇑F ∘ b) i = 0
j' : ι
hj's : j' ∈ s
hj'g : ¬g j' = 0
a : K
j : ι
hjs : j ∈ s
hgI✝ : a * g j ∉ ↑(RingHom.ker f)
g'' : (i : ι) → i ∈ s → R
hg'' : ∀ (i : ι) (a_1 : i ∈ s), (algebraMap R K) (g'' i a_1) = a * g i
this : (a : Prop) → Decidable a := Classical.propDecidable
g' : ι → R := fun i ↦ if h : i ∈ s then g'' i h else 0
hg' : ∀ i ∈ s, (algebraMap R K) (g' i) = a * g i
hgI : f (g' j) ≠ 0
i : ι
hi : i ∈ s
⊢ (a * g i) • F (b i) = (a • g i) • (⇑F ∘ b) i
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: n x y : ℤ
h : n = x ^ 2 + y ^ 2
hc : IsCoprime x y
u v : ℤ
huv : u * x + v * n = 1
H : u * y * (u * y) - -1 = n * (-v ^ 2 * n + u ^ 2 + 2 * v)
⊢ ↑(-1) = ↑(u * y * (u * y))

Tactic:
exact (ZMod.intCast_eq_intCast_iff_dvd_sub _ _ _).mpr (Int.natAbs_dvd.mpr ⟨_, H⟩)

Goal state after: