awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
⊢ 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
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
⊢ (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

Premises used: Polynomial.degree
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
⊢ 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

Premises used: Iff.mpr, Nat.pos_iff_ne_zero, Function.Injective.eq_iff, map_pow, Polynomial.degree_X_pow_sub_C, pow_mul, And.right, Iff.mp, mul_comm, add_zero, Nat.cast_injective, mul_ne_zero_iff, Polynomial.degree_mul
-- Module: Mathlib.FieldTheory.KummerPolynomial
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 : m * k = k
⊢ False

Tactic:
hm' ((mul_eq_right₀ (mul_ne_zero_iff.mp hn).2).mp hq)

Premises used: mul_eq_right₀, And.right, Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.FieldTheory.KummerPolynomial
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 : m * k = k
⊢ False

Tactic:
exact hm' ((mul_eq_right₀ (mul_ne_zero_iff.mp hn).2).mp hq)

Premises used: mul_eq_right₀, And.right, Iff.mp, mul_ne_zero_iff
-- Module: Mathlib.FieldTheory.KummerPolynomial
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
rw : ¬p = 0
⊢ ¬IsUnit (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))

Tactic:
rw [Polynomial.isUnit_iff_degree_eq_zero, degree_X_pow_sub_C hp.pos, Nat.cast_eq_zero]

Premises used: Nat.Prime.pos, Polynomial.degree_X_pow_sub_C, Nat.cast_eq_zero, Polynomial.isUnit_iff_degree_eq_zero
-- Module: Mathlib.FieldTheory.KummerPolynomial
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ ¬p = 0

Tactic:
hp.ne_zero

Premises used: Nat.Prime.ne_zero
-- Module: Mathlib.FieldTheory.KummerPolynomial
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
ha : ∀ (b : K), b ^ p ≠ a
⊢ ¬p = 0

Tactic:
exact hp.ne_zero

Premises used: Nat.Prime.ne_zero
-- Module: Mathlib.FieldTheory.KummerPolynomial
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]))

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
-- Module: Mathlib.FieldTheory.KummerPolynomial
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]))
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]))
⊢ 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)
-- Module: Mathlib.FieldTheory.KummerPolynomial
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])
suffices : g.natDegree = p
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X]))

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
-- Module: Mathlib.FieldTheory.KummerPolynomial
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])
by_contra : ∀ (h : ¬g.natDegree = p), False
⊢ g.natDegree = p

Tactic:
by_contra h
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
⊢ 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)
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
⊢ 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

Premises used: sub_eq_zero, Polynomial.eval₂_sub, Polynomial.eval₂_pow, Polynomial.eval₂_X, Polynomial.eval₂_C
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
rw₅ rw₆ : a ^ g.natDegree = a ^ g.natDegree
⊢ HPow.hPow (α := K) ((Algebra.norm K : (a : AdjoinRoot g) → K) (root g) : K) 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]

Premises used: PowerBasis.finrank, AdjoinRoot.algebraMap_eq, map_pow, AdjoinRoot.powerBasis_dim, Irreducible.ne_zero, Algebra.norm_algebraMap, AdjoinRoot.powerBasis
-- Module: Mathlib.FieldTheory.KummerPolynomial
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

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]
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
⊢ 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)))
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
key : HPow.hPow (α := K) ((Algebra.norm K : (a : AdjoinRoot g) → K) (root g) : K) p = a ^ g.natDegree
this : p.Coprime g.natDegree
⊢ False

Tactic:
ha _ ((pow_mem_range_pow_of_coprime this.symm a).mp ⟨_, key⟩).choose_spec

Premises used: Nat.Coprime.symm, Exists.choose_spec, Exists.intro, Iff.mp, pow_mem_range_pow_of_coprime
-- Module: Mathlib.FieldTheory.KummerPolynomial
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
key : HPow.hPow (α := K) ((Algebra.norm K : (a : AdjoinRoot g) → K) (root g) : K) p = a ^ g.natDegree
this : p.Coprime g.natDegree
⊢ False

Tactic:
exact ha _ ((pow_mem_range_pow_of_coprime this.symm a).mp ⟨_, key⟩).choose_spec

Premises used: Nat.Coprime.symm, Exists.choose_spec, Exists.intro, Iff.mp, pow_mem_range_pow_of_coprime
-- Module: Mathlib.FieldTheory.KummerPolynomial
Goal:
K : Type u
inst : Field K
p : ℕ
hp : Nat.Prime p
a : K
⊢ Irreducible (HSub.hSub (β := K[X]) (HPow.hPow (α := K[X]) X p) ((C : (a : K) → K[X]) a : K[X])) ↔ ∀ (b : K), b ^ p ≠ a

Tactic:
⟨(pow_ne_of_irreducible_X_pow_sub_C · dvd_rfl hp.ne_one), X_pow_sub_C_irreducible_of_prime hp⟩

Premises used: X_pow_sub_C_irreducible_of_prime, Nat.Prime.ne_one, Iff.intro, dvd_rfl, pow_ne_of_irreducible_X_pow_sub_C
-- Module: Mathlib.FieldTheory.Laurent
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
hp : Membership.mem (γ := Submonoid R[X]) R[X]⁰ p
rw : ∀ (x : R[X]), HMul.hMul (β := R[X]) x ((taylor r : (a : R[X]) → R[X]) p : R[X]) = 0 → x = 0
⊢ Membership.mem (α := R[X]) (γ := Submonoid R[X]) R[X]⁰ ((taylor r : (a : R[X]) → R[X]) p : R[X])

Tactic:
rw [mem_nonZeroDivisors_iff_right]

Premises used: mem_nonZeroDivisors_iff_right
-- Module: Mathlib.FieldTheory.Laurent
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 = (taylor (r - r) : (a : R[X]) → R[X]) x

Tactic:
simp
-- Module: Mathlib.FieldTheory.Laurent
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 = (taylor (r - r) : (a : R[X]) → R[X]) x

Tactic:
have : x = taylor (r - r) x := by simp
-- Module: Mathlib.FieldTheory.Laurent
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
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
rwa₅ :
  ∀ (hx : Eq (α := R[X]) ((taylor (-r) : (a : R[X]) → R[X]) x : R[X]) (0 : R[X]))
    (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
rwa₆ rwa₇ rwa₈ rwa₉ : ∀ (hx : x = 0) (this : x = (taylor (r - r) : (a : R[X]) → R[X]) x), x = 0
⊢ 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

Premises used: mul_right_mem_nonZeroDivisors_eq_zero_iff, Polynomial.taylor_mul, Polynomial.taylor_injective, sub_eq_add_neg, Polynomial.taylor_taylor, LinearMap.map_eq_zero_iff
-- Module: Mathlib.FieldTheory.Laurent
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
q : ↥R[X]⁰
⊢ Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) { toFractionRing := Localization.mk p q } : R⟮X⟯)
    ({
        toFractionRing :=
          Localization.mk ((taylor r : (a : R[X]) → R[X]) p)
            (Subtype.mk (p := fun (x : R[X]) ↦ Membership.mem (γ := Submonoid R[X]) R[X]⁰ x)
              ((taylor r : (a : R[X]) → R[X]) (↑q : R[X])) ⋯) } :
      R⟮X⟯)

Tactic:
map_apply_ofFractionRing_mk _ _ _ _

Premises used: RatFunc.map_apply_ofFractionRing_mk, Polynomial.comp
-- Module: Mathlib.FieldTheory.Laurent
Goal:
R : Type u
inst : CommRing R
r : R
p q : R[X]
inst_1 : IsDomain R
⊢ LE.le (α := Submonoid R[X]) R[X]⁰
    (Submonoid.comap (F := R[X] →+* R[X])
      { toFun := (⇑(taylor r) : (a : R[X]) → R[X]), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } R[X]⁰)

Tactic:
taylor_mem_nonZeroDivisors r

Premises used: Set.Mem, setOf, Set.inter, Set.preimage, RatFunc.taylor_mem_nonZeroDivisors, Polynomial.comp
-- Module: Mathlib.FieldTheory.Laurent
Goal:
R : Type u
inst : CommRing R
r : R
p q : R[X]
inst_1 : IsDomain R
⊢ LE.le (α := Submonoid R[X]) R[X]⁰
    (Submonoid.comap (F := R[X] →+* R[X])
      { toFun := (⇑(taylor r) : (a : R[X]) → R[X]), map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ } R[X]⁰)

Tactic:
exact taylor_mem_nonZeroDivisors r

Premises used: RatFunc.taylor_mem_nonZeroDivisors
-- Module: Mathlib.FieldTheory.Laurent
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
inst_1 : IsDomain R
rw :
  Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) (RatFunc.mk p 1) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
rw₁ :
  Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) (RatFunc.mk p 1) : R⟮X⟯)
    (RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1 : R⟮X⟯)
rw₂ :
  Eq (α := R⟮X⟯)
    ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯)
        (HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p : R⟮X⟯)
          ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)) :
      R⟮X⟯)
    (RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1 : R⟮X⟯)
rw₃ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) 1) : R⟮X⟯) =
    RatFunc.mk ((taylor r : (a : R[X]) → R[X]) p) 1
rw₄ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) 1) : R⟮X⟯) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)
rw₅ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) 1) : R⟮X⟯) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)
rw₆ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) 1 : R⟮X⟯)
rw₇ rw₈ :
  HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯) (1 : R⟮X⟯) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯) (1 : R⟮X⟯)
⊢ Eq (α := R⟮X⟯) ((laurentAux r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)

Tactic:
rw [← mk_one, ← mk_one, mk_eq_div, laurentAux_div, mk_eq_div, taylor_one, map_one, map_one]

Premises used: RatFunc.laurentAux_div, RatFunc.mk_eq_div, map_one, RatFunc.mk_one, Polynomial.taylor_one
-- Module: Mathlib.FieldTheory.Laurent
Goal:
R : Type u
inst : CommRing R
r : R
p q : R[X]
inst_1 : IsDomain R
⊢ (laurent r : (a : R⟮X⟯) → R⟮X⟯)
      (HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p : R⟮X⟯)
        ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) q : R⟮X⟯)) =
    HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) q) : R⟮X⟯)

Tactic:
laurentAux_div r p q

Premises used: Set.Mem, RatFunc.laurentAux_div
-- Module: Mathlib.FieldTheory.Laurent
Goal:
R : Type u
inst : CommRing R
r : R
p : R[X]
inst_1 : IsDomain R
⊢ Eq (α := R⟮X⟯) ((laurent r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) p) : R⟮X⟯)

Tactic:
laurentAux_algebraMap _ _

Premises used: Set.Mem, RatFunc.laurentAux_algebraMap
-- Module: Mathlib.FieldTheory.Laurent
Goal:
R : Type u
inst : CommRing R
r : R
inst_1 : IsDomain R
rw :
  (laurent r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X) =
    HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
rw₁ :
  (algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) Polynomial.X) =
    HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
rw₂ :
  (algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯)
      (HAdd.hAdd (α := R[X]) (β := R[X]) Polynomial.X ((Polynomial.C : (a : R) → R[X]) r : R[X])) =
    HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
rw₃ :
  HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) r) : R⟮X⟯) =
    HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
rw₄ rw₅ :
  HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((C : (a : R) → R⟮X⟯) r : R⟮X⟯) =
    HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) Polynomial.X : R⟮X⟯)
      ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)
⊢ (laurent r : (a : R⟮X⟯) → R⟮X⟯) X = HAdd.hAdd (α := R⟮X⟯) (β := R⟮X⟯) X ((C : (a : R) → R⟮X⟯) r : R⟮X⟯)

Tactic:
rw [← algebraMap_X, laurent_algebraMap, taylor_X, map_add, algebraMap_C]

Premises used: RatFunc.laurent_algebraMap, map_add, RatFunc.algebraMap_X, RatFunc.algebraMap_C, Polynomial.taylor_X
-- Module: Mathlib.FieldTheory.Laurent
Goal:
R : Type u
inst : CommRing R
r : R
inst_1 : IsDomain R
x : R
rw :
  Eq (α := R⟮X⟯)
    ((laurent r : (a : R⟮X⟯) → R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) x)) :
      R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) x) : R⟮X⟯)
rw₁ :
  Eq (α := R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((taylor r : (a : R[X]) → R[X]) ((Polynomial.C : (a : R) → R[X]) x)) :
      R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) x) : R⟮X⟯)
rw₂ rw₃ :
  Eq (α := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) x) : R⟮X⟯)
    ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) ((Polynomial.C : (a : R) → R[X]) x) : R⟮X⟯)
⊢ Eq (α := R⟮X⟯) ((laurent r : (a : R⟮X⟯) → R⟮X⟯) ((C : (a : R) → R⟮X⟯) x) : R⟮X⟯) ((C : (a : R) → R⟮X⟯) x : R⟮X⟯)

Tactic:
rw [← algebraMap_C, laurent_algebraMap, taylor_C]

Premises used: RatFunc.laurent_algebraMap, RatFunc.algebraMap_C, Polynomial.taylor_C
-- Module: Mathlib.FieldTheory.Laurent
Goal:
R : Type u
inst : CommRing R
f : R⟮X⟯
inst_1 : IsDomain R
f₁ :
  ∀ (p q : R[X]),
    q ≠ 0 →
      (laurent 0 : (a : R⟮X⟯) → R⟮X⟯)
          (HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p : R⟮X⟯)
            ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) q : R⟮X⟯)) =
        HDiv.hDiv (α := R⟮X⟯) (β := R⟮X⟯) ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) p : R⟮X⟯)
          ((algebraMap R[X] R⟮X⟯ : (a : R[X]) → R⟮X⟯) q : R⟮X⟯)
⊢ (laurent 0 : (a : R⟮X⟯) → R⟮X⟯) f = f

Tactic:
induction f using RatFunc.induction_on

Premises used: RatFunc.induction_on