Theorem: systemOfUnits.spanA_eq_spanZ (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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
⊢ Submodule.restrictScalars ℤ (Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    Submodule.span ℤ (Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1)
Tactic:
letI := Fact.mk hp
State after:
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
⊢ Submodule.restrictScalars ℤ (Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    Submodule.span ℤ (Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1)

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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
⊢ Submodule.restrictScalars ℤ (Submodule.span (CyclotomicIntegers ↑p) (Set.range f)) =
    Submodule.span ℤ (Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1)
Tactic:
rw [← Submodule.span_smul_of_span_eq_top (CyclotomicIntegers.powerBasis p).basis.span_eq,
  Set.range_smul_range]
State after:
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
⊢ Submodule.span ℤ (Set.range fun p_1 => (CyclotomicIntegers.powerBasis ↑p).basis p_1.1 • f p_1.2) =
    Submodule.span ℤ (Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1)

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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
⊢ Submodule.span ℤ (Set.range fun p_1 => (CyclotomicIntegers.powerBasis ↑p).basis p_1.1 • f p_1.2) =
    Submodule.span ℤ (Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1)
Tactic:
congr
State after:
case e_s
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
⊢ (Set.range fun p_1 => (CyclotomicIntegers.powerBasis ↑p).basis p_1.1 • f p_1.2) =
    Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1

State before:
case e_s
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
⊢ (Set.range fun p_1 => (CyclotomicIntegers.powerBasis ↑p).basis p_1.1 • f p_1.2) =
    Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1
Tactic:
ext
State after:
case e_s.h
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
x✝ : G
⊢ (x✝ ∈ Set.range fun p_1 => (CyclotomicIntegers.powerBasis ↑p).basis p_1.1 • f p_1.2) ↔
    x✝ ∈ Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1

State before:
case e_s.h
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
x✝ : G
⊢ (x✝ ∈ Set.range fun p_1 => (CyclotomicIntegers.powerBasis ↑p).basis p_1.1 • f p_1.2) ↔
    x✝ ∈ Set.range fun e => zeta ↑p ^ ↑e.2 • f e.1
Tactic:
simp only [PowerBasis.coe_basis, CyclotomicIntegers.powerBasis_gen, Set.mem_range, Prod.exists]
State after:
case e_s.h
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
x✝ : G
⊢ (∃ a b, zeta ↑p ^ ↑a • f b = x✝) ↔ ∃ a b, zeta ↑p ^ ↑b • f a = x✝

State before:
case e_s.h
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✝ : Module (CyclotomicIntegers ↑p) G
R : ℕ
f : Fin R → G
this : Fact (↑p).Prime := { out := hp }
x✝ : G
⊢ (∃ a b, zeta ↑p ^ ↑a • f b = x✝) ↔ ∃ a b, zeta ↑p ^ ↑b • f a = x✝
Tactic:
rw [exists_comm, CyclotomicIntegers.powerBasis_dim]
State after:
no goals