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

Proof state:
case intro.intro.intro
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})
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
y : S
hy : y ∈ adjoin R {x}
H : (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
⊢ ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k

Tactic:
refine ⟨y * x ^ k, ?_, ?_⟩

Result:
case intro.intro.intro.refine_1
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})
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
y : S
hy : y ∈ adjoin R {x}
H : (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
⊢ y * x ^ k ∈ adjoin R {x}

case intro.intro.intro.refine_2
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})
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
y : S
hy : y ∈ adjoin R {x}
H : (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
⊢ (algebraMap R S) p * (y * x ^ k) = x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k

Proof state:
case intro
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})
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
⊢ ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ i

Tactic:
rw [hk, pow_add]

Result:
case intro
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})
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
⊢ ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k

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})
⊢ ∀ (i : ℕ), (Polynomial.map (algebraMap R S) f).natDegree ≤ i → ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ i

Tactic:
intro i hi

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 : (aeval x) f = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
⊢ ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ i

Proof state:
case intro
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})
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
⊢ ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k

Tactic:
obtain ⟨y, hy, H⟩ := exists_mem_adjoin_mul_eq_pow_natDegree hx hmo hf

Result:
case intro.intro.intro
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})
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
y : S
hy : y ∈ adjoin R {x}
H : (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
⊢ ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k

Proof state:
case intro.intro.intro.refine_2
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})
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
y : S
hy : y ∈ adjoin R {x}
H : (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
⊢ (algebraMap R S) p * (y * x ^ k) = x ^ (Polynomial.map (algebraMap R S) f).natDegree * x ^ k

Tactic:
rw [← mul_assoc _ y, H]

Result:
no goals

Proof state:
case intro.intro.intro.refine_1
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})
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
y : S
hy : y ∈ adjoin R {x}
H : (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
⊢ y * x ^ k ∈ adjoin R {x}

Tactic:
exact Subalgebra.mul_mem _ hy (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
hx : (aeval x) f = 0
hmo : f.Monic
hf : f.IsWeaklyEisensteinAt (Submodule.span R {p})
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
⊢ ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ i

Tactic:
obtain ⟨k, hk⟩ := exists_add_of_le hi

Result:
case intro
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})
i : ℕ
hi : (Polynomial.map (algebraMap R S) f).natDegree ≤ i
k : ℕ
hk : i = (Polynomial.map (algebraMap R S) f).natDegree + k
⊢ ∃ y ∈ adjoin R {x}, (algebraMap R S) p * y = x ^ i