Theorem: systemOfUnits.existence' (FltRegular/NumberTheory/SystemOfUnits.lean)

State before:
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
⊢ Nonempty (systemOfUnits p G (R + 1))
Tactic:
obtain ⟨g, hg⟩ := ex_not_mem p hp G r hf S hR
State after:
case intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
⊢ Nonempty (systemOfUnits p G (R + 1))

State before:
case intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
⊢ Nonempty (systemOfUnits p G (R + 1))
Tactic:
refine ⟨⟨Fin.cases g S.units, ?_⟩⟩
State after:
case intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
⊢ LinearIndependent (CyclotomicIntegers ↑p) fun i => Fin.cases g S.units i

State before:
case intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
⊢ LinearIndependent (CyclotomicIntegers ↑p) fun i => Fin.cases g S.units i
Tactic:
refine LinearIndependent.fin_cons' g S.units S.linearIndependent (fun a y hy ↦ ?_)
State after:
case intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
hy : a • g + ↑y = 0
⊢ a = 0

State before:
case intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
hy : a • g + ↑y = 0
⊢ a = 0
Tactic:
by_contra! ha
State after:
case intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
hy : a • g + ↑y = 0
ha : a ≠ 0
⊢ False

State before:
case intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
hy : a • g + ↑y = 0
ha : a ≠ 0
⊢ False
Tactic:
letI := Fact.mk hp
State after:
case intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
hy : a • g + ↑y = 0
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
⊢ False

State before:
case intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
hy : a • g + ↑y = 0
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
⊢ False
Tactic:
obtain ⟨n, h0, f, Hf⟩ := CyclotomicIntegers.exists_dvd_int p _ ha
State after:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
hy : a • g + ↑y = 0
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
⊢ False

State before:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : (fun x => f • x) (a • g + ↑y) = (fun x => f • x) 0
⊢ False
Tactic:
simp only at hy
State after:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : f • (a • g + ↑y) = f • 0
⊢ False

State before:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : f • (a • g + ↑y) = f • 0
⊢ False
Tactic:
rw [smul_zero, smul_add, smul_smul, mul_comm f,
  ← Hf, ← eq_neg_iff_add_eq_zero, intCast_smul] at hy
State after:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : n • g = -(f • ↑y)
⊢ False

State before:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : n • g = -(f • ↑y)
⊢ False
Tactic:
apply hg _ h0
State after:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : n • g = -(f • ↑y)
⊢ n • g ∈ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)

State before:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : n • g = -(f • ↑y)
⊢ n • g ∈ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
Tactic:
rw [hy]
State after:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : n • g = -(f • ↑y)
⊢ -(f • ↑y) ∈ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)

State before:
case intro.intro.intro.intro
p : ℕ+
K : Type u_1
inst✝⁸ : Field K
inst✝⁷ : NumberField K
inst✝⁶ : IsCyclotomicExtension {p} ℚ K
k : Type u_2
inst✝⁵ : Field k
inst✝⁴ : NumberField k
hp : (↑p).Prime
G : Type u_3
H : Type u_4
inst✝³ : AddCommGroup G
r : ℕ
inst✝² : Module.Free ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝¹ inst✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
S : systemOfUnits p G R
hR : R < r
g : G
hg : ∀ (k : ℤ), k ≠ 0 → k • g ∉ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
a : CyclotomicIntegers ↑p
y : ↥(Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units))
ha : a ≠ 0
this : Fact (↑p).Prime := { out := hp }
n : ℤ
h0 : n ≠ 0
f : CyclotomicIntegers ↑p
Hf : ↑n = a * f
hy : n • g = -(f • ↑y)
⊢ -(f • ↑y) ∈ Submodule.span (CyclotomicIntegers ↑p) (Set.range S.units)
Tactic:
exact Submodule.neg_mem _ (Submodule.smul_mem _ _ y.2)
State after:
no goals