awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
n : ℕ
a : K
H : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X n) ((C : (a : K) → K[X]) a : K[X]))
m : ℕ
hm : m ∣ n
hm' : m ≠ 1
b : K
hn : n ≠ 0
⊢ b ^ m ≠ a
have obtain : ∀ (k : ℕ) (H : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (m * k)) ((C : (a : K) → K[X]) a : K[X])))
  (hn : m * k ≠ 0), b ^ m ≠ a
Tactic: obtain ⟨k, rfl⟩ := hm
Cleared hypotheses: n, H, hm, hn
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
H : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (m * k)) ((C : (a : K) → K[X]) (b ^ m) : K[X]))
⊢ False
have obtain : ∀ (q : K[X])
  (hq :
    HPow.hPow (α := K[X]) X k ^ m - HPow.hPow (α := K[X]) ((C : (a : K) → K[X]) b : K[X]) m =
      HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X k) ((C : (a : K) → K[X]) b : K[X]) * q),
  False
Tactic: obtain ⟨q, hq⟩ := sub_dvd_pow_sub_pow (X ^ k) (C b) m
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
H : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X (m * k)) ((C : (a : K) → K[X]) (b ^ m) : K[X]))
q : K[X]
hq :
  HPow.hPow (α := K[X]) X k ^ m - HPow.hPow (α := K[X]) ((C : (a : K) → K[X]) b : K[X]) m =
    HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X k) ((C : (a : K) → K[X]) b : K[X]) * q
⊢ False
have rw : ∀ (q : K[X]) (H : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X k) ((C : (a : K) → K[X]) b : K[X]) * q))
  (hq :
    HPow.hPow (α := K[X]) X k ^ m - HPow.hPow (α := K[X]) ((C : (a : K) → K[X]) b : K[X]) m =
      HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X k) ((C : (a : K) → K[X]) b : K[X]) * q),
  False
Tactic: rw [mul_comm, pow_mul, map_pow, hq] at H
Cleared hypotheses: H, q, hq
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (hypothesis)
Goal:
K : Type u
inst : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
q : K[X]
H : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X k) ((C : (a : K) → K[X]) b : K[X]) * q)
hq :
  HPow.hPow (α := K[X]) X k ^ m - HPow.hPow (α := K[X]) ((C : (a : K) → K[X]) b : K[X]) m =
    HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X k) ((C : (a : K) → K[X]) b : K[X]) * q
⊢ False
have this : q.degree = 0
Tactic: have : degree q = 0 := by
    simpa [isUnit_iff_degree_eq_zero, degree_X_pow_sub_C,
      Nat.pos_iff_ne_zero, (mul_ne_zero_iff.mp hn).2] using H.2 rfl
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (hypothesis)
Goal:
K : Type u
inst : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
q : K[X]
H : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X k) ((C : (a : K) → K[X]) b : K[X]) * q)
hq :
  HPow.hPow (α := K[X]) X k ^ m - HPow.hPow (α := K[X]) ((C : (a : K) → K[X]) b : K[X]) m =
    HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X k) ((C : (a : K) → K[X]) b : K[X]) * q
this : q.degree = 0
⊢ False
have hq₁ : (HPow.hPow (α := K[X]) X k ^ m - HPow.hPow (α := K[X]) ((C : (a : K) → K[X]) b : K[X]) m).degree =
  (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X k) ((C : (a : K) → K[X]) b : K[X]) * q).degree
Tactic: apply_fun degree at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (hypothesis)
Goal:
K : Type u
inst : Field K
m : ℕ
hm' : m ≠ 1
b : K
k : ℕ
hn : m * k ≠ 0
q : K[X]
H : Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X k) ((C : (a : K) → K[X]) b : K[X]) * q)
this : q.degree = 0
hq :
  (HPow.hPow (α := K[X]) X k ^ m - HPow.hPow (α := K[X]) ((C : (a : K) → K[X]) b : K[X]) m).degree =
    (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X k) ((C : (a : K) → K[X]) b : K[X]) * q).degree
⊢ False
have hq₁ : m * k = k
Tactic: simp only [this, ← pow_mul, mul_comm k m, degree_X_pow_sub_C, Nat.pos_iff_ne_zero.mpr hn,
    Nat.pos_iff_ne_zero.mpr (mul_ne_zero_iff.mp hn).2, degree_mul, ← map_pow, add_zero,
    Nat.cast_injective.eq_iff] at hq
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ ¬IsUnit (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
have rw : ¬p = 0
Tactic: rw [Polynomial.isUnit_iff_degree_eq_zero, degree_X_pow_sub_C hp.pos, Nat.cast_eq_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (hypothesis)
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
have this : ¬IsUnit (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
Tactic: have : ¬ IsUnit (X ^ p - C a) := by
    rw [Polynomial.isUnit_iff_degree_eq_zero, degree_X_pow_sub_C hp.pos, Nat.cast_eq_zero]
    exact hp.ne_zero
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this : ¬IsUnit (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
have have : ∀ (g : K[X]) (hg : Irreducible g)
  (hg' : g ∣ HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])),
  Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
Tactic: have ⟨g, hg, hg'⟩ := WfDvdMonoid.exists_irreducible_factor this (X_pow_sub_C_ne_zero hp.pos a)
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this : ¬IsUnit (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
g : K[X]
hg : Irreducible g
hg' : g ∣ HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
have suffices : g.natDegree = p
Tactic: suffices natDegree g = p from (associated_of_dvd_of_natDegree_le hg'
    (X_pow_sub_C_ne_zero hp.pos a) (this.trans natDegree_X_pow_sub_C.symm).ge).irreducible hg
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this : ¬IsUnit (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
g : K[X]
hg : Irreducible g
hg' : g ∣ HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])
⊢ g.natDegree = p
have by_contra : ∀ (h : ¬g.natDegree = p), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (hypothesis)
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this : ¬IsUnit (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
g : K[X]
hg : Irreducible g
hg' : g ∣ HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])
h : ¬g.natDegree = p
⊢ HPow.hPow (α := K) ((Algebra.norm K : (a : AdjoinRoot g) → K) (root g) : K) p = a ^ g.natDegree
have this₁ : eval₂ (of g) (root g) (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])) = 0
Tactic: have := eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hg' (AdjoinRoot.eval₂_root g)
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (hypothesis)
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this_1 : ¬IsUnit (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
g : K[X]
hg : Irreducible g
hg' : g ∣ HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])
h : ¬g.natDegree = p
this : eval₂ (of g) (root g) (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])) = 0
⊢ HPow.hPow (α := K) ((Algebra.norm K : (a : AdjoinRoot g) → K) (root g) : K) p = a ^ g.natDegree
have this₁ : root g ^ p = (of g : (a : K) → AdjoinRoot g) a
Tactic: rw [eval₂_sub, eval₂_pow, eval₂_C, eval₂_X, sub_eq_zero] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this_1 : ¬IsUnit (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
g : K[X]
hg : Irreducible g
hg' : g ∣ HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])
h : ¬g.natDegree = p
this : root g ^ p = (of g : (a : K) → AdjoinRoot g) a
⊢ HPow.hPow (α := K) ((Algebra.norm K : (a : AdjoinRoot g) → K) (root g) : K) p = a ^ g.natDegree
have rw : (Algebra.norm K : (a : AdjoinRoot g) → K) (root g ^ p) = a ^ g.natDegree
Tactic: rw [← map_pow, this, ← AdjoinRoot.algebraMap_eq, Algebra.norm_algebraMap,
      (powerBasis hg.ne_zero).finrank, powerBasis_dim hg.ne_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this_1 : ¬IsUnit (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
g : K[X]
hg : Irreducible g
hg' : g ∣ HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])
h : ¬g.natDegree = p
this : root g ^ p = (of g : (a : K) → AdjoinRoot g) a
rw : (Algebra.norm K : (a : AdjoinRoot g) → K) (root g ^ p) = a ^ g.natDegree
⊢ HPow.hPow (α := K) ((Algebra.norm K : (a : AdjoinRoot g) → K) (root g) : K) p = a ^ g.natDegree
have rw₁ : (Algebra.norm K : (a : AdjoinRoot g) → K) ((of g : (a : K) → AdjoinRoot g) a : AdjoinRoot g) = a ^ g.natDegree
Tactic: rw [← map_pow, this, ← AdjoinRoot.algebraMap_eq, Algebra.norm_algebraMap,
      (powerBasis hg.ne_zero).finrank, powerBasis_dim hg.ne_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this_1 : ¬IsUnit (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
g : K[X]
hg : Irreducible g
hg' : g ∣ HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])
h : ¬g.natDegree = p
this : root g ^ p = (of g : (a : K) → AdjoinRoot g) a
rw : (Algebra.norm K : (a : AdjoinRoot g) → K) (root g ^ p) = a ^ g.natDegree
rw₁ : (Algebra.norm K : (a : AdjoinRoot g) → K) ((of g : (a : K) → AdjoinRoot g) a : AdjoinRoot g) = a ^ g.natDegree
⊢ HPow.hPow (α := K) ((Algebra.norm K : (a : AdjoinRoot g) → K) (root g) : K) p = a ^ g.natDegree
have rw₂ : (Algebra.norm K : (a : AdjoinRoot g) → K)
    (((algebraMap K (AdjoinRoot g) : K →+* AdjoinRoot g) : (a : K) → AdjoinRoot g) a : AdjoinRoot g) =
  a ^ g.natDegree
Tactic: rw [← map_pow, this, ← AdjoinRoot.algebraMap_eq, Algebra.norm_algebraMap,
      (powerBasis hg.ne_zero).finrank, powerBasis_dim hg.ne_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this_1 : ¬IsUnit (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
g : K[X]
hg : Irreducible g
hg' : g ∣ HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])
h : ¬g.natDegree = p
this : root g ^ p = (of g : (a : K) → AdjoinRoot g) a
rw : (Algebra.norm K : (a : AdjoinRoot g) → K) (root g ^ p) = a ^ g.natDegree
rw₁ : (Algebra.norm K : (a : AdjoinRoot g) → K) ((of g : (a : K) → AdjoinRoot g) a : AdjoinRoot g) = a ^ g.natDegree
rw₂ :
  (Algebra.norm K : (a : AdjoinRoot g) → K)
      (((algebraMap K (AdjoinRoot g) : K →+* AdjoinRoot g) : (a : K) → AdjoinRoot g) a : AdjoinRoot g) =
    a ^ g.natDegree
⊢ HPow.hPow (α := K) ((Algebra.norm K : (a : AdjoinRoot g) → K) (root g) : K) p = a ^ g.natDegree
have rw₃ : a ^ Module.finrank K (AdjoinRoot g) = a ^ g.natDegree
Tactic: rw [← map_pow, this, ← AdjoinRoot.algebraMap_eq, Algebra.norm_algebraMap,
      (powerBasis hg.ne_zero).finrank, powerBasis_dim hg.ne_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this_1 : ¬IsUnit (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
g : K[X]
hg : Irreducible g
hg' : g ∣ HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])
h : ¬g.natDegree = p
this : root g ^ p = (of g : (a : K) → AdjoinRoot g) a
rw : (Algebra.norm K : (a : AdjoinRoot g) → K) (root g ^ p) = a ^ g.natDegree
rw₁ : (Algebra.norm K : (a : AdjoinRoot g) → K) ((of g : (a : K) → AdjoinRoot g) a : AdjoinRoot g) = a ^ g.natDegree
rw₂ :
  (Algebra.norm K : (a : AdjoinRoot g) → K)
      (((algebraMap K (AdjoinRoot g) : K →+* AdjoinRoot g) : (a : K) → AdjoinRoot g) a : AdjoinRoot g) =
    a ^ g.natDegree
rw₃ : a ^ Module.finrank K (AdjoinRoot g) = a ^ g.natDegree
⊢ HPow.hPow (α := K) ((Algebra.norm K : (a : AdjoinRoot g) → K) (root g) : K) p = a ^ g.natDegree
have rw₄ : a ^ (powerBasis sorry).dim = a ^ g.natDegree
Tactic: rw [← map_pow, this, ← AdjoinRoot.algebraMap_eq, Algebra.norm_algebraMap,
      (powerBasis hg.ne_zero).finrank, powerBasis_dim hg.ne_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (goal)
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this_1 : ¬IsUnit (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
g : K[X]
hg : Irreducible g
hg' : g ∣ HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])
h : ¬g.natDegree = p
this : root g ^ p = (of g : (a : K) → AdjoinRoot g) a
rw : (Algebra.norm K : (a : AdjoinRoot g) → K) (root g ^ p) = a ^ g.natDegree
rw₁ : (Algebra.norm K : (a : AdjoinRoot g) → K) ((of g : (a : K) → AdjoinRoot g) a : AdjoinRoot g) = a ^ g.natDegree
rw₂ :
  (Algebra.norm K : (a : AdjoinRoot g) → K)
      (((algebraMap K (AdjoinRoot g) : K →+* AdjoinRoot g) : (a : K) → AdjoinRoot g) a : AdjoinRoot g) =
    a ^ g.natDegree
rw₃ : a ^ Module.finrank K (AdjoinRoot g) = a ^ g.natDegree
rw₄ : a ^ (powerBasis ⋯).dim = a ^ g.natDegree
⊢ HPow.hPow (α := K) ((Algebra.norm K : (a : AdjoinRoot g) → K) (root g) : K) p = a ^ g.natDegree
have rw₅ : a ^ g.natDegree = a ^ g.natDegree
Tactic: rw [← map_pow, this, ← AdjoinRoot.algebraMap_eq, Algebra.norm_algebraMap,
      (powerBasis hg.ne_zero).finrank, powerBasis_dim hg.ne_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (hypothesis)
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this : ¬IsUnit (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
g : K[X]
hg : Irreducible g
hg' : g ∣ HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])
h : ¬g.natDegree = p
⊢ False
have key : HPow.hPow (α := K) ((Algebra.norm K : (a : AdjoinRoot g) → K) (root g) : K) p = a ^ g.natDegree
Tactic: have key : (Algebra.norm K (AdjoinRoot.root g)) ^ p = a ^ g.natDegree := by
    have := eval₂_eq_zero_of_dvd_of_eval₂_eq_zero _ _ hg' (AdjoinRoot.eval₂_root g)
    rw [eval₂_sub, eval₂_pow, eval₂_C, eval₂_X, sub_eq_zero] at this
    rw [← map_pow, this, ← AdjoinRoot.algebraMap_eq, Algebra.norm_algebraMap,
      (powerBasis hg.ne_zero).finrank, powerBasis_dim hg.ne_zero]
-- Lean 4 proof step from Mathlib.FieldTheory.KummerPolynomial (hypothesis)
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
this : ¬IsUnit (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))
g : K[X]
hg : Irreducible g
hg' : g ∣ HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])
h : ¬g.natDegree = p
key : HPow.hPow (α := K) ((Algebra.norm K : (a : AdjoinRoot g) → K) (root g) : K) p = a ^ g.natDegree
⊢ False
have this₁ : p.Coprime g.natDegree
Tactic: have : p.Coprime (natDegree g) := hp.coprime_iff_not_dvd.mpr (fun e ↦ h (((natDegree_le_of_dvd hg'
    (X_pow_sub_C_ne_zero hp.pos a)).trans_eq natDegree_X_pow_sub_C).antisymm (Nat.le_of_dvd
      (natDegree_pos_iff_degree_pos.mpr <| Polynomial.degree_pos_of_irreducible hg) e)))
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
⊢ Membership.mem (α := R[X]) (γ := Submonoid R[X]) R[X]⁰ ((taylor r : (a : R[X]) → R[X]) p : R[X])
have rw : ∀ (x : R[X]), HMul.hMul (β := R[X]) x ((taylor r : (a : R[X]) → R[X]) p : R[X]) = 0 → x = 0
Tactic: rw [mem_nonZeroDivisors_iff_right]
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (hypothesis)
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
x : R[X]
hx : HMul.hMul (β := R[X]) x ((taylor r : (a : R[X]) → R[X]) p : R[X]) = 0
⊢ x = 0
have this : x = (taylor (r - r) : (a : R[X]) → R[X]) x
Tactic: have : x = taylor (r - r) x := by simp
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
x : R[X]
hx : HMul.hMul (β := R[X]) x ((taylor r : (a : R[X]) → R[X]) p : R[X]) = 0
this : x = (taylor (r - r) : (a : R[X]) → R[X]) x
⊢ x = 0
have rwa : ∀
  (hx :
    HMul.hMul (α := R[X]) (β := R[X]) ((taylor (r - r) : (a : R[X]) → R[X]) x : R[X])
        ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
      0)
  (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
Tactic: rwa [this, sub_eq_add_neg, ← taylor_taylor, ← taylor_mul,
    LinearMap.map_eq_zero_iff _ (taylor_injective _), mul_right_mem_nonZeroDivisors_eq_zero_iff hp,
    LinearMap.map_eq_zero_iff _ (taylor_injective _)] at hx
Cleared hypotheses: hx, this
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
x : R[X]
hx : HMul.hMul (β := R[X]) x ((taylor r : (a : R[X]) → R[X]) p : R[X]) = 0
this : x = (taylor (r - r) : (a : R[X]) → R[X]) x
rwa :
  ∀
    (hx :
      HMul.hMul (α := R[X]) (β := R[X]) ((taylor (r - r) : (a : R[X]) → R[X]) x : R[X])
          ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
        0)
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
⊢ x = 0
have rwa₁ : ∀
  (hx :
    HMul.hMul (α := R[X]) (β := R[X]) ((taylor (r + -r) : (a : R[X]) → R[X]) x : R[X])
        ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
      0)
  (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
Tactic: rwa [this, sub_eq_add_neg, ← taylor_taylor, ← taylor_mul,
    LinearMap.map_eq_zero_iff _ (taylor_injective _), mul_right_mem_nonZeroDivisors_eq_zero_iff hp,
    LinearMap.map_eq_zero_iff _ (taylor_injective _)] at hx
Cleared hypotheses: hx, this
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
x : R[X]
hx : HMul.hMul (β := R[X]) x ((taylor r : (a : R[X]) → R[X]) p : R[X]) = 0
this : x = (taylor (r - r) : (a : R[X]) → R[X]) x
rwa :
  ∀
    (hx :
      HMul.hMul (α := R[X]) (β := R[X]) ((taylor (r - r) : (a : R[X]) → R[X]) x : R[X])
          ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
        0)
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
rwa₁ :
  ∀
    (hx :
      HMul.hMul (α := R[X]) (β := R[X]) ((taylor (r + -r) : (a : R[X]) → R[X]) x : R[X])
          ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
        0)
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
⊢ x = 0
have rwa₂ : ∀
  (hx :
    HMul.hMul (α := R[X]) (β := R[X]) ((taylor r : (a : R[X]) → R[X]) ((taylor (-r) : (a : R[X]) → R[X]) x) : R[X])
        ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
      0)
  (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
Tactic: rwa [this, sub_eq_add_neg, ← taylor_taylor, ← taylor_mul,
    LinearMap.map_eq_zero_iff _ (taylor_injective _), mul_right_mem_nonZeroDivisors_eq_zero_iff hp,
    LinearMap.map_eq_zero_iff _ (taylor_injective _)] at hx
Cleared hypotheses: hx, this
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
x : R[X]
hx : HMul.hMul (β := R[X]) x ((taylor r : (a : R[X]) → R[X]) p : R[X]) = 0
this : x = (taylor (r - r) : (a : R[X]) → R[X]) x
rwa :
  ∀
    (hx :
      HMul.hMul (α := R[X]) (β := R[X]) ((taylor (r - r) : (a : R[X]) → R[X]) x : R[X])
          ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
        0)
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
rwa₁ :
  ∀
    (hx :
      HMul.hMul (α := R[X]) (β := R[X]) ((taylor (r + -r) : (a : R[X]) → R[X]) x : R[X])
          ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
        0)
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
rwa₂ :
  ∀
    (hx :
      HMul.hMul (α := R[X]) (β := R[X]) ((taylor r : (a : R[X]) → R[X]) ((taylor (-r) : (a : R[X]) → R[X]) x) : R[X])
          ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
        0)
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
⊢ x = 0
have rwa₃ : ∀
  (hx :
    Eq (α := R[X])
      ((taylor r : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((taylor (-r) : (a : R[X]) → R[X]) x : R[X]) p) : R[X])
      (0 : R[X]))
  (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
Tactic: rwa [this, sub_eq_add_neg, ← taylor_taylor, ← taylor_mul,
    LinearMap.map_eq_zero_iff _ (taylor_injective _), mul_right_mem_nonZeroDivisors_eq_zero_iff hp,
    LinearMap.map_eq_zero_iff _ (taylor_injective _)] at hx
Cleared hypotheses: hx, this
-- Lean 4 proof step from Mathlib.FieldTheory.Laurent (goal)
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
x : R[X]
hx : HMul.hMul (β := R[X]) x ((taylor r : (a : R[X]) → R[X]) p : R[X]) = 0
this : x = (taylor (r - r) : (a : R[X]) → R[X]) x
rwa :
  ∀
    (hx :
      HMul.hMul (α := R[X]) (β := R[X]) ((taylor (r - r) : (a : R[X]) → R[X]) x : R[X])
          ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
        0)
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
rwa₁ :
  ∀
    (hx :
      HMul.hMul (α := R[X]) (β := R[X]) ((taylor (r + -r) : (a : R[X]) → R[X]) x : R[X])
          ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
        0)
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
rwa₂ :
  ∀
    (hx :
      HMul.hMul (α := R[X]) (β := R[X]) ((taylor r : (a : R[X]) → R[X]) ((taylor (-r) : (a : R[X]) → R[X]) x) : R[X])
          ((taylor r : (a : R[X]) → R[X]) p : R[X]) =
        0)
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
rwa₃ :
  ∀
    (hx :
      Eq (α := R[X])
        ((taylor r : (a : R[X]) → R[X]) (HMul.hMul (α := R[X]) ((taylor (-r) : (a : R[X]) → R[X]) x : R[X]) p) : R[X])
        (0 : R[X]))
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
⊢ x = 0
have rwa₄ : ∀ (hx : HMul.hMul (α := R[X]) ((taylor (-r) : (a : R[X]) → R[X]) x : R[X]) p = 0)
  (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
Tactic: rwa [this, sub_eq_add_neg, ← taylor_taylor, ← taylor_mul,
    LinearMap.map_eq_zero_iff _ (taylor_injective _), mul_right_mem_nonZeroDivisors_eq_zero_iff hp,
    LinearMap.map_eq_zero_iff _ (taylor_injective _)] at hx
Cleared hypotheses: hx, this