awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
p : R[X]
h : p.Separable
f : R →+* S
a b : R[X]
H : a * p + HMul.hMul (β := R[X]) b ((derivative : (a : R[X]) → R[X]) p : R[X]) = 1
rw :
  Polynomial.map f a * Polynomial.map f p + Polynomial.map f b * Polynomial.map f ((derivative : (a : R[X]) → R[X]) p) =
    1
rw₁ : Polynomial.map f (a * p) + Polynomial.map f b * Polynomial.map f ((derivative : (a : R[X]) → R[X]) p) = 1
rw₂ :
  Polynomial.map f (a * p) + Polynomial.map f (HMul.hMul (β := R[X]) b ((derivative : (a : R[X]) → R[X]) p : R[X])) = 1
rw₃ : Polynomial.map f (a * p + HMul.hMul (β := R[X]) b ((derivative : (a : R[X]) → R[X]) p : R[X])) = 1
rw₄ : Polynomial.map f 1 = 1
rw₅ rw₆ : Eq.{v + 1} (α := S[X]) 1 1
⊢ Polynomial.map f a * Polynomial.map f p +
      HMul.hMul (β := S[X]) (Polynomial.map f b) ((derivative : (a : S[X]) → S[X]) (Polynomial.map f p) : S[X]) =
    1

Tactic:
rw [derivative_map, ← Polynomial.map_mul, ← Polynomial.map_mul, ← Polynomial.map_add, H,
      Polynomial.map_one]

Premises used: Polynomial.map_one, Polynomial.map_mul, Polynomial.map_add, Polynomial.derivative_map
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
ha : Associated f g
h : f.Separable
⊢ g.Separable

Tactic:
grind [Separable.of_dvd, Associated.dvd']

Premises used: Associated.dvd', Polynomial.Separable.of_dvd
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
ha : Associated f g
⊢ f.Separable ↔ g.Separable

Tactic:
⟨ha.separable, ha.symm.separable⟩

Premises used: Associated.separable, Associated.symm, Iff.intro
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
hf : f.Separable
hg : IsUnit g
⊢ (f * g).Separable

Tactic:
(associated_mul_unit_right f g hg).separable hf

Premises used: Associated.separable, associated_mul_unit_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
hf : IsUnit f
hg : g.Separable
⊢ (f * g).Separable

Tactic:
(associated_unit_mul_right g f hf).separable hg

Premises used: Associated.separable, associated_unit_mul_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Nontrivial S
f : R →+* S
p : R[X]
h : p.Separable
x : S
hx : eval₂ f x p = 0
hx' : eval₂ f x ((derivative : (a : R[X]) → R[X]) p) = 0
obtain : ∀ (a b : R[X]) (e : a * p + HMul.hMul (β := R[X]) b ((derivative : (a : R[X]) → R[X]) p : R[X]) = 1), False
⊢ False

Tactic:
obtain ⟨a, b, e⟩ := h
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Nontrivial S
f : R →+* S
p : R[X]
x : S
hx : eval₂ f x p = 0
hx' : eval₂ f x ((derivative : (a : R[X]) → R[X]) p) = 0
a b : R[X]
e : a * p + HMul.hMul (β := R[X]) b ((derivative : (a : R[X]) → R[X]) p : R[X]) = 1
⊢ eval₂ f x (a * p + HMul.hMul (β := R[X]) b ((derivative : (a : R[X]) → R[X]) p : R[X])) = eval₂ f x 1

Tactic:
apply_fun Polynomial.eval₂ f x at e

Premises used: Polynomial.eval₂
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Nontrivial S
f : R →+* S
p : R[X]
x : S
hx : eval₂ f x p = 0
hx' : eval₂ f x ((derivative : (a : R[X]) → R[X]) p) = 0
a b : R[X]
e : eval₂ f x (a * p + HMul.hMul (β := R[X]) b ((derivative : (a : R[X]) → R[X]) p : R[X])) = eval₂ f x 1
⊢ False

Tactic:
simp only [eval₂_add, eval₂_mul, hx, mul_zero, hx', add_zero, eval₂_one, zero_ne_one] at e

Premises used: Polynomial.eval₂_one, zero_ne_one, MulZeroClass.mul_zero, Polynomial.eval₂_mul, add_zero, Polynomial.eval₂_add
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
inst_2 : Nontrivial S
inst_3 : Algebra R S
p : R[X]
h : p.Separable
x : S
hx : Eq.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) p : S) (0 : S)
⊢ Ne.{v + 1} (α := S) ((aeval x : (a : R[X]) → S) ((derivative : (a : R[X]) → R[X]) p : R[X]) : S) (0 : S)

Tactic:
h.eval₂_derivative_ne_zero (algebraMap R S) hx

Premises used: Algebra.algebraMap, MonoidHomClass.toMonoidHom, Polynomial.Separable.eval₂_derivative_ne_zero, RingHomClass.toRingHom
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
hp : p.Separable
hq : q * q ∣ p
obtain : ∀ (p : R[X]) (hp : (q * q * p).Separable), IsUnit q
⊢ IsUnit q

Tactic:
obtain ⟨p, rfl⟩ := hq

Premises used: rfl
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
apply : IsCoprime q q
⊢ IsUnit q

Tactic:
apply isCoprime_self.mp

Premises used: isCoprime_self, Iff.mp
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
simp :
  IsCoprime (q * q * p)
    (HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) q : R[X]) * p +
        HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) q : R[X]) * p +
      HMul.hMul (β := R[X]) (q * q) ((derivative : (a : R[X]) → R[X]) p : R[X]))
⊢ IsCoprime (q * (q * p))
    (q *
      (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) p +
          HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) p +
        HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) p : R[X])))

Tactic:
simp only [← mul_assoc, mul_add]

Premises used: mul_assoc, mul_add
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
q p : R[X]
hp : IsCoprime (q * q * p) ((derivative : (a : R[X]) → R[X]) (q * q * p))
⊢ IsCoprime (q * q * p) ((derivative : (a : R[X]) → R[X]) (q * q * p))

Tactic:
hp
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
q p : R[X]
hp : IsCoprime (q * q * p) ((derivative : (a : R[X]) → R[X]) (q * q * p))
h :
  HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) q : R[X]) * p +
        HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) q : R[X]) * p +
      HMul.hMul (β := R[X]) (q * q) ((derivative : (a : R[X]) → R[X]) p : R[X]) =
    (derivative : (a : R[X]) → R[X]) (q * q * p)
⊢ IsCoprime (q * q * p)
    (HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) q : R[X]) * p +
        HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) q : R[X]) * p +
      HMul.hMul (β := R[X]) (q * q) ((derivative : (a : R[X]) → R[X]) p : R[X]))

Tactic:
convert! hp using 1
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
q p : R[X]
hp : IsCoprime (q * q * p) ((derivative : (a : R[X]) → R[X]) (q * q * p))
h :
  HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) q : R[X]) * p +
        HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) q : R[X]) * p +
      HMul.hMul (β := R[X]) (q * q) ((derivative : (a : R[X]) → R[X]) p : R[X]) =
    (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) q +
          HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) q : R[X])) *
        p +
      HMul.hMul (β := R[X]) (q * q) ((derivative : (a : R[X]) → R[X]) p : R[X])
⊢ HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) q : R[X]) * p +
        HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) q : R[X]) * p +
      HMul.hMul (β := R[X]) (q * q) ((derivative : (a : R[X]) → R[X]) p : R[X]) =
    (derivative : (a : R[X]) → R[X]) (q * q * p)

Tactic:
rw [derivative_mul, derivative_mul]

Premises used: Polynomial.derivative_mul
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
q p : R[X]
hp : IsCoprime (q * q * p) ((derivative : (a : R[X]) → R[X]) (q * q * p))
⊢ HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) q : R[X]) * p +
        HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) q : R[X]) * p +
      HMul.hMul (β := R[X]) (q * q) ((derivative : (a : R[X]) → R[X]) p : R[X]) =
    (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) q +
          HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) q : R[X])) *
        p +
      HMul.hMul (β := R[X]) (q * q) ((derivative : (a : R[X]) → R[X]) p : R[X])

Tactic:
ring
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
⊢ IsCoprime (q * (q * p))
    (q *
      (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) p +
          HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) p +
        HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) p : R[X])))

Tactic:
have : IsCoprime (q * (q * p))
      (q * (derivative q * p + derivative q * p + q * derivative p)) := by
    simp only [← mul_assoc, mul_add]
    dsimp only [Separable] at hp
    convert! hp using 1
    rw [derivative_mul, derivative_mul]
    ring
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
this :
  IsCoprime (q * (q * p))
    (q *
      (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) p +
          HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) p +
        HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) p : R[X])))
⊢ IsCoprime q q

Tactic:
IsCoprime.of_mul_right_left (IsCoprime.of_mul_left_left this)

Premises used: IsCoprime.of_mul_right_left, IsCoprime.of_mul_left_left
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
this :
  IsCoprime (q * (q * p))
    (q *
      (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) p +
          HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) q : R[X]) p +
        HMul.hMul (β := R[X]) q ((derivative : (a : R[X]) → R[X]) p : R[X])))
⊢ IsCoprime q q

Tactic:
exact IsCoprime.of_mul_right_left (IsCoprime.of_mul_left_left this)

Premises used: IsCoprime.of_mul_right_left, IsCoprime.of_mul_left_left
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
hq : ¬IsUnit q
hsep : p.Separable
contrapose! : ∀ (hq : 1 < emultiplicity q p), IsUnit q
⊢ emultiplicity q p ≤ 1

Tactic:
contrapose! hq
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
apply : q * q ∣ p
⊢ IsUnit q

Tactic:
apply isUnit_of_self_mul_dvd_separable hsep

Premises used: Polynomial.isUnit_of_self_mul_dvd_separable
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
rw : HPow.hPow (β := ℕ) q 2 ∣ p
⊢ q * q ∣ p

Tactic:
rw [← sq]

Premises used: sq
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
hk : (↑2 : ℕ∞) ≤ emultiplicity q p
⊢ HPow.hPow (β := ℕ) q 2 ∣ p

Tactic:
apply pow_dvd_of_le_emultiplicity

Premises used: pow_dvd_of_le_emultiplicity
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ (↑2 : ℕ∞) ≤ emultiplicity q p

Tactic:
Order.add_one_le_of_lt hq

Premises used: WithTop.map₂, WithTop.some, Order.add_one_le_of_lt, Option.map₂
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ (↑2 : ℕ∞) ≤ emultiplicity q p

Tactic:
exact Order.add_one_le_of_lt hq

Premises used: Order.add_one_le_of_lt
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
hsep : p.Separable
rw : ∀ (x : R[X]), emultiplicity x p ≤ 1 ∨ IsUnit x
⊢ Squarefree p

Tactic:
rw [squarefree_iff_emultiplicity_le_one p]

Premises used: squarefree_iff_emultiplicity_le_one
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
hsep : p.Separable
⊢ ∀ (x : R[X]), emultiplicity x p ≤ 1 ∨ IsUnit x

Tactic:
fun f => or_iff_not_imp_right.mpr fun hunit => emultiplicity_le_one_of_separable hunit hsep

Premises used: Iff.mpr, Classical.or_iff_not_imp_right, Polynomial.emultiplicity_le_one_of_separable
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
hsep : p.Separable
⊢ ∀ (x : R[X]), emultiplicity x p ≤ 1 ∨ IsUnit x

Tactic:
exact fun f => or_iff_not_imp_right.mpr fun hunit => emultiplicity_le_one_of_separable hunit hsep

Premises used: Iff.mpr, Classical.or_iff_not_imp_right, Polynomial.emultiplicity_le_one_of_separable
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
hsep : p.Separable
rw rw₁ rw₂ : ∀ (x : R[X]), emultiplicity x p ≤ 1 ∨ IsUnit x
⊢ Squarefree p

Tactic:
classical
  rw [squarefree_iff_emultiplicity_le_one p]
  exact fun f => or_iff_not_imp_right.mpr fun hunit => emultiplicity_le_one_of_separable hunit hsep

Premises used: Iff.mpr, Classical.or_iff_not_imp_right, squarefree_iff_emultiplicity_le_one, Polynomial.emultiplicity_le_one_of_separable
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
x : R
⊢ (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])).Separable

Tactic:
simpa only [sub_eq_add_neg, C_neg] using separable_X_add_C (-x)

Premises used: Polynomial.separable_X_add_C, sub_eq_add_neg, Polynomial.C_neg, Neg.neg
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
f g : R[X]
hf : f.Separable
hg : g.Separable
h : IsCoprime f g
rw :
  IsCoprime (f * g)
    (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g +
      HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X]))
⊢ (f * g).Separable

Tactic:
rw [separable_def, derivative_mul]

Premises used: Polynomial.derivative_mul, Polynomial.separable_def
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
f g : R[X]
hf : f.Separable
hg : g.Separable
h : IsCoprime f g
⊢ IsCoprime (f * g)
    (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g +
      HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X]))

Tactic:
((hf.mul_right h).add_mul_left_right _).mul_left ((h.symm.mul_right hg).mul_add_right_right _)

Premises used: IsCoprime.mul_left, IsCoprime.symm, IsCoprime.mul_right, IsCoprime.mul_add_right_right, IsCoprime.add_mul_left_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
f g : R[X]
hf : f.Separable
hg : g.Separable
h : IsCoprime f g
⊢ IsCoprime (f * g)
    (HMul.hMul (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) g +
      HMul.hMul (β := R[X]) f ((derivative : (a : R[X]) → R[X]) g : R[X]))

Tactic:
exact
    ((hf.mul_right h).add_mul_left_right _).mul_left ((h.symm.mul_right hg).mul_add_right_right _)

Premises used: IsCoprime.mul_left, IsCoprime.symm, IsCoprime.mul_right, IsCoprime.mul_add_right_right, IsCoprime.add_mul_left_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
ι : Type u_1
f : ι → R[X]
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih :
  (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → Separable.{u} (R := R) (∏ x ∈ s, f x)
h1 : ∀ x ∈ insert a s, ∀ y ∈ insert a s, x ≠ y → IsCoprime (f x) (f y)
h2 : ∀ x ∈ insert a s, (f x).Separable
⊢ (f a).Separable ∧ ∀ x ∈ s, (f x).Separable

Tactic:
simp_rw [Finset.forall_mem_insert, forall_and] at h1 h2

Premises used: Finset.forall_mem_insert, forall_and
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
ι : Type u_1
f : ι → R[X]
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih :
  (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → Separable.{u} (R := R) (∏ x ∈ s, f x)
h1 : ∀ x ∈ insert a s, ∀ y ∈ insert a s, x ≠ y → IsCoprime (f x) (f y)
h2 : ∀ x ∈ insert a s, (f x).Separable
h2₁ : (f a).Separable ∧ ∀ x ∈ s, (f x).Separable
⊢ ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ x ∈ s, a ≠ x → IsCoprime (f a) (f x)) ∧
    (∀ (x : ι) (x_1 : x ∈ s), x ≠ a → IsCoprime (f x) (f a)) ∧
      ∀ (x : ι) (x_1 : x ∈ s), ∀ x_2 ∈ s, x ≠ x_2 → IsCoprime (f x) (f x_2)

Tactic:
simp_rw [Finset.forall_mem_insert, forall_and] at h1 h2

Premises used: Finset.forall_mem_insert, forall_and
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
ι : Type u_1
f : ι → R[X]
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih :
  (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → Separable.{u} (R := R) (∏ x ∈ s, f x)
h2 : (f a).Separable ∧ ∀ x ∈ s, (f x).Separable
h1 :
  ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ x ∈ s, a ≠ x → IsCoprime (f a) (f x)) ∧
    (∀ (x : ι) (x_1 : x ∈ s), x ≠ a → IsCoprime (f x) (f a)) ∧
      ∀ (x : ι) (x_1 : x ∈ s), ∀ x_2 ∈ s, x ≠ x_2 → IsCoprime (f x) (f x_2)
rw : (f a * ∏ x ∈ s, f x).Separable
⊢ Separable.{u} (R := R) (∏ x ∈ insert a s, f x)

Tactic:
rw [prod_insert has]

Premises used: Finset.prod_insert
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
ι : Type u_1
f : ι → R[X]
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih :
  (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → Separable.{u} (R := R) (∏ x ∈ s, f x)
h2 : (f a).Separable ∧ ∀ x ∈ s, (f x).Separable
h1 :
  ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ x ∈ s, a ≠ x → IsCoprime (f a) (f x)) ∧
    (∀ (x : ι) (x_1 : x ∈ s), x ≠ a → IsCoprime (f x) (f a)) ∧
      ∀ (x : ι) (x_1 : x ∈ s), ∀ x_2 ∈ s, x ≠ x_2 → IsCoprime (f x) (f x_2)
⊢ (f a * ∏ x ∈ s, f x).Separable

Tactic:
h2.1.mul (ih h1.2.2 h2.2)
        (IsCoprime.prod_right fun i his => h1.1.2 i his <| Ne.symm <| ne_of_mem_of_not_mem his has)

Premises used: Ne.symm, ne_of_mem_of_not_mem, And.right, And.left, Polynomial.Separable.mul, IsCoprime.prod_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
ι : Type u_1
f : ι → R[X]
s_1 : Finset ι
a : ι
s : Finset ι
has : a ∉ s
ih :
  (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → Separable.{u} (R := R) (∏ x ∈ s, f x)
h2 : (f a).Separable ∧ ∀ x ∈ s, (f x).Separable
h1 :
  ((a ≠ a → IsCoprime (f a) (f a)) ∧ ∀ x ∈ s, a ≠ x → IsCoprime (f a) (f x)) ∧
    (∀ (x : ι) (x_1 : x ∈ s), x ≠ a → IsCoprime (f x) (f a)) ∧
      ∀ (x : ι) (x_1 : x ∈ s), ∀ x_2 ∈ s, x ≠ x_2 → IsCoprime (f x) (f x_2)
⊢ (f a * ∏ x ∈ s, f x).Separable

Tactic:
exact
      h2.1.mul (ih h1.2.2 h2.2)
        (IsCoprime.prod_right fun i his => h1.1.2 i his <| Ne.symm <| ne_of_mem_of_not_mem his has)

Premises used: Ne.symm, ne_of_mem_of_not_mem, And.right, And.left, Polynomial.Separable.mul, IsCoprime.prod_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
ι : Type u_1
f : ι → R[X]
s : Finset ι
⊢ (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → Separable.{u} (R := R) (∏ x ∈ s, f x)

Tactic:
exact Finset.induction_on s (fun _ _ => separable_one) fun a s has ih h1 h2 => by
    simp_rw [Finset.forall_mem_insert, forall_and] at h1 h2; rw [prod_insert has]
    exact
      h2.1.mul (ih h1.2.2 h2.2)
        (IsCoprime.prod_right fun i his => h1.1.2 i his <| Ne.symm <| ne_of_mem_of_not_mem his has)
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
ι : Type u_1
f : ι → R[X]
s : Finset ι
⊢ (∀ x ∈ s, ∀ y ∈ s, x ≠ y → IsCoprime (f x) (f y)) → (∀ x ∈ s, (f x).Separable) → Separable.{u} (R := R) (∏ x ∈ s, f x)

Tactic:
classical
  exact Finset.induction_on s (fun _ _ => separable_one) fun a s has ih h1 h2 => by
    simp_rw [Finset.forall_mem_insert, forall_and] at h1 h2; rw [prod_insert has]
    exact
      h2.1.mul (ih h1.2.2 h2.2)
        (IsCoprime.prod_right fun i his => h1.1.2 i his <| Ne.symm <| ne_of_mem_of_not_mem his has)
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
ι : Type u_1
inst_1 : Fintype ι
f : ι → R[X]
h1 : Pairwise (IsCoprime on f)
h2 : ∀ (x : ι), (f x).Separable
⊢ Separable.{u} (R := R) (∏ x : ι, f x)

Tactic:
separable_prod' (fun _x _hx _y _hy hxy => h1 hxy) fun x _hx => h2 x

Premises used: Polynomial.separable_prod'
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : Separable.{u} (R := R) (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f i) : R[X]))
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
by_contra : ∀ (hxy : ¬x = y), False
⊢ x = y

Tactic:
by_contra hxy
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : Separable.{u} (R := R) (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f i) : R[X]))
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
rw :
  ∀ {y : ι}
    (hfs :
      (HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f y) : R[X])) 2 *
          ∏ x ∈ (s.erase x).erase y, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f x) : R[X])).Separable)
    (hx : x ∈ s) (hy : y ∈ s) (hfxy : f x = f y) (hxy : ¬x = y), False
⊢ False

Tactic:
rw [← insert_erase hx, prod_insert (notMem_erase _ _), ←
    insert_erase (mem_erase_of_ne_of_mem (Ne.symm hxy) hy), prod_insert (notMem_erase _ _), ←
    mul_assoc, hfxy, ← sq] at hfs

Premises used: Finset.prod_insert, mul_assoc, Finset.mem_erase_of_ne_of_mem, Ne.symm, sq, Finset.notMem_erase, Finset.insert_erase
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
x y : ι
hfs :
  (HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f y) : R[X])) 2 *
      ∏ x ∈ (s.erase x).erase y, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f x) : R[X])).Separable
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
hxy : ¬x = y
⊢ False

Tactic:
cases (hfs.of_mul_left.of_pow (not_isUnit_X_sub_C _) two_ne_zero).2

Premises used: Polynomial.Separable.of_mul_left, two_ne_zero, And.right, Polynomial.Separable.of_pow
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_1
f : ι → R
s : Finset ι
hfs : Separable.{u} (R := R) (∏ i ∈ s, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f i) : R[X]))
x y : ι
hx : x ∈ s
hy : y ∈ s
hfxy : f x = f y
by_contra by_contra₁ by_contra₂ : ∀ (hxy : ¬x = y), False
by_contra₃ :
  ∀ {y : ι}
    (hfs :
      (HPow.hPow (β := ℕ) (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f y) : R[X])) 2 *
          ∏ x ∈ (s.erase x).erase y, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f x) : R[X])).Separable)
    (hx : x ∈ s) (hy : y ∈ s) (hfxy : f x = f y) (hxy : ¬x = y), False
⊢ x = y

Tactic:
classical
  by_contra hxy
  rw [← insert_erase hx, prod_insert (notMem_erase _ _), ←
    insert_erase (mem_erase_of_ne_of_mem (Ne.symm hxy) hy), prod_insert (notMem_erase _ _), ←
    mul_assoc, hfxy, ← sq] at hfs
  cases (hfs.of_mul_left.of_pow (not_isUnit_X_sub_C _) two_ne_zero).2

Premises used: Finset.prod_insert, mul_assoc, Polynomial.Separable.of_mul_left, sq, two_ne_zero, And.right, Finset.notMem_erase, Polynomial.Separable.of_pow
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
ι : Type u_1
inst_2 : Fintype ι
f : ι → R
hfs : Separable.{u} (R := R) (∏ i : ι, HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (f i) : R[X]))
⊢ Function.Injective f

Tactic:
fun _x _y hfxy =>
  hfs.inj_of_prod_X_sub_C (mem_univ _) (mem_univ _) hfxy

Premises used: Finset.mem_univ, Polynomial.Separable.inj_of_prod_X_sub_C, Function.Injective
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
s : Multiset R
hs :
  Separable (R := R)
    (Multiset.prod (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) s))
rw : ∀ (a : R) (t : Multiset R), s ≠ a ::ₘ a ::ₘ t
⊢ s.Nodup

Tactic:
rw [Multiset.nodup_iff_ne_cons_cons]

Premises used: Multiset.nodup_iff_ne_cons_cons
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
a : R
t : Multiset R
hs :
  Separable (R := R)
    (Multiset.prod
      (Multiset.map (fun (a : R) ↦ HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X]))
        (a ::ₘ a ::ₘ t)))
⊢ False

Tactic:
not_isUnit_X_sub_C a (isUnit_of_self_mul_dvd_separable hs ?_)

Premises used: Polynomial.isUnit_of_self_mul_dvd_separable, Polynomial.not_isUnit_X_sub_C