mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ∑ j, ‖(basisMatrix K)ᵀ⁻¹ i j‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖ ≤
    ∑ j, ‖(basisMatrix K)ᵀ⁻¹‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ∑ j, ‖(basisMatrix K)ᵀ⁻¹‖ * ‖σ ((algebraMap (𝓞 K) K) α) j‖ ≤
    ∑ x, ‖fun i j ↦ (basisMatrix K)ᵀ⁻¹ i j‖ * house ((algebraMap (𝓞 K) K) α)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
σ : K →+* (K →+* ℂ) → ℂ := canonicalEmbedding K
⊢ ∑ x, ‖fun i j ↦ (basisMatrix K)ᵀ⁻¹ i j‖ * house ((algebraMap (𝓞 K) K) α) =
    ↑(finrank ℚ K) * ‖(basisMatrix K)ᵀ⁻¹‖ * house ((algebraMap (𝓞 K) K) α)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝² : Field K
inst✝¹ : NumberField K
inst✝ : DecidableEq (K →+* ℂ)
α : 𝓞 K
i : K →+* ℂ
⊢ ‖↑((((integralBasis K).reindex (equivReindex K).symm).repr ↑α) i)‖ ≤ c K * house ((algebraMap (𝓞 K) K) α)

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 0 ≤ supOfBasis K

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: ⊢ Tendsto (fun k ↦ ↑k ^ (↑k)⁻¹) atTop (𝓝 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: R : Type u_1
inst✝ : Semiring R
T : Type u_2
l : List T
y x : R
⊢ (List.mapIdx (fun i x_1 ↦ x * y ^ i) l).sum = x * (List.mapIdx (fun i x ↦ y ^ i) l).sum

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: T : Type u_1
F : Type u_2
inst✝ : DivisionRing F
l : List T
y : F
hy : y ≠ 1
⊢ (∑ i,
      match l.zipIdx[↑i] with
      | (a, i) => y ^ i) =
    ∑ i, y ^ ↑i

Tactic:
simp only

Goal state after:
T : Type u_1
F : Type u_2
inst✝ : DivisionRing F
l : List T
y : F
hy : y ≠ 1
⊢ ∑ x, y ^ l.zipIdx[↑x].2 = ∑ i, y ^ ↑i
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: T : Type u_1
F : Type u_2
inst✝ : DivisionRing F
l : List T
y : F
hy : y ≠ 1
e : Fin l.zipIdx.length ≃ Fin l.length := finCongr ⋯
x✝ : Fin l.zipIdx.length
⊢ y ^ l.zipIdx[↑x✝].2 = y ^ ↑(e x✝)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: T : Type u_1
F : Type u_2
inst✝ : DivisionRing F
l : List T
y : F
hy : y ≠ 1
⊢ (List.mapIdx (fun i x ↦ y ^ i) l).sum = (y ^ l.length - 1) / (y - 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
⊢ (∀ (n : ℕ), f ↑n = g ↑n) ↔ f = g

Tactic:
by

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
k' : α
hs : ∀ (b : K →+* ℂ), (fun l ↦ ((newBasis K).repr (a k' l.1 * (newBasis K) l.2)) b) = 0 (k', b)
l : β
b : K →+* ℂ
⊢ (newBasis K).repr (a k' l * (newBasis K) b) = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ 0 ≤ f ↑x.num

Tactic:
by

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
⊢ asiegel K a ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
x✝ : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n
c : ℝ
hc : 0 < c
h : ∀ (n : ℕ), f ↑n ^ c = g ↑n
x : ℚ
⊢ 0 ≤ f ↑x.den

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
β : Type u_3
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
⊢ ξ K x ≠ 0

Tactic:
by

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)
l : β
k : α
r : K →+* ℂ
⊢ a k l * (newBasis K) r = ∑ u, ↑(a' K a k l r u) * (newBasis K) u

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
⊢ (∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = g ↑n) ↔ f.IsEquiv g

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ∀ (x y : ℚ), ↑(padicNorm p (x * y)) = ↑(padicNorm p x) * ↑(padicNorm p y)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
n : ℤ
⊢ (padic p) ↑n ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
⊢ ∃ n, n ≠ 0 ∧ f ↑n ≠ 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
⊢ ∃ p, (0 < f ↑p ∧ f ↑p < 1) ∧ ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m

Tactic:
by

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)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
⊢ ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0

Tactic:
by

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)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
⊢ 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : v ∈ T
⊢ A *ᵥ v ∈ S

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ 2 ≤ p

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq β
⊢ #T = (B + 1) ^ n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
⊢ N i ≤ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
⊢ 0 ≤ P i + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
i : α
⊢ N i ≤ P i + 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
hp2 : 2 ≤ a * b
ha : a < a * b
hb : b < a * b
⊢ a * b ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
a b : ℕ
hp0 : 0 < f ↑(a * b)
hp1 : f ↑(a * b) < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → a * b ≤ m
hp2 : 2 ≤ a * b
ha : a < a * b
hb : b < a * b
ha₀ : a ≠ 0
hb₀ : b ≠ 0
n : ℕ
hn₀ : n ≠ 0
hn : n < a * b
⊢ 1 ≤ f ↑n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : Fintype α
inst✝¹ : Fintype β
A : Matrix α β ℤ
inst✝ : DecidableEq α
⊢ ↑(#S) = ∏ i, (P i - N i + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hA : A ≠ 0
⊢ 1 ≤ ‖A‖

Tactic:
by

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

Goal state before:
pp: case convert_4
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
C : ClassGroup (𝓞 K)
h₁ :
  ∀ (s : ℝ),
    {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ s} =
      ⇑(toMixed K) ⁻¹' {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ s}
h₂ : {x | x ∈ fundamentalCone K ∧ mixedEmbedding.norm x ≤ 1} = normLeOne K
J : ↥(Ideal (𝓞 K))⁰
hJ : ClassGroup.mk0 J = C⁻¹
h₃ : ↑(absNorm ↑J) ≠ 0
⊢ MeasureTheory.volume
      (frontier {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ 1}) =
    0

Tactic:
· rw [h₁, ← (toMixed K).coe_toHomeomorph, ← Homeomorph.preimage_frontier,
      (toMixed K).coe_toHomeomorph, (volumePreserving_toMixed K).measure_preimage
      measurableSet_frontier.nullMeasurableSet, h₂, volume_frontier_normLeOne]

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ Nat.Prime p

Tactic:
by

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)
⊢ Tendsto (fun s ↦ ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s ∧ ClassGroup.mk0 I = C }) / s) atTop
    (𝓝 (2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|)))

Tactic:
by

Goal state after:
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
i : α
x✝ : i ∈ univ
⊢ ↑n * max 1 ‖A‖ * ↑B = ∑ x, max 1 ‖A‖ * ↑B

Tactic:
by

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

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
s : ℝ
hs : 0 ≤ s
⊢ Fintype { I // ↑(absNorm ↑I) ≤ s }

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ x ^ ↑k < x ^ logb M (1 / 2)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ x ^ logb M (1 / 2) ≤ x ^ logb x (1 / 2)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
x : ℝ
hx0 : 0 < x
hx1 : x < 1
hxM : x ≤ M
⊢ x ^ k < 1 / 2

Tactic:
by

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)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
k : α
lin_0 : ∀ (u : K →+* ℂ), ∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r)) = 0
this : 0 = ∑ u, (∑ r, ∑ l, ↑(a' K a k l r u) * ↑(x (l, r))) * (newBasis K) u
⊢ 0 = ∑ r, ∑ l, ↑(x (l, r)) * ∑ u, ↑(a' K a k l r u) * (newBasis K) u

Tactic:
by

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

Goal state after:
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
⊢ ∏ x, (∑ x_1, ↑B * ↑(A x x_1)⁺ - ∑ x_1, ↑B * -↑(A x x_1)⁻ + 1) ≤ ∏ x, (↑n * max 1 ‖A‖ * ↑B + 1)

Tactic:
by

Goal state after:
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
⊢ ∏ x, (↑n * max 1 ‖A‖ * ↑B + 1) = (↑n * max 1 ‖A‖ * ↑B + 1) ^ m

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ f 1 = f (↑a * ↑p ^ k + ↑b * ↑m ^ k)

Tactic:
by

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

Goal state after:
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‖) ^ m * (↑B + 1) ^ m = ((↑n * max 1 ‖A‖) ^ e) ^ (↑n - ↑m) * (↑B + 1) ^ m

Tactic:
by

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

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ f (↑a * ↑p ^ k) + f (↑b * ↑m ^ k) ≤ 1 * f ↑p ^ k + 1 * f ↑m ^ k

Tactic:
by

Goal state after:
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‖) ^ e) ^ (↑n - ↑m) * (↑B + 1) ^ m < (↑B + 1) ^ (↑n - ↑m) * (↑B + 1) ^ m

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ TotallyBounded Set.univ

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ CompactSpace ℤ_[p]

Tactic:
by

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

Goal state before:
pp: p : ℕ
inst✝ : Fact (Nat.Prime p)
⊢ ProperSpace ℚ_[p]

Tactic:
by

Goal state after:
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
⊢ (↑B + 1) ^ (↑n - ↑m) * (↑B + 1) ^ m = (↑B + 1) ^ n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
hm : f ↑m < 1
M : ℝ := max (f ↑p) (f ↑m)
hM : M = max (f ↑p) (f ↑m)
k : ℕ := ⌈logb M (1 / 2)⌉₊ + 1
hk : k = ⌈logb M (1 / 2)⌉₊ + 1
a b : ℤ
bezout : a * ↑p ^ k + b * ↑m ^ k = 1
le_half : ∀ {x : ℝ}, 0 < x → x < 1 → x ≤ M → x ^ k < 1 / 2
⊢ 1 * f ↑p ^ k + 1 * f ↑m ^ k < 1

Tactic:
by

Goal state after:
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
⊢ #S < #T

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
m : ℕ
hpm : ¬p ∣ m
⊢ f ↑m = 1

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformAddGroup α
f : β → α
⊢ Summable f ↔ (CauchySeq fun s ↦ ∑ b ∈ s, f b) ∧ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
⊢ A *ᵥ (x - y) = 0

Tactic:
by

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)
x : β × (K →+* ℂ) → ℤ
hxl : x ≠ 0
inst✝ : Fintype β
hmulvec0 : asiegel K a *ᵥ x = 0
⊢ a *ᵥ ξ K x = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hp : 1 < ↑p
⊢ f ↑p = ↑p ^ (- -logb (↑p) (f ↑p))

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion

Goal state before:
pp: G : Type u_1
inst✝³ : AddGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformAddGroup G
inst✝ : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : U ∈ 𝓝 0
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : C ∈ 𝓝 0
C_closed : IsClosed C
⊢ C ∈ 𝓝 (toCompl 0)

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion

Goal state before:
pp: G : Type u_1
inst✝³ : AddGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformAddGroup G
inst✝ : NonarchimedeanAddGroup G
U : Set (Completion G)
hU : U ∈ 𝓝 0
C : Set (Completion G)
C_subset_U : id C ⊆ U
hC : C ∈ 𝓝 0
C_closed : IsClosed C
this : ⇑toCompl ⁻¹' C ∈ 𝓝 0
W : OpenAddSubgroup G
hCW : ↑W ⊆ ⇑toCompl ⁻¹' C
V : Set (Completion G) := ↑(map toCompl ↑W).topologicalClosure
⊢ IsOpen V

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.Nonarchimedean.Completion

Goal state before:
pp: G : Type u_1
inst✝³ : AddGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformAddGroup G
inst✝ : NonarchimedeanAddGroup G
⊢ ∀ U ∈ 𝓝 0, ∃ V, ↑V ⊆ U

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
p : ℕ
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
⊢ ∃ t, 0 < t ∧ f ↑p = ↑p ^ (-t)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : Fintype α
inst✝ : Fintype β
A : Matrix α β ℤ
hn : m < n
hm : 0 < m
x : β → ℤ
hxT : x ∈ T
y : β → ℤ
hyT : y ∈ T
hneq : x ≠ y
hfeq : A *ᵥ x = A *ᵥ y
⊢ 0 ≤ (↑n * max 1 ‖A‖) ^ e

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: α : Type u_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : α → G
hf : Tendsto f cofinite (𝓝 1)
⊢ CauchySeq fun s ↦ ∏ i ∈ s, f i

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n ↦ f (n + 1) / f n) atTop (𝓝 1)
this : Tendsto (fun p ↦ f p.2 / f p.1) atTop (𝓝 1)
⊢ CauchySeq f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : s ∈ 𝓝 1
t : OpenSubgroup G
ht : ↑t ⊆ s
⊢ ∃ N, ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n ↦ f (n + 1) / f n) atTop (𝓝 1)
s : Set G
hs : s ∈ 𝓝 1
t : OpenSubgroup G
ht : ↑t ⊆ s
N : ℕ
hN : ∀ (b : ℕ), N ≤ b → f (b + 1) / f b ∈ t
M : ℕ
hMN : N ≤ M
k : ℕ
ih : f (M, M + k).2 / f (M, M + k).1 ∈ ↑t
⊢ N ≤ M + k

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : IsUniformGroup G
inst✝ : NonarchimedeanGroup G
f : ℕ → G
hf : Tendsto (fun n ↦ f (n + 1) / f n) atTop (𝓝 1)
⊢ CauchySeq f

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_3
inst✝⁴ : Ring R
inst✝³ : UniformSpace R
inst✝² : IsUniformAddGroup R
inst✝¹ : NonarchimedeanRing R
inst✝ : CompleteSpace R
f : α → R
g : β → R
hf : Summable f
hg : Summable g
⊢ Summable fun i ↦ f i.1 * g i.2

Tactic:
by

Goal state after:
Module: Mathlib.Topology.Algebra.InfiniteSum.Nonarchimedean

Goal state before:
pp: α : Type u_1
β : Type u_2
R : Type u_3
inst✝³ : Ring R
inst✝² : UniformSpace R
inst✝¹ : IsUniformAddGroup R
inst✝ : NonarchimedeanRing R
f : α → R
g : β → R
a b : R
hf : HasSum f a
hg : HasSum g b
⊢ HasSum (fun i ↦ f i.1 * g i.2) (a * b)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
⊢ ∃! p, ∃ (x : Fact (Nat.Prime p)), f.IsEquiv (padic p)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
⊢ ∀ (x y : ℚ), |↑(x * y)| = |↑x| * |↑y|

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
⊢ ∀ (x : ℚ), 0 ≤ |↑x|

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
⊢ ∀ (x : ℚ), |↑x| = 0 ↔ x = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: f g : AbsoluteValue ℚ ℝ
⊢ ∀ (x y : ℚ), |↑(x + y)| ≤ |↑x| + |↑y|

Tactic:
by

Goal state after: