Theorem: diff_of_roots2 (FltRegular/NumberTheory/Cyclotomic/CyclRat.lean)

State before:
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
⊢ ∃ u, η₂ - η₁ = ↑u * (1 - η₁)
Tactic:
obtain ⟨u, hu⟩ := diff_of_roots ph hη₁ hη₂ hdiff hwlog
State after:
case intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ - η₂ = ↑u * (1 - η₁)
⊢ ∃ u, η₂ - η₁ = ↑u * (1 - η₁)

State before:
case intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ - η₂ = ↑u * (1 - η₁)
⊢ ∃ u, η₂ - η₁ = ↑u * (1 - η₁)
Tactic:
refine' ⟨-u, _⟩
State after:
case intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ - η₂ = ↑u * (1 - η₁)
⊢ η₂ - η₁ = ↑(-u) * (1 - η₁)

State before:
case intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ - η₂ = ↑u * (1 - η₁)
⊢ η₂ - η₁ = ↑(-u) * (1 - η₁)
Tactic:
rw [Units.val_neg, neg_mul, ← hu]
State after:
case intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ - η₂ = ↑u * (1 - η₁)
⊢ η₂ - η₁ = -(η₁ - η₂)

State before:
case intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hwlog : η₁ ≠ 1
u : (𝓞 (CyclotomicField p ℚ))ˣ
hu : η₁ - η₂ = ↑u * (1 - η₁)
⊢ η₂ - η₁ = -(η₁ - η₂)
Tactic:
ring
State after:
no goals