awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
this : coeff d q = 0
rwa : coeff d p + 0 ≠ 0
rwa₁ : coeff d p ≠ 0
rwa₂ : Ne.{u + 1} (α := R) ((p : (a : σ →₀ ℕ) → R) d : R) (0 : R)
⊢ coeff d p + coeff d q ≠ 0
have rwa₃ : d ∈ p.support
Tactic: rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
⊢ coeff d p + coeff d q ≠ 0
have a : coeff d q = 0
Tactic: suffices q.coeff d = 0 by rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d ≠ 0
⊢ coeff d q = 0
have h0₁ : d.support.Nonempty
Tactic: rw [Ne, ← Finsupp.support_eq_empty, ← Ne, ← Finset.nonempty_iff_ne_empty] at h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
h0 : d.support.Nonempty
⊢ coeff d q = 0
have a : ∀ (j : σ) (hj : j ∈ d.support), coeff d q = 0
Tactic: obtain ⟨j, hj⟩ := h0
Cleared hypotheses: h0
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b
d : σ →₀ ℕ
hd : d ∈ p.support
j : σ
hj : j ∈ d.support
⊢ coeff d q = 0
have a : ∀ (h : coeff d q ≠ 0), ∃ a ∈ p.degrees, ∃ b ∈ q.degrees, a = b
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : d ∈ p.support
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ a ∈ p.degrees, ∃ b ∈ q.degrees, a = b
have a : ∀ (hd : coeff d p ≠ 0) (j : σ) (hj : j ∈ d.support) (h : coeff d q ≠ 0), ∃ a ∈ p.degrees, ∃ b ∈ q.degrees, a = b
Tactic: rw [mem_support_iff] at hd
Cleared hypotheses: hd, j, hj, h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ ∃ a ∈ p.degrees, ∃ b ∈ q.degrees, a = b
have a : j ∈ p.degrees
Tactic: refine ⟨j, ?_, j, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
a : j ∈ p.degrees
⊢ ∃ a ∈ p.degrees, ∃ b ∈ q.degrees, a = b
have a₁ : j ∈ q.degrees
Tactic: refine ⟨j, ?_, j, ?_, rfl⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ j ∈ p.degrees
have a : ∃ (d : σ →₀ ℕ), coeff d p ≠ 0 ∧ j ∈ d.support
Tactic: rw [mem_degrees]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
d : σ →₀ ℕ
hd : coeff d p ≠ 0
j : σ
hj : j ∈ d.support
h : coeff d q ≠ 0
⊢ j ∈ q.degrees
have a : ∃ (d : σ →₀ ℕ), coeff d q ≠ 0 ∧ j ∈ d.support
Tactic: rw [mem_degrees]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
⊢ p.degrees ≤ (p + q).degrees
have a : ∀ b ∈ p.support, (toMultiset : (a : σ →₀ ℕ) → Multiset σ) b ≤ (p + q).degrees
Tactic: classical
  apply Finset.sup_le
  intro d hd
  rw [Multiset.disjoint_iff_ne] at h
  obtain rfl | h0 := eq_or_ne d 0
  · rw [toMultiset_zero]; apply Multiset.zero_le
  · refine Finset.le_sup_of_le (b := d) ?_ le_rfl
    rw [mem_support_iff, coeff_add]
    suffices q.coeff d = 0 by rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]
    rw [Ne, ← Finsupp.support_eq_empty, ← Ne, ← Finset.nonempty_iff_ne_empty] at h0
    obtain ⟨j, hj⟩ := h0
    contrapose! h
    rw [mem_support_iff] at hd
    refine ⟨j, ?_, j, ?_, rfl⟩
    all_goals rw [mem_degrees]; refine ⟨d, ?_, hj⟩; assumption
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
a a₁ : ∀ (d : σ →₀ ℕ) (hd : d ∈ p.support), (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
⊢ p.degrees ≤ (p + q).degrees
have a₂ : ∀ (h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b) (d : σ →₀ ℕ) (hd : d ∈ p.support),
  (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
Tactic: classical
  apply Finset.sup_le
  intro d hd
  rw [Multiset.disjoint_iff_ne] at h
  obtain rfl | h0 := eq_or_ne d 0
  · rw [toMultiset_zero]; apply Multiset.zero_le
  · refine Finset.le_sup_of_le (b := d) ?_ le_rfl
    rw [mem_support_iff, coeff_add]
    suffices q.coeff d = 0 by rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]
    rw [Ne, ← Finsupp.support_eq_empty, ← Ne, ← Finset.nonempty_iff_ne_empty] at h0
    obtain ⟨j, hj⟩ := h0
    contrapose! h
    rw [mem_support_iff] at hd
    refine ⟨j, ?_, j, ?_, rfl⟩
    all_goals rw [mem_degrees]; refine ⟨d, ?_, hj⟩; assumption
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
a a₁ : ∀ (d : σ →₀ ℕ) (hd : d ∈ p.support), (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
a₂ :
  ∀ (h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b) (d : σ →₀ ℕ) (hd : d ∈ p.support),
    (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
⊢ p.degrees ≤ (p + q).degrees
have a₃ : ∀ (h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b) (hd : 0 ∈ p.support),
  (toMultiset : (a : σ →₀ ℕ) → Multiset σ) 0 ≤ (p + q).degrees
Tactic: classical
  apply Finset.sup_le
  intro d hd
  rw [Multiset.disjoint_iff_ne] at h
  obtain rfl | h0 := eq_or_ne d 0
  · rw [toMultiset_zero]; apply Multiset.zero_le
  · refine Finset.le_sup_of_le (b := d) ?_ le_rfl
    rw [mem_support_iff, coeff_add]
    suffices q.coeff d = 0 by rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]
    rw [Ne, ← Finsupp.support_eq_empty, ← Ne, ← Finset.nonempty_iff_ne_empty] at h0
    obtain ⟨j, hj⟩ := h0
    contrapose! h
    rw [mem_support_iff] at hd
    refine ⟨j, ?_, j, ?_, rfl⟩
    all_goals rw [mem_degrees]; refine ⟨d, ?_, hj⟩; assumption
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
h : Disjoint p.degrees q.degrees
a a₁ : ∀ (d : σ →₀ ℕ) (hd : d ∈ p.support), (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
a₂ :
  ∀ (h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b) (d : σ →₀ ℕ) (hd : d ∈ p.support),
    (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
a₃ :
  ∀ (h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b) (hd : 0 ∈ p.support),
    (toMultiset : (a : σ →₀ ℕ) → Multiset σ) 0 ≤ (p + q).degrees
⊢ p.degrees ≤ (p + q).degrees
have a₄ : ∀ (h : ∀ a ∈ p.degrees, ∀ b ∈ q.degrees, a ≠ b) (d : σ →₀ ℕ) (hd : d ∈ p.support) (h0 : d ≠ 0),
  (toMultiset : (a : σ →₀ ℕ) → Multiset σ) d ≤ (p + q).degrees
Tactic: classical
  apply Finset.sup_le
  intro d hd
  rw [Multiset.disjoint_iff_ne] at h
  obtain rfl | h0 := eq_or_ne d 0
  · rw [toMultiset_zero]; apply Multiset.zero_le
  · refine Finset.le_sup_of_le (b := d) ?_ le_rfl
    rw [mem_support_iff, coeff_add]
    suffices q.coeff d = 0 by rwa [this, add_zero, coeff, ← Finsupp.mem_support_iff]
    rw [Ne, ← Finsupp.support_eq_empty, ← Ne, ← Finset.nonempty_iff_ne_empty] at h0
    obtain ⟨j, hj⟩ := h0
    contrapose! h
    rw [mem_support_iff] at hd
    refine ⟨j, ?_, j, ?_, rfl⟩
    all_goals rw [mem_degrees]; refine ⟨d, ?_, hj⟩; assumption
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
⊢ Membership.mem (γ := Multiset τ)
      (degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) i →
    i ∈ Multiset.map f φ.degrees
have rw : (∃ (d : τ →₀ ℕ),
    Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0 ∧ i ∈ d.support) →
  ∃ a ∈ φ.degrees, f a = i
Tactic: rw [mem_degrees, Multiset.mem_map]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
d : τ →₀ ℕ
hd : Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
hi : i ∈ d.support
⊢ ∃ a ∈ φ.degrees, f a = i
have obtain : ∀ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
  (hd :
    Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
  (hi : i ∈ (Finsupp.mapDomain f x).support), ∃ a ∈ φ.degrees, f a = i
Tactic: obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
Cleared hypotheses: d, hd, hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
hi : i ∈ (Finsupp.mapDomain f x).support
⊢ ∃ a ∈ φ.degrees, f a = i
have hi₁ : Ne (α := ℕ) ((x.sum fun (a : σ) ↦ Finsupp.single (f a) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)
Tactic: simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
hi : Ne (α := ℕ) ((x.sum fun (a : σ) ↦ Finsupp.single (f a) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)
⊢ ∃ a ∈ φ.degrees, f a = i
have hi₁ : Ne (α := ℕ) (∑ a ∈ x.support, ((Finsupp.single (f a) ((x : (a : σ) → ℕ) a) : τ →₀ ℕ) : (a : τ) → ℕ) i) 0
Tactic: rw [sum_apply, Finsupp.sum] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
hi : Ne (α := ℕ) (∑ a ∈ x.support, ((Finsupp.single (f a) ((x : (a : σ) → ℕ) a) : τ →₀ ℕ) : (a : τ) → ℕ) i) 0
⊢ ∃ a ∈ φ.degrees, f a = i
have contrapose! : ∀ (hi : ∀ (a : σ) (_ : a ∈ φ.degrees), f a ≠ i),
  Eq (α := ℕ) (∑ a ∈ x.support, ((Finsupp.single (f a) ((x : (a : σ) → ℕ) a) : τ →₀ ℕ) : (a : τ) → ℕ) i) 0
Tactic: contrapose! hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
hi : ∀ (a : σ) (_ : a ∈ φ.degrees), f a ≠ i
⊢ Eq (α := ℕ) (∑ a ∈ x.support, ((Finsupp.single (f a) ((x : (a : σ) → ℕ) a) : τ →₀ ℕ) : (a : τ) → ℕ) i) 0
have rw : ∀ x_1 ∈ x.support, Eq (α := ℕ) (((Finsupp.single (f x_1) ((x : (a : σ) → ℕ) x_1) : τ →₀ ℕ) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)
Tactic: rw [Finset.sum_eq_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
hi : ∀ (a : σ) (_ : a ∈ φ.degrees), f a ≠ i
j : σ
hj : j ∈ x.support
⊢ Eq (α := ℕ) (((Finsupp.single (f j) ((x : (a : σ) → ℕ) j) : τ →₀ ℕ) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)
have hi₁ : ∀ (a : σ) (_ : ∃ (d : σ →₀ ℕ), coeff d φ ≠ 0 ∧ a ∈ d.support), f a ≠ i
Tactic: simp only [mem_degrees] at hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (hypothesis)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
j : σ
hj : j ∈ x.support
hi : ∀ (a : σ) (_ : ∃ (d : σ →₀ ℕ), coeff d φ ≠ 0 ∧ a ∈ d.support), f a ≠ i
⊢ Eq (α := ℕ) (((Finsupp.single (f j) ((x : (a : σ) → ℕ) j) : τ →₀ ℕ) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)
have hi₁ : f j ≠ i
Tactic: specialize hi j ⟨x, hx, hj⟩
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
j : σ
hj : j ∈ x.support
hi : f j ≠ i
⊢ Eq (α := ℕ) (((Finsupp.single (f j) ((x : (a : σ) → ℕ) j) : τ →₀ ℕ) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)
have rw : Eq (α := ℕ) (if f j = i then (x : (a : σ) → ℕ) j else 0 : ℕ) (0 : ℕ)
Tactic: rw [Finsupp.single_apply, if_neg hi]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
i : τ
x : σ →₀ ℕ
hx : coeff x φ ≠ 0
hd : Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0
j : σ
hj : j ∈ x.support
hi : f j ≠ i
rw : Eq (α := ℕ) (if f j = i then (x : (a : σ) → ℕ) j else 0 : ℕ) (0 : ℕ)
⊢ Eq (α := ℕ) (((Finsupp.single (f j) ((x : (a : σ) → ℕ) j) : τ →₀ ℕ) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)
have rw₁ : Eq (α := ℕ) 0 0
Tactic: rw [Finsupp.single_apply, if_neg hi]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
⊢ degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) ⊆ Multiset.map f φ.degrees
have intro : ∀ ⦃i : τ⦄,
  Membership.mem (γ := Multiset τ)
      (degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) i →
    i ∈ Multiset.map f φ.degrees
Tactic: classical
  intro i
  rw [mem_degrees, Multiset.mem_map]
  rintro ⟨d, hd, hi⟩
  obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
  simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
  rw [sum_apply, Finsupp.sum] at hi
  contrapose! hi
  rw [Finset.sum_eq_zero]
  intro j hj
  simp only [mem_degrees] at hi
  specialize hi j ⟨x, hx, hj⟩
  rw [Finsupp.single_apply, if_neg hi]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
intro :
  ∀ ⦃i : τ⦄,
    Membership.mem (γ := Multiset τ)
        (degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) i →
      i ∈ Multiset.map f φ.degrees
⊢ degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) ⊆ Multiset.map f φ.degrees
have intro₁ : ∀ ⦃i : τ⦄,
  (∃ (d : τ →₀ ℕ),
      Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0 ∧ i ∈ d.support) →
    ∃ a ∈ φ.degrees, f a = i
Tactic: classical
  intro i
  rw [mem_degrees, Multiset.mem_map]
  rintro ⟨d, hd, hi⟩
  obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
  simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
  rw [sum_apply, Finsupp.sum] at hi
  contrapose! hi
  rw [Finset.sum_eq_zero]
  intro j hj
  simp only [mem_degrees] at hi
  specialize hi j ⟨x, hx, hj⟩
  rw [Finsupp.single_apply, if_neg hi]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
intro :
  ∀ ⦃i : τ⦄,
    Membership.mem (γ := Multiset τ)
        (degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) i →
      i ∈ Multiset.map f φ.degrees
intro₁ :
  ∀ ⦃i : τ⦄,
    (∃ (d : τ →₀ ℕ),
        Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0 ∧ i ∈ d.support) →
      ∃ a ∈ φ.degrees, f a = i
⊢ degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) ⊆ Multiset.map f φ.degrees
have intro₂ : ∀ ⦃i : τ⦄ (d : τ →₀ ℕ) (hd : Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
  (hi : i ∈ d.support), ∃ a ∈ φ.degrees, f a = i
Tactic: classical
  intro i
  rw [mem_degrees, Multiset.mem_map]
  rintro ⟨d, hd, hi⟩
  obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
  simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
  rw [sum_apply, Finsupp.sum] at hi
  contrapose! hi
  rw [Finset.sum_eq_zero]
  intro j hj
  simp only [mem_degrees] at hi
  specialize hi j ⟨x, hx, hj⟩
  rw [Finsupp.single_apply, if_neg hi]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
intro :
  ∀ ⦃i : τ⦄,
    Membership.mem (γ := Multiset τ)
        (degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) i →
      i ∈ Multiset.map f φ.degrees
intro₁ :
  ∀ ⦃i : τ⦄,
    (∃ (d : τ →₀ ℕ),
        Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0 ∧ i ∈ d.support) →
      ∃ a ∈ φ.degrees, f a = i
intro₂ :
  ∀ ⦃i : τ⦄ (d : τ →₀ ℕ)
    (hd : Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : i ∈ d.support), ∃ a ∈ φ.degrees, f a = i
⊢ degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) ⊆ Multiset.map f φ.degrees
have intro₃ : ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
  (hd :
    Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
  (hi : i ∈ (Finsupp.mapDomain f x).support), ∃ a ∈ φ.degrees, f a = i
Tactic: classical
  intro i
  rw [mem_degrees, Multiset.mem_map]
  rintro ⟨d, hd, hi⟩
  obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
  simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
  rw [sum_apply, Finsupp.sum] at hi
  contrapose! hi
  rw [Finset.sum_eq_zero]
  intro j hj
  simp only [mem_degrees] at hi
  specialize hi j ⟨x, hx, hj⟩
  rw [Finsupp.single_apply, if_neg hi]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
intro :
  ∀ ⦃i : τ⦄,
    Membership.mem (γ := Multiset τ)
        (degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) i →
      i ∈ Multiset.map f φ.degrees
intro₁ :
  ∀ ⦃i : τ⦄,
    (∃ (d : τ →₀ ℕ),
        Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0 ∧ i ∈ d.support) →
      ∃ a ∈ φ.degrees, f a = i
intro₂ :
  ∀ ⦃i : τ⦄ (d : τ →₀ ℕ)
    (hd : Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : i ∈ d.support), ∃ a ∈ φ.degrees, f a = i
intro₃ :
  ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
    (hd :
      Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : i ∈ (Finsupp.mapDomain f x).support), ∃ a ∈ φ.degrees, f a = i
⊢ degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) ⊆ Multiset.map f φ.degrees
have intro₄ : ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
  (hd :
    Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
  (hi : Ne (α := ℕ) ((x.sum fun (a : σ) ↦ Finsupp.single (f a) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)), ∃ a ∈ φ.degrees, f a = i
Tactic: classical
  intro i
  rw [mem_degrees, Multiset.mem_map]
  rintro ⟨d, hd, hi⟩
  obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
  simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
  rw [sum_apply, Finsupp.sum] at hi
  contrapose! hi
  rw [Finset.sum_eq_zero]
  intro j hj
  simp only [mem_degrees] at hi
  specialize hi j ⟨x, hx, hj⟩
  rw [Finsupp.single_apply, if_neg hi]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Degrees (goal)
Goal:
R : Type u
σ : Type u_1
τ : Type u_2
inst : CommSemiring R
f : σ → τ
φ : MvPolynomial σ R
intro :
  ∀ ⦃i : τ⦄,
    Membership.mem (γ := Multiset τ)
        (degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) i →
      i ∈ Multiset.map f φ.degrees
intro₁ :
  ∀ ⦃i : τ⦄,
    (∃ (d : τ →₀ ℕ),
        Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0 ∧ i ∈ d.support) →
      ∃ a ∈ φ.degrees, f a = i
intro₂ :
  ∀ ⦃i : τ⦄ (d : τ →₀ ℕ)
    (hd : Ne.{u + 1} (α := R) (coeff d ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : i ∈ d.support), ∃ a ∈ φ.degrees, f a = i
intro₃ :
  ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
    (hd :
      Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : i ∈ (Finsupp.mapDomain f x).support), ∃ a ∈ φ.degrees, f a = i
intro₄ :
  ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
    (hd :
      Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
    (hi : Ne (α := ℕ) ((x.sum fun (a : σ) ↦ Finsupp.single (f a) : (a : τ) → ℕ) i : ℕ) (0 : ℕ)),
    ∃ a ∈ φ.degrees, f a = i
⊢ degrees.{u, u_2} (R := R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ) ⊆ Multiset.map f φ.degrees
have intro₅ : ∀ ⦃i : τ⦄ (x : σ →₀ ℕ) (hx : coeff x φ ≠ 0)
  (hd :
    Ne.{u + 1} (α := R) (coeff (Finsupp.mapDomain f x) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) φ)) 0)
  (hi : Ne (α := ℕ) (∑ a ∈ x.support, ((Finsupp.single (f a) ((x : (a : σ) → ℕ) a) : τ →₀ ℕ) : (a : τ) → ℕ) i) 0),
  ∃ a ∈ φ.degrees, f a = i
Tactic: classical
  intro i
  rw [mem_degrees, Multiset.mem_map]
  rintro ⟨d, hd, hi⟩
  obtain ⟨x, rfl, hx⟩ := coeff_rename_ne_zero _ _ _ hd
  simp only [Finsupp.mapDomain, Finsupp.mem_support_iff] at hi
  rw [sum_apply, Finsupp.sum] at hi
  contrapose! hi
  rw [Finset.sum_eq_zero]
  intro j hj
  simp only [mem_degrees] at hi
  specialize hi j ⟨x, hx, hj⟩
  rw [Finsupp.single_apply, if_neg hi]