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

Goal state before:
pp: case e'_5.inl
Γ : 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)))
⊢ (if 2 * ↑0 / h Γ = 0 then 0 else (PowerSeries.coeff 0) (qExpansion (h Γ) ⇑f) * ↑(rexp (-π * (2 * ↑0 / h Γ) * t))) =
    if 0 = 0 then 0
    else (PowerSeries.coeff 0) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ 0

pp: case e'_5.inr
Γ : 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)))
n : ℕ
hn : n > 0
⊢ (if 2 * ↑n / h Γ = 0 then 0 else (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) * ↑(rexp (-π * (2 * ↑n / h Γ) * t))) =
    if n = 0 then 0
    else (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ n

Tactic:
· simp

Goal state after:
case e'_5.inr
Γ : 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)))
n : ℕ
hn : n > 0
⊢ (if 2 * ↑n / h Γ = 0 then 0 else (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) * ↑(rexp (-π * (2 * ↑n / h Γ) * t))) =
    if n = 0 then 0
    else (PowerSeries.coeff n) (qExpansion (h Γ) ⇑f) * Function.Periodic.qParam (h Γ) ↑(↑ofComplex (I * ↑t)) ^ n
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
a : ℕ
h_ind : emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p) (x - y) + ↑a
⊢ emultiplicity (↑p) (x ^ p ^ (a + 1) - y ^ p ^ (a + 1)) = emultiplicity (↑p) (x - y) + ↑(a + 1)

Tactic:
Nat.cast_add,

Goal state after:
case succ
R : Type u_1
inst✝¹ : CommRing R
x y : R
p : ℕ
inst✝ : IsDomain R
hp : Prime ↑p
hp1 : Odd p
hxy : ↑p ∣ x - y
hx : ¬↑p ∣ x
a : ℕ
h_ind : emultiplicity (↑p) (x ^ p ^ a - y ^ p ^ a) = emultiplicity (↑p) (x - y) + ↑a
⊢ emultiplicity (↑p) (x ^ p ^ (a + 1) - y ^ p ^ (a + 1)) = emultiplicity (↑p) (x - y) + (↑a + ↑1)
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: case inl
ι : 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 : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
⊢ (single A i (x i * r)) i = (x * single A i r) i

pp: case inr
ι : 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 : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
j : ι
hne : i ≠ j
⊢ (single A i (x i * r)) j = (x * single A i r) j

Tactic:
· simp

Goal state after:
case inr
ι : 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 : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
j : ι
hne : i ≠ j
⊢ (single A i (x i * r)) j = (x * single A i r) j
Module: Mathlib.Topology.Algebra.RestrictedProduct.Basic

Goal state before:
pp: case inl
ι : 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 : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
⊢ (single A i (r * x i)) i = (single A i r * x) i

pp: case inr
ι : 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 : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
j : ι
hne : i ≠ j
⊢ (single A i (r * x i)) j = (single A i r * x) j

Tactic:
· simp

Goal state after:
case inr
ι : 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 : ι) → MulZeroClass (G i)
inst✝¹ : ∀ (i : ι), ZeroMemClass (S i) (G i)
inst✝ : ∀ (i : ι), MulMemClass (S i) (G i)
i : ι
r : G i
x : Πʳ (i : ι), [G i, ↑(A i)]
j : ι
hne : i ≠ j
⊢ (single A i (r * x i)) j = (single A i r * x) j
Module: Mathlib.NumberTheory.ModularForms.LFunction

Goal state before:
pp: Γ : 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 : ℂ
⊢ 0 ≤ 2 * ↑n

Tactic:
by grind

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ (1 - 1) % 4 = 0

pp: x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ Odd x

Tactic:
· simp

Goal state after:
x y : ℤ
hxy : 2 ∣ x - y
hx : ¬2 ∣ x
hy : Odd y
d : ℕ
⊢ Odd x
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: x n : ℕ
h1x : 1 < x
hx : ¬2 ∣ x
hn : n ≠ 0
hneven : Even n
⊢ 2 ∣ x - 1

Tactic:
by grind

Goal state after:
Module: Mathlib.NumberTheory.Multiplicity

Goal state before:
pp: case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ x + (y + 1) ≠ 0

pp: case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ x ^ n + (y + 1) ^ n ≠ 0

Tactic:
· simp

Goal state after:
case succ
x p : ℕ
hp : Fact (Nat.Prime p)
hp1 : Odd p
hx : ¬p ∣ x
n : ℕ
hn : Odd n
y : ℕ
hxy : p ∣ x + (y + 1)
⊢ x ^ n + (y + 1) ^ n ≠ 0
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
⊢ u • x = 0 ↔ x = 0

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ by rw [h, smul_zero]⟩

Goal state after:
K : Type u_1
inst✝ : Field K
u : (𝓞 K)ˣ
x : mixedSpace K
h : u • x = 0
⊢ x = 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₀ }
⊢ ↑(↑x✝).mult * (Real.log |c| - Real.log (|c| ^ finrank ℚ K) * (↑(finrank ℚ K))⁻¹) = 0 x✝

Tactic:
Real.log_pow,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x✝ : { w // w ≠ w₀ }
⊢ ↑(↑x✝).mult * (Real.log |c| - ↑(finrank ℚ K) * Real.log |c| * (↑(finrank ℚ K))⁻¹) = 0 x✝
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord

Goal state before:
pp: case refine_1.refine_1
K : Type u_1
inst✝ : Field K
A : Set (mixedSpace K)
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
a : mixedSpace K
ha : a ∈ A
ha₂ : normAtAllPlaces a ∈ ⋂ w, {x | x ↑w ≠ 0}
⊢ normAtAllPlaces a ∈ normAtAllPlaces '' A

Tactic:
exact Set.mem_image_of_mem normAtAllPlaces ha

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

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
A : Set (mixedSpace K)
inst✝ : NumberField K
hA : normAtAllPlaces ⁻¹' normAtAllPlaces '' A = A
hm : MeasurableSet A
hA₁ : ∀ (x : mixedSpace K), x ∈ A ↔ (fun w ↦ ‖x.1 w‖, x.2) ∈ A
x : mixedSpace K
x✝ : x ∈ normAtComplexPlaces ⁻¹' normAtComplexPlaces '' plusPart A
a : mixedSpace K
ha₁ : a ∈ plusPart A
ha₂ : normAtComplexPlaces a = normAtComplexPlaces x
w : { w // w.IsReal }
this : a.1 w = x.1 w
⊢ 0 < a.1 w

Tactic:
exact ha₁.2 w

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✝ : NumberField K
x✝ : ∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤
u : (𝓞 K)ˣ
hu : Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤
⊢ ⊤ ≤ (unitsMulComplexConjInv K).range

pp: case refine_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
h : (unitsMulComplexConjInv K).range.index = 1
⊢ ∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤

Tactic:
· refine le_of_eq_of_le ?_ ((Subgroup.zpowers u).map_le_range (unitsMulComplexConjInv K))
    rw [MonoidHom.map_zpowers, ← hu]

Goal state after:
case refine_2
K : Type u_1
inst✝³ : Field K
inst✝² : CharZero K
inst✝¹ : IsCMField K
inst✝ : NumberField K
h : (unitsMulComplexConjInv K).range.index = 1
⊢ ∃ u, Subgroup.zpowers ((unitsMulComplexConjInv K) u) = ⊤
Module: Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
J : ↥(Ideal (𝓞 K))⁰
s : ℝ
hs : 0 ≤ s
x✝² : ↥(Finset.Iic ⌊s⌋₊)
i : ℕ
hi : i ∈ Finset.Iic ⌊s⌋₊
x✝¹ : ↥(Units.torsion K)
x✝ : ↥(Ideal (𝓞 K))⁰
⊢ (↑J ∣ ↑x✝ ∧ IsPrincipal ↑x✝ ∧ absNorm ↑x✝ ≤ ⌊s⌋₊) ∧ absNorm ↑x✝ = i ↔ ↑J ∣ ↑x✝ ∧ IsPrincipal ↑x✝ ∧ absNorm ↑x✝ = i

Tactic:
by grind

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
⊢ ∑ w, ↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) x)) w = ∑ i, Real.log (i x ^ i.mult)

Tactic:
Real.log_pow,

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : K
hx : x ≠ 0
⊢ ∑ w, ↑expMap.symm (normAtAllPlaces ((mixedEmbedding K) x)) w = ∑ x_1, ↑x_1.mult * Real.log (x_1 x)
Module: Mathlib.NumberTheory.NumberField.CMField

Goal state before:
pp: F : Type u_1
K : Type u_2
inst✝⁸ : Field F
inst✝⁷ : IsTotallyReal F
inst✝⁶ : Field K
inst✝⁵ : CharZero K
inst✝⁴ : Algebra.IsIntegral ℚ K
inst✝³ : IsTotallyComplex K
inst✝² : Algebra F K
inst✝¹ : IsQuadraticExtension F K
inst✝ : IsAbelianGalois ℚ K
φ : K →+* ℂ := Classical.choice ⋯
σ : Gal(K/ℚ)
hσ₁ : ComplexEmbedding.IsConj φ σ
ν : Gal(K/ℚ)
⊢ ComplexEmbedding.IsConj (φ.comp ↑ν.symm) (ν.symm⁻¹ * σ * ν.symm)

Tactic:
exact hσ₁.comp _

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
S : Set ℕ
inst✝ : IsCyclotomicExtension S ℚ K
this✝ : Algebra.IsIntegral ℚ K
n : ℕ
hn₁ : n ∈ S
hn₂ : 2 < n
this : NeZero n
⊢ n ≠ 0

Tactic:
by grind

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
⊢ ↑expMapBasis x = Real.exp (x w₀) • fun w ↦ ∏ i, w ((algebraMap (𝓞 K) K) ↑(fundSystem K (equivFinRank.symm i))) ^ x ↑i

Tactic:
by
  simp_rw [expMapBasis_apply, Basis.equivFun_symm_apply, Fintype.sum_eq_add_sum_subtype_ne _ w₀,
    expMap_add, expMap_smul, expMap_basis_of_eq, Pi.pow_def, Real.exp_one_rpow, Pi.mul_def,
    expMap_sum, expMap_smul, expMap_basis_of_ne, Pi.smul_def, smul_eq_mul, prod_apply, Pi.pow_apply,
    normAtAllPlaces_mixedEmbedding]

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
⊢ i - j ≠ 0

Tactic:
by grind

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
⊢ i - j < p

Tactic:
by grind

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

Goal state before:
pp: case inl
p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
η₁ : A
hη₁ hη₂ : η₁ ∈ nthRootsFinset p 1
⊢ ζ - 1 ∣ η₁ - η₁

pp: case inr
p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p 1
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p 1
h : η₁ ≠ η₂
⊢ ζ - 1 ∣ η₁ - η₂

Tactic:
· simp

Goal state after:
case inr
p : ℕ
A : Type u_1
ζ : A
inst✝¹ : CommRing A
inst✝ : IsDomain A
hζ : IsPrimitiveRoot ζ p
hp : Nat.Prime p
η₁ : A
hη₁ : η₁ ∈ nthRootsFinset p 1
η₂ : A
hη₂ : η₂ ∈ nthRootsFinset p 1
h : η₁ ≠ η₂
⊢ ζ - 1 ∣ η₁ - η₂
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:
abs_inv,

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.Cyclotomic.Ideal

Goal state before:
pp: case pos.succ
p : ℕ
hp : Fact (Nat.Prime p)
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : K
h : p = 2
n : ℕ
hK : IsCyclotomicExtension {p ^ (n + 1 + 1)} ℚ K
hζ : IsPrimitiveRoot ζ (p ^ (n + 1 + 1))
⊢ Associated ((Algebra.norm ℤ) (hζ.toInteger - 1)) ↑p

Tactic:
| succ n =>

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case inl
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hf_nontriv : ∀ (n : ℕ), n ≠ 0 → f ↑n = 1
⊢ f ↑0 = AbsoluteValue.trivial ↑0

pp: case inr
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hf_nontriv : ∀ (n : ℕ), n ≠ 0 → f ↑n = 1
n : ℕ
hn : n ≠ 0
⊢ f ↑n = AbsoluteValue.trivial ↑n

Tactic:
· simp

Goal state after:
case inr
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hf_nontriv : ∀ (n : ℕ), n ≠ 0 → f ↑n = 1
n : ℕ
hn : n ≠ 0
⊢ f ↑n = AbsoluteValue.trivial ↑n
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⌋₊ } + 1) / s

Tactic:
Nat.cast_add,

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)|)))
s : ℝ
hs : 0 ≤ s
⊢ ↑(Nat.card { I // absNorm ↑I ≤ ⌊s⌋₊ }) / s + s⁻¹ = (↑(Nat.card { I // absNorm ↑I ≤ ⌊s⌋₊ }) + ↑1) / s
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case inl
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
⊢ f ↑0 ≤ 1

pp: case inr
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
⊢ f ↑n ≤ 1

Tactic:
· simp

Goal state after:
case inr
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
⊢ f ↑n ≤ 1
Module: Mathlib.NumberTheory.Ostrowski

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

pp: case inr.inr
f : AbsoluteValue ℚ ℝ
n₀ : ℕ
hn₀ : 1 < n₀
h : f ↑n₀ ≤ 1
n : ℕ
h_ineq1 : ∀ {m : ℕ}, 1 ≤ m → f ↑m ≤ ↑n₀ * (logb ↑n₀ ↑m + 1)
h₀ : n ≠ 0
h_ineq2 : ∀ (k : ℕ), 0 < k → f ↑n ≤ (↑n₀ * (logb ↑n₀ ↑n + 1)) ^ (↑k)⁻¹ * ↑k ^ (↑k)⁻¹
h₁ : n ≠ 1
⊢ f ↑n ≤ 1

Tactic:
· simp

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

Goal state before:
pp: case inr.inl
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
hfm1 : 1 < f ↑m
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
hs0 : 0 < s
⊢ f ↑1 ^ s⁻¹ = real ↑1

pp: case inr.inr
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
hfm1 : 1 < f ↑m
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
hs0 : 0 < s
n : ℕ
h : 1 < n
⊢ f ↑n ^ s⁻¹ = real ↑n

Tactic:
· simp

Goal state after:
case inr.inr
f : AbsoluteValue ℚ ℝ
notbdd : ¬∀ (n : ℕ), f ↑n ≤ 1
m : ℕ
hm : ¬f ↑m ≤ 1
hfm1 : 1 < f ↑m
oneltm : 1 < m
s : ℝ := logb (↑m) (f ↑m)
hs : s = logb (↑m) (f ↑m)
hs0 : 0 < s
n : ℕ
h : 1 < n
⊢ f ↑n ^ s⁻¹ = real ↑n
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case calc_6
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
⊢ ↑h * c₂ K * (↑q * c₁ K * A) ^ (↑p / (↑q - ↑p)) ≤ c₁ K * (c₁ K * ↑q * A) ^ (↑p / (↑q - ↑p))

Tactic:
rw [mul_comm (q : ℝ) (c₁ K)]; rfl

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

Goal state before:
pp: M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
⊢ ∑ j ∈ range (R - 1), R.choose (j + 1) • Δ_[1]^[n + (j + 1)] f 0 + R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0 =
    ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (f (↑k + ↑R) - f ↑k)

Tactic:
(by lia : n + R = (n + ((R - 1) + 1))),

Goal state after:
M : Type u_1
G : Type u_2
inst✝¹ : AddCommMonoidWithOne M
inst✝ : AddCommGroup G
f : M → G
n R : ℕ
hR : 1 ≤ R
aux : Δ_[1]^[n + R] f 0 = R.choose (R - 1 + 1) • Δ_[1]^[n + R] f 0
⊢ ∑ j ∈ range (R - 1), R.choose (j + 1) • Δ_[1]^[n + (j + 1)] f 0 + R.choose (R - 1 + 1) • Δ_[1]^[n + (R - 1 + 1)] f 0 =
    ∑ k ∈ range (n + 1), ((-1) ^ (n - k) * ↑(n.choose k)) • (f (↑k + ↑R) - f ↑k)
Module: Mathlib.NumberTheory.Padics.MahlerBasis

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

Tactic:
rw [← Nat.cast_smul_eq_nsmul ℤ_[p], div_eq_inv_mul]

Goal state after:
case refine_1
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n i : ℕ
hi : i ∈ range (p ^ t - 1)
⊢ ‖↑((p ^ t).choose (i + 1)) • Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊ ≤ (↑p)⁻¹ * ‖Δ_[1]^[n + (i + 1)] (⇑f) 0‖₊
Module: Mathlib.NumberTheory.Padics.MahlerBasis

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

Tactic:
intro k hk

Goal state after:
p : ℕ
hp : Fact (Nat.Prime p)
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : Module ℤ_[p] E
inst✝¹ : IsBoundedSMul ℤ_[p] E
inst✝ : IsUltrametricDist E
f : C(ℤ_[p], E)
s t : ℕ
hst : ∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s
n k : ℕ
hk : k ≤ s
⊢ ‖Δ_[1]^[n + k * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ k
Module: Mathlib.NumberTheory.Padics.WithVal

Goal state before:
pp: case pos
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
n : ℕ
hn : Valued.v (↑p ^ n) = exp (-↑n)
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
h : (if x' - y' = 0 then 0 else exp (-padicValRat p (x' - y'))) < exp (-↑n)
H : x' - y' = 0
⊢ 0 ≤ (↑p ^ n)⁻¹

pp: case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
n : ℕ
hn : Valued.v (↑p ^ n) = exp (-↑n)
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
h : (if x' - y' = 0 then 0 else exp (-padicValRat p (x' - y'))) < exp (-↑n)
H : ¬x' - y' = 0
⊢ (↑p ^ padicValRat p (x' - y'))⁻¹ ≤ (↑p ^ n)⁻¹

Tactic:
· simp

Goal state after:
case neg
p : ℕ
inst✝ : Fact (Nat.Prime p)
hp0' : 0 < ↑p
hp0 : 0 < (↑p)⁻¹
hp1' : 1 < ↑p
hp1 : (↑p)⁻¹ < 1
n : ℕ
hn : Valued.v (↑p ^ n) = exp (-↑n)
x y : WithVal (Rat.padicValuation p)
x' : ℚ := (WithVal.equiv (Rat.padicValuation p)) x
hx : x' = (WithVal.equiv (Rat.padicValuation p)) x
y' : ℚ := (WithVal.equiv (Rat.padicValuation p)) y
hy : y' = (WithVal.equiv (Rat.padicValuation p)) y
h : (if x' - y' = 0 then 0 else exp (-padicValRat p (x' - y'))) < exp (-↑n)
H : ¬x' - y' = 0
⊢ (↑p ^ padicValRat p (x' - y'))⁻¹ ≤ (↑p ^ n)⁻¹