awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
a b c : R
hn : Eq.{u + 1} (α := R) (↑n : R) 0
hb_1 : IsUnit b
f : R[X] :=
  HAdd.hAdd (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
    ((C : (a : R) → R[X]) c : R[X])
e : R
hb : e * b = 1
hderiv : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) b : R[X])
rw :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f +
      HMul.hMul (β := R[X]) (HAdd.hAdd (β := R[X]) f ((C : (a : R) → R[X]) e : R[X])) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₁ :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f +
      (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X])) =
    1
rw₂ :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₃ :
  -HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) f + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₄ :
  -HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
⊢ HMul.hMul (α := R[X]) (-(derivative : (a : R[X]) → R[X]) f : R[X]) f +
      HMul.hMul (β := R[X]) (HAdd.hAdd (β := R[X]) f ((C : (a : R) → R[X]) e : R[X]))
        ((derivative : (a : R[X]) → R[X]) f : R[X]) =
    1
have rw₅ : 0 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) = 1
Tactic: rw [hderiv, right_distrib, ← add_assoc, neg_mul, mul_comm, neg_add_cancel, zero_add,
    ← map_mul, hb, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
a b c : R
hn : Eq.{u + 1} (α := R) (↑n : R) 0
hb_1 : IsUnit b
f : R[X] :=
  HAdd.hAdd (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
    ((C : (a : R) → R[X]) c : R[X])
e : R
hb : e * b = 1
hderiv : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) b : R[X])
rw :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f +
      HMul.hMul (β := R[X]) (HAdd.hAdd (β := R[X]) f ((C : (a : R) → R[X]) e : R[X])) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₁ :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f +
      (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X])) =
    1
rw₂ :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₃ :
  -HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) f + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₄ :
  -HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₅ : 0 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) = 1
⊢ HMul.hMul (α := R[X]) (-(derivative : (a : R[X]) → R[X]) f : R[X]) f +
      HMul.hMul (β := R[X]) (HAdd.hAdd (β := R[X]) f ((C : (a : R) → R[X]) e : R[X]))
        ((derivative : (a : R[X]) → R[X]) f : R[X]) =
    1
have rw₆ : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) = 1
Tactic: rw [hderiv, right_distrib, ← add_assoc, neg_mul, mul_comm, neg_add_cancel, zero_add,
    ← map_mul, hb, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
a b c : R
hn : Eq.{u + 1} (α := R) (↑n : R) 0
hb_1 : IsUnit b
f : R[X] :=
  HAdd.hAdd (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
    ((C : (a : R) → R[X]) c : R[X])
e : R
hb : e * b = 1
hderiv : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) b : R[X])
rw :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f +
      HMul.hMul (β := R[X]) (HAdd.hAdd (β := R[X]) f ((C : (a : R) → R[X]) e : R[X])) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₁ :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f +
      (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X])) =
    1
rw₂ :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₃ :
  -HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) f + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₄ :
  -HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₅ : 0 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) = 1
rw₆ : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) = 1
⊢ HMul.hMul (α := R[X]) (-(derivative : (a : R[X]) → R[X]) f : R[X]) f +
      HMul.hMul (β := R[X]) (HAdd.hAdd (β := R[X]) f ((C : (a : R) → R[X]) e : R[X]))
        ((derivative : (a : R[X]) → R[X]) f : R[X]) =
    1
have rw₇ : Eq (α := R[X]) ((C : (a : R) → R[X]) (e * b) : R[X]) (1 : R[X])
Tactic: rw [hderiv, right_distrib, ← add_assoc, neg_mul, mul_comm, neg_add_cancel, zero_add,
    ← map_mul, hb, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
a b c : R
hn : Eq.{u + 1} (α := R) (↑n : R) 0
hb_1 : IsUnit b
f : R[X] :=
  HAdd.hAdd (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
    ((C : (a : R) → R[X]) c : R[X])
e : R
hb : e * b = 1
hderiv : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) b : R[X])
rw :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f +
      HMul.hMul (β := R[X]) (HAdd.hAdd (β := R[X]) f ((C : (a : R) → R[X]) e : R[X])) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₁ :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f +
      (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X])) =
    1
rw₂ :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₃ :
  -HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) f + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₄ :
  -HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₅ : 0 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) = 1
rw₆ : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) = 1
rw₇ : Eq (α := R[X]) ((C : (a : R) → R[X]) (e * b) : R[X]) (1 : R[X])
⊢ HMul.hMul (α := R[X]) (-(derivative : (a : R[X]) → R[X]) f : R[X]) f +
      HMul.hMul (β := R[X]) (HAdd.hAdd (β := R[X]) f ((C : (a : R) → R[X]) e : R[X]))
        ((derivative : (a : R[X]) → R[X]) f : R[X]) =
    1
have rw₈ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1
Tactic: rw [hderiv, right_distrib, ← add_assoc, neg_mul, mul_comm, neg_add_cancel, zero_add,
    ← map_mul, hb, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
n : ℕ
a b c : R
hn : Eq.{u + 1} (α := R) (↑n : R) 0
hb_1 : IsUnit b
f : R[X] :=
  HAdd.hAdd (β := R[X])
    (HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) a : R[X]) (HPow.hPow (α := R[X]) X n) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) b : R[X]) X)
    ((C : (a : R) → R[X]) c : R[X])
e : R
hb : e * b = 1
hderiv : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) b : R[X])
rw :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f +
      HMul.hMul (β := R[X]) (HAdd.hAdd (β := R[X]) f ((C : (a : R) → R[X]) e : R[X])) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₁ :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f +
      (HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
        HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X])) =
    1
rw₂ :
  HMul.hMul (α := R[X]) (-(C : (a : R) → R[X]) b : R[X]) f + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₃ :
  -HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) b : R[X]) f + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₄ :
  -HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) + HMul.hMul (β := R[X]) f ((C : (a : R) → R[X]) b : R[X]) +
      HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) =
    1
rw₅ : 0 + HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) = 1
rw₆ : HMul.hMul (α := R[X]) (β := R[X]) ((C : (a : R) → R[X]) e : R[X]) ((C : (a : R) → R[X]) b : R[X]) = 1
rw₇ : Eq (α := R[X]) ((C : (a : R) → R[X]) (e * b) : R[X]) (1 : R[X])
rw₈ : Eq.{u + 1} (α := R[X]) ((C : (a : R) → R[X]) 1) 1
⊢ HMul.hMul (α := R[X]) (-(derivative : (a : R[X]) → R[X]) f : R[X]) f +
      HMul.hMul (β := R[X]) (HAdd.hAdd (β := R[X]) f ((C : (a : R) → R[X]) e : R[X]))
        ((derivative : (a : R[X]) → R[X]) f : R[X]) =
    1
have rw₉ : Eq.{u + 1} (α := R[X]) 1 1
Tactic: rw [hderiv, right_distrib, ← add_assoc, neg_mul, mul_comm, neg_add_cancel, zero_add,
    ← map_mul, hb, map_one]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
⊢ rootMultiplicity x p ≤ 1
have pos : ∀ (hp : p = 0), rootMultiplicity x p ≤ 1
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
pos : ∀ (hp : p = 0), rootMultiplicity x p ≤ 1
⊢ rootMultiplicity x p ≤ 1
have neg : ∀ (hp : ¬p = 0), rootMultiplicity x p ≤ 1
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
hp : ¬p = 0
⊢ rootMultiplicity x p ≤ 1
have neg : emultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p ≤ 1
Tactic: rw [rootMultiplicity_eq_multiplicity, if_neg hp, ← Nat.cast_le (α := ℕ∞),
    Nat.cast_one, ← (finiteMultiplicity_X_sub_C x hp).emultiplicity_eq_multiplicity]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
⊢ rootMultiplicity x p ≤ 1
have pos : ∀ (hp : p = 0), rootMultiplicity x p ≤ 1
Tactic: classical
  by_cases hp : p = 0
  · simp [hp]
  rw [rootMultiplicity_eq_multiplicity, if_neg hp, ← Nat.cast_le (α := ℕ∞),
    Nat.cast_one, ← (finiteMultiplicity_X_sub_C x hp).emultiplicity_eq_multiplicity]
  apply emultiplicity_le_one_of_separable (not_isUnit_X_sub_C _) hsep
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
pos : ∀ (hp : p = 0), rootMultiplicity x p ≤ 1
⊢ rootMultiplicity x p ≤ 1
have neg : ∀ (hp : ¬p = 0), rootMultiplicity x p ≤ 1
Tactic: classical
  by_cases hp : p = 0
  · simp [hp]
  rw [rootMultiplicity_eq_multiplicity, if_neg hp, ← Nat.cast_le (α := ℕ∞),
    Nat.cast_one, ← (finiteMultiplicity_X_sub_C x hp).emultiplicity_eq_multiplicity]
  apply emultiplicity_le_one_of_separable (not_isUnit_X_sub_C _) hsep
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : Nontrivial R
p : R[X]
hsep : p.Separable
x : R
pos : ∀ (hp : p = 0), rootMultiplicity x p ≤ 1
neg neg₁ : ∀ (hp : ¬p = 0), rootMultiplicity x p ≤ 1
⊢ rootMultiplicity x p ≤ 1
have neg₂ : ∀ (hp : ¬p = 0), emultiplicity (HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) x : R[X])) p ≤ 1
Tactic: classical
  by_cases hp : p = 0
  · simp [hp]
  rw [rootMultiplicity_eq_multiplicity, if_neg hp, ← Nat.cast_le (α := ℕ∞),
    Nat.cast_one, ← (finiteMultiplicity_X_sub_C x hp).emultiplicity_eq_multiplicity]
  apply emultiplicity_le_one_of_separable (not_isUnit_X_sub_C _) hsep
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
p : R[X]
hsep : p.Separable
x : R
⊢ Multiset.count x p.roots ≤ 1
have rw : rootMultiplicity x p ≤ 1
Tactic: rw [count_roots p]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : Irreducible f
h : Ne (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
g : F[X]
hg1 : Membership.mem (γ := Set F[X]) (nonunits F[X]) g
_hg2 : g ≠ 0
h_1 : g ∣ f
hg4 : g ∣ (derivative : (a : F[X]) → F[X]) f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : (↑u : F[X]) = p
| f
have rw : g * (↑u : F[X])
Tactic: rw [hg3, ← hu]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : Irreducible f
h : Ne (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
g : F[X]
hg1 : Membership.mem (γ := Set F[X]) (nonunits F[X]) g
_hg2 : g ≠ 0
h_1 : g ∣ f
hg4 : g ∣ (derivative : (a : F[X]) → F[X]) f
p : F[X]
hg3 : f = g * p
u : F[X]ˣ
hu : (↑u : F[X]) = p
⊢ f ∣ (derivative : (a : F[X]) → F[X]) f
have conv_lhs : g * (↑u : F[X]) ∣ (derivative : (a : F[X]) → F[X]) f
Tactic: conv_lhs => rw [hg3, ← hu]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
S : Type u_1
inst_1 : CommRing S
inst_2 : Nontrivial S
f : F →+* S
p : F[X]
⊢ (map f p).Separable ↔ p.Separable
have refine : ∀ (H : (map f p).Separable), p.Separable
Tactic: refine ⟨fun H ↦ ?_, fun H ↦ H.map⟩
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
S : Type u_1
inst_1 : CommRing S
inst_2 : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
⊢ p.Separable
have obtain : ∀ (m : Ideal S) (hm : m.IsMaximal), p.Separable
Tactic: obtain ⟨m, hm⟩ := Ideal.exists_maximal S
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
F : Type u
inst : Field F
S : Type u_1
inst_1 : CommRing S
inst_2 : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
⊢ p.Separable
have this : (map (Ideal.Quotient.mk m) (map f p)).Separable
Tactic: have := Separable.map H (f := Ideal.Quotient.mk m)
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
S : Type u_1
inst_1 : CommRing S
inst_2 : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
this : (map (Ideal.Quotient.mk m) (map f p)).Separable
⊢ p.Separable
have rwa : ∀ (this : (map (RingHom.comp (Ideal.Quotient.mk m) f) p).Separable), p.Separable
Tactic: rwa [map_map, separable_def, derivative_map, isCoprime_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
S : Type u_1
inst_1 : CommRing S
inst_2 : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
this : (map (Ideal.Quotient.mk m) (map f p)).Separable
rwa : ∀ (this : (map (RingHom.comp (Ideal.Quotient.mk m) f) p).Separable), p.Separable
⊢ p.Separable
have rwa₁ : ∀
  (this :
    IsCoprime (map (RingHom.comp (Ideal.Quotient.mk m) f) p)
      ((derivative : (a : (S ⧸ m)[X]) → (S ⧸ m)[X]) (map (RingHom.comp (Ideal.Quotient.mk m) f) p))),
  p.Separable
Tactic: rwa [map_map, separable_def, derivative_map, isCoprime_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
S : Type u_1
inst_1 : CommRing S
inst_2 : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
this : (map (Ideal.Quotient.mk m) (map f p)).Separable
rwa : ∀ (this : (map (RingHom.comp (Ideal.Quotient.mk m) f) p).Separable), p.Separable
rwa₁ :
  ∀
    (this :
      IsCoprime (map (RingHom.comp (Ideal.Quotient.mk m) f) p)
        ((derivative : (a : (S ⧸ m)[X]) → (S ⧸ m)[X]) (map (RingHom.comp (Ideal.Quotient.mk m) f) p))),
    p.Separable
⊢ p.Separable
have rwa₂ : ∀
  (this :
    IsCoprime (map (RingHom.comp (Ideal.Quotient.mk m) f) p)
      (map (RingHom.comp (Ideal.Quotient.mk m) f) ((derivative : (a : F[X]) → F[X]) p))),
  p.Separable
Tactic: rwa [map_map, separable_def, derivative_map, isCoprime_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
S : Type u_1
inst_1 : CommRing S
inst_2 : Nontrivial S
f : F →+* S
p : F[X]
H : (map f p).Separable
m : Ideal S
hm : m.IsMaximal
this : (map (Ideal.Quotient.mk m) (map f p)).Separable
rwa : ∀ (this : (map (RingHom.comp (Ideal.Quotient.mk m) f) p).Separable), p.Separable
rwa₁ :
  ∀
    (this :
      IsCoprime (map (RingHom.comp (Ideal.Quotient.mk m) f) p)
        ((derivative : (a : (S ⧸ m)[X]) → (S ⧸ m)[X]) (map (RingHom.comp (Ideal.Quotient.mk m) f) p))),
    p.Separable
rwa₂ :
  ∀
    (this :
      IsCoprime (map (RingHom.comp (Ideal.Quotient.mk m) f) p)
        (map (RingHom.comp (Ideal.Quotient.mk m) f) ((derivative : (a : F[X]) → F[X]) p))),
    p.Separable
⊢ p.Separable
have rwa₃ : ∀ (this : IsCoprime p ((derivative : (a : F[X]) → F[X]) p)), p.Separable
Tactic: rwa [map_map, separable_def, derivative_map, isCoprime_map] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
ι : Type u_1
f : ι → F
s : Finset ι
H : ∀ x ∈ s, ∀ y ∈ s, f x = f y → x = y
⊢ Separable.{u} (R := F) (∏ i ∈ s, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (f i) : F[X]))
have rw : Separable.{u} (R := F) (∏ x ∈ s.attach, HSub.hSub (α := F[X]) (β := F[X]) X ((C : (a : F) → F[X]) (f (↑x : ι)) : F[X]))
Tactic: rw [← prod_attach]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
ι : Type u_1
inst_1 : Fintype ι
f : ι → F
⊢ (∀ (x : ι),
      Membership.mem (γ := Finset ι) univ x → ∀ (y : ι), Membership.mem (γ := Finset ι) univ y → f x = f y → x = y) ↔
    Function.Injective f
have simp_rw : (∀ (x : ι), True → ∀ (y : ι), True → f x = f y → x = y) ↔ Function.Injective f
Tactic: simp_rw [mem_univ, true_imp_iff, Function.Injective]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
ι : Type u_1
inst_1 : Fintype ι
f : ι → F
simp_rw : (∀ (x : ι), True → ∀ (y : ι), True → f x = f y → x = y) ↔ Function.Injective f
⊢ (∀ (x : ι),
      Membership.mem (γ := Finset ι) univ x → ∀ (y : ι), Membership.mem (γ := Finset ι) univ y → f x = f y → x = y) ↔
    Function.Injective f
have simp_rw₁ : (∀ (x y : ι), f x = f y → x = y) ↔ Function.Injective f
Tactic: simp_rw [mem_univ, true_imp_iff, Function.Injective]
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ (g : F[X]), Irreducible g ∧ (expand F p : (a : F[X]) → F[X]) g = f
have inl : ∀ [HF : CharP F 0], f.Separable ∨ ¬f.Separable ∧ ∃ (g : F[X]), Irreducible g ∧ (expand F 0 : (a : F[X]) → F[X]) g = f
Tactic: rcases p.eq_zero_or_pos with (rfl | hp)
Cleared hypotheses: p, HF
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
inl :
  ∀ [HF : CharP F 0], f.Separable ∨ ¬f.Separable ∧ ∃ (g : F[X]), Irreducible g ∧ (expand F 0 : (a : F[X]) → F[X]) g = f
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ (g : F[X]), Irreducible g ∧ (expand F p : (a : F[X]) → F[X]) g = f
have inr : ∀ (hp : p > 0), f.Separable ∨ ¬f.Separable ∧ ∃ (g : F[X]), Irreducible g ∧ (expand F p : (a : F[X]) → F[X]) g = f
Tactic: rcases p.eq_zero_or_pos with (rfl | hp)
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
HF : CharP F 0
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ (g : F[X]), Irreducible g ∧ (expand F 0 : (a : F[X]) → F[X]) g = f
have this : CharZero F
Tactic: haveI := CharP.charP_to_charZero F
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
HF : CharP F 0
this : CharZero F
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ (g : F[X]), Irreducible g ∧ (expand F 0 : (a : F[X]) → F[X]) g = f
have this₁ : f.natDegree = 0
Tactic: have := natDegree_eq_zero_of_derivative_eq_zero H
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
F : Type u
inst : Field F
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
HF : CharP F 0
this_1 : CharZero F
this : f.natDegree = 0
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ (g : F[X]), Irreducible g ∧ (expand F 0 : (a : F[X]) → F[X]) g = f
have this₁ : f.natDegree ≠ 0
Tactic: have := (natDegree_pos_iff_degree_pos.mpr <| degree_pos_of_irreducible hf).ne'
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (hypothesis)
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
hp : p > 0
⊢ f.Separable ∨ ¬f.Separable ∧ ∃ (g : F[X]), Irreducible g ∧ (expand F p : (a : F[X]) → F[X]) g = f
have this : IsLocalHom (R := F[X]) (S := F[X]) (F := F[X] →ₐ[F] F[X]) (expand F p)
Tactic: haveI := isLocalHom_expand F hp
-- Lean 4 proof step from Mathlib.FieldTheory.Separable (goal)
Goal:
F : Type u
inst : Field F
p : ℕ
HF : CharP F p
f : F[X]
hf : Irreducible f
H : Eq (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
hp : p > 0
this : IsLocalHom (R := F[X]) (S := F[X]) (F := F[X] →ₐ[F] F[X]) (expand F p)
⊢ ¬f.Separable
have rw : ¬Ne (α := F[X]) ((derivative : (a : F[X]) → F[X]) f : F[X]) (0 : F[X])
Tactic: rw [separable_iff_derivative_ne_zero hf, Classical.not_not, H]