awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Supported (goal)
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
p : MvPolynomial σ R
s : Set σ
mp :
  (∃ (x : MvPolynomial.{u_1, u} { x : σ // x ∈ s } R),
      (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R) x =
        p) →
    (↑p.vars : Set σ) ⊆ s
⊢ (∃ (x : MvPolynomial.{u_1, u} { x : σ // x ∈ s } R),
      (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R) x =
        p) ↔
    (↑p.vars : Set σ) ⊆ s
have mpr : (↑p.vars : Set σ) ⊆ s →
  ∃ (x : MvPolynomial.{u_1, u} { x : σ // x ∈ s } R),
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R) x = p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Supported (goal)
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s : Set σ
p : MvPolynomial.{u_1, u} { x : σ // x ∈ s } R
⊢ (↑(vars.{u, u_1} (R := R)
          ((rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) :
              (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R)
            p)) :
      Set σ) ⊆
    s
have mp : (↑(Finset.image (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) p.vars) : Set σ) ⊆ s
Tactic: refine _root_.trans (Finset.coe_subset.2 (vars_rename _ _)) ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Supported (goal)
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
p : MvPolynomial σ R
s : Set σ
⊢ Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (supported R s) p ↔ (↑p.vars : Set σ) ⊆ s
have rw : Membership.mem (γ := Subalgebra R (MvPolynomial σ R))
    (AlgHom.range (A := MvPolynomial.{u_1, u} { x : σ // x ∈ s } R) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))))
    p ↔
  (↑p.vars : Set σ) ⊆ s
Tactic: classical
  rw [supported_eq_range_rename, AlgHom.mem_range]
  constructor
  · rintro ⟨p, rfl⟩
    refine _root_.trans (Finset.coe_subset.2 (vars_rename _ _)) ?_
    simp
  · intro hs
    exact exists_rename_eq_of_vars_subset_range p ((↑) : s → σ) Subtype.val_injective (by simpa)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Supported (goal)
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
p : MvPolynomial σ R
s : Set σ
rw :
  Membership.mem (γ := Subalgebra R (MvPolynomial σ R))
      (AlgHom.range (A := MvPolynomial.{u_1, u} { x : σ // x ∈ s } R) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))))
      p ↔
    (↑p.vars : Set σ) ⊆ s
⊢ Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (supported R s) p ↔ (↑p.vars : Set σ) ⊆ s
have rw₁ : (∃ (x : MvPolynomial.{u_1, u} { x : σ // x ∈ s } R),
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R) x =
      p) ↔
  (↑p.vars : Set σ) ⊆ s
Tactic: classical
  rw [supported_eq_range_rename, AlgHom.mem_range]
  constructor
  · rintro ⟨p, rfl⟩
    refine _root_.trans (Finset.coe_subset.2 (vars_rename _ _)) ?_
    simp
  · intro hs
    exact exists_rename_eq_of_vars_subset_range p ((↑) : s → σ) Subtype.val_injective (by simpa)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Supported (goal)
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
p : MvPolynomial σ R
s : Set σ
rw :
  Membership.mem (γ := Subalgebra R (MvPolynomial σ R))
      (AlgHom.range (A := MvPolynomial.{u_1, u} { x : σ // x ∈ s } R) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))))
      p ↔
    (↑p.vars : Set σ) ⊆ s
rw₁ rw₂ rw₃ :
  (∃ (x : MvPolynomial.{u_1, u} { x : σ // x ∈ s } R),
      (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R) x =
        p) ↔
    (↑p.vars : Set σ) ⊆ s
⊢ Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (supported R s) p ↔ (↑p.vars : Set σ) ⊆ s
have mp : (∃ (x : MvPolynomial.{u_1, u} { x : σ // x ∈ s } R),
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R) x =
      p) →
  (↑p.vars : Set σ) ⊆ s
Tactic: classical
  rw [supported_eq_range_rename, AlgHom.mem_range]
  constructor
  · rintro ⟨p, rfl⟩
    refine _root_.trans (Finset.coe_subset.2 (vars_rename _ _)) ?_
    simp
  · intro hs
    exact exists_rename_eq_of_vars_subset_range p ((↑) : s → σ) Subtype.val_injective (by simpa)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Supported (goal)
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
p : MvPolynomial σ R
s : Set σ
rw :
  Membership.mem (γ := Subalgebra R (MvPolynomial σ R))
      (AlgHom.range (A := MvPolynomial.{u_1, u} { x : σ // x ∈ s } R) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))))
      p ↔
    (↑p.vars : Set σ) ⊆ s
rw₁ rw₂ rw₃ :
  (∃ (x : MvPolynomial.{u_1, u} { x : σ // x ∈ s } R),
      (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R) x =
        p) ↔
    (↑p.vars : Set σ) ⊆ s
mp :
  (∃ (x : MvPolynomial.{u_1, u} { x : σ // x ∈ s } R),
      (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R) x =
        p) →
    (↑p.vars : Set σ) ⊆ s
⊢ Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (supported R s) p ↔ (↑p.vars : Set σ) ⊆ s
have mpr : (↑p.vars : Set σ) ⊆ s →
  ∃ (x : MvPolynomial.{u_1, u} { x : σ // x ∈ s } R),
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } R) → MvPolynomial σ R) x = p
Tactic: classical
  rw [supported_eq_range_rename, AlgHom.mem_range]
  constructor
  · rintro ⟨p, rfl⟩
    refine _root_.trans (Finset.coe_subset.2 (vars_rename _ _)) ?_
    simp
  · intro hs
    exact exists_rename_eq_of_vars_subset_range p ((↑) : s → σ) Subtype.val_injective (by simpa)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Supported (goal)
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
p : MvPolynomial σ R
⊢ Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (supported R (↑p.vars : Set σ)) p
have rw : (↑p.vars : Set σ) ⊆ (↑p.vars : Set σ)
Tactic: rw [mem_supported]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Supported (goal)
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s t : Set σ
inst_1 : Nontrivial R
⊢ LE.le (α := Subalgebra R (MvPolynomial σ R)) (supported R s) (supported R t) ↔ s ⊆ t
have mp : LE.le (α := Subalgebra R (MvPolynomial σ R)) (supported R s) (supported R t) → s ⊆ t
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Supported (goal)
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s t : Set σ
inst_1 : Nontrivial R
mp : LE.le (α := Subalgebra R (MvPolynomial σ R)) (supported R s) (supported R t) → s ⊆ t
⊢ LE.le (α := Subalgebra R (MvPolynomial σ R)) (supported R s) (supported R t) ↔ s ⊆ t
have mpr : s ⊆ t → LE.le (α := Subalgebra R (MvPolynomial σ R)) (supported R s) (supported R t)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Supported (hypothesis)
Goal:
σ : Type u_1
s : Set σ
R : Type u_2
inst : CommRing R
F : MvPolynomial σ ℤ
hF : (↑F.vars : Set σ) ⊆ s
⊢ ∃ (f : ((↑s : Type u_1) → R) → R),
    ∀ (x : σ → R),
      f (x ∘ Subtype.val (p := fun (x : σ) ↦ x ∈ s)) =
        ((aeval (R := ℤ) x : AlgHom.{0, u_1, u_2} ℤ (MvPolynomial σ ℤ) R) : (a : MvPolynomial σ ℤ) → R) F
have hF₁ : ∃ (x : MvPolynomial { x : σ // x ∈ s } ℤ),
  (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } ℤ) → MvPolynomial σ ℤ) x = F
Tactic: rw [← mem_supported, supported_eq_range_rename, AlgHom.mem_range] at hF
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Supported (goal)
Goal:
σ : Type u_1
s : Set σ
R : Type u_2
inst : CommRing R
F : MvPolynomial σ ℤ
hF :
  ∃ (x : MvPolynomial { x : σ // x ∈ s } ℤ),
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } ℤ) → MvPolynomial σ ℤ) x = F
⊢ ∃ (f : ((↑s : Type u_1) → R) → R),
    ∀ (x : σ → R),
      f (x ∘ Subtype.val (p := fun (x : σ) ↦ x ∈ s)) =
        ((aeval (R := ℤ) x : AlgHom.{0, u_1, u_2} ℤ (MvPolynomial σ ℤ) R) : (a : MvPolynomial σ ℤ) → R) F
have obtain : ∀ (F' : MvPolynomial { x : σ // x ∈ s } ℤ)
  (hF' :
    (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } ℤ) → MvPolynomial σ ℤ) F' =
      F),
  ∃ (f : ((↑s : Type u_1) → R) → R),
    ∀ (x : σ → R),
      f (x ∘ Subtype.val (p := fun (x : σ) ↦ x ∈ s)) =
        ((aeval (R := ℤ) x : AlgHom.{0, u_1, u_2} ℤ (MvPolynomial σ ℤ) R) : (a : MvPolynomial σ ℤ) → R) F
Tactic: obtain ⟨F', hF'⟩ := hF
Cleared hypotheses: hF
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Supported (goal)
Goal:
σ : Type u_1
s : Set σ
R : Type u_2
inst : CommRing R
F : MvPolynomial σ ℤ
F' : MvPolynomial { x : σ // x ∈ s } ℤ
hF' :
  (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) : (a : MvPolynomial { x : σ // x ∈ s } ℤ) → MvPolynomial σ ℤ) F' = F
⊢ ∃ (f : ((↑s : Type u_1) → R) → R),
    ∀ (x : σ → R),
      f (x ∘ Subtype.val (p := fun (x : σ) ↦ x ∈ s)) =
        ((aeval (R := ℤ) x : AlgHom.{0, u_1, u_2} ℤ (MvPolynomial σ ℤ) R) : (a : MvPolynomial σ ℤ) → R) F
have h : ∀ (x : σ → R),
  Eq.{u_2 + 1} (α := R)
    ((fun (z : (↑s : Type u_1) → R) ↦
          (((aeval (R := ℤ) z : AlgHom.{0, u_1, u_2} ℤ (MvPolynomial (↑s : Type u_1) ℤ) R) :
                (a : MvPolynomial (↑s : Type u_1) ℤ) → R)
              F' :
            R))
        (x ∘ Subtype.val (p := fun (x : σ) ↦ x ∈ s)) :
      R)
    (((aeval (R := ℤ) x : AlgHom.{0, u_1, u_2} ℤ (MvPolynomial σ ℤ) R) : (a : MvPolynomial σ ℤ) → R) F : R)
Tactic: use fun z ↦ aeval z F'
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) 0) ∅
have rw : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset (degrees.{u, u_1} (R := R) 0)) ∅
Tactic: rw [vars_def, degrees_zero, Multiset.toFinset_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
rw : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset (degrees.{u, u_1} (R := R) 0)) ∅
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) 0) ∅
have rw₁ : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset 0) ∅
Tactic: rw [vars_def, degrees_zero, Multiset.toFinset_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
rw : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset (degrees.{u, u_1} (R := R) 0)) ∅
rw₁ : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset 0) ∅
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) 0) ∅
have rw₂ : Eq.{u_1 + 1} (α := Finset σ) ∅ ∅
Tactic: rw [vars_def, degrees_zero, Multiset.toFinset_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) 0) ∅
have classical : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset (degrees.{u, u_1} (R := R) 0)) ∅
Tactic: classical rw [vars_def, degrees_zero, Multiset.toFinset_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
classical : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset (degrees.{u, u_1} (R := R) 0)) ∅
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) 0) ∅
have classical₁ : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset 0) ∅
Tactic: classical rw [vars_def, degrees_zero, Multiset.toFinset_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
classical : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset (degrees.{u, u_1} (R := R) 0)) ∅
classical₁ : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset 0) ∅
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) 0) ∅
have classical₂ : Eq.{u_1 + 1} (α := Finset σ) ∅ ∅
Tactic: classical rw [vars_def, degrees_zero, Multiset.toFinset_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
r : R
s : σ →₀ ℕ
inst : CommSemiring R
h : r ≠ 0
⊢ vars.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) r) = s.support
have rw : Multiset.toFinset (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) r)) = s.support
Tactic: rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
r : R
s : σ →₀ ℕ
inst : CommSemiring R
h : r ≠ 0
rw : Multiset.toFinset (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) r)) = s.support
⊢ vars.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) r) = s.support
have rw₁ : Multiset.toFinset ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) = s.support
Tactic: rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
r : R
s : σ →₀ ℕ
inst : CommSemiring R
h : r ≠ 0
rw : Multiset.toFinset (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) r)) = s.support
rw₁ : Multiset.toFinset ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) = s.support
⊢ vars.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) r) = s.support
have rw₂ : s.support = s.support
Tactic: rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
r : R
s : σ →₀ ℕ
inst : CommSemiring R
h : r ≠ 0
⊢ vars.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) r) = s.support
have classical : Multiset.toFinset (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) r)) = s.support
Tactic: classical rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
r : R
s : σ →₀ ℕ
inst : CommSemiring R
h : r ≠ 0
classical : Multiset.toFinset (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) r)) = s.support
⊢ vars.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) r) = s.support
have classical₁ : Multiset.toFinset ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) = s.support
Tactic: classical rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
r : R
s : σ →₀ ℕ
inst : CommSemiring R
h : r ≠ 0
classical : Multiset.toFinset (degrees.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) r)) = s.support
classical₁ : Multiset.toFinset ((toMultiset : (a : σ →₀ ℕ) → Multiset σ) s) = s.support
⊢ vars.{u, u_1} (R := R) ((monomial s : (a : R) → MvPolynomial σ R) r) = s.support
have classical₂ : s.support = s.support
Tactic: classical rw [vars_def, degrees_monomial_eq _ _ h, Finsupp.toFinset_toMultiset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
r : R
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) r)) ∅
have rw : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset (degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) r))) ∅
Tactic: rw [vars_def, degrees_C, Multiset.toFinset_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
r : R
inst : CommSemiring R
rw : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset (degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) r))) ∅
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) r)) ∅
have rw₁ : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset 0) ∅
Tactic: rw [vars_def, degrees_C, Multiset.toFinset_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
r : R
inst : CommSemiring R
rw : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset (degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) r))) ∅
rw₁ : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset 0) ∅
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) r)) ∅
have rw₂ : Eq.{u_1 + 1} (α := Finset σ) ∅ ∅
Tactic: rw [vars_def, degrees_C, Multiset.toFinset_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
r : R
inst : CommSemiring R
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) r)) ∅
have classical : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset (degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) r))) ∅
Tactic: classical rw [vars_def, degrees_C, Multiset.toFinset_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
r : R
inst : CommSemiring R
classical :
  Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset (degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) r))) ∅
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) r)) ∅
have classical₁ : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset 0) ∅
Tactic: classical rw [vars_def, degrees_C, Multiset.toFinset_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
r : R
inst : CommSemiring R
classical :
  Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset (degrees.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) r))) ∅
classical₁ : Eq.{u_1 + 1} (α := Finset σ) (Multiset.toFinset 0) ∅
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) r)) ∅
have classical₂ : Eq.{u_1 + 1} (α := Finset σ) ∅ ∅
Tactic: classical rw [vars_def, degrees_C, Multiset.toFinset_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ vars.{u, u_1} (R := R) (X n) = {n}
have rw : Eq (α := Finset σ) (vars.{u, u_1} (R := R) ((monomial (Finsupp.single n 1) : (a : R) → MvPolynomial σ R) 1)) {n}
Tactic: rw [X, vars_monomial (one_ne_zero' R), Finsupp.support_single _ (one_ne_zero' ℕ)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
inst_1 : Nontrivial R
rw : Eq (α := Finset σ) (vars.{u, u_1} (R := R) ((monomial (Finsupp.single n 1) : (a : R) → MvPolynomial σ R) 1)) {n}
⊢ vars.{u, u_1} (R := R) (X n) = {n}
have rw₁ : Finsupp.support (M := ℕ) (Finsupp.single n 1) = {n}
Tactic: rw [X, vars_monomial (one_ne_zero' R), Finsupp.support_single _ (one_ne_zero' ℕ)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
n : σ
inst : CommSemiring R
inst_1 : Nontrivial R
rw : Eq (α := Finset σ) (vars.{u, u_1} (R := R) ((monomial (Finsupp.single n 1) : (a : R) → MvPolynomial σ R) 1)) {n}
rw₁ : Finsupp.support (M := ℕ) (Finsupp.single n 1) = {n}
⊢ vars.{u, u_1} (R := R) (X n) = {n}
have rw₂ : Eq (α := Finset σ) {n} {n}
Tactic: rw [X, vars_monomial (one_ne_zero' R), Finsupp.support_single _ (one_ne_zero' ℕ)]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
f : MvPolynomial σ R
x : σ →₀ ℕ
H : x ∈ f.support
v : σ
h : v ∉ f.vars
⊢ Eq (α := ℕ) ((x : (a : σ) → ℕ) v : ℕ) (0 : ℕ)
have contrapose! : ∀ (h : Ne (α := ℕ) ((x : (a : σ) → ℕ) v : ℕ) (0 : ℕ)), v ∈ f.vars
Tactic: contrapose! h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
s : σ →₀ ℕ
h : s ∈ p.support
i : σ
hi : i ∈ s.support
⊢ i ∈ p.vars
have contrapose! : ∀ (hi : i ∉ p.vars), i ∉ s.support
Tactic: contrapose! hi
Cleared hypotheses: hi
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)
⊢ p.vars = ∅
have rw : Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) ((C : (a : R) → MvPolynomial σ R) (coeff 0 p))) ∅
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
⊢ p.vars = ∅ ↔ p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)
have refine : ∀ (h : p.vars = ∅), p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ by rw [h]; simp⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.vars = ∅
⊢ p = (C : (a : R) → MvPolynomial σ R) (coeff 0 p)
have rw : p.totalDegree = 0
Tactic: rw [← totalDegree_eq_zero_iff_eq_C]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.vars = ∅
⊢ p.totalDegree = 0
have suffices : p.degrees.card = 0
Tactic: suffices p.degrees.card = 0 by grind [totalDegree_le_degrees_card p]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.vars = ∅
⊢ p.degrees.card = 0
have h₁ : p.degrees = 0
Tactic: rw [vars_def, Multiset.toFinset_eq_empty] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
h : p.vars = ∅
⊢ p.degrees.card = 0
have h₁ : p.degrees = 0
Tactic: classical rw [vars_def, Multiset.toFinset_eq_empty] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
p q : MvPolynomial σ R
x : σ
hx : x ∈ (p + q).vars
⊢ x ∈ p.vars ∪ q.vars
have simp : ∀ (hx : x ∈ (p + q).degrees), x ∈ p.degrees ∨ x ∈ q.degrees
Tactic: simp only [vars_def, Finset.mem_union, Multiset.mem_toFinset] at hx ⊢
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
h : Disjoint p.vars q.vars
⊢ (p + q).vars = p.vars ∪ q.vars
have refine : ∀ (x : σ) (hx : x ∈ p.vars ∪ q.vars), x ∈ (p + q).vars
Tactic: refine (vars_add_subset p q).antisymm fun x hx => ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
h : Disjoint p.vars q.vars
x : σ
hx : x ∈ p.vars ∪ q.vars
⊢ x ∈ (p + q).vars
have simp : ∀ (h : Disjoint p.degrees q.degrees) (hx : x ∈ p.degrees.toFinset ∪ q.degrees.toFinset), x ∈ (p + q).degrees.toFinset
Tactic: simp only [vars_def, Multiset.disjoint_toFinset] at h hx ⊢
Cleared hypotheses: h, hx
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p q : MvPolynomial σ R
inst_1 : DecidableEq σ
x : σ
h : Disjoint p.degrees q.degrees
hx : x ∈ p.degrees.toFinset ∪ q.degrees.toFinset
⊢ x ∈ (p + q).degrees.toFinset
have rwa : x ∈ (p.degrees ∪ q.degrees).toFinset
Tactic: rwa [degrees_add_of_disjoint h, Multiset.toFinset_union]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
inst_1 : DecidableEq σ
φ ψ : MvPolynomial σ R
⊢ (φ * ψ).vars ⊆ φ.vars ∪ ψ.vars
have simp_rw : (φ * ψ).degrees ⊆ φ.degrees + ψ.degrees
Tactic: simp_rw [vars_def, ← Multiset.toFinset_add, Multiset.toFinset_subset]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
ih : (φ ^ n).vars ⊆ φ.vars
⊢ (φ ^ (n + 1)).vars ⊆ φ.vars
have succ : (φ * φ ^ n).vars ⊆ φ.vars
Tactic: rw [pow_succ']
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
ih : (φ ^ n).vars ⊆ φ.vars
⊢ (φ * φ ^ n).vars ⊆ φ.vars
have succ : φ.vars ∪ (φ ^ n).vars ⊆ φ.vars
Tactic: apply Finset.Subset.trans (vars_mul _ _)