-- Mathlib/FieldTheory/SplittingField/Construction.lean
lemma isCoprime_iff_aeval_ne_zero (f g : K[X]) : IsCoprime f g ↔ ∀ {A : Type v} [CommRing A]
    [IsDomain A] [Algebra K A] (a : A), aeval a f ≠ 0 ∨ aeval a g ≠ 0

Proof state:
case refine_1
K : Type v
inst✝ : Field K
f g : K[X]
h : (aeval 0) f ≠ 0 ∨ (aeval 0) g ≠ 0
⊢ ¬(f = 0 ∧ g = 0)

Tactic:
contrapose! h

Result:
case refine_1
K : Type v
inst✝ : Field K
f g : K[X]
h : f = 0 ∧ g = 0
⊢ (aeval 0) f = 0 ∧ (aeval 0) g = 0

Proof state:
case refine_2.intro.intro
K : Type v
inst✝ : Field K
x : K[X]
hx : x ∈ nonunits K[X]
x✝ : x ≠ 0
w✝¹ w✝ : K[X]
h : ¬((aeval (AdjoinRoot.root x.factor)) (x * w✝¹) = 0 ∧ (aeval (AdjoinRoot.root x.factor)) (x * w✝) = 0)
⊢ False

Tactic:
simp only [AdjoinRoot.aeval_eq, AdjoinRoot.mk_eq_zero,
  dvd_mul_of_dvd_left <| factor_dvd_of_not_isUnit hx, true_and, not_true] at h

Result:
no goals

Proof state:
case refine_1
K : Type v
inst✝ : Field K
f g : K[X]
h :
  ∀ {A : Type v} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : Algebra K A] (a : A),
    (aeval a) f ≠ 0 ∨ (aeval a) g ≠ 0
⊢ ¬(f = 0 ∧ g = 0)

Tactic:
replace h := @h K _ _ _ 0

Result:
case refine_1
K : Type v
inst✝ : Field K
f g : K[X]
h : (aeval 0) f ≠ 0 ∨ (aeval 0) g ≠ 0
⊢ ¬(f = 0 ∧ g = 0)

Proof state:
case refine_1
K : Type v
inst✝ : Field K
f g : K[X]
h : f = 0 ∧ g = 0
⊢ (aeval 0) f = 0 ∧ (aeval 0) g = 0

Tactic:
rw [h.left, h.right, map_zero, and_self]

Result:
no goals

Proof state:
case refine_2.intro.intro
K : Type v
inst✝ : Field K
x : K[X]
hx : x ∈ nonunits K[X]
x✝ : x ≠ 0
w✝¹ w✝ : K[X]
h :
  ∀ {A : Type v} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : Algebra K A] (a : A),
    (aeval a) (x * w✝¹) ≠ 0 ∨ (aeval a) (x * w✝) ≠ 0
⊢ False

Tactic:
replace h := not_and_or.mpr <| h <| AdjoinRoot.root x.factor

Result:
case refine_2.intro.intro
K : Type v
inst✝ : Field K
x : K[X]
hx : x ∈ nonunits K[X]
x✝ : x ≠ 0
w✝¹ w✝ : K[X]
h : ¬((aeval (AdjoinRoot.root x.factor)) (x * w✝¹) = 0 ∧ (aeval (AdjoinRoot.root x.factor)) (x * w✝) = 0)
⊢ False

Proof state:
K : Type v
inst✝ : Field K
f g : K[X]
⊢ IsCoprime f g ↔
    ∀ {A : Type v} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : Algebra K A] (a : A),
      (aeval a) f ≠ 0 ∨ (aeval a) g ≠ 0

Tactic:
refine ⟨fun h => aeval_ne_zero_of_isCoprime h, fun h => isCoprime_of_dvd _ _ ?_ fun x hx _ => ?_⟩

Result:
case refine_1
K : Type v
inst✝ : Field K
f g : K[X]
h :
  ∀ {A : Type v} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : Algebra K A] (a : A),
    (aeval a) f ≠ 0 ∨ (aeval a) g ≠ 0
⊢ ¬(f = 0 ∧ g = 0)

case refine_2
K : Type v
inst✝ : Field K
f g : K[X]
h :
  ∀ {A : Type v} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : Algebra K A] (a : A),
    (aeval a) f ≠ 0 ∨ (aeval a) g ≠ 0
x : K[X]
hx : x ∈ nonunits K[X]
x✝ : x ≠ 0
⊢ x ∣ f → ¬x ∣ g

Proof state:
case refine_2
K : Type v
inst✝ : Field K
f g : K[X]
h :
  ∀ {A : Type v} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : Algebra K A] (a : A),
    (aeval a) f ≠ 0 ∨ (aeval a) g ≠ 0
x : K[X]
hx : x ∈ nonunits K[X]
x✝ : x ≠ 0
⊢ x ∣ f → ¬x ∣ g

Tactic:
rintro ⟨_, rfl⟩ ⟨_, rfl⟩

Result:
case refine_2.intro.intro
K : Type v
inst✝ : Field K
x : K[X]
hx : x ∈ nonunits K[X]
x✝ : x ≠ 0
w✝¹ w✝ : K[X]
h :
  ∀ {A : Type v} [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : Algebra K A] (a : A),
    (aeval a) (x * w✝¹) ≠ 0 ∨ (aeval a) (x * w✝) ≠ 0
⊢ False