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

Goal state before:
pp: case h.inl.«0»
k : ℕ
ihn :
  ∀ m < 0,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even 0
hk : 0 < 3
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑0) =
    ↑(if 0 ≡ 2 [MOD 12] then 0 / 12 else 0 / 12 + 1)

pp: case h.inl.«1»
k : ℕ
ihn :
  ∀ m < 1,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even 1
hk : 1 < 3
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑1) =
    ↑(if 1 ≡ 2 [MOD 12] then 1 / 12 else 1 / 12 + 1)

pp: case h.inl.«2»
k : ℕ
ihn :
  ∀ m < 2,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even 2
hk : 2 < 3
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑2) =
    ↑(if 2 ≡ 2 [MOD 12] then 2 / 12 else 2 / 12 + 1)

Tactic:
· simpa using! levelOne_weight_zero_rank_one

Goal state after:
case h.inl.«1»
k : ℕ
ihn :
  ∀ m < 1,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even 1
hk : 1 < 3
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑1) =
    ↑(if 1 ≡ 2 [MOD 12] then 1 / 12 else 1 / 12 + 1)

case h.inl.«2»
k : ℕ
ihn :
  ∀ m < 2,
    Even m →
      Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑m) =
        ↑(if m ≡ 2 [MOD 12] then m / 12 else m / 12 + 1)
hk2 : Even 2
hk : 2 < 3
⊢ Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range ↑2) =
    ↑(if 2 ≡ 2 [MOD 12] then 2 / 12 else 2 / 12 + 1)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case right
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ x.re ∈ interior (Set.Icc (-(1 / 2)) (1 / 2))

Tactic:
apply Set.mem_of_mem_of_subset ((Set.mem_preimage.mp (ho1 hx))) (interior_mono ?_)

Goal state after:
ho1 : interior 𝒟 ⊆ UpperHalfPlane.re ⁻¹' interior (UpperHalfPlane.re '' 𝒟)
ho2 : interior 𝒟 ⊆ (fun τ ↦ ‖↑τ‖) ⁻¹' interior ((fun τ ↦ ‖↑τ‖) '' 𝒟)
x : ℍ
hx : x ∈ interior 𝒟
⊢ UpperHalfPlane.re '' 𝒟 ⊆ Set.Icc (-(1 / 2)) (1 / 2)
Module: Mathlib.NumberTheory.Modular

Goal state before:
pp: case left
y : ℝ
⊢ IsClosed {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}

Tactic:
apply (isClosed_le continuous_const Complex.continuous_im).inter
    apply (isClosed_le Complex.continuous_im continuous_const).inter
    apply (isClosed_le (continuous_abs.comp Complex.continuous_re) continuous_const).inter
    exact isClosed_le continuous_const continuous_norm

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

Goal state before:
pp: 𝒢 : Subgroup (GL (Fin 2) ℝ)
inst✝ : 𝒢.IsArithmetic
k : ℤ
hk : k < 0
f : ModularForm 𝒢 k
⊢ f = 0

Tactic:
by
  suffices ModularForm.norm 𝒮ℒ f = 0 by simpa [ModularForm.norm_eq_zero_iff]
  ext
  rw [ModularFormClass.levelOne_neg_weight_eq_zero
    (mul_neg_of_neg_of_pos hk <| mod_cast Nat.pos_of_ne_zero 𝒢.relIndex_ne_zero)
    (ModularForm.norm 𝒮ℒ f), Pi.zero_apply, zero_apply]

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

Goal state before:
pp: K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
x : K
r : ℝ
hr : Complex.ofRealHom r = (extensionEmbedding v) { toCompletion := ↑(WithAbs.toAbs (↑v) x) }
⊢ (star v.embedding) x = v.embedding x

Tactic:
rw [extensionEmbedding_coe, ← WithAbs.equiv_symm_apply, RingEquiv.apply_symm_apply] at hr

Goal state after:
K : Type u_1
inst✝ : Field K
v : InfinitePlace K
hv : (extensionEmbedding v).fieldRange = Complex.ofRealHom.fieldRange
x : K
r : ℝ
hr : Complex.ofRealHom r = v.embedding x
⊢ (star v.embedding) x = v.embedding x
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: ι : Type u_1
S : ι → Type u_3
G : ι → Type u_4
inst✝³ : (i : ι) → SetLike (S i) (G i)
A : (i : ι) → S i
inst✝² : DecidableEq ι
inst✝¹ : (i : ι) → Group (G i)
inst✝ : ∀ (i : ι), SubgroupClass (S i) (G i)
i : ι
r : G i
n : ℤ
⊢ mulSingle A i (r ^ n) = mulSingle A i r ^ n

Tactic:
by
  ext; simp [Pi.mulSingle_zpow, RestrictedProduct.zpow_apply]

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: m : ℤ
eq : (2 * m + 1) ^ 2 - 1 = 4 * (m * (m + 1))
⊢ 8 ∣ (2 * m + 1) ^ 2 - 1

Tactic:
simpa [eq] using (mul_dvd_mul_iff_left four_ne_zero).mpr (two_dvd_mul_add_one m)

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: m : ℕ
eq : (2 * m + 1) ^ 2 - 1 = 4 * (m * (m + 1))
⊢ 8 ∣ (2 * m + 1) ^ 2 - 1

Tactic:
simpa [eq] using (mul_dvd_mul_iff_left four_ne_zero).mpr (two_dvd_mul_add_one m)

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
x : mixedSpace K
⊢ A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)

Tactic:
← Set.indicator_comp_right,

Goal state after:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
x : mixedSpace K
⊢ A.indicator 1 x = (normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A).indicator (1 ∘ normAtComplexPlaces) x
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ (∫⁻ (x : InfinitePlace K → ℝ) in Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
      (normAtComplexPlaces '' A).indicator (fun x_1 ↦ (∏ x_2, ENNReal.ofReal (x ↑x_2)) * 1 x_1)
          (normAtComplexPlaces (mixedSpaceOfRealSpace x)) *
        ENNReal.ofReal (2 * π) ^ Fintype.card { w // w.IsComplex } ∂Measure.pi fun x ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w) ∂Measure.pi fun x ↦ volume

Tactic:
← Set.indicator_comp_right,

Goal state after:
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A = A
hm : MeasurableSet A
hA' : ∀ {x : mixedSpace K}, A.indicator 1 x = (normAtComplexPlaces '' A).indicator 1 (normAtComplexPlaces x)
⊢ (∫⁻ (x : InfinitePlace K → ℝ) in Set.univ.pi fun w ↦ if w.IsReal then Set.univ else Set.Ioi 0,
      (⇑mixedSpaceOfRealSpace ⁻¹' normAtComplexPlaces ⁻¹' normAtComplexPlaces '' A).indicator
          (((fun x_1 ↦ (∏ x_2, ENNReal.ofReal (x ↑x_2)) * 1 x_1) ∘ normAtComplexPlaces) ∘ ⇑mixedSpaceOfRealSpace) x *
        ENNReal.ofReal (2 * π) ^ Fintype.card { w // w.IsComplex } ∂Measure.pi fun x ↦ volume) =
    ENNReal.ofReal (2 * π) ^ nrComplexPlaces K *
      ∫⁻ (x : realSpace K) in normAtComplexPlaces '' A, ∏ w, ENNReal.ofReal (x ↑w) ∂Measure.pi fun x ↦ volume
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
⊢ ↑(finrank ℚ K) * regOfFamily u =
    |(of fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩))))).det|

Tactic:
let f : Fin (rank K + 1) ≃ InfinitePlace K :=
    (finSuccEquiv _).trans ((Equiv.optionSubtype _).symm e.symm).val

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
u : Fin (rank K) → (𝓞 K)ˣ
w' : InfinitePlace K
e : { w // w ≠ w' } ≃ Fin (rank K)
f : Fin (rank K + 1) ≃ InfinitePlace K := (finSuccEquiv (rank K)).trans ↑((Equiv.optionSubtype w').symm e.symm)
⊢ ↑(finrank ℚ K) * regOfFamily u =
    |(of fun i w ↦ if h : i = w' then ↑w.mult else ↑w.mult * Real.log (w ((algebraMap (𝓞 K) K) ↑(u (e ⟨i, h⟩))))).det|
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
⊢ regOfFamily (realFundSystem K) = 2 ^ rank K * regulator ↥K⁺

Tactic:
classical
  let W₀ := (equivInfinitePlace K).symm w₀
  let f : {w : InfinitePlace K // w ≠ W₀} ≃ {w : InfinitePlace K⁺ // w ≠ w₀} :=
    (equivInfinitePlace K).subtypeEquiv fun w ↦ by rw [not_iff_not, Equiv.eq_symm_apply]
  let g := ((finCongr (units_rank_eq_units_rank K).symm).trans (equivFinRank K⁺)).trans f.symm
  rw [show (2 : ℝ) ^ rank K = |∏ w : {w : InfinitePlace K⁺ // w ≠ w₀}, 2| by
    rw [Finset.prod_const, abs_pow, abs_of_pos zero_lt_two, ← units_rank_eq_units_rank K, rank]
    simp]
  rw [regulator_eq_regOfFamily_fundSystem, regOfFamily_eq_det _ W₀ g.symm, regOfFamily_eq_det',
    ← abs_mul, ← Matrix.det_mul_column, ← Matrix.det_reindex_self f, Matrix.reindex_apply]
  congr; ext i w
  rw [Matrix.submatrix_apply, Matrix.of_apply, Matrix.of_apply,
    show f.symm w = (equivInfinitePlace K).symm w.1 by rfl,
    show algebraMap (𝓞 K) K _ = algebraMap K⁺ K _ by rfl, equivInfinitePlace_symm_apply]
  simp [f, g]

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i x✝ : { w // w ≠ w₀ }
⊢ realSpaceToLogSpace (completeFamily K ↑i) x✝ = ↑((basisUnitLattice K) (equivFinRank.symm i)) x✝

Tactic:
rw [← logEmbedding_fundSystem, ← logMap_eq_logEmbedding, completeFamily, dif_neg,
    realSpaceToLogSpace_expMap_symm]

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
i x✝ : { w // w ≠ w₀ }
⊢ (algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨↑i, ⋯⟩)) ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w i : InfinitePlace K
hw : ¬w = w₀
⊢ (completeBasis K) w i = ↑i.mult * Real.log (i ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w, hw⟩))))

Tactic:
completeBasis_apply_of_ne K ⟨w, hw⟩,

Goal state after:
case neg
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w i : InfinitePlace K
hw : ¬w = w₀
⊢ ↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w, hw⟩)))))
      i =
    ↑i.mult * Real.log (i ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm ⟨w, hw⟩))))
Module: Mathlib.NumberTheory.NumberField.Units.Regulator

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ regulator K = ZLattice.covolume (span ℤ (Set.range ⇑(basisOfIsMaxRank ⋯))) volume

Tactic:
regulator,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ ZLattice.covolume (unitLattice K) volume = ZLattice.covolume (span ℤ (Set.range ⇑(basisOfIsMaxRank ⋯))) volume
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : realSpace K
⊢ ∏ w, ↑expMapBasis x w ^ w.mult = Real.exp (x w₀) ^ finrank ℚ K

Tactic:
simp_rw [expMapBasis_apply', Pi.smul_def, smul_eq_mul, mul_pow, prod_mul_distrib,
    prod_pow_eq_pow_sum, sum_mult_eq, ← prod_pow]
  rw [prod_comm]
  simp_rw [Real.rpow_pow_comm (apply_nonneg _ _), Real.finsetProd_rpow _ _
    fun _ _ ↦ pow_nonneg (apply_nonneg _ _) _, prod_eq_abs_norm, Units.norm, Rat.cast_one,
    Real.one_rpow, prod_const_one, mul_one]

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

Tactic:
exact measurableSet_Iic

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

Goal state before:
pp: case pos
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w : InfinitePlace K
x✝ : w ∈ Set.univ
h✝ : w = w₀
⊢ Set.Iic 0 =ᵐ[volume] Set.Iio 0

Tactic:
exact Iio_ae_eq_Iic.symm

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ₚ
⊢ 𝒑.inertiaDegIn (𝓞 K) = orderOf ↑p ∧ 𝒑.ramificationIdxIn (𝓞 K) = p ^ k * (p - 1)

Tactic:
obtain ⟨Pₚ, hP₁, _⟩ := exists_maximal_ideal_liesOver_of_isIntegral 𝒑 (S := 𝓞 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 𝒑
⊢ 𝒑.inertiaDegIn (𝓞 K) = orderOf ↑p ∧ 𝒑.ramificationIdxIn (𝓞 K) = p ^ k * (p - 1)
Module: Mathlib.NumberTheory.NumberField.ExistsRamified

Goal state before:
pp: K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
H : Module.finrank ℚ K ≠ 1
⊢ ∃ P, ∃ (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P

Tactic:
obtain ⟨p, hp1, hp2⟩ := NumberField.exists_not_isUnramifiedIn (𝒪 := 𝒪) H

Goal state after:
K : Type u_1
𝒪 : Type u_2
inst✝⁴ : Field K
inst✝³ : NumberField K
inst✝² : CommRing 𝒪
inst✝¹ : Algebra 𝒪 K
inst✝ : IsIntegralClosure 𝒪 ℤ K
H : Module.finrank ℚ K ≠ 1
p : ℕ
hp1 : Nat.Prime p
hp2 : ¬Algebra.IsUnramifiedIn 𝒪 (Ideal.span {↑p})
⊢ ∃ P, ∃ (x : P.IsMaximal), ¬Algebra.IsUnramifiedAt ℤ P
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 : ℝ
hJ : ClassGroup.mk0 J = C⁻¹
I : ↥(Ideal (𝓞 K))⁰
⊢ ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C ↔
    ClassGroup.mk0 ⟨↑↑((Equiv.dvd J) I), ⋯⟩ = 1 ∧ ↑(absNorm ↑↑((Equiv.dvd J) I)) ≤ s * ↑(absNorm ↑J)

Tactic:
Equiv.dvd_apply,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hJ : ClassGroup.mk0 J = C⁻¹
I : ↥(Ideal (𝓞 K))⁰
⊢ ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C ↔ ClassGroup.mk0 ⟨↑(J * I), ⋯⟩ = 1 ∧ ↑(absNorm ↑(J * I)) ≤ s * ↑(absNorm ↑J)
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ (↑n * max 1 ‖A‖ * ↑B + 1) ^ m ≤ (↑n * max 1 ‖A‖) ^ m * (↑B + 1) ^ m

Tactic:
← mul_pow,

Goal state after:
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ (↑n * max 1 ‖A‖ * ↑B + 1) ^ m ≤ (↑n * max 1 ‖A‖ * (↑B + 1)) ^ m
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: 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)|)))
s : ℝ
hs : 0 ≤ s
⊢ ↑(Nat.card { I // absNorm ↑I ≤ ⌊s⌋₊ }) / s + s⁻¹ = ↑(Nat.card { I // absNorm I ≤ ⌊s⌋₊ }) / s

Tactic:
rw [Ideal.card_norm_le_eq_card_norm_le_add_one, Nat.cast_add, Nat.cast_one, add_div, one_div]

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

Goal state before:
pp: case calc_4
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
p q : ℕ
hpq : p < q
x : β × (K →+* ℂ) → ℤ
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
hxbound : ‖x‖ ≤ (↑q * ↑(finrank ℚ K) * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p))
h : ℕ := finrank ℚ K
l : β
H₀ : 0 ≤ supOfBasis K
H₁ : 0 < ↑q - ↑p
⊢ ∑ r, ‖x (l, r)‖ * supOfBasis K ≤ ∑ _r, (↑q * ↑h * ‖asiegel K a‖) ^ (↑p / (↑q - ↑p)) * supOfBasis K

Tactic:
gcongr with r _
    exact le_trans (norm_le_pi_norm x ⟨l, r⟩) hxbound

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: b : ℤ
a : Solution₁ (b * b)
ha : 1 < a.x
hp : a.x ^ 2 - b ^ 2 * a.y ^ 2 = 1
⊢ False

Tactic:
← mul_pow,

Goal state after:
b : ℤ
a : Solution₁ (b * b)
ha : 1 < a.x
hp : a.x ^ 2 - (b * a.y) ^ 2 = 1
⊢ False
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case zero
d : ℤ
a : Solution₁ d
hax : 0 < a.x
⊢ 0 < (a ^ 0).x

Tactic:
simp only [pow_zero, x_one, zero_lt_one]

Goal state after:
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
a : ℤ_[p]
ncs_der_val :
  ∀ (n : ℕ), ‖(Polynomial.aeval (↑ncs n)) (Polynomial.derivative F)‖ = ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
⊢ Tendsto (fun i ↦ ‖(Polynomial.aeval (↑ncs i)) (Polynomial.derivative F)‖) atTop
    (𝓝 ‖(Polynomial.aeval a) (Polynomial.derivative F)‖)

Tactic:
convert! @tendsto_const_nhds ℝ _ ℕ _ _

Goal state after:
case e'_3
p : ℕ
inst✝² : Fact (Nat.Prime p)
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : Algebra R ℤ_[p]
ncs : CauSeq ℤ_[p] norm
F : Polynomial R
a : ℤ_[p]
ncs_der_val :
  ∀ (n : ℕ), ‖(Polynomial.aeval (↑ncs n)) (Polynomial.derivative F)‖ = ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
x✝ : ℕ
⊢ ‖(Polynomial.aeval (↑ncs x✝)) (Polynomial.derivative F)‖ = ‖(Polynomial.aeval a) (Polynomial.derivative F)‖
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: x y : ℤ
hy : y ≠ 0
a : ℤ
h₀ : 0 < a * a
hxy : x ^ 2 - a ^ 2 * y ^ 2 = 1
⊢ False

Tactic:
← mul_pow,

Goal state after:
x y : ℤ
hy : y ≠ 0
a : ℤ
h₀ : 0 < a * a
hxy : x ^ 2 - (a * y) ^ 2 = 1
⊢ False
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a : Solution₁ d
h : IsFundamental a
⊢ StrictMono fun n ↦ (a ^ n).y

Tactic:
by
  have H : ∀ n : ℤ, 0 ≤ n → (a ^ n).y < (a ^ (n + 1)).y := by
    intro n hn
    rw [← sub_pos, zpow_add, zpow_one, y_mul, add_sub_assoc]
    rw [show (a ^ n).y * a.x - (a ^ n).y = (a ^ n).y * (a.x - 1) by ring]
    refine
      add_pos_of_pos_of_nonneg (mul_pos (x_zpow_pos h.x_pos _) h.2.1)
        (mul_nonneg ?_ (by rw [sub_nonneg]; exact h.1.le))
    rcases hn.eq_or_lt with (rfl | hn)
    · simp only [zpow_zero, y_one, le_refl]
    · exact (y_zpow_pos h.x_pos h.2.1 hn).le
  refine strictMono_int_of_lt_succ fun n => ?_
  rcases le_or_gt 0 n with hn | hn
  · exact H n hn
  · let m : ℤ := -n - 1
    have hm : n = -m - 1 := by simp only [m, neg_sub, sub_neg_eq_add, add_tsub_cancel_left]
    rw [hm, sub_add_cancel, ← neg_add', zpow_neg, zpow_neg, y_inv, y_inv, neg_lt_neg_iff]
    exact H _ (by lia)

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ a₁.y ^ 2 ≤ a.y ^ 2

Tactic:
← mul_le_mul_iff_right₀ h.d_pos,

Goal state after:
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
H : d * (a₁.y ^ 2 - a.y ^ 2) = a₁.x ^ 2 - a.x ^ 2
⊢ d * a₁.y ^ 2 ≤ d * a.y ^ 2
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case calc.step
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ |a.y| < |a.x| * |a₁.y|

Tactic:
←
    abs_mul,

Goal state after:
case calc.step
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a : Solution₁ d
hax : 1 < a.x
hay : 0 < a.y
⊢ |a.y| < |a.x * a₁.y|
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case h.inl
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
x : ℕ
ih : ∀ m < x, ∀ {a : Solution₁ d}, 0 ≤ a.y → ↑m = a.x → 0 < ↑m → ∃ n, a = a₁ ^ n
a : Solution₁ d
hay : 0 ≤ a.y
hax' : ↑x = a.x
hax : 0 < ↑x
hy : 0 = a.y
⊢ ∃ n, a = a₁ ^ n

Tactic:
refine ⟨0, ?_⟩
    rcases eq_one_or_neg_one_iff_y_eq_zero.2 hy.symm with rfl | rfl
    · simp
    · simp at hax'

Goal state after:
Module: Mathlib.NumberTheory.Pell

Goal state before:
pp: case inr.inr.inr
d : ℤ
a₁ : Solution₁ d
h : IsFundamental a₁
a b : Solution₁ d
hbx : 0 < b.x
hby : 0 ≤ b.y
n : ℕ
hn : b = a₁ ^ n
hb : a ∈ {-b⁻¹}
⊢ ∃ n, a = a₁ ^ n ∨ a = -a₁ ^ n

Tactic:
· rw [Set.mem_singleton_iff] at hb
    rw [hb]
    exact ⟨-n, Or.inr (by simp [hn])⟩

Goal state after:
Module: Mathlib.NumberTheory.SumTwoSquares

Goal state before:
pp: case zero
hn : Squarefree 0
H : ∀ q ∈ Nat.primeFactors 0, q % 4 ≠ 3
⊢ IsSquare (-1)

Tactic:
exact False.elim (hn.ne_zero rfl)

Goal state after:
Module: Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart

Goal state before:
pp: f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
h : |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ≤ c
hx : x ∈ Set.Ioc 0 1
⊢ x ^ (p - 1) * ‖s‖ ^ (p - 1) ≤ |max (x * ‖s‖) 1| ^ p

Tactic:
← mul_pow,

Goal state after:
f : ℤ[X]
s : ℂ
this : Bornology.IsBounded ((fun x ↦ max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖) '' Set.Ioc 0 1)
c : ℝ
p : ℕ
x : ℝ
h : |max (x * ‖s‖) 1 * ‖(aeval (↑x * s)) f‖| ≤ c
hx : x ∈ Set.Ioc 0 1
⊢ (x * ‖s‖) ^ (p - 1) ≤ |max (x * ‖s‖) 1| ^ p
Module: Mathlib.NumberTheory.Transcendental.Liouville.Basic

Goal state before:
pp: case neg
Z : Type u_1
N : Type u_2
R : Type u_3
inst✝ : PseudoMetricSpace R
d : N → ℝ
j : Z → N → R
f : R → R
α : R
ε M : ℝ
d0 : ∀ (a : N), 1 ≤ d a
e0 : 0 < ε
B : ∀ ⦃y : R⦄, y ∈ closedBall α ε → dist (f α) (f y) ≤ dist α y * M
L : ∀ ⦃z : Z⦄ ⦃a : N⦄, j z a ∈ closedBall α ε → 1 ≤ d a * dist (f α) (f (j z a))
me0 : 0 < max (1 / ε) M
z : Z
a : N
dm1 : ¬1 ≤ dist α (j z a) * max (1 / ε) M
⊢ 1 ≤ d a * (dist α (j z a) * max (1 / ε) M)

Tactic:
· -- `j z a = z / (a + 1)`: we prove that this ratio is close to `α`
    have : j z a ∈ closedBall α ε := by
      refine mem_closedBall'.mp (le_trans ?_ ((one_div_le me0 e0).mpr (le_max_left _ _)))
      exact (le_div_iff₀ me0).mpr (not_le.mp dm1).le
    -- use the "separation from `1`" (assumption `L`) for numerators,
    refine (L this).trans ?_
    -- remove a common factor and use the Lipschitz assumption `B`
    gcongr
    · exact zero_le_one.trans (d0 a)
    · refine (B this).trans ?_
      gcongr
      apply le_max_right

Goal state after: