mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.RingTheory.Fintype

Goal state before:
pp: case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
⊢ 0 ∉ {1, -1}

Tactic:
·

Goal state after:
case inr
R : Type u_1
inst✝² : Ring R
inst✝¹ : Fintype R
inst✝ : DecidableEq R
h✝ : Fintype.card R ≤ 3
h : Fintype.card R = 3
this : Nontrivial R
⊢ 0 ∉ {1, -1}
Module: Mathlib.RingTheory.Fintype

Goal state before:
pp: case pos
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : Finite M₀
a : M₀
h : IsUnit a
⊢ orderOf a < Nat.card M₀

pp: case neg
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : Finite M₀
a : M₀
h : ¬IsUnit a
⊢ orderOf a < Nat.card M₀

Tactic:
·

Goal state after:
case pos
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : Finite M₀
a : M₀
h : IsUnit a
⊢ orderOf a < Nat.card M₀
Module: Mathlib.RingTheory.Fintype

Goal state before:
pp: case neg
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : Finite M₀
a : M₀
h : ¬IsUnit a
⊢ orderOf a < Nat.card M₀

Tactic:
·

Goal state after:
case neg
M₀ : Type u_1
inst✝² : MonoidWithZero M₀
inst✝¹ : Nontrivial M₀
inst✝ : Finite M₀
a : M₀
h : ¬IsUnit a
⊢ orderOf a < Nat.card M₀
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
x : 𝓞 K
hx : x ≠ 0
hx' : (algebraMap (𝓞 K) K) x ≠ 0
f : InfinitePlace K → ℝ≥0 := fun w ↦ ⟨w ↑x / 2, ⋯⟩
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : ∏ w, g w ^ w.mult = ↑B
y : 𝓞 K
h_ynz : y ≠ 0
h_yle : ∀ (w : InfinitePlace K), w ↑y < ↑(g w)
w : InfinitePlace K
hw : w ≠ w₁
⊢ ↑(f w) < w ↑x

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
x : 𝓞 K
hx : x ≠ 0
hx' : (algebraMap (𝓞 K) K) x ≠ 0
f : InfinitePlace K → ℝ≥0 := fun w ↦ ⟨w ↑x / 2, ⋯⟩
this : ∀ (w : InfinitePlace K), w ≠ w₁ → f w ≠ 0
g : InfinitePlace K → ℝ≥0
h_geqf : ∀ (w : InfinitePlace K), w ≠ w₁ → g w = f w
h_gprod : ∏ w, g w ^ w.mult = ↑B
y : 𝓞 K
h_ynz : y ≠ 0
h_yle : ∀ (w : InfinitePlace K), w ↑y < ↑(g w)
w : InfinitePlace K
hw : w ≠ w₁
⊢ ↑(f w) < w ↑x
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
r : ℕ
hr3 : r < 3
hr : r ∈ Finset.Ico 0 3
h : (algebraMap (𝓞 K) K) ↑u = ζ ^ r
⊢ u = η ^ r ∨ u = -η ^ r

pp: case inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
r : ℕ
hr3 : r < 3
hr : r ∈ Finset.Ico 0 3
h : (algebraMap (𝓞 K) K) ↑u = -ζ ^ r
⊢ u = η ^ r ∨ u = -η ^ r

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
r : ℕ
hr3 : r < 3
hr : r ∈ Finset.Ico 0 3
h : (algebraMap (𝓞 K) K) ↑u = ζ ^ r
⊢ u = η ^ r ∨ u = -η ^ r
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
r : ℕ
hr3 : r < 3
hr : r ∈ Finset.Ico 0 3
h : (algebraMap (𝓞 K) K) ↑u = -ζ ^ r
⊢ u = η ^ r ∨ u = -η ^ r

Tactic:
·

Goal state after:
case inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
u : (𝓞 K)ˣ
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hrank : rank K = 0
x : ↥(torsion K)
e : Fin (rank K) → ℤ
hxu : u = ↑x
n : ℕ
hnpos : 0 < n
hn : (algebraMap (𝓞 K) K) ↑u ^ ↑⟨n, hnpos⟩ = 1
r : ℕ
hr3 : r < 3
hr : r ∈ Finset.Ico 0 3
h : (algebraMap (𝓞 K) K) ↑u = -ζ ^ r
⊢ u = η ^ r ∨ u = -η ^ r
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
⊢ ∃ u, ∀ (w : InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (𝓞 K) K) ↑u)) < 0

pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
⊢ ∃ n m, n < m ∧ Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}

Tactic:
·

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
w₁ : InfinitePlace K
B : ℕ
hB : minkowskiBound K 1 < ↑(convexBodyLTFactor K) * ↑B
n m : ℕ
hnm : n < m
h : Ideal.span {↑(seq K w₁ hB n)} = Ideal.span {↑(seq K w₁ hB m)}
⊢ ∃ u, ∀ (w : InfinitePlace K), w ≠ w₁ → Real.log (w ((algebraMap (𝓞 K) K) ↑u)) < 0
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case «0»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑1 - ↑n
⊢ 1 = 1 ∨ 1 = -1

pp: case «1»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-1) - ↑n
⊢ -1 = 1 ∨ -1 = -1

pp: case «2»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑⋯.unit - ↑n
⊢ ⋯.unit = 1 ∨ ⋯.unit = -1

pp: case «3»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit) - ↑n
⊢ -⋯.unit = 1 ∨ -⋯.unit = -1

pp: case «4»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(⋯.unit ^ 2) - ↑n
⊢ ⋯.unit ^ 2 = 1 ∨ ⋯.unit ^ 2 = -1

pp: case «5»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ -⋯.unit ^ 2 = 1 ∨ -⋯.unit ^ 2 = -1

Tactic:
·

Goal state after:
case «0»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑1 - ↑n
⊢ 1 = 1 ∨ 1 = -1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case «1»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-1) - ↑n
⊢ -1 = 1 ∨ -1 = -1

pp: case «2»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑⋯.unit - ↑n
⊢ ⋯.unit = 1 ∨ ⋯.unit = -1

pp: case «3»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit) - ↑n
⊢ -⋯.unit = 1 ∨ -⋯.unit = -1

pp: case «4»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(⋯.unit ^ 2) - ↑n
⊢ ⋯.unit ^ 2 = 1 ∨ ⋯.unit ^ 2 = -1

pp: case «5»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ -⋯.unit ^ 2 = 1 ∨ -⋯.unit ^ 2 = -1

Tactic:
·

Goal state after:
case «1»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-1) - ↑n
⊢ -1 = 1 ∨ -1 = -1
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 < |v w w| - v w w + ∑ x, v w x

pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
⊢ v w x < 0

Tactic:
·

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 < |v w w| - v w w + ∑ x, v w x
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 ≤ |v w w| - v w w

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 < ∑ x, v w x

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 ≤ |v w w| - v w w
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case «2»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑⋯.unit - ↑n
⊢ False

pp: case «3»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit) - ↑n
⊢ False

pp: case «4»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(⋯.unit ^ 2) - ↑n
⊢ False

pp: case «5»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ False

Tactic:
·

Goal state after:
case «2»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑⋯.unit - ↑n
⊢ False
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case «3»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit) - ↑n
⊢ False

pp: case «4»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(⋯.unit ^ 2) - ↑n
⊢ False

pp: case «5»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ False

Tactic:
·

Goal state after:
case «3»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit) - ↑n
⊢ False
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 < ∑ x, v w x

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w : { w // w ≠ w₀ }
⊢ 0 < ∑ x, v w x
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case «4»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(⋯.unit ^ 2) - ↑n
⊢ False

pp: case «5»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ False

Tactic:
·

Goal state after:
case «4»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(⋯.unit ^ 2) - ↑n
⊢ False
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case «5»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ False

Tactic:
·

Goal state after:
case «5»
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
hcong : ∃ n, 3 ∣ ↑(-⋯.unit ^ 2) - ↑n
⊢ False
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
⊢ v w x < 0

Tactic:
·

Goal state after:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
⊢ v w x < 0
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
⊢ 0 < ↑(↑x).mult

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
⊢ ↑x ≠ ↑w

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
⊢ 0 < ↑(↑x).mult
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
⊢ ↑x ≠ ↑w

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
B : Basis { w // w ≠ w₀ } ℝ ({ w // w ≠ w₀ } → ℝ) := Pi.basisFun ℝ { w // w ≠ w₀ }
v : { w // w ≠ w₀ } → logSpace K := fun w ↦ (logEmbedding K) (Additive.ofMul ⋯.choose)
w x : { w // w ≠ w₀ }
hx : x ∈ univ.erase w
⊢ ↑x ≠ ↑w
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Metric.closedBall 0 1 ∈ nhds 0

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Metric.closedBall 0 1).Finite

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ Metric.closedBall 0 1 ∈ nhds 0
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Metric.closedBall 0 1).Finite

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Metric.closedBall 0 1).Finite
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 0
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 1
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = -1
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
·

Goal state after:
case inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 0
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 1
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = -1
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
·

Goal state after:
case inr.inl
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = 1
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Submodule.map (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))).toIntLinearMap ⊤).FG

pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (⊤ ⊓ (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))).toIntLinearMap.ker).FG

Tactic:
·

Goal state after:
case refine_1
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (Submodule.map (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))).toIntLinearMap ⊤).FG
Module: Mathlib.NumberTheory.NumberField.Units.DirichletTheorem

Goal state before:
pp: case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (⊤ ⊓ (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))).toIntLinearMap.ker).FG

Tactic:
·

Goal state after:
case refine_2
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
⊢ (⊤ ⊓ (MonoidHom.toAdditive (QuotientGroup.mk' (torsion K))).toIntLinearMap.ker).FG
Module: Mathlib.NumberTheory.NumberField.Cyclotomic.Three

Goal state before:
pp: case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = -1
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1

Tactic:
·

Goal state after:
case inr.inr
K : Type u_1
inst✝² : Field K
ζ : K
hζ : IsPrimitiveRoot ζ 3
x : 𝓞 K
inst✝¹ : NumberField K
inst✝ : IsCyclotomicExtension {3} ℚ K
this : Finite (𝓞 K ⧸ Ideal.span {λ})
x✝² : Fintype (𝓞 K ⧸ Ideal.span {λ}) := Fintype.ofFinite (𝓞 K ⧸ Ideal.span {λ})
x✝¹ : Ring (𝓞 K ⧸ Ideal.span {λ}) := (Ideal.Quotient.commRing (Ideal.span {λ})).toRing
x✝ : AddGroup (𝓞 K ⧸ Ideal.span {λ}) := x✝¹.toAddGroupWithOne.toAddGroup
h3 : Fintype.card (𝓞 K ⧸ Ideal.span {λ}) = 3
h : (Ideal.Quotient.mk (Ideal.span {λ})) x = -1
⊢ λ ∣ x ∨ λ ∣ x - 1 ∨ λ ∣ x + 1