-- Mathlib/RingTheory/Polynomial/Eisenstein/Basic.lean
theorem exists_mem_adjoin_mul_eq_pow_natDegree {x : S} (hx : aeval x f = 0) (hmo : f.Monic)
    (hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})) : ∃ y ∈ adjoin R ({x} : Set S),
    (algebraMap R S) p * y = x ^ (f.map (algebraMap R S)).natDegree

Proof state:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
φ : ℕ → R
hx :
  x ^ (Polynomial.map (algebraMap R S) f).natDegree =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ -1 * ∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (algebraMap R S) (φ ↑i) * x ^ ↑i ∈ adjoin R {x}

Tactic:
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)) _))

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
φ : ℕ → R
hx :
  x ^ (Polynomial.map (algebraMap R S) f).natDegree =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree

Tactic:
rw [hx, ← mul_sum, neg_eq_neg_one_mul, ← mul_assoc (-1 : S), mul_comm (-1 : S), mul_assoc]

Result:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
φ : ℕ → R
hx :
  x ^ (Polynomial.map (algebraMap R S) f).natDegree =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ y ∈ adjoin R {x},
    (algebraMap R S) p * y =
      (algebraMap R S) p *
        (-1 * ∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (algebraMap R S) (φ ↑i) * x ^ ↑i)

Proof state:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx : (aeval x) f = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
⊢ ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree

Tactic:
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

Result:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx :
  x ^ (Polynomial.map (algebraMap R S) f).natDegree +
      ∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i =
    0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
⊢ ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree

Proof state:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
hx :
  x ^ (Polynomial.map (algebraMap R S) f).natDegree =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
this : ∀ n < f.natDegree, p ∣ f.coeff n
⊢ ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree

Tactic:
choose! φ hφ using this

Result:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
hx :
  x ^ (Polynomial.map (algebraMap R S) f).natDegree =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
φ : ℕ → R
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree

Proof state:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
hx :
  x ^ (Polynomial.map (algebraMap R S) f).natDegree =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
n : ℕ
hn : n < f.natDegree
⊢ p ∣ f.coeff n

Tactic:
exact mem_span_singleton.1 (by simpa using hf.mem hn)

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hx :
  x ^ (Polynomial.map (algebraMap R S) f).natDegree +
      ∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i =
    0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
⊢ ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree

Tactic:
replace hx := eq_neg_of_add_eq_zero_left hx

Result:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
hx :
  x ^ (Polynomial.map (algebraMap R S) f).natDegree =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
⊢ ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree

Proof state:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
hx :
  x ^ (Polynomial.map (algebraMap R S) f).natDegree =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (Polynomial.map (algebraMap R S) f).coeff ↑i * x ^ ↑i
n : ℕ
hn : n < f.natDegree
⊢ f.coeff n ∈ span {p}

Tactic:
simpa using hf.mem hn

Result:
no goals

Proof state:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
φ : ℕ → R
hx :
  x ^ (Polynomial.map (algebraMap R S) f).natDegree =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ ∃ y ∈ adjoin R {x},
    (algebraMap R S) p * y =
      (algebraMap R S) p *
        (-1 * ∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (algebraMap R S) (φ ↑i) * x ^ ↑i)

Tactic:
refine
  ⟨-1 * ∑ i : Fin (f.map (algebraMap R S)).natDegree, (algebraMap R S) (φ i.1) * x ^ i.1, ?_, rfl⟩

Result:
R : Type u
inst✝² : CommRing R
f : R[X]
S : Type v
inst✝¹ : CommRing S
inst✝ : Algebra R S
p : R
x : S
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
φ : ℕ → R
hx :
  x ^ (Polynomial.map (algebraMap R S) f).natDegree =
    -∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (algebraMap R S) p * ((algebraMap R S) (φ ↑i) * x ^ ↑i)
hφ : ∀ n < f.natDegree, f.coeff n = p * φ n
⊢ -1 * ∑ i : Fin (Polynomial.map (algebraMap R S) f).natDegree, (algebraMap R S) (φ ↑i) * x ^ ↑i ∈ adjoin R {x}