Theorem: coprime_c_aux (FltRegular/CaseII/InductionStep.lean)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η₁ ≠ η₂
⊢ ((𝔦↑η₁) ⊔ 𝔦↑η₂) ∣ 𝔪 * 𝔭
Tactic:
have : 𝔭 = Ideal.span (singleton <| (η₁ : 𝓞 K) - η₂) := by
  rw [Ideal.span_singleton_eq_span_singleton]
  exact hζ.unit'_coe.associated_sub_one hpri.out η₁.prop η₂.prop (Subtype.coe_injective.ne hη)
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η₁ ≠ η₂
this : 𝔭 = Ideal.span {↑η₁ - ↑η₂}
⊢ ((𝔦↑η₁) ⊔ 𝔦↑η₂) ∣ 𝔪 * 𝔭

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η₁ ≠ η₂
this : 𝔭 = Ideal.span {↑η₁ - ↑η₂}
⊢ ((𝔦↑η₁) ⊔ 𝔦↑η₂) ∣ 𝔪 * 𝔭
Tactic:
rw [(gcd_mul_right' 𝔭 𝔵 𝔶).symm.dvd_iff_dvd_right, dvd_gcd_iff]
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η₁ ≠ η₂
this : 𝔭 = Ideal.span {↑η₁ - ↑η₂}
⊢ ((𝔦↑η₁) ⊔ 𝔦↑η₂) ∣ 𝔵 * 𝔭 ∧ ((𝔦↑η₁) ⊔ 𝔦↑η₂) ∣ 𝔶 * 𝔭

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η₁ ≠ η₂
this : 𝔭 = Ideal.span {↑η₁ - ↑η₂}
⊢ ((𝔦↑η₁) ⊔ 𝔦↑η₂) ∣ 𝔵 * 𝔭 ∧ ((𝔦↑η₁) ⊔ 𝔦↑η₂) ∣ 𝔶 * 𝔭
Tactic:
simp_rw [this, Ideal.span_singleton_mul_span_singleton, Ideal.dvd_span_singleton,
  Ideal.mem_span_singleton_sup, Ideal.mem_span_singleton]
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η₁ ≠ η₂
this : 𝔭 = Ideal.span {↑η₁ - ↑η₂}
⊢ (∃ a b, x + y * ↑η₂ ∣ b ∧ a * (x + y * ↑η₁) + b = x * (↑η₁ - ↑η₂)) ∧
    ∃ a b, x + y * ↑η₂ ∣ b ∧ a * (x + y * ↑η₁) + b = y * (↑η₁ - ↑η₂)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η₁ ≠ η₂
this : 𝔭 = Ideal.span {↑η₁ - ↑η₂}
⊢ (∃ a b, x + y * ↑η₂ ∣ b ∧ a * (x + y * ↑η₁) + b = x * (↑η₁ - ↑η₂)) ∧
    ∃ a b, x + y * ↑η₂ ∣ b ∧ a * (x + y * ↑η₁) + b = y * (↑η₁ - ↑η₂)
Tactic:
refine ⟨⟨-η₂, _, ⟨η₁, rfl⟩, ?_⟩, ⟨1, _, ⟨-1, rfl⟩, ?_⟩⟩
State after:
case refine_1
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η₁ ≠ η₂
this : 𝔭 = Ideal.span {↑η₁ - ↑η₂}
⊢ -↑η₂ * (x + y * ↑η₁) + (x + y * ↑η₂) * ↑η₁ = x * (↑η₁ - ↑η₂)

case refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η₁ ≠ η₂
this : 𝔭 = Ideal.span {↑η₁ - ↑η₂}
⊢ 1 * (x + y * ↑η₁) + (x + y * ↑η₂) * -1 = y * (↑η₁ - ↑η₂)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η₁ ≠ η₂
⊢ 𝔭 = Ideal.span {↑η₁ - ↑η₂}
Tactic:
rw [Ideal.span_singleton_eq_span_singleton]
State after:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η₁ ≠ η₂
⊢ Associated π (↑η₁ - ↑η₂)

State before:
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η₁ ≠ η₂
⊢ Associated π (↑η₁ - ↑η₂)
Tactic:
exact hζ.unit'_coe.associated_sub_one hpri.out η₁.prop η₂.prop (Subtype.coe_injective.ne hη)
State after:
no goals

State before:
case refine_1
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η₁ ≠ η₂
this : 𝔭 = Ideal.span {↑η₁ - ↑η₂}
⊢ -↑η₂ * (x + y * ↑η₁) + (x + y * ↑η₂) * ↑η₁ = x * (↑η₁ - ↑η₂)
Tactic:
ring
State after:
no goals

State before:
case refine_2
K : Type u_1
p : ℕ+
hpri : Fact p.Prime
inst✝³ : Field K
inst✝² : NumberField K
inst✝¹ : IsCyclotomicExtension {p} ℚ K
hp : p ≠ 2
inst✝ : Fintype (ClassGroup (𝓞 K))
hreg : (↑p).Coprime (Fintype.card (ClassGroup (𝓞 K)))
ζ : K
hζ : IsPrimitiveRoot ζ ↑p
x y z : 𝓞 K
ε : (𝓞 K)ˣ
m : ℕ
e : x ^ ↑p + y ^ ↑p = ↑ε * (π ^ (m + 1) * z) ^ ↑p
hy : ¬π ∣ y
hz : ¬π ∣ z
η η₁ η₂ : { x // x ∈ nthRootsFinset (↑p) (𝓞 K) }
hη : η₁ ≠ η₂
this : 𝔭 = Ideal.span {↑η₁ - ↑η₂}
⊢ 1 * (x + y * ↑η₁) + (x + y * ↑η₂) * -1 = y * (↑η₁ - ↑η₂)
Tactic:
ring
State after:
no goals