awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Multiplicity
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)
insert :
  ∀ (a : β) (s : Finset β) (has : a ∉ s) (ih : emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)),
    emultiplicity p (∏ x ∈ Insert.insert a s, f x) = ∑ x ∈ Insert.insert a s, emultiplicity p (f x)
⊢ emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ 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

Premises used: Finset.prod_empty, emultiplicity_of_one_right, Insert.insert, Prime.not_unit, Finset.sum_empty, emultiplicity_mul
-- Module: Mathlib.RingTheory.Multiplicity
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)
insert :
  ∀ (a : β) (s : Finset β) (has : a ∉ s) (ih : emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ s, emultiplicity p (f x)),
    emultiplicity p (∏ x ∈ Insert.insert a s, f x) = ∑ x ∈ Insert.insert a s, emultiplicity p (f x)
⊢ emultiplicity p (∏ x ∈ s, f x) = ∑ x ∈ 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

Premises used: Finset.prod_empty, emultiplicity_of_one_right, Insert.insert, Prime.not_unit, Finset.sum_empty, emultiplicity_mul
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a : α
hp : Prime p
⊢ emultiplicity p (HPow.hPow (β := ℕ) a 0) = (↑0 : ℕ∞) * emultiplicity p a

Tactic:
simp [emultiplicity_of_one_right hp.not_unit]

Premises used: emultiplicity_of_one_right, Prime.not_unit
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a : α
hp : Prime p
k : ℕ
hk : emultiplicity p (a ^ k) = (↑k : ℕ∞) * emultiplicity p a
⊢ emultiplicity p (a ^ (k + 1)) = (↑(k + 1) : ℕ∞) * emultiplicity p a

Tactic:
simp [pow_succ, emultiplicity_mul hp, hk, add_mul]

Premises used: add_mul, pow_succ, emultiplicity_mul
-- Module: Mathlib.RingTheory.Multiplicity
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
succ :
  ∀ (k : ℕ) (hk : emultiplicity p (a ^ k) = (↑k : ℕ∞) * emultiplicity p a),
    emultiplicity p (a ^ (k + 1)) = (↑(k + 1) : ℕ∞) * emultiplicity p a
⊢ emultiplicity p (a ^ k) = (↑k : ℕ∞) * 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]

Premises used: add_mul, emultiplicity_of_one_right, pow_succ, Prime.not_unit, Nat.zero, Nat.succ, emultiplicity_mul
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p a : α
hp : Prime p
ha : FiniteMultiplicity p a
k : ℕ
⊢ multiplicity p (a ^ k) = k * multiplicity p a

Tactic:
exact_mod_cast (ha.pow hp).emultiplicity_eq_multiplicity ▸
    ha.emultiplicity_eq_multiplicity ▸ emultiplicity_pow hp
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
hk : p ^ n ∣ p ^ n
hsucc : ¬p ^ (n + 1) ∣ p ^ n
⊢ emultiplicity p (p ^ n) = (↑n : ℕ∞)

Tactic:
apply emultiplicity_eq_of_dvd_of_not_dvd

Premises used: emultiplicity_eq_of_dvd_of_not_dvd
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ p ^ n ∣ p ^ n

Tactic:
rfl
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
hsucc : ¬n + 1 ≤ n
⊢ ¬p ^ (n + 1) ∣ p ^ n

Tactic:
rw [pow_dvd_pow_iff h0 hu]

Premises used: pow_dvd_pow_iff
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ ¬n + 1 ≤ n

Tactic:
apply Nat.not_succ_le_self

Premises used: Nat.not_succ_le_self
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
h0 : p ≠ 0
hu : ¬IsUnit p
n : ℕ
⊢ multiplicity p (p ^ n) = n

Tactic:
multiplicity_eq_of_emultiplicity_eq_some (emultiplicity_pow_self h0 hu n)

Premises used: emultiplicity_pow_self, multiplicity_eq_of_emultiplicity_eq_some
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
hp : Prime p
n : ℕ
⊢ emultiplicity p (p ^ n) = (↑n : ℕ∞)

Tactic:
emultiplicity_pow_self hp.ne_zero hp.not_unit n

Premises used: emultiplicity_pow_self, Prime.not_unit, Prime.ne_zero
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
p : α
hp : Prime p
n : ℕ
⊢ multiplicity p (p ^ n) = n

Tactic:
multiplicity_pow_self hp.ne_zero hp.not_unit n

Premises used: Prime.not_unit, multiplicity_pow_self, Prime.ne_zero
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
h : ¬0 < multiplicity p a
⊢ multiplicity p a = 0

Tactic:
apply Nat.eq_zero_of_not_pos

Premises used: Nat.eq_zero_of_not_pos
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
⊢ p ∣ a

Tactic:
simpa [multiplicity_eq_zero] using nh.ne.symm

Premises used: multiplicity_eq_zero, Ne.symm, LT.lt.ne
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
p a b : ℕ
hp : p ≠ 1
hle : multiplicity p a ≤ multiplicity p b
hab : a.Coprime b
nh : 0 < multiplicity p a
⊢ p ∣ a

Tactic:
have da : p ∣ a := by simpa [multiplicity_eq_zero] using nh.ne.symm
-- Module: Mathlib.RingTheory.Multiplicity
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
⊢ p ∣ b

Tactic:
simpa [multiplicity_eq_zero] using (nh.trans_le hle).ne.symm

Premises used: multiplicity_eq_zero, Ne.symm, LT.lt.trans_le, LT.lt.ne
-- Module: Mathlib.RingTheory.Multiplicity
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
⊢ p ∣ b

Tactic:
have db : p ∣ b := by simpa [multiplicity_eq_zero] using (nh.trans_le hle).ne.symm
-- Module: Mathlib.RingTheory.Multiplicity
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
⊢ p ∣ a.gcd b

Tactic:
have := Nat.dvd_gcd da db
-- Module: Mathlib.RingTheory.Multiplicity
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
⊢ p = 1

Tactic:
rw [Coprime.gcd_eq_one hab, Nat.dvd_one] at this

Premises used: Nat.dvd_one, Nat.Coprime.gcd_eq_one
-- Module: Mathlib.RingTheory.Multiplicity
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 = 1
⊢ False

Tactic:
hp this
-- Module: Mathlib.RingTheory.Multiplicity
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 = 1
⊢ False

Tactic:
exact hp this
-- Module: Mathlib.RingTheory.Multiplicity
Goal:
a b : ℤ
⊢ FiniteMultiplicity a b ↔ FiniteMultiplicity a.natAbs b.natAbs

Tactic:
simp only [FiniteMultiplicity.def, ← Int.natAbs_dvd_natAbs, Int.natAbs_pow]

Premises used: Int.natAbs_pow, Int.natAbs_dvd_natAbs, FiniteMultiplicity.def
-- Module: Mathlib.RingTheory.Multiplicity
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
rw₃ rw₄ : a.natAbs ≠ 1 ∧ b ≠ 0 ↔ a.natAbs ≠ 1 ∧ b ≠ 0
⊢ FiniteMultiplicity a b ↔ a.natAbs ≠ 1 ∧ b ≠ 0

Tactic:
rw [finiteMultiplicity_iff_finiteMultiplicity_natAbs, Nat.finiteMultiplicity_iff,
    pos_iff_ne_zero, Int.natAbs_ne_zero]

Premises used: Int.finiteMultiplicity_iff_finiteMultiplicity_natAbs, pos_iff_ne_zero, Int.natAbs_ne_zero, Nat.finiteMultiplicity_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ_1 : Type u
R_1 : Type v
inst : CommSemiring R_1
p m : ℕ
σ : Type u_1
R : Type u_2
inst_1 : CommSemiring R
inst_2 : Small.{u, u_2} R
inst_3 : Small.{u, u_1} σ
⊢ Small.{u, max u_2 u_1} (MvPolynomial σ R)

Tactic:
inferInstanceAs (Small.{u} ((σ →₀ ℕ) →₀ R))

Premises used: _private.0.MvPolynomial.instSmall._proof_1
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
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
rw₃ rw₄ : p ∣ n ↔ p ∣ n
⊢ Eq (α := MvPolynomial σ R) (↑n : MvPolynomial σ R) 0 ↔ p ∣ n

Tactic:
rw [← C_eq_coe_nat, ← C_0, C_inj, CharP.cast_eq_zero_iff R p]

Premises used: MvPolynomial.C_0, MvPolynomial.C_eq_coe_nat, CharP.cast_eq_zero_iff, MvPolynomial.C_inj
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
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
rwa₃ rwa₄ rwa₅ rwa₆ : ∀ (hxy : x = y), x = y
⊢ x = y

Tactic:
rwa [← C_eq_coe_nat, ← C_eq_coe_nat, C_inj, Nat.cast_inj] at hxy

Premises used: Nat.cast_inj, MvPolynomial.C_eq_coe_nat, MvPolynomial.C_inj
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m : ℕ
inst_1 : ExpChar R p
zero : ∀ [CharZero R], ExpChar (MvPolynomial σ R) 1
prime : Nat.Prime p → ∀ [CharP R p], ExpChar (MvPolynomial σ R) p
⊢ ExpChar (MvPolynomial σ R) p

Tactic:
cases ‹ExpChar R p›

Premises used: ExpChar
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
m : ℕ
inst_1 : CharZero R
⊢ ExpChar (MvPolynomial σ R) 1

Tactic:
ExpChar.zero

Premises used: ExpChar.zero
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
p m : ℕ
hprime : Nat.Prime p
hchar : CharP R p
⊢ ExpChar (MvPolynomial σ R) p

Tactic:
ExpChar.prime ‹_›

Premises used: ExpChar.prime
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
m : ℕ
inst_1 : CharZero R
⊢ ExpChar (MvPolynomial σ R) 1

Tactic:
exacts [ExpChar.zero, ExpChar.prime ‹_›]

Premises used: ExpChar.zero, ExpChar.prime
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
rw :
  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)))
⊢ Finsupp.mapRange (⇑f : (a : R) → S) ⋯ p = (map f : (a : MvPolynomial σ R) → MvPolynomial σ S) p

Tactic:
rw [p.as_sum, Finsupp.mapRange_finsetSum, map_sum (map f)]

Premises used: MvPolynomial.as_sum, map_sum, Finsupp.mapRange_finsetSum, MvPolynomial.map
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
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)))

Tactic:
Finset.sum_congr rfl fun n _ => ?_

Premises used: AddMonoidAlgebra, Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
p : MvPolynomial σ R
f : R →+* S
refine :
  ∀ 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)))
⊢ 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)))

Tactic:
refine Finset.sum_congr rfl fun n _ => ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
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)))
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)
rw₃ rw₄ :
  Eq (α := Finsupp.{u, u_2} (σ →₀ ℕ) S)
    ((monomial n : (a : S) → MvPolynomial σ S) ((f : (a : R) → S) (coeff n p)) : MvPolynomial σ S)
    ((monomial n : (a : S) → MvPolynomial σ S) ((f : (a : R) → S) (coeff n p)) : MvPolynomial σ S)
⊢ 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)))

Tactic:
rw [map_monomial, ← single_eq_monomial, Finsupp.mapRange_single, single_eq_monomial]

Premises used: MvPolynomial.single_eq_monomial, MvPolynomial.map_monomial, Finsupp.mapRange_single
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
s t : Set (σ →₀ ℕ)
h : s ⊆ t
⊢ LE.le (α := Submodule R (MvPolynomial σ R)) (restrictSupport R s) (restrictSupport R t)

Tactic:
Finsupp.supported_mono h

Premises used: Set.Mem, Finsupp.supported_mono, AddMonoidAlgebra
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
s : Set (σ →₀ ℕ)
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
    (span R ((fun (x : σ →₀ ℕ) ↦ (monomial x : (a : R) → MvPolynomial σ R) 1) '' s))

Tactic:
Finsupp.supported_eq_span_single ..

Premises used: Finsupp.supported_eq_span_single, AddMonoidAlgebra, MvPolynomial.restrictSupport, Finsupp.single
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
s : Set (σ →₀ ℕ)
r : MvPolynomial σ R
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s) r ↔ (↑r.support : Set (σ →₀ ℕ)) ⊆ s

Tactic:
.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.Subset
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
s : Set (σ →₀ ℕ)
m : σ →₀ ℕ
r : R
pos :
  r = 0 →
    (Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
        ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
      m ∈ s ∨ r = 0)
neg :
  ¬r = 0 →
    (Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
        ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
      m ∈ s ∨ r = 0)
⊢ Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
      ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    m ∈ s ∨ r = 0

Tactic:
by_cases r = 0
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
s : Set (σ →₀ ℕ)
m : σ →₀ ℕ
r : R
h : r = 0
⊢ Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
      ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    m ∈ s ∨ r = 0

Tactic:
simp [mem_restrictSupport_iff, support_monomial, *]

Premises used: MvPolynomial.support_monomial, MvPolynomial.mem_restrictSupport_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
s : Set (σ →₀ ℕ)
m : σ →₀ ℕ
r : R
h : ¬r = 0
⊢ Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
      ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    m ∈ s ∨ r = 0

Tactic:
simp [mem_restrictSupport_iff, support_monomial, *]

Premises used: MvPolynomial.support_monomial, MvPolynomial.mem_restrictSupport_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
s : Set (σ →₀ ℕ)
m : σ →₀ ℕ
r : R
pos :
  r = 0 →
    (Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
        ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
      m ∈ s ∨ r = 0)
neg :
  ¬r = 0 →
    (Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
        ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
      m ∈ s ∨ r = 0)
pos₁ :
  r = 0 →
    (Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
        ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
      m ∈ s ∨ r = 0)
neg₁ :
  ¬r = 0 →
    (Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
        ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
      m ∈ s ∨ r = 0)
pos₂ :
  r = 0 →
    (Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
        ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
      m ∈ s ∨ r = 0)
neg₂ :
  ¬r = 0 →
    (Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
        ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
      m ∈ s ∨ r = 0)
pos₃ :
  r = 0 →
    (Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
        ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
      m ∈ s ∨ r = 0)
neg₃ :
  ¬r = 0 →
    (Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
        ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
      m ∈ s ∨ r = 0)
⊢ Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R s)
      ((monomial m : (a : R) → MvPolynomial σ R) r : MvPolynomial σ R) ↔
    m ∈ s ∨ r = 0

Tactic:
classical
  by_cases r = 0 <;> simp [mem_restrictSupport_iff, support_monomial, *]

Premises used: MvPolynomial.support_monomial, MvPolynomial.mem_restrictSupport_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
a : LE.le (α := Submodule R (MvPolynomial σ R)) (restrictSupport R 0) 1
a₁ : LE.le (α := Submodule R (MvPolynomial σ R)) 1 (restrictSupport R 0)
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (restrictSupport R 0) 1

Tactic:
apply le_antisymm

Premises used: le_antisymm
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
a :
  Subset.{u} (α := Set (σ →₀ ℕ)) 0
    ((fun (x : σ →₀ ℕ) ↦ (monomial x : (a : R) → MvPolynomial σ R) 1) ⁻¹' (↑1 : Set (MvPolynomial σ R)))
⊢ LE.le (α := Submodule R (MvPolynomial σ R)) (restrictSupport R 0) 1

Tactic:
rw [restrictSupport_eq_span, Submodule.span_le, Set.image_subset_iff]

Premises used: Set.image_subset_iff, MvPolynomial.restrictSupport_eq_span, Submodule.span_le
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
⊢ Eq (α := MvPolynomial σ R) ((C : (a : R) → MvPolynomial σ R) 1) 1

Tactic:
simp
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
⊢ Subset.{u} (α := Set (σ →₀ ℕ)) 0
    ((fun (x : σ →₀ ℕ) ↦ (monomial x : (a : R) → MvPolynomial σ R) 1) ⁻¹' (↑1 : Set (MvPolynomial σ R)))

Tactic:
simpa using ⟨1, by simp⟩
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
x : R
⊢ Membership.mem (α := MvPolynomial σ R) (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R 0)
    ((toSpanSingleton R (MvPolynomial σ R) 1 : (a : R) → MvPolynomial σ R) x : MvPolynomial σ R)

Tactic:
simp [mem_restrictSupport_iff, Set.subset_def, coeff_one]

Premises used: Set.subset_def, MvPolynomial.mem_restrictSupport_iff, MvPolynomial.coeff_one
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
a : LE.le (α := Submodule R (MvPolynomial σ R)) (restrictSupport R 0) 1
a₁ a₂ : LE.le (α := Submodule R (MvPolynomial σ R)) 1 (restrictSupport R 0)
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (restrictSupport R 0) 1

Tactic:
classical
  apply le_antisymm
  · rw [restrictSupport_eq_span, Submodule.span_le, Set.image_subset_iff]
    simpa using ⟨1, by simp⟩
  · rintro _ ⟨x, rfl⟩
    simp [mem_restrictSupport_iff, Set.subset_def, coeff_one]

Premises used: Set.subset_def, MvPolynomial.mem_restrictSupport_iff, MvPolynomial.coeff_one, le_antisymm, Set.image_subset_iff, MvPolynomial.restrictSupport_eq_span, Submodule.span_le, rfl
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
h :
  ∀ (x : MvPolynomial σ R),
    Membership.mem (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R univ) x ↔
      Membership.mem (γ := Submodule R (MvPolynomial σ R)) ⊤ x
⊢ Eq (α := Submodule R (MvPolynomial σ R)) (restrictSupport R univ) ⊤

Tactic:
ext
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
x : MvPolynomial σ R
⊢ Membership.mem (γ := Submodule R (MvPolynomial σ R)) (restrictSupport R univ) x ↔
    Membership.mem (γ := Submodule R (MvPolynomial σ R)) ⊤ x

Tactic:
simp [mem_restrictSupport_iff]

Premises used: MvPolynomial.mem_restrictSupport_iff
-- Module: Mathlib.RingTheory.MvPolynomial.Basic
Goal:
σ : Type u
R : Type v
inst : CommSemiring R
n : ℕ
s : Set (σ →₀ ℕ)
zero :
  restrictSupport R (HSMul.hSMul (α := ℕ) 0 s) =
    HPow.hPow (α := Submodule R (MvPolynomial σ R)) (β := ℕ) (restrictSupport R s) 0
succ :
  ∀ (n : ℕ),
    restrictSupport R (n • s) = HPow.hPow (α := Submodule R (MvPolynomial σ R)) (restrictSupport R s) n →
      restrictSupport R ((n + 1) • s) = HPow.hPow (α := Submodule R (MvPolynomial σ R)) (restrictSupport R s) (n + 1)
⊢ restrictSupport R (n • s) = HPow.hPow (α := Submodule R (MvPolynomial σ R)) (restrictSupport R s) n

Tactic:
induction n