Theorem: systemOfUnits.IsFundamental.corollary (FltRegular/NumberTheory/Hilbert92.lean)

State before:
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
ha : ∃ i, ¬↑↑p ∣ a i
⊢ ∀ (g : G), (1 - zeta ↑p) • g ≠ ∑ i : Fin r, a i • S.units i
Tactic:
intro g hg
State after:
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
ha : ∃ i, ¬↑↑p ∣ a i
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
⊢ False

State before:
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
ha : ∃ i, ¬↑↑p ∣ a i
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
⊢ False
Tactic:
obtain ⟨i, hi⟩ := ha
State after:
case intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
⊢ False

State before:
case intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
⊢ False
Tactic:
letI := Fact.mk hp
State after:
case intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
⊢ False

State before:
case intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
⊢ False
Tactic:
obtain ⟨x, y, e⟩ := CyclotomicIntegers.isCoprime_one_sub_zeta p (a i) hi
State after:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
⊢ False

State before:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
⊢ False
Tactic:
let b' : Fin r → A := fun j ↦ x * (1 - zeta ↑p) + y * (a j)
State after:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
⊢ False

State before:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
⊢ False
Tactic:
let b := Finsupp.ofSupportFinite b' (Set.toFinite (Function.support _))
State after:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
⊢ False

State before:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
⊢ False
Tactic:
have hb : b i = 1 := by rw [← e]; rfl
State after:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ False

State before:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ False
Tactic:
apply lemma2 p hp G r hf S hs i b hb (x • ∑ i, S.units i + y • g)
State after:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ (1 - zeta ↑p) • (x • ∑ i : Fin r, S.units i + y • g) = (Finsupp.total (Fin r) G A S.units) b

State before:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ (1 - zeta ↑p) • (x • ∑ i : Fin r, S.units i + y • g) = (Finsupp.total (Fin r) G A S.units) b
Tactic:
rw [smul_add, smul_smul _ y, mul_comm, ← smul_smul, hg, smul_sum, smul_sum, smul_sum,
  ← sum_add_distrib, Finsupp.total_apply, Finsupp.sum_fintype]
State after:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ ∑ x_1 : Fin r, ((1 - zeta ↑p) • x • S.units x_1 + y • a x_1 • S.units x_1) = ∑ i : Fin r, b i • S.units i

case intro.intro.intro.h
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ ∀ (i : Fin r), 0 • S.units i = 0

State before:
case intro.intro.intro
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ ∑ x_1 : Fin r, ((1 - zeta ↑p) • x • S.units x_1 + y • a x_1 • S.units x_1) = ∑ i : Fin r, b i • S.units i

case intro.intro.intro.h
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ ∀ (i : Fin r), 0 • S.units i = 0
Tactic:
congr
State after:
case intro.intro.intro.e_f
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ (fun x_1 => (1 - zeta ↑p) • x • S.units x_1 + y • a x_1 • S.units x_1) = fun i => b i • S.units i

case intro.intro.intro.h
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ ∀ (i : Fin r), 0 • S.units i = 0

State before:
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
⊢ b i = 1
Tactic:
rw [← e]
State after:
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
⊢ b i = x * (1 - zeta ↑p) + y * ↑(a i)

State before:
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
⊢ b i = x * (1 - zeta ↑p) + y * ↑(a i)
Tactic:
rfl
State after:
no goals

State before:
case intro.intro.intro.e_f
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ (fun x_1 => (1 - zeta ↑p) • x • S.units x_1 + y • a x_1 • S.units x_1) = fun i => b i • S.units i
Tactic:
ext j
State after:
case intro.intro.intro.e_f.h
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
j : Fin r
⊢ (1 - zeta ↑p) • x • S.units j + y • a j • S.units j = b j • S.units j

State before:
case intro.intro.intro.e_f.h
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
j : Fin r
⊢ (1 - zeta ↑p) • x • S.units j + y • a j • S.units j = b j • S.units j
Tactic:
simp only [smul_smul, Finsupp.ofSupportFinite_coe, add_smul, b', b]
State after:
case intro.intro.intro.e_f.h
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
j : Fin r
⊢ ((1 - zeta ↑p) * x) • S.units j + y • a j • S.units j = (x * (1 - zeta ↑p)) • S.units j + (y * ↑(a j)) • S.units j

State before:
case intro.intro.intro.e_f.h
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
j : Fin r
⊢ ((1 - zeta ↑p) * x) • S.units j + y • a j • S.units j = (x * (1 - zeta ↑p)) • S.units j + (y * ↑(a j)) • S.units j
Tactic:
congr 1
State after:
case intro.intro.intro.e_f.h.e_a
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
j : Fin r
⊢ ((1 - zeta ↑p) * x) • S.units j = (x * (1 - zeta ↑p)) • S.units j

case intro.intro.intro.e_f.h.e_a
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
j : Fin r
⊢ y • a j • S.units j = (y * ↑(a j)) • S.units j

State before:
case intro.intro.intro.e_f.h.e_a
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
j : Fin r
⊢ ((1 - zeta ↑p) * x) • S.units j = (x * (1 - zeta ↑p)) • S.units j
Tactic:
rw [mul_comm]
State after:
no goals

State before:
case intro.intro.intro.e_f.h.e_a
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
j : Fin r
⊢ y • a j • S.units j = (y * ↑(a j)) • S.units j
Tactic:
rw [← intCast_smul (k := A), smul_smul]
State after:
no goals

State before:
case intro.intro.intro.h
p : ℕ+
K : Type u_1
inst✝¹⁰ : Field K
inst✝⁹ : NumberField 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
inst✝⁵ : CommGroup H
inst✝⁴ : Fintype H
hCard : Fintype.card H = ↑p
σ : H
hσ : Subgroup.zpowers σ = ⊤
r : ℕ
inst✝³ : DistribMulAction H G
inst✝² : Module.Free ℤ G
inst✝¹ : Module.Finite ℤ G
hf : finrank ℤ G = r * (↑p - 1)
inst✝ : Module A G
S : systemOfUnits p G r
hs : IsFundamental p G r S
a : Fin r → ℤ
g : G
hg : (1 - zeta ↑p) • g = ∑ i : Fin r, a i • S.units i
i : Fin r
hi : ¬↑↑p ∣ a i
this : Fact (↑p).Prime := { out := hp }
x y : A
e : x * (1 - zeta ↑p) + y * ↑(a i) = 1
b' : Fin r → A := fun j => x * (1 - zeta ↑p) + y * ↑(a j)
b : Fin r →₀ A := Finsupp.ofSupportFinite b' ⋯
hb : b i = 1
⊢ ∀ (i : Fin r), 0 • S.units i = 0
Tactic:
simp
State after:
no goals