Theorem: FltRegular.CaseI.pow_sub_intGalConj_mem (FltRegular/NumberTheory/Cyclotomic/CaseI.lean)

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
⊢ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p) ∈ Ideal.span {↑↑p}
Tactic:
have : Fact (p : ℕ).Prime := ⟨hp⟩
State after:
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
⊢ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p) ∈ Ideal.span {↑↑p}

State before:
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
⊢ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p) ∈ Ideal.span {↑↑p}
Tactic:
obtain ⟨a, ha⟩ := exists_int_sub_pow_prime_dvd p α
State after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
ha : α ^ ↑p - ↑a ∈ Ideal.span {↑↑p}
⊢ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p) ∈ Ideal.span {↑↑p}

State before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
ha : α ^ ↑p - ↑a ∈ Ideal.span {↑↑p}
⊢ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p) ∈ Ideal.span {↑↑p}
Tactic:
rw [Ideal.mem_span_singleton] at ha ⊢
State after:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
ha : ↑↑p ∣ α ^ ↑p - ↑a
⊢ ↑↑p ∣ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)

State before:
case intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
ha : ↑↑p ∣ α ^ ↑p - ↑a
⊢ ↑↑p ∣ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)
Tactic:
obtain ⟨γ, hγ⟩ := ha
State after:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
γ : 𝓞 K
hγ : α ^ ↑p - ↑a = ↑↑p * γ
⊢ ↑↑p ∣ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)

State before:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
γ : 𝓞 K
hγ : α ^ ↑p - ↑a = ↑↑p * γ
⊢ ↑↑p ∣ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)
Tactic:
rw [sub_eq_iff_eq_add] at hγ
State after:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
γ : 𝓞 K
hγ : α ^ ↑p = ↑↑p * γ + ↑a
⊢ ↑↑p ∣ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)

State before:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
γ : 𝓞 K
hγ : α ^ ↑p = ↑↑p * γ + ↑a
⊢ ↑↑p ∣ α ^ ↑p - (intGal ↑(galConj K p)) (α ^ ↑p)
Tactic:
rw [hγ, _root_.map_add, _root_.map_mul, map_natCast, map_intCast, add_sub_add_right_eq_sub,
  ← mul_sub]
State after:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
γ : 𝓞 K
hγ : α ^ ↑p = ↑↑p * γ + ↑a
⊢ ↑↑p ∣ ↑↑p * (γ - (intGal ↑(galConj K p)) γ)

State before:
case intro.intro
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i : ℤ
hp : (↑p).Prime
α : 𝓞 K
this : Fact (↑p).Prime
a : ℤ
γ : 𝓞 K
hγ : α ^ ↑p = ↑↑p * γ + ↑a
⊢ ↑↑p ∣ ↑↑p * (γ - (intGal ↑(galConj K p)) γ)
Tactic:
exact dvd_mul_right _ _
State after:
no goals