Theorem: FltRegular.CaseI.exists_int_sum_eq_zero'_aux (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✝ x y i : ℤ
⊢ (intGal ↑(galConj K p)) (↑x + ↑y * ↑(hζ.unit' ^ i)) = ↑x + ↑y * ↑(hζ.unit' ^ (-i))
Tactic:
ext1
State after:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ ↑((intGal ↑(galConj K p)) (↑x + ↑y * ↑(hζ.unit' ^ i))) = ↑(↑x + ↑y * ↑(hζ.unit' ^ (-i)))

State before:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ ↑((intGal ↑(galConj K p)) (↑x + ↑y * ↑(hζ.unit' ^ i))) = ↑(↑x + ↑y * ↑(hζ.unit' ^ (-i)))
Tactic:
rw [intGal_apply_coe]
State after:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ ↑(galConj K p) ↑(↑x + ↑y * ↑(hζ.unit' ^ i)) = ↑(↑x + ↑y * ↑(hζ.unit' ^ (-i)))

State before:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ ↑(galConj K p) ↑(↑x + ↑y * ↑(hζ.unit' ^ i)) = ↑(↑x + ↑y * ↑(hζ.unit' ^ (-i)))
Tactic:
simp only [_root_.map_add, map_intCast, _root_.map_mul, AlgHom.coe_coe, zpow_neg, map_units_inv,
  add_right_inj, mul_eq_mul_left_iff, Int.cast_eq_zero]
State after:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) ((algebraMap (𝓞 K) K) ↑(hζ.unit' ^ i)) = ((algebraMap (𝓞 K) K) ↑(hζ.unit' ^ i))⁻¹ ∨ y = 0

State before:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) ((algebraMap (𝓞 K) K) ↑(hζ.unit' ^ i)) = ((algebraMap (𝓞 K) K) ↑(hζ.unit' ^ i))⁻¹ ∨ y = 0
Tactic:
simp_rw [NumberField.Units.coe_zpow]
State after:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i) = ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i)⁻¹ ∨ y = 0

State before:
case h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i) = ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i)⁻¹ ∨ y = 0
Tactic:
left
State after:
case h.h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i) = ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i)⁻¹

State before:
case h.h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i) = ((algebraMap (𝓞 K) K) ↑hζ.unit' ^ i)⁻¹
Tactic:
push_cast
State after:
case h.h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) (ζ ^ i) = (ζ ^ i)⁻¹

State before:
case h.h
p : ℕ+
K : Type u_1
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {p} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
i✝ x y i : ℤ
⊢ (galConj K p) (ζ ^ i) = (ζ ^ i)⁻¹
Tactic:
simp only [map_zpow₀, galConj_zeta_runity hζ, inv_zpow', zpow_neg]
State after:
no goals