awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
zero : ∀ [CharZero R] [ExpChar R 1], (expand R 1 : (a : R[X]) → R[X]) (contract 1 f) = f
prime : ∀ (hprime : Nat.Prime p) [hchar : CharP R p], (expand R p : (a : R[X]) → R[X]) (contract p f) = f
⊢ (expand R p : (a : R[X]) → R[X]) (contract p f) = f

Tactic:
obtain _ | @⟨_, hprime, hchar⟩ := ‹ExpChar R p›

Premises used: ExpChar
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
inst_1 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
inst_2 : CharZero R
inst_3 : ExpChar R 1
zero : contract 1 f = f
zero₁ zero₂ : f = f
⊢ (expand R 1 : (a : R[X]) → R[X]) (contract 1 f) = f

Tactic:
rw [expand_one, contract_one]

Premises used: Polynomial.expand_one, Polynomial.contract_one
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hprime : Nat.Prime p
hchar : CharP R p
⊢ Fact (CharP R p)

Tactic:
haveI := Fact.mk hchar
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hprime : Nat.Prime p
hchar : CharP R p
this : Fact (CharP R p)
⊢ (expand R p : (a : R[X]) → R[X]) (contract p f) = f

Tactic:
expand_contract p hf hprime.ne_zero

Premises used: Polynomial.expand_contract, Nat.Prime.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
inst_2 : NoZeroDivisors R
f : R[X]
hf : Eq (α := R[X]) ((derivative : (a : R[X]) → R[X]) f : R[X]) (0 : R[X])
hprime : Nat.Prime p
hchar : CharP R p
this : Fact (CharP R p)
⊢ (expand R p : (a : R[X]) → R[X]) (contract p f) = f

Tactic:
exact expand_contract p hf hprime.ne_zero

Premises used: Polynomial.expand_contract, Nat.Prime.ne_zero
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
⊢ map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) f) = f ^ p

Tactic:
f.induction_on' (fun a b ha hb => ?_) fun n a => ?_

Premises used: Polynomial.induction_on'
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
refine_1 :
  ∀ (a b : R[X]) (ha : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) a) = a ^ p)
    (hb : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b) = b ^ p),
    map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) (a + b)) = (a + b) ^ p
refine_2 :
  ∀ (n : ℕ) (a : R),
    map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) a)) =
      HPow.hPow (α := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) p
⊢ map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) f) = f ^ p

Tactic:
refine f.induction_on' (fun a b ha hb => ?_) fun n a => ?_
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f a b : R[X]
ha : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) a) = a ^ p
hb : map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b) = b ^ p
refine_1 :
  map (frobenius R p)
      (HAdd.hAdd (α := R[X]) (β := R[X]) ((expand R p : (a : R[X]) → R[X]) a : R[X])
        ((expand R p : (a : R[X]) → R[X]) b : R[X])) =
    (a + b) ^ p
refine_1₁ :
  HAdd.hAdd (α := R[X]) (map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) a))
      (map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b)) =
    (a + b) ^ p
refine_1₂ : a ^ p + map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) b) = (a + b) ^ p
refine_1₃ : a ^ p + b ^ p = (a + b) ^ p
refine_1₄ refine_1₅ : a ^ p + b ^ p = a ^ p + b ^ p
⊢ map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) (a + b)) = (a + b) ^ p

Tactic:
rw [map_add, Polynomial.map_add, ha, hb, add_pow_expChar]

Premises used: Polynomial.map_add, map_add, add_pow_expChar
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
n : ℕ
a : R
refine_2 :
  HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a ^ p) : R[X]) (HPow.hPow (α := R[X]) X (n * p)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a ^ p) : R[X]) (HPow.hPow (α := R[X]) X n ^ p)
⊢ map (frobenius R p) ((expand R p : (a : R[X]) → R[X]) ((monomial n : (a : R) → R[X]) a)) =
    HPow.hPow (α := R[X]) ((monomial n : (a : R) → R[X]) a : R[X]) p

Tactic:
rw [expand_monomial, map_monomial, ← C_mul_X_pow_eq_monomial, ← C_mul_X_pow_eq_monomial,
      mul_pow, ← C.map_pow, frobenius_def]

Premises used: Polynomial.C, Polynomial.map_monomial, Polynomial.C_mul_X_pow_eq_monomial, Polynomial.expand_monomial, frobenius_def, mul_pow, RingHom.map_pow
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
n : ℕ
a : R
⊢ HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a ^ p) : R[X]) (HPow.hPow (α := R[X]) X (n * p)) =
    HMul.hMul (α := R[X]) ((C : (a : R) → R[X]) (a ^ p) : R[X]) (HPow.hPow (α := R[X]) X n ^ p)

Tactic:
ring
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
⊢ map (iterateFrobenius R p 0) ((expand R (HPow.hPow (β := ℕ) p 0) : (a : R[X]) → R[X]) f) = f ^ HPow.hPow (β := ℕ) p 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f) = f ^ p ^ k
succ : f ^ p ^ (k + 1) = map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f)
⊢ map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f) = f ^ p ^ (k + 1)

Tactic:
symm
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f) = f ^ p ^ k
rw : HPow.hPow (α := R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f)) p
| f ^ p ^ (k + 1)

Tactic:
rw [pow_succ, pow_mul, ← n_ih]

Premises used: pow_succ, pow_mul
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f) = f ^ p ^ k
succ :
  HPow.hPow (α := R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f)) p =
    map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f)
⊢ f ^ p ^ (k + 1) = map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f)

Tactic:
conv_lhs => rw [pow_succ, pow_mul, ← n_ih]

Premises used: pow_succ, pow_mul
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
k : ℕ
n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f) = f ^ p ^ k
succ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f))
succ₁ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (k + 1)) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
succ₂ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p (1 + k)) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
succ₃ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (RingHom.comp (iterateFrobenius R p 1) (iterateFrobenius R p k))
      ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f))
succ₄ :
  Eq (α := R[X])
    (map (frobenius R p)
      ((expand R p : (a : R[X]) → R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p 1) (map (iterateFrobenius R p k) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f)))
succ₅ :
  Eq (α := R[X])
    (map (frobenius R p)
      (map (iterateFrobenius R p k) ((expand R p : (a : R[X]) → R[X]) ((expand R (p ^ k) : (a : R[X]) → R[X]) f))))
    (map (iterateFrobenius R p 1) (map (iterateFrobenius R p k) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f)))
succ₆ :
  Eq (α := R[X]) (map (frobenius R p) (map (iterateFrobenius R p k) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f)))
    (map (iterateFrobenius R p 1) (map (iterateFrobenius R p k) ((expand R (p * p ^ k) : (a : R[X]) → R[X]) f)))
⊢ HPow.hPow (α := R[X]) (map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f)) p =
    map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f)

Tactic:
simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]

Premises used: Polynomial.map_expand, add_comm, iterateFrobenius_add, Polynomial.expand_mul, iterateFrobenius_one, Polynomial.map_frobenius_expand, Polynomial.map_map, pow_succ'
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommSemiring R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
n : ℕ
zero :
  map (iterateFrobenius R p 0) ((expand R (HPow.hPow (β := ℕ) p 0) : (a : R[X]) → R[X]) f) = f ^ HPow.hPow (β := ℕ) p 0
succ :
  ∀ (k : ℕ) (n_ih : map (iterateFrobenius R p k) ((expand R (p ^ k) : (a : R[X]) → R[X]) f) = f ^ p ^ k),
    map (iterateFrobenius R p (k + 1)) ((expand R (p ^ (k + 1)) : (a : R[X]) → R[X]) f) = f ^ p ^ (k + 1)
⊢ map (iterateFrobenius R p n) ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = f ^ p ^ n

Tactic:
induction n with
  | zero => simp
  | succ k n_ih =>
    symm
    conv_lhs => rw [pow_succ, pow_mul, ← n_ih]
    simp_rw [← map_frobenius_expand p, pow_succ', add_comm k, iterateFrobenius_add,
      ← map_map, ← map_expand, ← expand_mul, iterateFrobenius_one]

Premises used: Polynomial.map_expand, pow_succ, pow_mul, iterateFrobenius_add, Polynomial.expand_mul, iterateFrobenius_one, Polynomial.map_frobenius_expand, Polynomial.map_map, pow_succ'
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
p n : ℕ
inst_1 : ExpChar R p
f : R[X]
r : R
inl : rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) 0) = p ^ n * rootMultiplicity (r ^ p ^ n) 0
inr :
  ∀ (h0 : f ≠ 0), rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
⊢ rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
obtain rfl | h0 := eq_or_ne f 0

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
p n : ℕ
inst_1 : ExpChar R p
r : R
⊢ rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) 0) = p ^ n * rootMultiplicity (r ^ p ^ n) 0

Tactic:
simp
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
p n : ℕ
inst_1 : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
inr :
  ∀ (g : R[X])
    (hg :
      f =
        HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r ^ p ^ n) : R[X]) ^ rootMultiplicity (r ^ p ^ n) f *
          g)
    (ndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r ^ p ^ n) : R[X]) ∣ g),
    rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
⊢ rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
obtain ⟨g, hg, ndvd⟩ := f.exists_eq_pow_rootMultiplicity_mul_and_not_dvd h0 (r ^ p ^ n)

Premises used: Polynomial.exists_eq_pow_rootMultiplicity_mul_and_not_dvd, HPow.hPow
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
p n : ℕ
inst_1 : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg :
  f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r ^ p ^ n) : R[X]) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r ^ p ^ n) : R[X]) ∣ g
⊢ ¬IsRoot ((expand R (p ^ n) : (a : R[X]) → R[X]) g) r

Tactic:
rw [dvd_iff_isRoot, ← eval_X (x := r), ← eval_pow, ← isRoot_comp, ← expand_eq_comp_X_pow] at ndvd

Premises used: Polynomial.eval_X, Polynomial.eval_pow, Polynomial.expand_eq_comp_X_pow, Polynomial.isRoot_comp, Polynomial.dvd_iff_isRoot
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
p n : ℕ
inst_1 : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg :
  f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r ^ p ^ n) : R[X]) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬IsRoot ((expand R (p ^ n) : (a : R[X]) → R[X]) g) r
rw : p ^ n * rootMultiplicity (r ^ p ^ n) f
| rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f)

Tactic:
rw [hg, map_mul, map_pow, map_sub, expand_X, expand_C, map_pow, ← sub_pow_expChar_pow,
    ← pow_mul, mul_comm, rootMultiplicity_mul_X_sub_C_pow (expand_ne_zero (expChar_pow_pos R p n)
      |>.mpr <| right_ne_zero_of_mul <| hg ▸ h0), rootMultiplicity_eq_zero ndvd, zero_add]

Premises used: Iff.mpr, map_sub, Polynomial.expand_C, right_ne_zero_of_mul, Polynomial.rootMultiplicity_mul_X_sub_C_pow, map_pow, zero_add, pow_mul, Polynomial.expand_X, map_mul, expChar_pow_pos, mul_comm, Polynomial.rootMultiplicity_eq_zero, Polynomial.expand_ne_zero, sub_pow_expChar_pow
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
p n : ℕ
inst_1 : ExpChar R p
f : R[X]
r : R
h0 : f ≠ 0
g : R[X]
hg :
  f = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) (r ^ p ^ n) : R[X]) ^ rootMultiplicity (r ^ p ^ n) f * g
ndvd : ¬IsRoot ((expand R (p ^ n) : (a : R[X]) → R[X]) g) r
conv_lhs : rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f
inr : p ^ n * rootMultiplicity (r ^ p ^ n) f = p ^ n * rootMultiplicity (r ^ p ^ n) f
⊢ rootMultiplicity r ((expand R (p ^ n) : (a : R[X]) → R[X]) f) = p ^ n * rootMultiplicity (r ^ p ^ n) f

Tactic:
conv_lhs => rw [hg, map_mul, map_pow, map_sub, expand_X, expand_C, map_pow, ← sub_pow_expChar_pow,
    ← pow_mul, mul_comm, rootMultiplicity_mul_X_sub_C_pow (expand_ne_zero (expChar_pow_pos R p n)
      |>.mpr <| right_ne_zero_of_mul <| hg ▸ h0), rootMultiplicity_eq_zero ndvd, zero_add]

Premises used: Iff.mpr, map_sub, Polynomial.expand_C, right_ne_zero_of_mul, Polynomial.rootMultiplicity_mul_X_sub_C_pow, map_pow, zero_add, pow_mul, Polynomial.expand_X, map_mul, expChar_pow_pos, mul_comm, Polynomial.rootMultiplicity_eq_zero, Polynomial.expand_ne_zero, sub_pow_expChar_pow
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
p : ℕ
inst_1 : ExpChar R p
f : R[X]
r : R
rw :
  rootMultiplicity r ((expand R (HPow.hPow (β := ℕ) p 1) : (a : R[X]) → R[X]) f) =
    HPow.hPow (β := ℕ) p 1 * rootMultiplicity (r ^ HPow.hPow (β := ℕ) p 1) f
rw₁ rw₂ :
  HPow.hPow (β := ℕ) p 1 * rootMultiplicity (r ^ HPow.hPow (β := ℕ) p 1) f =
    HPow.hPow (β := ℕ) p 1 * rootMultiplicity (r ^ HPow.hPow (β := ℕ) p 1) f
⊢ rootMultiplicity r ((expand R p : (a : R[X]) → R[X]) f) = p * rootMultiplicity (r ^ p) f

Tactic:
rw [← pow_one p, rootMultiplicity_expand_pow]

Premises used: Polynomial.rootMultiplicity_expand_pow, pow_one
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : 0 < p
⊢ IsLocalHom (R := R[X]) (S := R[X]) (F := R[X] →ₐ[R] R[X]) (expand R p)

Tactic:
⟨fun f hf1 => ?_⟩

Premises used: IsLocalHom.mk
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : 0 < p
refine : ∀ (f : R[X]) (hf1 : IsUnit (M := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])), IsUnit f
⊢ IsLocalHom (R := R[X]) (S := R[X]) (F := R[X] →ₐ[R] R[X]) (expand R p)

Tactic:
refine ⟨fun f hf1 => ?_⟩
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (M := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
    ((C : (a : R) → R[X]) (coeff ((expand R p : (a : R[X]) → R[X]) f) 0) : R[X])

Tactic:
have hf2 := eq_C_of_degree_eq_zero (degree_eq_zero_of_isUnit hf1)
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (M := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
hf2 :
  Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
    ((C : (a : R) → R[X]) (coeff ((expand R p : (a : R[X]) → R[X]) f) 0) : R[X])
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])

Tactic:
rw [coeff_expand hp, if_pos (dvd_zero _), p.zero_div] at hf2

Premises used: dvd_zero, Nat.zero_div, if_pos, Polynomial.coeff_expand
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (M := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
hf2 : Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
⊢ IsUnit (f.coeff 0)

Tactic:
rw [hf2, isUnit_C] at hf1

Premises used: Polynomial.isUnit_C
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (M := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
hf2 : Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
hf1₁ : IsUnit (f.coeff 0)
⊢ Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])

Tactic:
rw [hf2, isUnit_C] at hf1

Premises used: Polynomial.isUnit_C
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : Eq (α := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
⊢ f = (C : (a : R) → R[X]) (f.coeff 0)

Tactic:
rw [expand_eq_C hp] at hf2

Premises used: Polynomial.expand_eq_C
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : 0 < p
f : R[X]
hf1 : IsUnit (f.coeff 0)
hf2 : f = (C : (a : R) → R[X]) (f.coeff 0)
rwa : IsUnit (M := R[X]) ((C : (a : R) → R[X]) (f.coeff 0) : R[X])
rwa₁ rwa₂ rwa₃ rwa₄ : IsUnit (f.coeff 0)
⊢ IsUnit f

Tactic:
rwa [hf2, isUnit_C]

Premises used: Polynomial.isUnit_C
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
hf : Irreducible (M := R[X]) ((expand R p : (a : R[X]) → R[X]) f : R[X])
⊢ Irreducible f

Tactic:
let _ := isLocalHom_expand R hp.bot_lt
  hf.of_map

Premises used: Irreducible.of_map, Polynomial.isLocalHom_expand, Ne.bot_lt
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n : ℕ
hf : Irreducible (M := R[X]) ((expand R (p ^ Nat.zero) : (a : R[X]) → R[X]) f : R[X])
rwa : ∀ (hf : Irreducible (M := R[X]) ((expand R 1 : (a : R[X]) → R[X]) f : R[X])), Irreducible f
rwa₁ rwa₂ rwa₃ rwa₄ : ∀ (hf : Irreducible f), Irreducible f
⊢ Irreducible f

Tactic:
rwa [pow_zero, expand_one] at hf

Premises used: Polynomial.expand_one, pow_zero
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n_1 n : ℕ
ih : Irreducible (M := R[X]) ((expand R (p ^ n) : (a : R[X]) → R[X]) f : R[X]) → Irreducible f
hf : Irreducible (M := R[X]) ((expand R (p ^ n.succ) : (a : R[X]) → R[X]) f : R[X])
⊢ Irreducible (M := R[X]) ((expand R (p * p ^ n) : (a : R[X]) → R[X]) f : R[X])

Tactic:
rw [pow_succ'] at hf

Premises used: pow_succ'
-- Module: Mathlib.Algebra.Polynomial.Expand
Goal:
R : Type u
inst : CommRing R
inst_1 : IsDomain R
p : ℕ
hp : p ≠ 0
f : R[X]
n_1 n : ℕ
ih : Irreducible (M := R[X]) ((expand R (p ^ n) : (a : R[X]) → R[X]) f : R[X]) → Irreducible f
hf : Irreducible (M := R[X]) ((expand R (p * p ^ n) : (a : R[X]) → R[X]) f : R[X])
rwa rwa₁ rwa₂ rwa₃ : Irreducible (M := R[X]) ((expand R (p * p ^ n) : (a : R[X]) → R[X]) f : R[X])
⊢ Irreducible (M := R[X]) ((expand R p : (a : R[X]) → R[X]) ((expand R (p ^ n) : (a : R[X]) → R[X]) f) : R[X])

Tactic:
rwa [expand_expand]

Premises used: Polynomial.expand_expand
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hnezero : Ne (α := R[X]) ((derivative : (a : R[X]) → R[X]) p : R[X]) (0 : R[X])
⊢ rootMultiplicity t p - 1 ≤ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p)

Tactic:
(le_rootMultiplicity_iff hnezero).2 <|
    pow_sub_one_dvd_derivative_of_pow_dvd (p.pow_rootMultiplicity_dvd t)

Premises used: Iff.mpr, Polynomial.pow_rootMultiplicity_dvd, Polynomial.pow_sub_one_dvd_derivative_of_pow_dvd, Polynomial.le_rootMultiplicity_iff
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(rootMultiplicity t p) : R)
pos : ∀ (h : p = 0), rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
neg : ∀ (h : ¬p = 0), rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1

Tactic:
by_cases h : p = 0
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(rootMultiplicity t p) : R)
h : p = 0
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1

Tactic:
simp only [h, map_zero, rootMultiplicity_zero]

Premises used: map_zero, Polynomial.rootMultiplicity_zero
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(rootMultiplicity t p) : R)
h : ¬p = 0
neg :
  ∀ (g : R[X]) (hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p * g)
    (hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g),
    rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1

Tactic:
obtain ⟨g, hp, hndvd⟩ := p.exists_eq_pow_rootMultiplicity_mul_and_not_dvd h t

Premises used: Polynomial.exists_eq_pow_rootMultiplicity_mul_and_not_dvd
-- Module: Mathlib.Algebra.Polynomial.FieldDivision
Goal:
R : Type u
inst : CommRing R
p : R[X]
t : R
hpt : p.IsRoot t
hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑(rootMultiplicity t p) : R)
h : ¬p = 0
g : R[X]
hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ rootMultiplicity t p * g
hndvd : ¬HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ∣ g
neg :
  let m := rootMultiplicity t p;
  ∀ (hnzd : Membership.mem (γ := Submonoid R) (nonZeroDivisors R) (↑m : R))
    (hp : p = HSub.hSub (α := R[X]) (β := R[X]) X ((C : (a : R) → R[X]) t : R[X]) ^ m * g),
    rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = m - 1
⊢ rootMultiplicity t ((derivative : (a : R[X]) → R[X]) p) = rootMultiplicity t p - 1

Tactic:
set m := p.rootMultiplicity t

Premises used: Polynomial.rootMultiplicity