awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v ∨ a = 0
pos : ∀ (hv : 1 = a * v), False
⊢ False
have pos₁ : ∀ (ha : FiniteMultiplicity.{u_1} (α := α) 0 0), False
Tactic: obtain hv | rfl := hv
Cleared hypotheses: a, ha, hv
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
a : α
ha : FiniteMultiplicity a a
v : α
hv : 1 = a * v
⊢ False
have this : IsUnit a
Tactic: have : IsUnit a := .of_mul_eq_one v hv.symm
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b
have hdiva : p ^ multiplicity p a ∣ a
Tactic: have hdiva : p ^ multiplicity p a ∣ a := pow_multiplicity_dvd ..
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b
have hdivb : p ^ multiplicity p b ∣ b
Tactic: have hdivb : p ^ multiplicity p b ∣ b := pow_multiplicity_dvd ..
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
⊢ p ^ (multiplicity p a + multiplicity p b) ∣ a * b
have rw : p ^ multiplicity p a * p ^ multiplicity p b ∣ a * b
Tactic: rw [pow_add]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b
have hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b
Tactic: have hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b := by
    rw [pow_add]; gcongr
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b
have hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b
Tactic: have hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b :=
    fun h =>
    not_or_intro (hfin.mul_left.not_pow_dvd_of_multiplicity_lt (lt_succ_self _))
      (hfin.mul_right.not_pow_dvd_of_multiplicity_lt (lt_succ_self _))
      (_root_.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul hp hdiva hdivb h)
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
hdiva : p ^ multiplicity p a ∣ a
hdivb : p ^ multiplicity p b ∣ b
hdiv : p ^ (multiplicity p a + multiplicity p b) ∣ a * b
hsucc : ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b
⊢ multiplicity p (a * b) = multiplicity p a + multiplicity p b
have rw : p ^ (multiplicity p a + multiplicity p b) ∣ a * b ∧ ¬p ^ (multiplicity p a + multiplicity p b + 1) ∣ a * b
Tactic: rw [hfin.multiplicity_eq_iff]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b
have pos : ∀ (hfin : FiniteMultiplicity p (a * b)), emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b
Tactic: by_cases hfin : FiniteMultiplicity p (a * b)
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
pos : ∀ (hfin : FiniteMultiplicity p (a * b)), emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b
have neg : ∀ (hfin : ¬FiniteMultiplicity p (a * b)), emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b
Tactic: by_cases hfin : FiniteMultiplicity p (a * b)
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b
have pos : (↑(multiplicity p (a * b)) : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑(multiplicity p a) : ℕ∞) (↑(multiplicity p b) : ℕ∞)
Tactic: rw [hfin.emultiplicity_eq_multiplicity, hfin.mul_left.emultiplicity_eq_multiplicity,
      hfin.mul_right.emultiplicity_eq_multiplicity]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : FiniteMultiplicity p (a * b)
⊢ (↑(multiplicity p (a * b)) : ℕ∞) = HAdd.hAdd (α := ℕ∞) (↑(multiplicity p a) : ℕ∞) (↑(multiplicity p b) : ℕ∞)
have pos : multiplicity p (a * b) = multiplicity p a + multiplicity p b
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a b : α
hp : Prime p
hfin : ¬FiniteMultiplicity p (a * b)
⊢ emultiplicity p (a * b) = emultiplicity p a + emultiplicity p b
have neg : ¬FiniteMultiplicity p a ∨ ¬FiniteMultiplicity p b
Tactic: rw [emultiplicity_eq_top.2 hfin, eq_comm, WithTop.add_eq_top, emultiplicity_eq_top,
      emultiplicity_eq_top]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
f : β → α
⊢ emultiplicity p (∏ x ∈ ∅, f x) = ∑ x ∈ ∅, emultiplicity p (f x)
have empty : emultiplicity p 1 = 0
Tactic: simp only [Finset.sum_empty, Finset.prod_empty]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
s : Finset β
f : β → α
⊢ emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)
have empty : emultiplicity p (∏ x ∈ ∅, f x) = ∑ x ∈ ∅, emultiplicity p (f x)
Tactic: induction s using Finset.induction with
  | empty =>
    simp only [Finset.sum_empty, Finset.prod_empty]
    exact emultiplicity_of_one_right hp.not_unit
  | insert a s has ih => simpa [has, ← ih] using emultiplicity_mul hp
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
s : Finset β
f : β → α
empty : emultiplicity p (∏ x ∈ ∅, f x) = ∑ x ∈ ∅, emultiplicity p (f x)
⊢ emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)
have insert : ∀ (a : β) (s : Finset β) (has : a ∉ s) (ih : emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)),
  emultiplicity p (∏ x ∈ insert a s, f x) = ∑ x ∈ insert a s, emultiplicity p (f x)
Tactic: induction s using Finset.induction with
  | empty =>
    simp only [Finset.sum_empty, Finset.prod_empty]
    exact emultiplicity_of_one_right hp.not_unit
  | insert a s has ih => simpa [has, ← ih] using emultiplicity_mul hp
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
s : Finset β
f : β → α
⊢ emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)
have empty : emultiplicity p (∏ x ∈ ∅, f x) = ∑ x ∈ ∅, emultiplicity p (f x)
Tactic: classical
  induction s using Finset.induction with
  | empty =>
    simp only [Finset.sum_empty, Finset.prod_empty]
    exact emultiplicity_of_one_right hp.not_unit
  | insert a s has ih => simpa [has, ← ih] using emultiplicity_mul hp
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
β : Type u_3
p : α
hp : Prime p
s : Finset β
f : β → α
empty : emultiplicity p (∏ x ∈ ∅, f x) = ∑ x ∈ ∅, emultiplicity p (f x)
⊢ emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)
have insert : ∀ (a : β) (s : Finset β) (has : a ∉ s) (ih : emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)),
  emultiplicity p (∏ x ∈ insert a s, f x) = ∑ x ∈ insert a s, emultiplicity p (f x)
Tactic: classical
  induction s using Finset.induction with
  | empty =>
    simp only [Finset.sum_empty, Finset.prod_empty]
    exact emultiplicity_of_one_right hp.not_unit
  | insert a s has ih => simpa [has, ← ih] using emultiplicity_mul hp
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a : α
hp : Prime p
k : ℕ
⊢ emultiplicity p (a ^ k) = (↑k : ℕ∞) * emultiplicity p a
have zero : emultiplicity p (HPow.hPow (β := ℕ) a 0) = (↑0 : ℕ∞) * emultiplicity p a
Tactic: induction k with
  | zero => simp [emultiplicity_of_one_right hp.not_unit]
  | succ k hk => simp [pow_succ, emultiplicity_mul hp, hk, add_mul]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a : α
hp : Prime p
k : ℕ
zero : emultiplicity p (HPow.hPow (β := ℕ) a 0) = (↑0 : ℕ∞) * emultiplicity p a
⊢ emultiplicity p (a ^ k) = (↑k : ℕ∞) * emultiplicity p a
have succ : ∀ (k : ℕ) (hk : emultiplicity p (a ^ k) = (↑k : ℕ∞) * emultiplicity p a),
  emultiplicity p (a ^ (k + 1)) = (↑(k + 1) : ℕ∞) * emultiplicity p a
Tactic: induction k with
  | zero => simp [emultiplicity_of_one_right hp.not_unit]
  | succ k hk => simp [pow_succ, emultiplicity_mul hp, hk, add_mul]
Cleared hypotheses: k
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ emultiplicity p (p ^ n) = (↑n : ℕ∞)
have hk : p ^ n ∣ p ^ n
Tactic: apply emultiplicity_eq_of_dvd_of_not_dvd
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
hk : p ^ n ∣ p ^ n
⊢ emultiplicity p (p ^ n) = (↑n : ℕ∞)
have hsucc : ¬p ^ (n + 1) ∣ p ^ n
Tactic: apply emultiplicity_eq_of_dvd_of_not_dvd
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ ¬p ^ (n + 1) ∣ p ^ n
have hsucc : ¬n + 1 ≤ n
Tactic: rw [pow_dvd_pow_iff h0 hu]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
⊢ multiplicity p a = 0
have h : ¬0 < multiplicity p a
Tactic: apply Nat.eq_zero_of_not_pos
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
⊢ False
have da : p ∣ a
Tactic: have da : p ∣ a := by simpa [multiplicity_eq_zero] using nh.ne.symm
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
⊢ False
have db : p ∣ b
Tactic: have db : p ∣ b := by simpa [multiplicity_eq_zero] using (nh.trans_le hle).ne.symm
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
db : p ∣ b
⊢ False
have this : p ∣ a.gcd b
Tactic: have := Nat.dvd_gcd da db
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (hypothesis)
Goal:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
da : p ∣ a
db : p ∣ b
this : p ∣ a.gcd b
⊢ False
have this₁ : p = 1
Tactic: rw [Coprime.gcd_eq_one hab, Nat.dvd_one] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
a b : ℤ
⊢ FiniteMultiplicity a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0
have rw : FiniteMultiplicity a.natAbs b.natAbs ↔ a.natAbs ≠ 1 ∧ b ≠ 0
Tactic: rw [finiteMultiplicity_iff_finiteMultiplicity_natAbs, Nat.finiteMultiplicity_iff,
    pos_iff_ne_zero, Int.natAbs_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
a b : ℤ
rw : FiniteMultiplicity a.natAbs b.natAbs ↔ a.natAbs ≠ 1 ∧ b ≠ 0
⊢ FiniteMultiplicity a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0
have rw₁ : a.natAbs ≠ 1 ∧ 0 < b.natAbs ↔ a.natAbs ≠ 1 ∧ b ≠ 0
Tactic: rw [finiteMultiplicity_iff_finiteMultiplicity_natAbs, Nat.finiteMultiplicity_iff,
    pos_iff_ne_zero, Int.natAbs_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
a b : ℤ
rw : FiniteMultiplicity a.natAbs b.natAbs ↔ a.natAbs ≠ 1 ∧ b ≠ 0
rw₁ : a.natAbs ≠ 1 ∧ 0 < b.natAbs ↔ a.natAbs ≠ 1 ∧ b ≠ 0
⊢ FiniteMultiplicity a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0
have rw₂ : a.natAbs ≠ 1 ∧ b.natAbs ≠ 0 ↔ a.natAbs ≠ 1 ∧ b ≠ 0
Tactic: rw [finiteMultiplicity_iff_finiteMultiplicity_natAbs, Nat.finiteMultiplicity_iff,
    pos_iff_ne_zero, Int.natAbs_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.Multiplicity (goal)
Goal:
a b : ℤ
rw : FiniteMultiplicity a.natAbs b.natAbs ↔ a.natAbs ≠ 1 ∧ b ≠ 0
rw₁ : a.natAbs ≠ 1 ∧ 0 < b.natAbs ↔ a.natAbs ≠ 1 ∧ b ≠ 0
rw₂ : a.natAbs ≠ 1 ∧ b.natAbs ≠ 0 ↔ a.natAbs ≠ 1 ∧ b ≠ 0
⊢ FiniteMultiplicity a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0
have rw₃ : a.natAbs ≠ 1 ∧ b ≠ 0 ↔ a.natAbs ≠ 1 ∧ b ≠ 0
Tactic: rw [finiteMultiplicity_iff_finiteMultiplicity_natAbs, Nat.finiteMultiplicity_iff,
    pos_iff_ne_zero, Int.natAbs_ne_zero]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m : ℕ
inst_1 : CharP R p
n : ℕ
⊢ Eq (α := MvPolynomial σ R) (↑n : MvPolynomial σ R) 0 ↔ p ∣ n
have rw : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑n : R)) 0 ↔ p ∣ n
Tactic: rw [← C_eq_coe_nat, ← C_0, C_inj, CharP.cast_eq_zero_iff R p]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m : ℕ
inst_1 : CharP R p
n : ℕ
rw : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑n : R)) 0 ↔ p ∣ n
⊢ Eq (α := MvPolynomial σ R) (↑n : MvPolynomial σ R) 0 ↔ p ∣ n
have rw₁ : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑n : R)) ((C : (a : R) → MvPolynomial σ R) 0) ↔ p ∣ n
Tactic: rw [← C_eq_coe_nat, ← C_0, C_inj, CharP.cast_eq_zero_iff R p]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m : ℕ
inst_1 : CharP R p
n : ℕ
rw : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑n : R)) 0 ↔ p ∣ n
rw₁ :
  Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑n : R)) ((C : (a : R) → MvPolynomial σ R) 0) ↔ p ∣ n
⊢ Eq (α := MvPolynomial σ R) (↑n : MvPolynomial σ R) 0 ↔ p ∣ n
have rw₂ : Eq.{v + 1} (α := R) (↑n : R) 0 ↔ p ∣ n
Tactic: rw [← C_eq_coe_nat, ← C_0, C_inj, CharP.cast_eq_zero_iff R p]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m : ℕ
inst_1 : CharP R p
n : ℕ
rw : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑n : R)) 0 ↔ p ∣ n
rw₁ :
  Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑n : R)) ((C : (a : R) → MvPolynomial σ R) 0) ↔ p ∣ n
rw₂ : Eq.{v + 1} (α := R) (↑n : R) 0 ↔ p ∣ n
⊢ Eq (α := MvPolynomial σ R) (↑n : MvPolynomial σ R) 0 ↔ p ∣ n
have rw₃ : p ∣ n ↔ p ∣ n
Tactic: rw [← C_eq_coe_nat, ← C_0, C_inj, CharP.cast_eq_zero_iff R p]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m : ℕ
inst_1 : CharZero R
x y : ℕ
hxy : Eq (α := MvPolynomial σ R) (↑x : MvPolynomial σ R) (↑y : MvPolynomial σ R)
⊢ x = y
have rwa : ∀ (hxy : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑x : R)) (↑y : MvPolynomial σ R)), x = y
Tactic: rwa [← C_eq_coe_nat, ← C_eq_coe_nat, C_inj, Nat.cast_inj] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m : ℕ
inst_1 : CharZero R
x y : ℕ
hxy : Eq (α := MvPolynomial σ R) (↑x : MvPolynomial σ R) (↑y : MvPolynomial σ R)
rwa : ∀ (hxy : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑x : R)) (↑y : MvPolynomial σ R)), x = y
⊢ x = y
have rwa₁ : ∀
  (hxy :
    Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑x : R)) ((C : (a : R) → MvPolynomial σ R) (↑y : R))),
  x = y
Tactic: rwa [← C_eq_coe_nat, ← C_eq_coe_nat, C_inj, Nat.cast_inj] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m : ℕ
inst_1 : CharZero R
x y : ℕ
hxy : Eq (α := MvPolynomial σ R) (↑x : MvPolynomial σ R) (↑y : MvPolynomial σ R)
rwa : ∀ (hxy : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑x : R)) (↑y : MvPolynomial σ R)), x = y
rwa₁ :
  ∀
    (hxy :
      Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑x : R))
        ((C : (a : R) → MvPolynomial σ R) (↑y : R))),
    x = y
⊢ x = y
have rwa₂ : ∀ (hxy : Eq.{v + 1} (α := R) (↑x : R) (↑y : R)), x = y
Tactic: rwa [← C_eq_coe_nat, ← C_eq_coe_nat, C_inj, Nat.cast_inj] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m : ℕ
inst_1 : CharZero R
x y : ℕ
hxy : Eq (α := MvPolynomial σ R) (↑x : MvPolynomial σ R) (↑y : MvPolynomial σ R)
rwa : ∀ (hxy : Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑x : R)) (↑y : MvPolynomial σ R)), x = y
rwa₁ :
  ∀
    (hxy :
      Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) (↑x : R))
        ((C : (a : R) → MvPolynomial σ R) (↑y : R))),
    x = y
rwa₂ : ∀ (hxy : Eq.{v + 1} (α := R) (↑x : R) (↑y : R)), x = y
⊢ x = y
have rwa₃ : ∀ (hxy : x = y), x = y
Tactic: rwa [← C_eq_coe_nat, ← C_eq_coe_nat, C_inj, Nat.cast_inj] at hxy
Cleared hypotheses: hxy
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m : ℕ
inst_1 : ExpChar R p
⊢ ExpChar (MvPolynomial σ R) p
have zero : ∀ [CharZero R], ExpChar (MvPolynomial σ R) 1
Tactic: cases ‹ExpChar R p›
Cleared hypotheses: p, inst_1
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m : ℕ
inst_1 : ExpChar R p
zero : ∀ [CharZero R], ExpChar (MvPolynomial σ R) 1
⊢ ExpChar (MvPolynomial σ R) p
have prime : Nat.Prime p → ∀ [CharP R p], ExpChar (MvPolynomial σ R) p
Tactic: cases ‹ExpChar R p›
Cleared hypotheses: inst_1
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ Finsupp.mapRange (⇑f : (a : R) → S) ⋯ p = (map f : (a : MvPolynomial σ R) → MvPolynomial σ S) p
have rw : Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S)
  (∑ x ∈ p.support, Finsupp.mapRange (⇑f : (a : R) → S) sorry ((monomial x : (a : R) → MvPolynomial σ R) (coeff x p)))
  (∑ x ∈ p.support,
    (map f : (a : MvPolynomial σ R) → MvPolynomial σ S) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x p)))
Tactic: rw [p.as_sum, Finsupp.mapRange_finsetSum, map_sum (map f)]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
⊢ Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S)
    (∑ x ∈ p.support, Finsupp.mapRange (⇑f : (a : R) → S) ⋯ ((monomial x : (a : R) → MvPolynomial σ R) (coeff x p)))
    (∑ x ∈ p.support,
      (map f : (a : MvPolynomial σ R) → MvPolynomial σ S) ((monomial x : (a : R) → MvPolynomial σ R) (coeff x p)))
have refine : ∀ n ∈ p.support,
  Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S)
    (Finsupp.mapRange (⇑f : (a : R) → S) sorry ((monomial n : (a : R) → MvPolynomial σ R) (coeff n p)))
    ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) ((monomial n : (a : R) → MvPolynomial σ R) (coeff n p)))
Tactic: refine Finset.sum_congr rfl fun n _ => ?_
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
n : σ →₀ ℕ
h : n ∈ p.support
⊢ Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S)
    (Finsupp.mapRange (⇑f : (a : R) → S) ⋯ ((monomial n : (a : R) → MvPolynomial σ R) (coeff n p)))
    ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) ((monomial n : (a : R) → MvPolynomial σ R) (coeff n p)))
have rw : Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S)
  (Finsupp.mapRange (⇑f : (a : R) → S) sorry ((monomial n : (a : R) → MvPolynomial σ R) (coeff n p)))
  ((monomial n : (a : S) → MvPolynomial σ S) ((f : (a : R) → S) (coeff n p)))
Tactic: rw [map_monomial, ← single_eq_monomial, Finsupp.mapRange_single, single_eq_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
n : σ →₀ ℕ
h : n ∈ p.support
rw :
  Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S)
    (Finsupp.mapRange (⇑f : (a : R) → S) ⋯ ((monomial n : (a : R) → MvPolynomial σ R) (coeff n p)))
    ((monomial n : (a : S) → MvPolynomial σ S) ((f : (a : R) → S) (coeff n p)))
⊢ Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S)
    (Finsupp.mapRange (⇑f : (a : R) → S) ⋯ ((monomial n : (a : R) → MvPolynomial σ R) (coeff n p)))
    ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) ((monomial n : (a : R) → MvPolynomial σ R) (coeff n p)))
have rw₁ : Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S) (Finsupp.mapRange (⇑f : (a : R) → S) sorry (Finsupp.single n (coeff n p)))
  ((monomial n : (a : S) → MvPolynomial σ S) ((f : (a : R) → S) (coeff n p)))
Tactic: rw [map_monomial, ← single_eq_monomial, Finsupp.mapRange_single, single_eq_monomial]
-- Lean 4 proof step from Mathlib.RingTheory.MvPolynomial.Basic (goal)
Goal:
σ : Type u
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
n : σ →₀ ℕ
h : n ∈ p.support
rw :
  Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S)
    (Finsupp.mapRange (⇑f : (a : R) → S) ⋯ ((monomial n : (a : R) → MvPolynomial σ R) (coeff n p)))
    ((monomial n : (a : S) → MvPolynomial σ S) ((f : (a : R) → S) (coeff n p)))
rw₁ :
  Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S) (Finsupp.mapRange (⇑f : (a : R) → S) ⋯ (Finsupp.single n (coeff n p)))
    ((monomial n : (a : S) → MvPolynomial σ S) ((f : (a : R) → S) (coeff n p)))
⊢ Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S)
    (Finsupp.mapRange (⇑f : (a : R) → S) ⋯ ((monomial n : (a : R) → MvPolynomial σ R) (coeff n p)))
    ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S) ((monomial n : (a : R) → MvPolynomial σ R) (coeff n p)))
have rw₂ : Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S) (Finsupp.single n ((f : (a : R) → S) (coeff n p)) : Finsupp.{u, u_2} (σ →₀ ℕ) S)
  ((monomial n : (a : S) → MvPolynomial σ S) ((f : (a : R) → S) (coeff n p)) : MvPolynomial σ S)
Tactic: rw [map_monomial, ← single_eq_monomial, Finsupp.mapRange_single, single_eq_monomial]