[GOAL]
R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
A : Type v
inst✝ : CommRing A
φ : R →+* A
⊢ IsWeaklyEisensteinAt (Polynomial.map φ f) (Ideal.map φ 𝓟)
[PROOFSTEP]
refine' (IsWeaklyEisensteinAt_iff _ _).2 fun hn => _
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
A : Type v
inst✝ : CommRing A
φ : R →+* A
n✝ : ℕ
hn : n✝ < natDegree (Polynomial.map φ f)
⊢ coeff (Polynomial.map φ f) n✝ ∈ Ideal.map φ 𝓟
[PROOFSTEP]
rw [coeff_map]
[GOAL]
R : Type u
inst✝¹ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
A : Type v
inst✝ : CommRing A
φ : R →+* A
n✝ : ℕ
hn : n✝ < natDegree (Polynomial.map φ f)
⊢ ↑φ (coeff f n✝) ∈ Ideal.map φ 𝓟
[PROOFSTEP]
exact mem_map_of_mem _ (hf.mem (lt_of_lt_of_le hn (natDegree_map_le _ _)))
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
[PROOFSTEP]
rw [aeval_def, Polynomial.eval₂_eq_eval_map, eval_eq_sum_range, range_add_one, sum_insert not_mem_range_self, sum_range,
  (hmo.map (algebraMap R S)).coeff_natDegree, one_mul] at hx 
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) +
      ∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i =
    0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
[PROOFSTEP]
replace hx := eq_neg_of_add_eq_zero_left hx
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
[PROOFSTEP]
have : ∀ n < f.natDegree, p ∣ f.coeff n := by
  intro n hn
  refine' mem_span_singleton.1 (by simpa using hf.mem hn)
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
⊢ ∀ (n : ℕ), n < natDegree f → p ∣ coeff f n
[PROOFSTEP]
intro n hn
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
n : ℕ
hn : n < natDegree f
⊢ p ∣ coeff f n
[PROOFSTEP]
refine' mem_span_singleton.1 (by simpa using hf.mem hn)
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
n : ℕ
hn : n < natDegree f
⊢ coeff f n ∈ span {p}
[PROOFSTEP]
simpa using hf.mem hn
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
this : ∀ (n : ℕ), n < natDegree f → p ∣ coeff f n
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
[PROOFSTEP]
choose! φ hφ using this
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
[PROOFSTEP]
conv_rhs at hx =>
  congr
  congr
  ·skip
  ext i
  rw [coeff_map, hφ i.1 (lt_of_lt_of_le i.2 (natDegree_map_le _ _)), RingHom.map_mul, mul_assoc]
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
[PROOFSTEP]
  congr
  congr
  ·skip
  ext i
  rw [coeff_map, hφ i.1 (lt_of_lt_of_le i.2 (natDegree_map_le _ _)), RingHom.map_mul, mul_assoc]
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
[PROOFSTEP]
  congr
  congr
  ·skip
  ext i
  rw [coeff_map, hφ i.1 (lt_of_lt_of_le i.2 (natDegree_map_le _ _)), RingHom.map_mul, mul_assoc]
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
[PROOFSTEP]
congr
[GOAL]
case a
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| ∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
[PROOFSTEP]
congr
[GOAL]
case a.s
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| univ
case a.f
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| fun i => coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
[PROOFSTEP]
·skip
[GOAL]
case a.s
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| univ
[PROOFSTEP]
skip
[GOAL]
case a.s
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| univ
[PROOFSTEP]
skip
[GOAL]
case a.s
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| univ
[PROOFSTEP]
skip
[GOAL]
case a.f
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
| fun i => coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
[PROOFSTEP]
ext i
[GOAL]
case a.f.h
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
i : Fin (natDegree (Polynomial.map (algebraMap R S) f))
| coeff (Polynomial.map (algebraMap R S) f) ↑i * x ^ ↑i
[PROOFSTEP]
rw [coeff_map, hφ i.1 (lt_of_lt_of_le i.2 (natDegree_map_le _ _)), RingHom.map_mul, mul_assoc]
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
φ : ℕ → R
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)),
        ↑(algebraMap R S) p * (↑(algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
[PROOFSTEP]
rw [hx, ← mul_sum, neg_eq_neg_one_mul, ← mul_assoc (-1 : S), mul_comm (-1 : S), mul_assoc]
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
φ : ℕ → R
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)),
        ↑(algebraMap R S) p * (↑(algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
⊢ ∃ y,
    y ∈ adjoin R {x} ∧
      ↑(algebraMap R S) p * y =
        ↑(algebraMap R S) p *
          (-1 * ∑ x_1 : Fin (natDegree (Polynomial.map (algebraMap R S) f)), ↑(algebraMap R S) (φ ↑x_1) * x ^ ↑x_1)
[PROOFSTEP]
refine' ⟨-1 * ∑ i : Fin (f.map (algebraMap R S)).natDegree, (algebraMap R S) (φ i.1) * x ^ i.1, _, rfl⟩
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
φ : ℕ → R
hx :
  x ^ natDegree (Polynomial.map (algebraMap R S) f) =
    -∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)),
        ↑(algebraMap R S) p * (↑(algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ (n : ℕ), n < natDegree f → coeff f n = p * φ n
⊢ -1 * ∑ i : Fin (natDegree (Polynomial.map (algebraMap R S) f)), ↑(algebraMap R S) (φ ↑i) * x ^ ↑i ∈ adjoin R {x}
[PROOFSTEP]
exact
  Subalgebra.mul_mem _ (Subalgebra.neg_mem _ (Subalgebra.one_mem _))
    (Subalgebra.sum_mem _ fun i _ =>
      Subalgebra.mul_mem _ (Subalgebra.algebraMap_mem _ _)
        (Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton x)) _))
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
⊢ ∀ (i : ℕ), natDegree (Polynomial.map (algebraMap R S) f) ≤ i → ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ i
[PROOFSTEP]
intro i hi
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ i
[PROOFSTEP]
obtain ⟨k, hk⟩ := exists_add_of_le hi
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ i
[PROOFSTEP]
rw [hk, pow_add]
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
[PROOFSTEP]
obtain ⟨y, hy, H⟩ := exists_mem_adjoin_mul_eq_pow_natDegree hx hmo hf
[GOAL]
case intro.intro.intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
y : S
hy : y ∈ adjoin R {x}
H : ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
⊢ ∃ y, y ∈ adjoin R {x} ∧ ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
[PROOFSTEP]
refine' ⟨y * x ^ k, _, _⟩
[GOAL]
case intro.intro.intro.refine'_1
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
y : S
hy : y ∈ adjoin R {x}
H : ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
⊢ y * x ^ k ∈ adjoin R {x}
[PROOFSTEP]
exact Subalgebra.mul_mem _ hy (Subalgebra.pow_mem _ (subset_adjoin (Set.mem_singleton x)) _)
[GOAL]
case intro.intro.intro.refine'_2
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf✝ : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
hf : IsWeaklyEisensteinAt f (Submodule.span R {p})
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
y : S
hy : y ∈ adjoin R {x}
H : ↑(algebraMap R S) p * y = x ^ natDegree (Polynomial.map (algebraMap R S) f)
⊢ ↑(algebraMap R S) p * (y * x ^ k) = x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k
[PROOFSTEP]
rw [← mul_assoc _ y, H]
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
hroot : IsRoot f x
hmo : Monic f
⊢ ∀ (i : ℕ), natDegree f ≤ i → x ^ i ∈ 𝓟
[PROOFSTEP]
intro i hi
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
⊢ x ^ i ∈ 𝓟
[PROOFSTEP]
obtain ⟨k, hk⟩ := exists_add_of_le hi
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ x ^ i ∈ 𝓟
[PROOFSTEP]
rw [hk, pow_add]
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ x ^ natDegree f * x ^ k ∈ 𝓟
[PROOFSTEP]
suffices x ^ f.natDegree ∈ 𝓟 by exact mul_mem_right (x ^ k) 𝓟 this
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
this : x ^ natDegree f ∈ 𝓟
⊢ x ^ natDegree f * x ^ k ∈ 𝓟
[PROOFSTEP]
exact mul_mem_right (x ^ k) 𝓟 this
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
hroot : IsRoot f x
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ x ^ natDegree f ∈ 𝓟
[PROOFSTEP]
rw [IsRoot.def, eval_eq_sum_range, Finset.range_add_one, Finset.sum_insert Finset.not_mem_range_self, Finset.sum_range,
  hmo.coeff_natDegree, one_mul] at *
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
hroot : x ^ natDegree f + ∑ i : Fin (natDegree f), coeff f ↑i * x ^ ↑i = 0
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ x ^ natDegree f ∈ 𝓟
[PROOFSTEP]
rw [eq_neg_of_add_eq_zero_left hroot, Ideal.neg_mem_iff]
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : R
hroot : x ^ natDegree f + ∑ i : Fin (natDegree f), coeff f ↑i * x ^ ↑i = 0
hmo : Monic f
i : ℕ
hi : natDegree f ≤ i
k : ℕ
hk : i = natDegree f + k
⊢ ∑ i : Fin (natDegree f), coeff f ↑i * x ^ ↑i ∈ 𝓟
[PROOFSTEP]
refine' Submodule.sum_mem _ fun i _ => mul_mem_right _ _ (hf.mem (Fin.is_lt i))
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
⊢ ∀ (i : ℕ), natDegree (Polynomial.map (algebraMap R S) f) ≤ i → x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
[PROOFSTEP]
suffices x ^ (f.map (algebraMap R S)).natDegree ∈ 𝓟.map (algebraMap R S)
  by
  intro i hi
  obtain ⟨k, hk⟩ := exists_add_of_le hi
  rw [hk, pow_add]
  refine' mul_mem_right _ _ this
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
this : x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
⊢ ∀ (i : ℕ), natDegree (Polynomial.map (algebraMap R S) f) ≤ i → x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
[PROOFSTEP]
intro i hi
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
this : x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
⊢ x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
[PROOFSTEP]
obtain ⟨k, hk⟩ := exists_add_of_le hi
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
this : x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ x ^ i ∈ Ideal.map (algebraMap R S) 𝓟
[PROOFSTEP]
rw [hk, pow_add]
[GOAL]
case intro
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
this : x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
i : ℕ
hi : natDegree (Polynomial.map (algebraMap R S) f) ≤ i
k : ℕ
hk : i = natDegree (Polynomial.map (algebraMap R S) f) + k
⊢ x ^ natDegree (Polynomial.map (algebraMap R S) f) * x ^ k ∈ Ideal.map (algebraMap R S) 𝓟
[PROOFSTEP]
refine' mul_mem_right _ _ this
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : ↑(aeval x) f = 0
hmo : Monic f
⊢ x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
[PROOFSTEP]
rw [aeval_def, eval₂_eq_eval_map, ← IsRoot.def] at hx 
[GOAL]
R : Type u
inst✝² : CommRing R
𝓟 : Ideal R
f : R[X]
hf : IsWeaklyEisensteinAt f 𝓟
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
x : S
hx : IsRoot (Polynomial.map (algebraMap R S) f) x
hmo : Monic f
⊢ x ^ natDegree (Polynomial.map (algebraMap R S) f) ∈ Ideal.map (algebraMap R S) 𝓟
[PROOFSTEP]
refine' pow_natDegree_le_of_root_of_monic_mem (hf.map _) hx (hmo.map _) _ rfl.le
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
⊢ IsWeaklyEisensteinAt (scaleRoots p x) P
[PROOFSTEP]
refine' ⟨fun i => _⟩
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < natDegree (scaleRoots p x)
⊢ coeff (scaleRoots p x) n✝ ∈ P
[PROOFSTEP]
rw [coeff_scaleRoots]
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i : n✝ < natDegree (scaleRoots p x)
⊢ coeff p n✝ * x ^ (natDegree p - n✝) ∈ P
[PROOFSTEP]
rw [natDegree_scaleRoots, ← tsub_pos_iff_lt] at i 
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
p : R[X]
x : R
P : Ideal R
hP : x ∈ P
n✝ : ℕ
i✝ : n✝ < natDegree p
i : 0 < natDegree p - n✝
⊢ coeff p n✝ * x ^ (natDegree p - n✝) ∈ P
[PROOFSTEP]
exact Ideal.mul_mem_left _ _ (Ideal.pow_mem_of_mem P hP _ i)
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ↑f
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
⊢ x ∣ y ^ natDegree p
[PROOFSTEP]
rw [← natDegree_scaleRoots p x, ← Ideal.mem_span_singleton]
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ↑f
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
⊢ y ^ natDegree (scaleRoots p x) ∈ span {x}
[PROOFSTEP]
refine'
  (scaleRoots.isWeaklyEisensteinAt _ (Ideal.mem_span_singleton.mpr <| dvd_refl x)).pow_natDegree_le_of_root_of_monic_mem
    _ ((monic_scaleRoots_iff x).mpr hp) _ le_rfl
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : Function.Injective ↑f
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
⊢ IsRoot (scaleRoots p x) y
[PROOFSTEP]
rw [injective_iff_map_eq_zero'] at hf 
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), ↑f a = 0 ↔ a = 0
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
⊢ IsRoot (scaleRoots p x) y
[PROOFSTEP]
have : eval₂ _ _ (p.scaleRoots x) = 0 := scaleRoots_eval₂_eq_zero f h
[GOAL]
R : Type u
A : Type u_1
inst✝¹ : CommRing R
inst✝ : CommRing A
f : R →+* A
hf : ∀ (a : R), ↑f a = 0 ↔ a = 0
p : R[X]
hp : Monic p
x y : R
z : A
h : eval₂ f z p = 0
hz : ↑f x * z = ↑f y
this : eval₂ f (↑f x * z) (scaleRoots p x) = 0
⊢ IsRoot (scaleRoots p x) y
[PROOFSTEP]
rwa [hz, Polynomial.eval₂_at_apply, hf] at this 
[GOAL]
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsEisensteinAt f 𝓟
n : ℕ
hn : n ≠ natDegree f
⊢ coeff f n ∈ 𝓟
[PROOFSTEP]
cases' ne_iff_lt_or_gt.1 hn with h₁ h₂
[GOAL]
case inl
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsEisensteinAt f 𝓟
n : ℕ
hn : n ≠ natDegree f
h₁ : n < natDegree f
⊢ coeff f n ∈ 𝓟
[PROOFSTEP]
exact hf.mem h₁
[GOAL]
case inr
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsEisensteinAt f 𝓟
n : ℕ
hn : n ≠ natDegree f
h₂ : n > natDegree f
⊢ coeff f n ∈ 𝓟
[PROOFSTEP]
rw [coeff_eq_zero_of_natDegree_lt h₂]
[GOAL]
case inr
R : Type u
inst✝ : CommSemiring R
𝓟 : Ideal R
f : R[X]
hf : IsEisensteinAt f 𝓟
n : ℕ
hn : n ≠ natDegree f
h₂ : n > natDegree f
⊢ 0 ∈ 𝓟
[PROOFSTEP]
exact Ideal.zero_mem _
