awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
A B : IntermediateField F E
f : E →ₐ[F] L
⊢ (map f A).relfinrank (map f B) = A.relfinrank B

Tactic:
simpa using congr(toNat $(lift_relrank_map_map A B f))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
A B : IntermediateField F E
f : L →ₐ[F] E
⊢ Cardinal.lift.{v, w} ((comap f A).relrank (comap f B)) = Cardinal.lift.{w, v} (A.relrank (B ⊓ f.fieldRange))

Tactic:
A.toSubfield.lift_relrank_comap_comap_eq_lift_relrank_inf B.toSubfield f.toRingHom

Premises used: Subsemiring.comap, Subfield.comap, AlgHom.toRingHom, Subring.comap, IntermediateField.toSubfield, IntermediateField.relrank, Subfield.lift_relrank_comap_comap_eq_lift_relrank_inf
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
L : Type v
inst_3 : Field L
inst_4 : Algebra F L
f : L →ₐ[F] E
⊢ (comap f A).relrank (comap f B) = A.relrank (B ⊓ f.fieldRange)

Tactic:
simpa only [lift_id] using lift_relrank_comap_comap_eq_lift_relrank_inf A B f

Premises used: IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_inf, Cardinal.lift_id
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
A B : IntermediateField F E
f : L →ₐ[F] E
⊢ (comap f A).relfinrank (comap f B) = A.relfinrank (B ⊓ f.fieldRange)

Tactic:
simpa using congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_inf A B f))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
A B : IntermediateField F E
f : L →ₐ[F] E
h : B ≤ f.fieldRange
⊢ Cardinal.lift.{v, w} ((comap f A).relrank (comap f B)) = Cardinal.lift.{w, v} (A.relrank B)

Tactic:
simpa only [inf_of_le_left h] using lift_relrank_comap_comap_eq_lift_relrank_inf A B f

Premises used: inf_of_le_left, IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_inf
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
L : Type v
inst_3 : Field L
inst_4 : Algebra F L
f : L →ₐ[F] E
h : B ≤ f.fieldRange
⊢ (comap f A).relrank (comap f B) = A.relrank B

Tactic:
simpa only [lift_id] using lift_relrank_comap_comap_eq_lift_relrank_of_le A B f h

Premises used: IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_of_le, Cardinal.lift_id
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
A B : IntermediateField F E
f : L →ₐ[F] E
h : B ≤ f.fieldRange
⊢ (comap f A).relfinrank (comap f B) = A.relfinrank B

Tactic:
simpa using congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_of_le A B f h))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
A B : IntermediateField F E
f : L →ₐ[F] E
h : Function.Surjective.{w + 1, v + 1} (α := L) (β := E) (⇑f : (a : L) → E)
⊢ Cardinal.lift.{v, w} ((comap f A).relrank (comap f B)) = Cardinal.lift.{w, v} (A.relrank B)

Tactic:
lift_relrank_comap_comap_eq_lift_relrank_of_le A B f fun x _ ↦ h x

Premises used: IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_of_le
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
L : Type v
inst_3 : Field L
inst_4 : Algebra F L
f : L →ₐ[F] E
h : Function.Surjective (α := L) (β := E) (⇑f : (a : L) → E)
⊢ (comap f A).relrank (comap f B) = A.relrank B

Tactic:
simpa using lift_relrank_comap_comap_eq_lift_relrank_of_surjective A B f h

Premises used: IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_of_surjective
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
L : Type w
inst_3 : Field L
inst_4 : Algebra F L
A B : IntermediateField F E
f : L →ₐ[F] E
h : Function.Surjective.{w + 1, v + 1} (α := L) (β := E) (⇑f : (a : L) → E)
⊢ (comap f A).relfinrank (comap f B) = A.relfinrank B

Tactic:
simpa using congr(toNat $(lift_relrank_comap_comap_eq_lift_relrank_of_surjective A B f h))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
h : A ≤ B
⊢ A.relrank B * Module.rank (↥B) E = Module.rank (↥A) E

Tactic:
Subfield.relrank_mul_rank_top h

Premises used: Set.Mem, Subfield.relrank_mul_rank_top, IntermediateField.relrank
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
h : A ≤ B
⊢ A.relfinrank B * finrank (↥B) E = finrank (↥A) E

Tactic:
simpa using congr(toNat $(relrank_mul_rank_top h))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
h : A ≤ B
rw : Module.rank F ↥A * Module.rank ↥A ↥(extendScalars h) = Module.rank F ↥B
⊢ Module.rank F ↥A * A.relrank B = Module.rank F ↥B

Tactic:
rw [relrank_eq_rank_of_le h]

Premises used: IntermediateField.relrank_eq_rank_of_le
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
h : A ≤ B
this : Algebra ↥A ↥B := (inclusion h).toAlgebra
⊢ Module.rank F ↥A * Module.rank ↥A ↥(extendScalars h) = Module.rank F ↥B

Tactic:
rank_mul_rank F A B

Premises used: Set.Mem, rank_mul_rank, Membership.mem, Subtype, IntermediateField.extendScalars, Subfield.extendScalars, RingHom.codRestrict, Subfield.toIntermediateField
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
h : A ≤ B
this : Algebra ↥A ↥B := (inclusion h).toAlgebra
⊢ Module.rank F ↥A * Module.rank ↥A ↥(extendScalars h) = Module.rank F ↥B

Tactic:
exact rank_mul_rank F A B

Premises used: rank_mul_rank, Membership.mem, Subtype
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
h : A ≤ B
⊢ finrank.{u, v} F ↥A * A.relfinrank B = finrank.{u, v} F ↥B

Tactic:
simpa using congr(toNat $(rank_bot_mul_relrank h))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
h : A ≤ B
⊢ A.relrank B ∣ Module.rank (↥A) E

Tactic:
dvd_of_mul_right_eq _ (relrank_mul_rank_top h)

Premises used: IntermediateField.relrank_mul_rank_top, dvd_of_mul_right_eq
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
h : A ≤ B
⊢ A.relfinrank B ∣ finrank (↥A) E

Tactic:
dvd_of_mul_right_eq _ (relfinrank_mul_finrank_top h)

Premises used: IntermediateField.relfinrank_mul_finrank_top, dvd_of_mul_right_eq
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
⊢ A.relrank B ∣ Module.rank F ↥B

Tactic:
inf_relrank_right A B ▸ dvd_of_mul_left_eq _ (rank_bot_mul_relrank inf_le_right)

Premises used: IntermediateField.inf_relrank_right, dvd_of_mul_left_eq, inf_le_right, Eq.rec, IntermediateField.rank_bot_mul_relrank
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
⊢ A.relfinrank B ∣ finrank.{u, v} F ↥B

Tactic:
inf_relfinrank_right A B ▸ dvd_of_mul_left_eq _ (finrank_bot_mul_relfinrank inf_le_right)

Premises used: dvd_of_mul_left_eq, inf_le_right, IntermediateField.inf_relfinrank_right, Eq.rec, IntermediateField.finrank_bot_mul_relfinrank
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B C : IntermediateField F E
h1 : A ≤ B
h2 : B ≤ C
⊢ A.relrank B * B.relrank C = A.relrank C

Tactic:
Subfield.relrank_mul_relrank h1 h2

Premises used: IntermediateField.relrank, Subfield.relrank_mul_relrank
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B C : IntermediateField F E
h1 : A ≤ B
h2 : B ≤ C
⊢ A.relfinrank B * B.relfinrank C = A.relfinrank C

Tactic:
simpa using congr(toNat $(relrank_mul_relrank h1 h2))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B C : IntermediateField F E
⊢ A.relrank (B ⊓ C) * B.relrank C = (A ⊓ B).relrank C

Tactic:
Subfield.relrank_inf_mul_relrank A.toSubfield B.toSubfield C.toSubfield

Premises used: Subfield.relrank_inf_mul_relrank, IntermediateField.toSubfield, IntermediateField.relrank
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B C : IntermediateField F E
⊢ A.relfinrank (B ⊓ C) * B.relfinrank C = (A ⊓ B).relfinrank C

Tactic:
simpa using congr(toNat $(relrank_inf_mul_relrank A B C))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B C : IntermediateField F E
h : B ≤ C
⊢ A.relrank B * B.relrank C = (A ⊓ B).relrank C

Tactic:
simpa only [inf_of_le_left h] using relrank_inf_mul_relrank A B C

Premises used: inf_of_le_left, IntermediateField.relrank_inf_mul_relrank
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B C : IntermediateField F E
h : B ≤ C
⊢ A.relfinrank B * B.relfinrank C = (A ⊓ B).relfinrank C

Tactic:
simpa using congr(toNat $(relrank_mul_relrank_eq_inf_relrank A h))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B C : IntermediateField F E
h : A ≤ B
⊢ A.relrank (B ⊓ C) * B.relrank C = A.relrank C

Tactic:
simpa only [inf_of_le_left h] using relrank_inf_mul_relrank A B C

Premises used: inf_of_le_left, IntermediateField.relrank_inf_mul_relrank
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B C : IntermediateField F E
h : A ≤ B
⊢ A.relfinrank (B ⊓ C) * B.relfinrank C = A.relfinrank C

Tactic:
simpa using congr(toNat $(relrank_inf_mul_relrank_of_le C h))
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
⊢ relrank ⊤ A = 1

Tactic:
relrank_eq_one_of_le le_top

Premises used: IntermediateField.relrank_eq_one_of_le, le_top
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
⊢ relfinrank ⊤ A = 1

Tactic:
relfinrank_eq_one_of_le le_top

Premises used: IntermediateField.relfinrank_eq_one_of_le, le_top
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
rw : A.relrank ⊤ = A.relrank ⊤ * Module.rank (↥⊤) E
rw₁ : A.relrank ⊤ = A.relrank ⊤ * 1
rw₂ rw₃ : A.relrank ⊤ = A.relrank ⊤
⊢ A.relrank ⊤ = Module.rank (↥A) E

Tactic:
rw [← relrank_mul_rank_top (show A ≤ ⊤ from le_top), IntermediateField.rank_top, mul_one]

Premises used: IntermediateField.relrank_mul_rank_top, IntermediateField.rank_top, le_top, mul_one
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
⊢ A.relfinrank ⊤ = finrank (↥A) E

Tactic:
simp [relfinrank_eq_toNat_relrank, finrank]

Premises used: IntermediateField.relfinrank_eq_toNat_relrank, Module.finrank
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
rw : relrank ⊥ A = Module.rank F ↥⊥ * relrank ⊥ A
rw₁ : relrank ⊥ A = 1 * relrank ⊥ A
rw₂ rw₃ : relrank ⊥ A = relrank ⊥ A
⊢ relrank ⊥ A = Module.rank F ↥A

Tactic:
rw [← rank_bot_mul_relrank (show ⊥ ≤ A from bot_le), IntermediateField.rank_bot, one_mul]

Premises used: IntermediateField.rank_bot, IntermediateField.rank_bot_mul_relrank, bot_le, one_mul
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
⊢ relfinrank ⊥ A = finrank.{u, v} F ↥A

Tactic:
simp [relfinrank_eq_toNat_relrank, finrank]

Premises used: IntermediateField.relfinrank_eq_toNat_relrank, Module.finrank
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
⊢ A.relrank ⊥ = 1

Tactic:
relrank_eq_one_of_le bot_le

Premises used: IntermediateField.relrank_eq_one_of_le, bot_le
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A : IntermediateField F E
⊢ A.relfinrank ⊥ = 1

Tactic:
relfinrank_eq_one_of_le bot_le

Premises used: IntermediateField.relfinrank_eq_one_of_le, bot_le
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B C : IntermediateField F E
h : A ≤ B
⊢ B.relrank C ∣ A.relrank C

Tactic:
dvd_of_mul_left_eq _ (relrank_inf_mul_relrank_of_le C h)

Premises used: dvd_of_mul_left_eq, IntermediateField.relrank_inf_mul_relrank_of_le
-- Module: Mathlib.FieldTheory.Relrank
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B C : IntermediateField F E
h : A ≤ B
⊢ B.relfinrank C ∣ A.relfinrank C

Tactic:
dvd_of_mul_left_eq _ (relfinrank_inf_mul_relfinrank_of_le C h)

Premises used: dvd_of_mul_left_eq, IntermediateField.relfinrank_inf_mul_relfinrank_of_le
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
⊢ f.Separable ↔ IsCoprime f ((derivative : (a : R[X]) → R[X]) f)

Tactic:
Iff.rfl

Premises used: Iff.rfl, Polynomial.Separable
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
⊢ f.Separable ↔ ∃ (a : R[X]) (b : R[X]), a * f + HMul.hMul (β := R[X]) b ((derivative : (a : R[X]) → R[X]) f : R[X]) = 1

Tactic:
Iff.rfl

Premises used: Iff.rfl, Polynomial.Separable, IsCoprime
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
inst_1 : Nontrivial R
x y : R[X]
h : x * 0 + y * (derivative : (a : R[X]) → R[X]) 0 = 1
⊢ False

Tactic:
simp only [derivative_zero, mul_zero, add_zero, zero_ne_one] at h

Premises used: zero_ne_one, MulZeroClass.mul_zero, Polynomial.derivative_zero, add_zero
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
inst_1 : Nontrivial R
f : R[X]
h : f.Separable
⊢ f ≠ 0

Tactic:
(not_separable_zero <| · ▸ h)

Premises used: Polynomial.not_separable_zero, Not
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
⊢ Separable.{u} (R := R) 1

Tactic:
isCoprime_one_left

Premises used: Polynomial.Separable, isCoprime_one_left
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
inst_1 : Subsingleton R
f : R[X]
⊢ f.Separable

Tactic:
simp [Separable, IsCoprime, eq_iff_true_of_subsingleton]

Premises used: Polynomial.Separable, eq_iff_true_of_subsingleton, IsCoprime
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
a : R
rw : IsCoprime (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) 1
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).Separable

Tactic:
rw [separable_def, derivative_add, derivative_X, derivative_C, add_zero]

Premises used: Polynomial.derivative_X, Polynomial.separable_def, Polynomial.derivative_C, add_zero, Polynomial.derivative_add
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
a : R
⊢ IsCoprime (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) 1

Tactic:
isCoprime_one_right

Premises used: isCoprime_one_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
a : R
⊢ IsCoprime (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) 1

Tactic:
exact isCoprime_one_right

Premises used: isCoprime_one_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
rw : IsCoprime.{u} (R := R[X]) X 1
⊢ Separable.{u} (R := R) X

Tactic:
rw [separable_def, derivative_X]

Premises used: Polynomial.derivative_X, Polynomial.separable_def
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
⊢ IsCoprime.{u} (R := R[X]) X 1

Tactic:
isCoprime_one_right

Premises used: isCoprime_one_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
⊢ IsCoprime.{u} (R := R[X]) X 1

Tactic:
exact isCoprime_one_right

Premises used: isCoprime_one_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
r : R
rw :
  IsCoprime (R := R[X]) ((C : (a : R) → R[X]) r : R[X])
      ((derivative : (a : R[X]) → R[X]) ((C : (a : R) → R[X]) r) : R[X]) ↔
    IsUnit r
rw₁ : IsCoprime (R := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]) ↔ IsUnit r
rw₂ : IsUnit (M := R[X]) ((C : (a : R) → R[X]) r : R[X]) ↔ IsUnit r
rw₃ rw₄ : IsUnit r ↔ IsUnit r
⊢ Separable.{u} (R := R) ((C : (a : R) → R[X]) r) ↔ IsUnit r

Tactic:
rw [separable_def, derivative_C, isCoprime_zero_right, isUnit_C]

Premises used: Polynomial.isUnit_C, Polynomial.separable_def, Polynomial.derivative_C, isCoprime_zero_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
h : (f * g).Separable
⊢ IsCoprime f ((derivative : (a : R[X]) → R[X]) (f * g))

Tactic:
have := h.of_mul_left_left
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
h : (f * g).Separable
this : IsCoprime f ((derivative : (a : R[X]) → R[X]) (f * g))
⊢ IsCoprime f
    (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:
rw [derivative_mul] at this

Premises used: Polynomial.derivative_mul
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
h : (f * g).Separable
this :
  IsCoprime f
    (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.Separable

Tactic:
IsCoprime.of_mul_right_left (IsCoprime.of_add_mul_left_right this)

Premises used: IsCoprime.of_mul_right_left, Polynomial.Separable, IsCoprime.of_add_mul_left_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
h : (f * g).Separable
this :
  IsCoprime f
    (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.Separable

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

Premises used: IsCoprime.of_mul_right_left, IsCoprime.of_add_mul_left_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
h : (f * g).Separable
⊢ (g * f).Separable

Tactic:
rw [mul_comm] at h

Premises used: mul_comm
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
h : (g * f).Separable
⊢ g.Separable

Tactic:
h.of_mul_left

Premises used: Polynomial.Separable.of_mul_left
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
h : (g * f).Separable
⊢ g.Separable

Tactic:
exact h.of_mul_left

Premises used: Polynomial.Separable.of_mul_left
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
hf : f.Separable
hfg : g ∣ f
rcases : ∀ (f' : R[X]) (hf : (g * f').Separable), g.Separable
⊢ g.Separable

Tactic:
rcases hfg with ⟨f', rfl⟩

Premises used: rfl
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
g f' : R[X]
hf : (g * f').Separable
⊢ g.Separable

Tactic:
Separable.of_mul_left hf

Premises used: Polynomial.Separable.of_mul_left
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
g f' : R[X]
hf : (g * f').Separable
⊢ g.Separable

Tactic:
exact Separable.of_mul_left hf

Premises used: Polynomial.Separable.of_mul_left
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F[X]
f : F[X]
hf : f.Separable
g : F[X]
⊢ (EuclideanDomain.gcd f g).Separable

Tactic:
Separable.of_dvd hf (EuclideanDomain.gcd_dvd_left f g)

Premises used: EuclideanDomain.gcd_dvd_left, Polynomial.Separable.of_dvd
-- Module: Mathlib.FieldTheory.Separable
Goal:
F : Type u_1
inst : Field F
inst_1 : DecidableEq F[X]
g f : F[X]
hg : g.Separable
⊢ (EuclideanDomain.gcd f g).Separable

Tactic:
Separable.of_dvd hg (EuclideanDomain.gcd_dvd_right f g)

Premises used: EuclideanDomain.gcd_dvd_right, Polynomial.Separable.of_dvd
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
h : (f * g).Separable
this :
  IsCoprime f
    (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]))
⊢ IsCoprime f g

Tactic:
IsCoprime.of_mul_right_right (IsCoprime.of_add_mul_left_right this)

Premises used: IsCoprime.of_mul_right_right, IsCoprime.of_add_mul_left_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
h : (f * g).Separable
this :
  IsCoprime f
    (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]))
⊢ IsCoprime f g

Tactic:
exact IsCoprime.of_mul_right_right (IsCoprime.of_add_mul_left_right this)

Premises used: IsCoprime.of_mul_right_right, IsCoprime.of_add_mul_left_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n : ℕ
h : (f ^ (n + 2)).Separable
⊢ (f ^ n * f * f).Separable

Tactic:
rw [pow_succ, pow_succ] at h

Premises used: pow_succ
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n : ℕ
h : (f ^ n * f * f).Separable
⊢ IsUnit f ∨ f.Separable ∧ n + 2 = 1 ∨ n + 2 = 0

Tactic:
Or.inl (isCoprime_self.1 h.isCoprime.of_mul_left_right)

Premises used: isCoprime_self, Polynomial.Separable.isCoprime, Iff.mp, Or.inl, IsCoprime.of_mul_left_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n : ℕ
h : (f ^ n * f * f).Separable
⊢ IsUnit f ∨ f.Separable ∧ n + 2 = 1 ∨ n + 2 = 0

Tactic:
exact Or.inl (isCoprime_self.1 h.isCoprime.of_mul_left_right)

Premises used: isCoprime_self, Polynomial.Separable.isCoprime, Iff.mp, Or.inl, IsCoprime.of_mul_left_right
-- Module: Mathlib.FieldTheory.Separable
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
hf : ¬IsUnit f
n : ℕ
hn : n ≠ 0
hfs : (f ^ n).Separable
⊢ f.Separable ∧ n = 1

Tactic:
(hfs.of_pow'.resolve_left hf).resolve_right hn

Premises used: Or.resolve_left, Polynomial.Separable.of_pow', Or.resolve_right