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

Goal state before:
pp: case convert_2
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
x✝¹ : euclidean.mixedSpace K
x✝ : ℝ
h : 0 ≤ x✝
⊢ mixedEmbedding.norm ((toMixed K) (x✝ • x✝¹)) =
    x✝ ^ Module.finrank ℝ (euclidean.mixedSpace K) * mixedEmbedding.norm ((toMixed K) x✝¹)

pp: case convert_3
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
⊢ MeasurableSet {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ 1}

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:
·

Goal state after:
case convert_2
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
x✝¹ : euclidean.mixedSpace K
x✝ : ℝ
h : 0 ≤ x✝
⊢ mixedEmbedding.norm ((toMixed K) (x✝ • x✝¹)) =
    x✝ ^ Module.finrank ℝ (euclidean.mixedSpace K) * mixedEmbedding.norm ((toMixed K) x✝¹)
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ -(↑B * (A i j)⁻) ≤ v j * A i j

pp: case h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ v j * A i j ≤ ↑B * (A i j)⁺

pp: case h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ v j * A i j ≤ ↑B * (A i j)⁺

Tactic:
·

Goal state after:
case h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ -(↑B * (A i j)⁻) ≤ v j * A i j
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:
·

Goal state after:
case inl
f : AbsoluteValue ℚ ℝ
bdd : ∀ (n : ℕ), f ↑n ≤ 1
hf_nontriv : ∀ (n : ℕ), n ≠ 0 → f ↑n = 1
⊢ f ↑0 = AbsoluteValue.trivial ↑0
Module: Mathlib.NumberTheory.Ostrowski

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

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.SiegelsLemma

Goal state before:
pp: case h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ v j * A i j ≤ ↑B * (A i j)⁺

pp: case h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ v j * A i j ≤ ↑B * (A i j)⁺

Tactic:
·

Goal state after:
case h.inl
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : 0 ≤ A i j
⊢ v j * A i j ≤ ↑B * (A i j)⁺
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ v j * A i j ≤ ↑B * (A i j)⁺

Tactic:
·

Goal state after:
case h.inr
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
v : β → ℤ
hv : 0 ≤ v ∧ v ≤ B'
mulVec_def : A *ᵥ v = fun i ↦ ∑ j, A i j * v j
i : α
j : β
a✝ : j ∈ univ
hsign : A i j ≤ 0
⊢ v j * A i j ≤ ↑B * (A i j)⁺
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case convert_3
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
⊢ MeasurableSet {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ 1}

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:
·

Goal state after:
case convert_3
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
⊢ MeasurableSet {x | x ∈ ⇑(toMixed K) ⁻¹' fundamentalCone K ∧ mixedEmbedding.norm ((toMixed K) x) ≤ 1}
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:
·

Goal state after:
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
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * ↑(classNumber K) /
      (↑(torsionOrder K) * √|↑(discr K)|) =
    ∑ c, 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|)

pp: case convert_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (fun b ↦ ∑ c, ↑(Nat.card { I // ↑(absNorm ↑I) ≤ b ∧ ClassGroup.mk0 I = c }) / b) =ᶠ[atTop] fun s ↦
    ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s }) / s

Tactic:
·

Goal state after:
case e'_5
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K * ↑(classNumber K) /
      (↑(torsionOrder K) * √|↑(discr K)|) =
    ∑ c, 2 ^ nrRealPlaces K * (2 * π) ^ nrComplexPlaces K * regulator K / (↑(torsionOrder K) * √|↑(discr K)|)
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case refine_1
α : 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
⊢ 0 ≤ ∑ x_1, ↑B * ↑(A i x_1)⁺ - ∑ x_1, ↑B * -↑(A i x_1)⁻ + 1

pp: case refine_2
α : 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
⊢ ∑ x_1, ↑B * ↑(A i x_1)⁺ - ∑ x_1, ↑B * -↑(A i x_1)⁻ + 1 ≤ ↑n * max 1 ‖A‖ * ↑B + 1

Tactic:
·

Goal state after:
case refine_1
α : 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
⊢ 0 ≤ ∑ x_1, ↑B * ↑(A i x_1)⁺ - ∑ x_1, ↑B * -↑(A i x_1)⁻ + 1
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case refine_2
α : 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
⊢ ∑ x_1, ↑B * ↑(A i x_1)⁺ - ∑ x_1, ↑B * -↑(A i x_1)⁻ + 1 ≤ ↑n * max 1 ‖A‖ * ↑B + 1

Tactic:
·

Goal state after:
case refine_2
α : 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
⊢ ∑ x_1, ↑B * ↑(A i x_1)⁺ - ∑ x_1, ↑B * -↑(A i x_1)⁻ + 1 ≤ ↑n * max 1 ‖A‖ * ↑B + 1
Module: Mathlib.NumberTheory.NumberField.Ideal.Asymptotics

Goal state before:
pp: case convert_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (fun b ↦ ∑ c, ↑(Nat.card { I // ↑(absNorm ↑I) ≤ b ∧ ClassGroup.mk0 I = c }) / b) =ᶠ[atTop] fun s ↦
    ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s }) / s

Tactic:
·

Goal state after:
case convert_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (fun b ↦ ∑ c, ↑(Nat.card { I // ↑(absNorm ↑I) ≤ b ∧ ClassGroup.mk0 I = c }) / b) =ᶠ[atTop] fun s ↦
    ↑(Nat.card { I // ↑(absNorm ↑I) ≤ s }) / s
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)|)))
⊢ 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:
apply this.congr'

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)|)))
⊢ (fun x ↦ ↑(Nat.card { I // ↑(absNorm ↑I) ≤ x }) / x + x⁻¹) =ᶠ[atTop] fun s ↦ ↑(Nat.card { I // ↑(absNorm I) ≤ s }) / s
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case hz
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ 0 < ↑n - ↑m

pp: case hxy
α : 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 < ↑B + 1

Tactic:
·

Goal state after:
case hz
α : Type u_1
β : Type u_2
inst✝³ : Fintype α
inst✝² : Fintype β
A : Matrix α β ℤ
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
hn : m < n
hm : 0 < m
⊢ 0 < ↑n - ↑m
Module: Mathlib.NumberTheory.SiegelsLemma

Goal state before:
pp: case hxy
α : 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 < ↑B + 1

Tactic:
·

Goal state after:
case hxy
α : 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 < ↑B + 1
Module: Mathlib.NumberTheory.Padics.ProperSpace

Goal state before:
pp: case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ z.appr k ∈ ↑(Finset.range (p ^ k))

pp: case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ dist z ↑(z.appr k) < ε

Tactic:
·

Goal state after:
case refine_1
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ z.appr k ∈ ↑(Finset.range (p ^ k))
Module: Mathlib.NumberTheory.Padics.ProperSpace

Goal state before:
pp: case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ dist z ↑(z.appr k) < ε

Tactic:
·

Goal state after:
case refine_2
p : ℕ
inst✝ : Fact (Nat.Prime p)
ε : ℝ
hε : ε > 0
k : ℕ
hk : ↑p ^ (-↑k) < ε
z : ℤ_[p]
x✝ : z ∈ Set.univ
⊢ dist z ↑(z.appr k) < ε
Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion

Goal state before:
pp: case mp
α : 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

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

Tactic:
·

Goal state after:
case mp
α : 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
Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion

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

Tactic:
·

Goal state after:
case mpr
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformAddGroup α
f : β → α
⊢ (CauchySeq fun s ↦ ∑ b ∈ s, f b) ∧ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl → Summable f
Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion

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

pp: case mpr.right
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s ↦ ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl

Tactic:
·

Goal state after:
case mpr.left
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s ↦ ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ Summable (⇑toCompl ∘ f)
Module: Mathlib.Topology.Algebra.InfiniteSum.GroupCompletion

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

Tactic:
·

Goal state after:
case mpr.right
α : Type u_1
β : Type u_2
inst✝² : AddCommGroup α
inst✝¹ : UniformSpace α
inst✝ : IsUniformAddGroup α
f : β → α
h_cauchy : CauchySeq fun s ↦ ∑ b ∈ s, f b
h_tsum : ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
⊢ ∑' (i : β), toCompl (f i) ∈ Set.range ⇑toCompl
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)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
⊢ ∀ (i : α × (K →+* ℂ)) (j : β × (K →+* ℂ)), ‖asiegel K a i j‖ ≤ c₂ K * A

pp: case hr
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
⊢ 0 ≤ c₂ K * A

Tactic:
·

Goal state after:
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
⊢ ∀ (i : α × (K →+* ℂ)) (j : β × (K →+* ℂ)), ‖asiegel K a i j‖ ≤ c₂ K * A
Module: Mathlib.NumberTheory.NumberField.House

Goal state before:
pp: case calc_1
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ ‖asiegel K a kr lu‖ = ↑|asiegel K a kr lu|

pp: case calc_2
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ ↑|asiegel K a kr lu| ≤ c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1 * (newBasis K) lu.2))

pp: case calc_3
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1 * (newBasis K) lu.2)) ≤
    c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2))

pp: case calc_4
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * house ((algebraMap (𝓞 K) K) (a kr.1 lu.1)) * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) ≤
    c K * A * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2))

pp: case calc_5
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * A * house ((algebraMap (𝓞 K) K) ((newBasis K) lu.2)) ≤ c K * A * supOfBasis K

pp: case calc_6
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ c K * A * supOfBasis K ≤ c₂ K * A

Tactic:
·

Goal state after:
case calc_1
K : Type u_1
inst✝⁴ : Field K
inst✝³ : NumberField K
α : Type u_2
β : Type u_3
a : Matrix α β (𝓞 K)
inst✝² : Fintype β
A : ℝ
habs : ∀ (k : α) (l : β), house ((algebraMap (𝓞 K) K) (a k l)) ≤ A
inst✝¹ : DecidableEq (K →+* ℂ)
inst✝ : Fintype α
Apos : 0 ≤ A
this : 0 ≤ c K
kr : α × (K →+* ℂ)
lu : β × (K →+* ℂ)
⊢ ‖asiegel K a kr lu‖ = ↑|asiegel K a kr lu|
Module: Mathlib.NumberTheory.Ostrowski

Goal state before:
pp: case refine_1
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hp : Nat.Prime p
this : Fact (Nat.Prime p)
t : ℝ
ht : 0 < t
hpt : f ↑p = ↑p ^ (-t)
n : ℕ
⊢ f ↑n ^ t⁻¹ = (padic p) ↑n

pp: case refine_2
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hp : Nat.Prime p
this : Fact (Nat.Prime p)
t : ℝ
ht : 0 < t
hpt : f ↑p = ↑p ^ (-t)
q : ℕ
x✝ : (fun p ↦ ∃ (h : Fact (Nat.Prime p)), ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic p) ↑n) q
hq : Fact (Nat.Prime q)
heq : ∃ c, 0 < c ∧ ∀ (n : ℕ), f ↑n ^ c = (padic q) ↑n
⊢ q = p

Tactic:
·

Goal state after:
case refine_1
f : AbsoluteValue ℚ ℝ
hf_nontriv : f.IsNontrivial
bdd : ∀ (n : ℕ), f ↑n ≤ 1
p : ℕ
hmin : ∀ (m : ℕ), 0 < f ↑m ∧ f ↑m < 1 → p ≤ m
hp0 : 0 < f ↑p
hp1 : f ↑p < 1
hp : Nat.Prime p
this : Fact (Nat.Prime p)
t : ℝ
ht : 0 < t
hpt : f ↑p = ↑p ^ (-t)
n : ℕ
⊢ f ↑n ^ t⁻¹ = (padic p) ↑n