awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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 ⊓ B).relrank A = B.relrank A
have rw : (B ⊓ A).relrank A = B.relrank A
Tactic: rw [inf_comm, inf_relrank_right]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
Goal:
F : Type u
E : Type v
inst : Field F
inst_1 : Field E
inst_2 : Algebra F E
A B : IntermediateField F E
rw : (B ⊓ A).relrank A = B.relrank A
⊢ (A ⊓ B).relrank A = B.relrank A
have rw₁ : B.relrank A = B.relrank A
Tactic: rw [inf_comm, inf_relrank_right]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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
⊢ Cardinal.lift.{v, w} ((map f A).relrank (map f B)) = Cardinal.lift.{w, v} (A.relrank B)
have rw : Cardinal.lift.{w, v} ((comap f (map f A)).relrank B) = Cardinal.lift.{w, v} (A.relrank B)
Tactic: rw [← lift_relrank_comap, comap_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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
rw : Cardinal.lift.{w, v} ((comap f (map f A)).relrank B) = Cardinal.lift.{w, v} (A.relrank B)
⊢ Cardinal.lift.{v, w} ((map f A).relrank (map f B)) = Cardinal.lift.{w, v} (A.relrank B)
have rw₁ : Cardinal.lift.{w, v} (A.relrank B) = Cardinal.lift.{w, v} (A.relrank B)
Tactic: rw [← lift_relrank_comap, comap_map]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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
⊢ Module.rank F ↥A * A.relrank B = Module.rank F ↥B
have rw : Module.rank F ↥A * Module.rank ↥A ↥(extendScalars h) = Module.rank F ↥B
Tactic: rw [relrank_eq_rank_of_le h]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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 ⊤ = Module.rank (↥A) E
have rw : A.relrank ⊤ = A.relrank ⊤ * Module.rank (↥⊤) E
Tactic: rw [← relrank_mul_rank_top (show A ≤ ⊤ from le_top), IntermediateField.rank_top, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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
⊢ A.relrank ⊤ = Module.rank (↥A) E
have rw₁ : A.relrank ⊤ = A.relrank ⊤ * 1
Tactic: rw [← relrank_mul_rank_top (show A ≤ ⊤ from le_top), IntermediateField.rank_top, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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
⊢ A.relrank ⊤ = Module.rank (↥A) E
have rw₂ : A.relrank ⊤ = A.relrank ⊤
Tactic: rw [← relrank_mul_rank_top (show A ≤ ⊤ from le_top), IntermediateField.rank_top, mul_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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 = Module.rank F ↥A
have rw : relrank ⊥ A = Module.rank F ↥⊥ * relrank ⊥ A
Tactic: rw [← rank_bot_mul_relrank (show ⊥ ≤ A from bot_le), IntermediateField.rank_bot, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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
⊢ relrank ⊥ A = Module.rank F ↥A
have rw₁ : relrank ⊥ A = 1 * relrank ⊥ A
Tactic: rw [← rank_bot_mul_relrank (show ⊥ ≤ A from bot_le), IntermediateField.rank_bot, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Relrank (goal)
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
⊢ relrank ⊥ A = Module.rank F ↥A
have rw₂ : relrank ⊥ A = relrank ⊥ A
Tactic: rw [← rank_bot_mul_relrank (show ⊥ ≤ A from bot_le), IntermediateField.rank_bot, one_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommSemiring R
a : R
⊢ (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])).Separable
have rw : IsCoprime (HAdd.hAdd (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) a : R[X])) 1
Tactic: rw [separable_def, derivative_add, derivative_X, derivative_C, add_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommSemiring R
⊢ Separable.{u} (R := R) X
have rw : IsCoprime.{u} (R := R[X]) X 1
Tactic: rw [separable_def, derivative_X]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommSemiring R
r : R
⊢ Separable.{u} (R := R) ((C : (a : R) → R[X]) r) ↔ IsUnit r
have 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
Tactic: rw [separable_def, derivative_C, isCoprime_zero_right, isUnit_C]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ Separable.{u} (R := R) ((C : (a : R) → R[X]) r) ↔ IsUnit r
have rw₁ : IsCoprime (R := R[X]) ((C : (a : R) → R[X]) r : R[X]) (0 : R[X]) ↔ IsUnit r
Tactic: rw [separable_def, derivative_C, isCoprime_zero_right, isUnit_C]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ Separable.{u} (R := R) ((C : (a : R) → R[X]) r) ↔ IsUnit r
have rw₂ : IsUnit (M := R[X]) ((C : (a : R) → R[X]) r : R[X]) ↔ IsUnit r
Tactic: rw [separable_def, derivative_C, isCoprime_zero_right, isUnit_C]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ Separable.{u} (R := R) ((C : (a : R) → R[X]) r) ↔ IsUnit r
have rw₃ : IsUnit r ↔ IsUnit r
Tactic: rw [separable_def, derivative_C, isCoprime_zero_right, isUnit_C]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
h : (f * g).Separable
⊢ f.Separable
have this : IsCoprime f ((derivative : (a : R[X]) → R[X]) (f * g))
Tactic: have := h.of_mul_left_left
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
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))
⊢ f.Separable
have 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]))
Tactic: rw [derivative_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
h : (f * g).Separable
⊢ g.Separable
have h₁ : (g * f).Separable
Tactic: rw [mul_comm] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
hf : f.Separable
hfg : g ∣ f
⊢ g.Separable
have rcases : ∀ (f' : R[X]) (hf : (g * f').Separable), g.Separable
Tactic: rcases hfg with ⟨f', rfl⟩
Cleared hypotheses: f, hf, hfg
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
f g : R[X]
h : (f * g).Separable
⊢ IsCoprime f g
have this : IsCoprime f ((derivative : (a : R[X]) → R[X]) (f * g))
Tactic: have := h.of_mul_left_left
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
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 g
have 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]))
Tactic: rw [derivative_mul] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
f : R[X]
n : ℕ
h : (f ^ (n + 2)).Separable
⊢ IsUnit f ∨ f.Separable ∧ n + 2 = 1 ∨ n + 2 = 0
have h₁ : (f ^ n * f * f).Separable
Tactic: rw [pow_succ, pow_succ] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ 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
have rw : Polynomial.map f a * Polynomial.map f p + Polynomial.map f b * Polynomial.map f ((derivative : (a : R[X]) → R[X]) p) = 1
Tactic: rw [derivative_map, ← Polynomial.map_mul, ← Polynomial.map_mul, ← Polynomial.map_add, H,
      Polynomial.map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ 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
have rw₁ : Polynomial.map f (a * p) + Polynomial.map f b * Polynomial.map f ((derivative : (a : R[X]) → R[X]) p) = 1
Tactic: rw [derivative_map, ← Polynomial.map_mul, ← Polynomial.map_mul, ← Polynomial.map_add, H,
      Polynomial.map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ 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
have rw₂ : Polynomial.map f (a * p) + Polynomial.map f (HMul.hMul (β := R[X]) b ((derivative : (a : R[X]) → R[X]) p : R[X])) = 1
Tactic: rw [derivative_map, ← Polynomial.map_mul, ← Polynomial.map_mul, ← Polynomial.map_add, H,
      Polynomial.map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ 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
have rw₃ : Polynomial.map f (a * p + HMul.hMul (β := R[X]) b ((derivative : (a : R[X]) → R[X]) p : R[X])) = 1
Tactic: rw [derivative_map, ← Polynomial.map_mul, ← Polynomial.map_mul, ← Polynomial.map_add, H,
      Polynomial.map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ 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
have rw₄ : Polynomial.map f 1 = 1
Tactic: rw [derivative_map, ← Polynomial.map_mul, ← Polynomial.map_mul, ← Polynomial.map_add, H,
      Polynomial.map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ 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
have rw₅ : Eq.{v + 1} (α := S[X]) 1 1
Tactic: rw [derivative_map, ← Polynomial.map_mul, ← Polynomial.map_mul, ← Polynomial.map_add, H,
      Polynomial.map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ False
have obtain : ∀ (a b : R[X]) (e : a * p + HMul.hMul (β := R[X]) b ((derivative : (a : R[X]) → R[X]) p : R[X]) = 1), False
Tactic: obtain ⟨a, b, e⟩ := h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
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
⊢ False
have e₁ : 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
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
hp : p.Separable
hq : q * q ∣ p
⊢ IsUnit q
have obtain : ∀ (p : R[X]) (hp : (q * q * p).Separable), IsUnit q
Tactic: obtain ⟨p, rfl⟩ := hq
Cleared hypotheses: p, hp, hq
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
⊢ IsUnit q
have apply : IsCoprime q q
Tactic: apply isCoprime_self.mp
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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])))
have 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]))
Tactic: simp only [← mul_assoc, mul_add]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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)
    (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]))
have 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)
Tactic: convert! hp using 1
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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]) =
    (derivative : (a : R[X]) → R[X]) (q * q * p)
have 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])
Tactic: rw [derivative_mul, derivative_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
R : Type u
inst : CommSemiring R
q p : R[X]
hp : (q * q * p).Separable
⊢ IsCoprime q q
have 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])))
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
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
hq : ¬IsUnit q
hsep : p.Separable
⊢ emultiplicity q p ≤ 1
have contrapose! : ∀ (hq : 1 < emultiplicity q p), IsUnit q
Tactic: contrapose! hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ IsUnit q
have apply : q * q ∣ p
Tactic: apply isUnit_of_self_mul_dvd_separable hsep
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ q * q ∣ p
have rw : HPow.hPow (β := ℕ) q 2 ∣ p
Tactic: rw [← sq]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommSemiring R
p q : R[X]
hsep : p.Separable
hq : 1 < emultiplicity q p
⊢ HPow.hPow (β := ℕ) q 2 ∣ p
have hk : (↑2 : ℕ∞) ≤ emultiplicity q p
Tactic: apply pow_dvd_of_le_emultiplicity
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
hsep : p.Separable
⊢ Squarefree p
have rw : ∀ (x : R[X]), emultiplicity x p ≤ 1 ∨ IsUnit x
Tactic: rw [squarefree_iff_emultiplicity_le_one p]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommSemiring R
p : R[X]
hsep : p.Separable
⊢ Squarefree p
have rw : ∀ (x : R[X]), emultiplicity x p ≤ 1 ∨ IsUnit x
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
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
f g : R[X]
hf : f.Separable
hg : g.Separable
h : IsCoprime f g
⊢ (f * g).Separable
have 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]))
Tactic: rw [separable_def, derivative_mul]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
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
⊢ Separable.{u} (R := R) (∏ x ∈ insert a s, f x)
have h2₁ : (f a).Separable ∧ ∀ x ∈ s, (f x).Separable
Tactic: simp_rw [Finset.forall_mem_insert, forall_and] at h1 h2
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
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
⊢ Separable.{u} (R := R) (∏ x ∈ insert a s, f x)
have 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)
Tactic: simp_rw [Finset.forall_mem_insert, forall_and] at h1 h2
Cleared hypotheses: h1, h2
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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)
⊢ Separable.{u} (R := R) (∏ x ∈ insert a s, f x)
have rw : (f a * ∏ x ∈ s, f x).Separable
Tactic: rw [prod_insert has]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
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
⊢ x = y
have by_contra : ∀ (hxy : ¬x = y), False
Tactic: by_contra hxy