-- Mathlib/RingTheory/AdjoinRoot.lean
theorem of.injective_of_degree_ne_zero [IsDomain R] (hf : f.degree ≠ 0) :
    Function.Injective (AdjoinRoot.of f)

Proof state:
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
⊢ Function.Injective ⇑(of f)

Tactic:
rw [injective_iff_map_eq_zero]

Result:
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
⊢ ∀ (a : R), (of f) a = 0 → a = 0

Proof state:
case neg
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : f ∣ C p
h : ¬f = 0
⊢ p = 0

Tactic:
contrapose! hf with h_contra

Result:
case neg
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ f.degree = 0

Proof state:
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ C p ≠ 0

Tactic:
rwa [Ne, C_eq_zero]

Result:
no goals

Proof state:
case neg
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ f.degree = 0

Tactic:
rw [← degree_C h_contra]

Result:
case neg
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ f.degree = (C p).degree

Proof state:
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : f ∣ C p
⊢ p = 0

Tactic:
by_cases h : f = 0

Result:
case pos
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : f ∣ C p
h : f = 0
⊢ p = 0

case neg
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : f ∣ C p
h : ¬f = 0
⊢ p = 0

Proof state:
case neg
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ f.degree = (C p).degree

Tactic:
apply le_antisymm (degree_le_of_dvd hp (by rwa [Ne, C_eq_zero])) _

Result:
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ (C p).degree ≤ f.degree

Proof state:
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : (of f) p = 0
⊢ p = 0

Tactic:
rw [AdjoinRoot.of, RingHom.comp_apply, AdjoinRoot.mk_eq_zero] at hp

Result:
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : f ∣ C p
⊢ p = 0

Proof state:
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : f ∣ C p
h : f = 0
⊢ 0 ∣ C p

Tactic:
rwa [h] at hp

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
⊢ ∀ (a : R), (of f) a = 0 → a = 0

Tactic:
intro p hp

Result:
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : (of f) p = 0
⊢ p = 0

Proof state:
case pos
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
hf : f.degree ≠ 0
p : R
hp : f ∣ C p
h : f = 0
⊢ p = 0

Tactic:
exact C_eq_zero.mp (eq_zero_of_zero_dvd (by rwa [h] at hp))

Result:
no goals

Proof state:
R : Type u
inst✝¹ : CommRing R
f : R[X]
inst✝ : IsDomain R
p : R
hp : f ∣ C p
h : ¬f = 0
h_contra : p ≠ 0
⊢ (C p).degree ≤ f.degree

Tactic:
rwa [degree_C h_contra, zero_le_degree_iff]

Result:
no goals