awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
p : ℕ
h_1 : ExpChar F p
x y : F
hy : eval y (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X p) ((C : (a : F) → F[X]) x : F[X])) = 0
⊢ (frobenius F p : (a : F) → F) y = x
have rwa : ∀ (hy : eval y (HPow.hPow (α := F[X]) X p) - eval y ((C : (a : F) → F[X]) x) = 0), (frobenius F p : (a : F) → F) y = x
Tactic: rwa [eval_sub, eval_X_pow, eval_C, sub_eq_zero] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
p : ℕ
h_1 : ExpChar F p
x y : F
hy : eval y (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X p) ((C : (a : F) → F[X]) x : F[X])) = 0
rwa :
  ∀ (hy : eval y (HPow.hPow (α := F[X]) X p) - eval y ((C : (a : F) → F[X]) x) = 0), (frobenius F p : (a : F) → F) y = x
⊢ (frobenius F p : (a : F) → F) y = x
have rwa₁ : ∀ (hy : y ^ p - eval y ((C : (a : F) → F[X]) x) = 0), (frobenius F p : (a : F) → F) y = x
Tactic: rwa [eval_sub, eval_X_pow, eval_C, sub_eq_zero] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
p : ℕ
h_1 : ExpChar F p
x y : F
hy : eval y (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X p) ((C : (a : F) → F[X]) x : F[X])) = 0
rwa :
  ∀ (hy : eval y (HPow.hPow (α := F[X]) X p) - eval y ((C : (a : F) → F[X]) x) = 0), (frobenius F p : (a : F) → F) y = x
rwa₁ : ∀ (hy : y ^ p - eval y ((C : (a : F) → F[X]) x) = 0), (frobenius F p : (a : F) → F) y = x
⊢ (frobenius F p : (a : F) → F) y = x
have rwa₂ : ∀ (hy : y ^ p - x = 0), (frobenius F p : (a : F) → F) y = x
Tactic: rwa [eval_sub, eval_X_pow, eval_C, sub_eq_zero] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (goal)
Goal:
F : Type u_1
inst : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
p : ℕ
h_1 : ExpChar F p
x y : F
hy : eval y (HSub.hSub (β := F[X]) (HPow.hPow (α := F[X]) X p) ((C : (a : F) → F[X]) x : F[X])) = 0
rwa :
  ∀ (hy : eval y (HPow.hPow (α := F[X]) X p) - eval y ((C : (a : F) → F[X]) x) = 0), (frobenius F p : (a : F) → F) y = x
rwa₁ : ∀ (hy : y ^ p - eval y ((C : (a : F) → F[X]) x) = 0), (frobenius F p : (a : F) → F) y = x
rwa₂ : ∀ (hy : y ^ p - x = 0), (frobenius F p : (a : F) → F) y = x
⊢ (frobenius F p : (a : F) → F) y = x
have rwa₃ : ∀ (hy : y ^ p = x), (frobenius F p : (a : F) → F) y = x
Tactic: rwa [eval_sub, eval_X_pow, eval_C, sub_eq_zero] at hy
Cleared hypotheses: hy
-- Lean 4 proof step from Mathlib.FieldTheory.SeparableDegree (hypothesis)
Goal:
F : Type u_1
inst : Field F
h : ∀ (f : F[X]), f.natSepDegree = 1 → f.Splits
p : ℕ
h_1 : ExpChar F p
⊢ PerfectField F
have this : PerfectRing F p
Tactic: haveI := PerfectRing.ofSurjective F p fun x ↦ by
    obtain ⟨y, hy⟩ := Splits.exists_eval_eq_zero
      (h _ (pow_one p ▸ natSepDegree_X_pow_char_pow_sub_C p 1 x))
      ((degree_X_pow_sub_C (expChar_pos F p) x).symm ▸ Nat.cast_pos.2 (expChar_pos F p)).ne'
    exact ⟨y, by rwa [eval_sub, eval_X_pow, eval_C, sub_eq_zero] at hy⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
i : ι
⊢ Eq (α := K)
    ((Polynomial.aeval (a i) : (a : Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) → K)
        (F.toPolynomialAdjoinImageCompl a i) :
      K)
    (0 : K)
have rw : Eq (α := K)
  ((AlgHom.restrictScalars k (Polynomial.aeval (a i)) : (a : Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) → K)
      (F.toPolynomialAdjoinImageCompl a i) :
    K)
  ((aeval a : (a : MvPolynomial ι k) → K) F : K)
Tactic: rw [← hFa, ← AlgHom.restrictScalars_apply k]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
i : ι
⊢ Eq (α := K)
    ((AlgHom.restrictScalars k (Polynomial.aeval (a i)) : (a : Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) → K)
        (F.toPolynomialAdjoinImageCompl a i) :
      K)
    ((aeval a : (a : MvPolynomial ι k) → K) F : K)
have simp_rw : Eq.{u_2 + 1} (α := K)
  ((AlgHom.comp (B := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (AlgHom.restrictScalars k (Polynomial.aeval (a i)))
          (AlgHom.comp
            (Polynomial.mapAlgHom
              (aeval fun (j : { j : ι // j ≠ i }) ↦
                Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
                  (a (↑j : ι)) sorry))
            (AlgHom.comp
              (↑(optionEquivLeft k { b : ι // b ≠ i }) :
                MvPolynomial (Option { b : ι // b ≠ i }) k →ₐ[k] Polynomial (MvPolynomial { b : ι // b ≠ i } k))
              (↑(renameEquiv k (Equiv.optionSubtypeNe i).symm) :
                MvPolynomial ι k →ₐ[k] MvPolynomial (Option { b : ι // b ≠ i }) k))) :
        (a : MvPolynomial ι k) → K)
      F :
    K)
  ((aeval a : (a : MvPolynomial ι k) → K) F : K)
Tactic: simp_rw [toPolynomialAdjoinImageCompl, ← AlgEquiv.coe_algHom, ← AlgHom.comp_apply]
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
i : ι
⊢ Eq.{u_2 + 1} (α := K)
    ((AlgHom.comp (B := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (AlgHom.restrictScalars k (Polynomial.aeval (a i)))
            (AlgHom.comp
              (Polynomial.mapAlgHom
                (aeval fun (j : { j : ι // j ≠ i }) ↦
                  Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
                    (a (↑j : ι)) ⋯))
              (AlgHom.comp
                (↑(optionEquivLeft k { b : ι // b ≠ i }) :
                  MvPolynomial (Option { b : ι // b ≠ i }) k →ₐ[k] Polynomial (MvPolynomial { b : ι // b ≠ i } k))
                (↑(renameEquiv k (Equiv.optionSubtypeNe i).symm) :
                  MvPolynomial ι k →ₐ[k] MvPolynomial (Option { b : ι // b ≠ i }) k))) :
          (a : MvPolynomial ι k) → K)
        F :
      K)
    ((aeval a : (a : MvPolynomial ι k) → K) F : K)
have e_a : Eq (α := MvPolynomial ι k →ₐ[k] K)
  (AlgHom.comp (B := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (AlgHom.restrictScalars k (Polynomial.aeval (a i)))
    (AlgHom.comp
      (Polynomial.mapAlgHom
        (aeval fun (j : { j : ι // j ≠ i }) ↦
          Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
            (a (↑j : ι)) sorry))
      (AlgHom.comp
        (↑(optionEquivLeft k { b : ι // b ≠ i }) :
          MvPolynomial (Option { b : ι // b ≠ i }) k →ₐ[k] Polynomial (MvPolynomial { b : ι // b ≠ i } k))
        (↑(renameEquiv k (Equiv.optionSubtypeNe i).symm) :
          MvPolynomial ι k →ₐ[k] MvPolynomial (Option { b : ι // b ≠ i }) k))))
  (aeval a)
Tactic: congr
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
i : ι
⊢ Eq (α := MvPolynomial ι k →ₐ[k] K)
    (AlgHom.comp (B := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (AlgHom.restrictScalars k (Polynomial.aeval (a i)))
      (AlgHom.comp
        (Polynomial.mapAlgHom
          (aeval fun (j : { j : ι // j ≠ i }) ↦
            Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
              (a (↑j : ι)) ⋯))
        (AlgHom.comp
          (↑(optionEquivLeft k { b : ι // b ≠ i }) :
            MvPolynomial (Option { b : ι // b ≠ i }) k →ₐ[k] Polynomial (MvPolynomial { b : ι // b ≠ i } k))
          (↑(renameEquiv k (Equiv.optionSubtypeNe i).symm) :
            MvPolynomial ι k →ₐ[k] MvPolynomial (Option { b : ι // b ≠ i }) k))))
    (aeval a)
have e_a : ∀ (i_1 : ι),
  Eq.{u_2 + 1} (α := K)
    ((AlgHom.comp (B := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (AlgHom.restrictScalars k (Polynomial.aeval (a i)))
            (AlgHom.comp
              (Polynomial.mapAlgHom
                (aeval fun (j : { j : ι // j ≠ i }) ↦
                  Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
                    (a (↑j : ι)) sorry))
              (AlgHom.comp
                (↑(optionEquivLeft k { b : ι // b ≠ i }) :
                  MvPolynomial (Option { b : ι // b ≠ i }) k →ₐ[k] Polynomial (MvPolynomial { b : ι // b ≠ i } k))
                (↑(renameEquiv k (Equiv.optionSubtypeNe i).symm) :
                  MvPolynomial ι k →ₐ[k] MvPolynomial (Option { b : ι // b ≠ i }) k))) :
          (a : MvPolynomial ι k) → K)
        (X i_1) :
      K)
    ((aeval a : (a : MvPolynomial ι k) → K) (X i_1) : K)
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent.{u_3, u_1, u_2} k (A := K) fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
⊢ a '' {i}ᶜ = Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
have h : ∀ (x : K),
  x ∈ a '' {i}ᶜ ↔ Membership.mem (γ := Set K) (Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)) x
Tactic: ext
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent.{u_3, u_1, u_2} k (A := K) fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
⊢ Irreducible (M := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) (F.toPolynomialAdjoinImageCompl a i)
have this : a '' {i}ᶜ = Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
Tactic: have : a '' {i}ᶜ = Set.range (fun x : {j | j ≠ i} ↦ a x) := by ext; simp
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent.{u_3, u_1, u_2} k (A := K) fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
this : a '' {i}ᶜ = Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
⊢ Irreducible.{u_2} (M := Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    ((Polynomial.mapAlgHom
            (aeval fun (j : { j : ι // j ≠ i }) ↦
              Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
                (a (↑j : ι)) ⋯) :
          (a_1 : Polynomial (MvPolynomial { j : ι // j ≠ i } k)) → Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
        ((optionEquivLeft k { b : ι // b ≠ i } :
            (a : MvPolynomial (Option { b : ι // b ≠ i }) k) → Polynomial (MvPolynomial { b : ι // b ≠ i } k))
          ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
              (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
            F)) :
      Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
have h : Eq (α := (a_1 : Polynomial (MvPolynomial.{u_3, u_1} { j : ι // j ≠ i } k)) → Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
  (⇑(Polynomial.mapAlgHom
        (aeval fun (j : { j : ι // j ≠ i }) ↦
          Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
            (a (↑j : ι)) sorry)) :
    (a_1 : Polynomial (MvPolynomial { j : ι // j ≠ i } k)) → Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
  (⇑(Polynomial.mapAlgEquiv
        (H.aevalEquiv.trans
          (Subalgebra.equivOfEq (Algebra.adjoin k (Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)))
            (Algebra.adjoin k (a '' {i}ᶜ)) sorry))) :
    (a_1 : Polynomial (MvPolynomial { b : ι // b ≠ i } k)) → Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
Tactic: convert!
    hF.map (renameEquiv k (Equiv.optionSubtypeNe i).symm) |>.map (optionEquivLeft k _) |>.map
      (Polynomial.mapAlgEquiv
        (H.aevalEquiv.trans (Subalgebra.equivOfEq _ _ congr(Algebra.adjoin k $this.symm))))
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
hF : Irreducible F
i : ι
H : AlgebraicIndependent.{u_3, u_1, u_2} k (A := K) fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
this : a '' {i}ᶜ = Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)
⊢ Eq (α :=
    (a_1 : Polynomial (MvPolynomial.{u_3, u_1} { j : ι // j ≠ i } k)) → Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (⇑(Polynomial.mapAlgHom
          (aeval fun (j : { j : ι // j ≠ i }) ↦
            Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x)
              (a (↑j : ι)) ⋯)) :
      (a_1 : Polynomial (MvPolynomial { j : ι // j ≠ i } k)) → Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (⇑(↑(Polynomial.mapAlgEquiv
              (H.aevalEquiv.trans
                (Subalgebra.equivOfEq
                  (Algebra.adjoin k (Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)))
                  (Algebra.adjoin k (a '' {i}ᶜ)) ⋯))) :
          Polynomial (MvPolynomial { b : ι // b ≠ i } k) →ₐ[k] Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))) :
      (a_1 : Polynomial (MvPolynomial { b : ι // b ≠ i } k)) → Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ)))
have h : (aeval fun (j : { j : ι // j ≠ i }) ↦
    Subtype.mk (p := fun (x : K) ↦ Membership.mem (γ := Subalgebra k K) (Algebra.adjoin k (a '' {i}ᶜ)) x) (a (↑j : ι))
      sorry) =
  (↑(H.aevalEquiv.trans
        (Subalgebra.equivOfEq (Algebra.adjoin k (Set.range fun (x : (↑{j : ι | j ≠ i} : Type u_3)) ↦ a (↑x : ι)))
          (Algebra.adjoin k (a '' {i}ᶜ)) sorry)) :
    MvPolynomial (↑{j : ι | j ≠ i} : Type u_3) k →ₐ[k] ↥(Algebra.adjoin k (a '' {i}ᶜ)))
Tactic: congr
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
⊢ Irreducible F
have refine : ∀ (q₁ q₂ : MvPolynomial ι k) (e : F = q₁ * q₂), IsUnit q₁ ∨ IsUnit q₂
Tactic: refine ⟨fun h' ↦ (h'.map (aeval a)).ne_zero hFa, fun q₁ q₂ e ↦ ?_⟩
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
⊢ IsUnit q₁ ∨ IsUnit q₂
have inr : ∀
  (this :
    ∀ (q₁ q₂ : MvPolynomial ι k) (e : F = q₁ * q₂)
      (h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)), IsUnit q₁ ∨ IsUnit q₂)
  (h₁ : ¬Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)), IsUnit q₁ ∨ IsUnit q₂
Tactic: wlog h₁ : aeval a q₁ = 0 generalizing q₁ q₂
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
inr :
  ∀
    (this :
      ∀ (q₁ q₂ : MvPolynomial ι k) (e : F = q₁ * q₂)
        (h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)), IsUnit q₁ ∨ IsUnit q₂)
    (h₁ : ¬Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)), IsUnit q₁ ∨ IsUnit q₂
⊢ IsUnit q₁ ∨ IsUnit q₂
have wlog : ∀ (q₁ q₂ : MvPolynomial ι k) (e : F = q₁ * q₂)
  (h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)), IsUnit q₁ ∨ IsUnit q₂
Tactic: wlog h₁ : aeval a q₁ = 0 generalizing q₁ q₂
Cleared hypotheses: q₁, q₂, e
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)
⊢ IsUnit q₁ ∨ IsUnit q₂
have ne : q₁ ≠ 0 ∧ q₂ ≠ 0
Tactic: have ne := mul_ne_zero_iff.mp (e ▸ hF0)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
⊢ IsUnit q₁ ∨ IsUnit q₂
have this : F.totalDegree ≤ q₁.totalDegree
Tactic: have := HF q₁ ne.1 h₁
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
this : F.totalDegree ≤ q₁.totalDegree
⊢ IsUnit q₁ ∨ IsUnit q₂
have this₁ : q₂.totalDegree = 0
Tactic: rw [e, totalDegree_mul_of_isDomain ne.1 ne.2, add_le_iff_nonpos_right, nonpos_iff_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
this : q₂.totalDegree = 0
⊢ IsUnit q₁ ∨ IsUnit q₂
have refine : IsUnit (coeff 0 q₂)
Tactic: refine .inr (isUnit_iff_totalDegree_of_isReduced.mpr ⟨?_, this⟩)
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (hypothesis)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
hF0 : F ≠ 0
hFa : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F : K) (0 : K)
q₁ q₂ : MvPolynomial ι k
e : F = q₁ * q₂
h₁ : Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) q₁ : K) (0 : K)
ne : q₁ ≠ 0 ∧ q₂ ≠ 0
this : q₂.totalDegree = 0
⊢ IsUnit (coeff 0 q₂)
have ne₁ : q₁ ≠ 0 ∧
  Ne (α := MvPolynomial ι k) ((C : (a : k) → MvPolynomial ι k) (coeff 0 q₂) : MvPolynomial ι k) (0 : MvPolynomial ι k)
Tactic: rw [totalDegree_eq_zero_iff_eq_C.mp this] at ne
Cleared hypotheses: ne, this
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : Ne (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
H :
  Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
F₀ : Polynomial (MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k) :=
  (optionEquivLeft k { b : ι // b ≠ i } :
      (a : MvPolynomial (Option { b : ι // b ≠ i }) k) → Polynomial (MvPolynomial { b : ι // b ≠ i } k))
    ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
        (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
      F)
⊢ False
have refine_3 : ∀
  (H :
    F.totalDegree ≤
      totalDegree.{u_1, u_3} (R := k) (σ := ι)
        ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) : (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
          (F₀.coeff ((σ : (a : ι) → ℕ) i)))),
  False
Tactic: have H := HF (rename (↑) (F₀.coeff (σ i))) ?_ ?_
-- Lean 4 proof step from Mathlib.FieldTheory.SeparablyGenerated (goal)
Goal:
k : Type u_1
K : Type u_2
ι : Type u_3
inst : Field k
inst_1 : Field K
inst_2 : Algebra k K
a : ι → K
F : MvPolynomial ι k
HF :
  ∀ (F' : MvPolynomial ι k),
    F' ≠ 0 →
      Eq.{u_2 + 1} (α := K) ((aeval a : (a : MvPolynomial ι k) → K) F' : K) (0 : K) → F.totalDegree ≤ F'.totalDegree
σ : ι →₀ ℕ
hσ : σ ∈ F.support
i : ι
hσi : Ne (α := ℕ) ((σ : (a : ι) → ℕ) i : ℕ) (0 : ℕ)
H :
  Eq (α := ↥(Algebra.adjoin k (a '' {i}ᶜ)))
    (Polynomial.coeff (F.toPolynomialAdjoinImageCompl a i) ((σ : (a : ι) → ℕ) i)) 0
F₀ : Polynomial (MvPolynomial.{u_3, u_1} { b : ι // b ≠ i } k) :=
  (optionEquivLeft k { b : ι // b ≠ i } :
      (a : MvPolynomial (Option { b : ι // b ≠ i }) k) → Polynomial (MvPolynomial { b : ι // b ≠ i } k))
    ((renameEquiv k (Equiv.optionSubtypeNe i).symm :
        (a : MvPolynomial ι k) → MvPolynomial (Option { b : ι // b ≠ i }) k)
      F)
refine_3 :
  ∀
    (H :
      F.totalDegree ≤
        totalDegree.{u_1, u_3} (R := k) (σ := ι)
          ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) :
              (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
            (F₀.coeff ((σ : (a : ι) → ℕ) i)))),
    False
⊢ False
have refine_1 : Ne (α := MvPolynomial ι k)
  ((rename (Subtype.val (p := fun (b : ι) ↦ b ≠ i)) : (a : MvPolynomial { b : ι // b ≠ i } k) → MvPolynomial ι k)
      (F₀.coeff ((σ : (a : ι) → ℕ) i)) :
    MvPolynomial ι k)
  (0 : MvPolynomial ι k)
Tactic: have H := HF (rename (↑) (F₀.coeff (σ i))) ?_ ?_