Theorem: fltIdeals_coprime2_lemma
Proof state before:
case a.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
h : ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
I : Ideal (𝓞 (CyclotomicField p ℚ)) := fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
P : Ideal (𝓞 (CyclotomicField p ℚ))
hP1 : P.IsMaximal
hP2 : I ≤ P
hiP : fltIdeals p x y hη₁ ≤ P
hel1 : ∃ v, ↑v * ↑y * (1 - η₁) ∈ I
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
⊢ False
Tactic:
have HC : 1 - η₁ ∈ P → False := by
  intro h
  have eta_sub_one_ne_zero := sub_ne_zero.mpr (Ne.symm hwlog)
  have hηprime : IsPrime (Ideal.span ({1 - η₁} : Set R)) := by
    rw [span_singleton_prime eta_sub_one_ne_zero]
    apply one_sub_zeta_prime hη₁ hwlog
  have H5 : IsPrime (Ideal.span ({(p : ℤ)} : Set ℤ)) := by
    have h2 : (p : ℤ) ≠ 0 := by simp
    have h1 : Prime (p : ℤ) := by
      rw [← prime_iff_prime_int]
      exact Fact.out
    rw [span_singleton_prime h2]
    apply h1
  have hηP : Ideal.span ({1 - η₁} : Set R) = P := by
    have hle : Ideal.span ({1 - η₁} : Set R) ≤ P := by rw [span_le]; simp [h]
    apply (@Ring.DimensionLeOne.prime_le_prime_iff_eq _ _ _ _ _ hηprime hPrime _).1 hle
    intro hbot
    rw [span_eq_bot] at hbot
    simp only [Set.mem_singleton_iff, forall_eq, sub_eq_zero] at hbot
    exact hwlog hbot.symm
  have hcapZ : P.comap (Int.castRingHom R) = Ideal.span ({(p : ℤ)} : Set ℤ) := by
    have H1 : Ideal.span ({(p : ℤ)} : Set ℤ) ≤ P.comap (Int.castRingHom R) := by
      rw [← hηP]
      apply le_comap_of_map_le _
      rw [map_span]
      simp
      rw [span_singleton_le_span_singleton]
      apply zeta_sub_one_dvb_p ph hη₁ hwlog
    have H2 : IsPrime (P.comap (Int.castRingHom R)) := by
      exact IsPrime.comap _
    have H4 : Ideal.span ({(p : ℤ)} : Set ℤ) ≠ ⊥ := by simp
    apply ((@Ring.DimensionLeOne.prime_le_prime_iff_eq _ _ _ _ _ H5 H2 H4).1 H1).symm
  have hxyinP : (x + y : R) ∈ P := by
    have H1 : (x : R) + η₁ * y ∈ P := by
      apply hiP
      apply Submodule.mem_span_singleton_self
    have H2 : η₁ * y = y - y * (1 - η₁) := by ring
    rw [H2] at H1
    have H3 : ↑x + (↑y - ↑y * (1 - η₁)) = ↑x + ↑y + -↑y * (1 - η₁) := by ring
    rw [H3] at H1
    have H4 : -↑y * (1 - η₁) ∈ P := by
      rw [← hηP]; rw [Ideal.mem_span_singleton']
      refine' ⟨-(y : R), rfl⟩
    apply (Ideal.add_mem_iff_left P H4).1 H1
  have hxyinP2 : x + y ∈ Ideal.span ({(p : ℤ)} : Set ℤ) := by rw [← hcapZ]; simp [hxyinP]
  rw [mem_span_singleton] at hxyinP2
  apply absurd hxyinP2 hp2
Proof state after:
case a.intro.intro
p : ℕ+
L : Type u
inst✝³ : Field L
inst✝² : CharZero L
inst✝¹ : IsCyclotomicExtension {p} ℚ L
inst✝ : Fact (↑p).Prime
ph : 5 ≤ p
x y : ℤ
η₁ η₂ : 𝓞 (CyclotomicField p ℚ)
hη₁ : η₁ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hη₂ : η₂ ∈ nthRootsFinset (↑p) (𝓞 (CyclotomicField p ℚ))
hdiff : η₁ ≠ η₂
hp : IsCoprime x y
hp2 : ¬↑↑p ∣ x + y
hwlog : η₁ ≠ 1
h : ¬fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂ = ⊤
I : Ideal (𝓞 (CyclotomicField p ℚ)) := fltIdeals p x y hη₁ ⊔ fltIdeals p x y hη₂
P : Ideal (𝓞 (CyclotomicField p ℚ))
hP1 : P.IsMaximal
hP2 : I ≤ P
hiP : fltIdeals p x y hη₁ ≤ P
hel1 : ∃ v, ↑v * ↑y * (1 - η₁) ∈ I
hel2 : ∃ v, ↑v * ↑x * (1 - η₁) ∈ I
hel11 : ↑y * (1 - η₁) ∈ P
hel22 : ↑x * (1 - η₁) ∈ P
hPrime : P.IsPrime
hprime2 : ↑y ∈ P ∨ 1 - η₁ ∈ P
hprime3 : ↑x ∈ P ∨ 1 - η₁ ∈ P
HC : 1 - η₁ ∈ P → False
⊢ False