awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) :=
  (finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p
hp' : p' = (finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
i : Fin n →₀ ℕ
hi : i ∈ pₖ.support
calc_2 : degreeOf 0 p ≤ p'.natDegree
⊢ HDiv.hDiv (α := ℚ≥0) (↑(degreeOf 0 p) : ℚ≥0) (↑(#(S 0)) : ℚ≥0) +
      ∑ i_1 : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((i : (a : Fin n) → ℕ) i_1) : ℚ≥0) (↑(#(S i_1.succ)) : ℚ≥0) ≤
    HDiv.hDiv (α := ℚ≥0) (↑p'.natDegree : ℚ≥0) (↑(#(S 0)) : ℚ≥0) +
      ∑ i_1 : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((i : (a : Fin n) → ℕ) i_1) : ℚ≥0) (↑(#(S i_1.succ)) : ℚ≥0)

Tactic:
gcongr
-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin (n + 1)) R
hp : p ≠ 0
S : Fin (n + 1) → Finset R
p' : Polynomial (MvPolynomial (Fin n) R) :=
  (finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p
hp' : p' = (finSuccEquiv R n : (a : MvPolynomial (Fin (n + 1)) R) → Polynomial (MvPolynomial (Fin n) R)) p
k : ℕ := p'.natDegree
hk : k = p'.natDegree
pₖ : MvPolynomial (Fin n) R := p'.leadingCoeff
hpₖ : pₖ = p'.leadingCoeff
hp'₀ : p' ≠ 0
hpₖ₀ : pₖ ≠ 0
i : Fin n →₀ ℕ
hi : i ∈ pₖ.support
⊢ degreeOf 0 p ≤ p'.natDegree

Tactic:
simp [natDegree_finSuccEquiv, p']

Premises used: MvPolynomial.natDegree_finSuccEquiv
-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Fin n → Finset R
⊢ HDiv.hDiv (α := ℚ≥0)
      (↑(Finset.card.{u_1} (α := Fin n → R)
            ({x ∈ piFinset (δ := fun (a : Fin n) ↦ R) fun (i : Fin n) ↦ S i |
              Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)})) :
        ℚ≥0)
      (∏ i : Fin n, (↑(#(S i)) : ℚ≥0)) ≤
    p.support.sup fun (s : Fin n →₀ ℕ) ↦
      ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#(S i)) : ℚ≥0)

Tactic:
schwartz_zippel_sup_sum hp S

Premises used: MvPolynomial.schwartz_zippel_sup_sum
-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Fin n → Finset R
s : Fin n →₀ ℕ
hs : s ∈ p.support
h : ∀ (i : Fin n), Membership.mem (γ := Finset (Fin n)) univ i → (s : (a : Fin n) → ℕ) i ≤ degreeOf i p
⊢ LE.le (α := ℚ≥0) (∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#(S i)) : ℚ≥0))
    (∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑(degreeOf i p) : ℚ≥0) (↑(#(S i)) : ℚ≥0))

Tactic:
gcongr with i
-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Fin n → Finset R
s : Fin n →₀ ℕ
hs : s ∈ p.support
i : Fin n
h : Membership.mem (γ := Finset (Fin n)) univ i
⊢ (s : (a : Fin n) → ℕ) i ≤ degreeOf i p

Tactic:
monomial_le_degreeOf i hs

Premises used: MvPolynomial.monomial_le_degreeOf
-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Fin n → Finset R
s : Fin n →₀ ℕ
hs : s ∈ p.support
i : Fin n
h : Membership.mem (γ := Finset (Fin n)) univ i
⊢ (s : (a : Fin n) → ℕ) i ≤ degreeOf i p

Tactic:
exact monomial_le_degreeOf i hs

Premises used: MvPolynomial.monomial_le_degreeOf
-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Fin n → Finset R
⊢ HDiv.hDiv (α := ℚ≥0)
      (↑(Finset.card.{u_1} (α := Fin n → R)
            ({x ∈ piFinset (δ := fun (a : Fin n) ↦ R) fun (i : Fin n) ↦ S i |
              Eq (α := R) ((eval x : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)})) :
        ℚ≥0)
      (∏ i : Fin n, (↑(#(S i)) : ℚ≥0)) ≤
    ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑(degreeOf i p) : ℚ≥0) (↑(#(S i)) : ℚ≥0)

Tactic:
calc
    _ ≤ p.support.sup fun s ↦ ∑ i, (s i / #(S i) : ℚ≥0) := schwartz_zippel_sup_sum hp S
    _ ≤ ∑ i, (p.degreeOf i / #(S i) : ℚ≥0) := Finset.sup_le fun s hs ↦ by
      gcongr with i; exact monomial_le_degreeOf i hs

Premises used: Finset.univ, HDiv.hDiv, Finset.sup_le, Nat.cast, MvPolynomial.support, MvPolynomial.schwartz_zippel_sup_sum, Finset.card, Finset.sup, DFunLike.coe, Finset.sum
-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
⊢ (↑(Finset.card.{u_1} (α := Fin n → R)
            ({f ∈ piFinset (δ := fun (a : Fin n) ↦ R) fun (x : Fin n) ↦ S |
              Eq (α := R) ((eval f : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)})) :
        ℚ≥0) /
      HPow.hPow (α := ℚ≥0) (↑(#S) : ℚ≥0) n =
    HDiv.hDiv (α := ℚ≥0)
      (↑(Finset.card.{u_1} (α := Fin n → R)
            ({f ∈ piFinset (δ := fun (a : Fin n) ↦ R) fun (x : Fin n) ↦ S |
              Eq (α := R) ((eval f : (a : MvPolynomial (Fin n) R) → R) p : R) (0 : R)})) :
        ℚ≥0)
      (∏ i : Fin n, (↑(#S) : ℚ≥0))

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
inl :
  (p.support.sup fun (s : Fin n →₀ ℕ) ↦
      ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(Finset.card.{u_1} (α := R) ∅) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (↑p.totalDegree : ℚ≥0) (↑(Finset.card.{u_1} (α := R) ∅) : ℚ≥0)
inr :
  ∀ (hs : S.Nonempty),
    (p.support.sup fun (s : Fin n →₀ ℕ) ↦
        ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#S) : ℚ≥0)) =
      HDiv.hDiv (α := ℚ≥0) (↑p.totalDegree : ℚ≥0) (↑(#S) : ℚ≥0)
⊢ (p.support.sup fun (s : Fin n →₀ ℕ) ↦
      ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#S) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (↑p.totalDegree : ℚ≥0) (↑(#S) : ℚ≥0)

Tactic:
obtain rfl | hs := S.eq_empty_or_nonempty

Premises used: rfl, Finset.eq_empty_or_nonempty
-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
inl : Eq (α := ℚ≥0) (p.support.sup fun (s : Fin n →₀ ℕ) ↦ 0) 0
⊢ (p.support.sup fun (s : Fin n →₀ ℕ) ↦
      ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(Finset.card.{u_1} (α := R) ∅) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (↑p.totalDegree : ℚ≥0) (↑(Finset.card.{u_1} (α := R) ∅) : ℚ≥0)

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
⊢ Eq (α := ℚ≥0) (p.support.sup fun (s : Fin n →₀ ℕ) ↦ 0) 0

Tactic:
simp only [← _root_.bot_eq_zero, sup_bot]

Premises used: Finset.sup_bot, bot_eq_zero
-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
inr :
  (p.support.sup fun (s : Fin n →₀ ℕ) ↦
      ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#S) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (p.support.sup fun (i : Fin n →₀ ℕ) ↦ (↑(i.sum fun (x : Fin n) (e : ℕ) ↦ e) : ℚ≥0))
      (↑(#S) : ℚ≥0)
⊢ (p.support.sup fun (s : Fin n →₀ ℕ) ↦
      ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#S) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (↑p.totalDegree : ℚ≥0) (↑(#S) : ℚ≥0)

Tactic:
simp_rw [totalDegree, Nat.cast_finsetSup]

Premises used: MvPolynomial.totalDegree, Nat.cast_finsetSup
-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ LE.le (α := ℚ≥0) 0 (↑(#S) : ℚ≥0)

Tactic:
positivity
-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
inr :
  Eq (α := ℚ≥0)
    (p.support.sup fun (s : Fin n →₀ ℕ) ↦
      ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#S) : ℚ≥0))
    (p.support.sup fun (i : Fin n →₀ ℕ) ↦
      HDiv.hDiv (α := ℚ≥0) (↑(i.sum fun (x : Fin n) (e : ℕ) ↦ e) : ℚ≥0) (↑(#S) : ℚ≥0))
⊢ (p.support.sup fun (s : Fin n →₀ ℕ) ↦
      ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#S) : ℚ≥0)) =
    HDiv.hDiv (α := ℚ≥0) (p.support.sup fun (i : Fin n →₀ ℕ) ↦ (↑(i.sum fun (x : Fin n) (e : ℕ) ↦ e) : ℚ≥0))
      (↑(#S) : ℚ≥0)

Tactic:
rw [sup_div₀ (by positivity)]

Premises used: Finset.sup_div₀
-- Module: Mathlib.Algebra.MvPolynomial.SchwartzZippel
Goal:
R : Type u_1
inst : CommRing R
inst_1 : IsDomain R
inst_2 : DecidableEq R
n : ℕ
p : MvPolynomial (Fin n) R
hp : p ≠ 0
S : Finset R
hs : S.Nonempty
⊢ Eq (α := ℚ≥0)
    (p.support.sup fun (s : Fin n →₀ ℕ) ↦
      ∑ i : Fin n, HDiv.hDiv (α := ℚ≥0) (↑((s : (a : Fin n) → ℕ) i) : ℚ≥0) (↑(#S) : ℚ≥0))
    (p.support.sup fun (i : Fin n →₀ ℕ) ↦
      HDiv.hDiv (α := ℚ≥0) (↑(i.sum fun (x : Fin n) (e : ℕ) ↦ e) : ℚ≥0) (↑(#S) : ℚ≥0))

Tactic:
simp [← sum_div, Finsupp.sum_fintype]

Premises used: Finsupp.sum_fintype, Finset.sum_div
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s : Set σ
rw :
  Eq (α := Subalgebra R (MvPolynomial σ R))
    (AlgHom.range (A := MvPolynomial.{u_1, u} (↑s : Type u_1) R) (aeval fun (x : (↑s : Type u_1)) ↦ X (↑x : σ)))
    (AlgHom.range (A := MvPolynomial.{u_1, u} { x : σ // x ∈ s } R)
      (aeval (X ∘ Subtype.val (p := fun (x : σ) ↦ x ∈ s))))
⊢ Eq (α := Subalgebra R (MvPolynomial σ R)) (supported R s)
    (AlgHom.range (A := MvPolynomial.{u_1, u} { x : σ // x ∈ s } R) (rename (Subtype.val (p := fun (x : σ) ↦ x ∈ s))))

Tactic:
rw [supported, Set.image_eq_range, adjoin_range_eq_range_aeval, rename]

Premises used: Set.image_eq_range, Algebra.adjoin_range_eq_range_aeval, MvPolynomial.rename, MvPolynomial.supported
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s : Set σ
⊢ Eq (α := Subalgebra R (MvPolynomial σ R))
    (AlgHom.range (A := MvPolynomial.{u_1, u} (↑s : Type u_1) R) (aeval fun (x : (↑s : Type u_1)) ↦ X (↑x : σ)))
    (AlgHom.range (A := MvPolynomial.{u_1, u} { x : σ // x ∈ s } R)
      (aeval (X ∘ Subtype.val (p := fun (x : σ) ↦ x ∈ s))))

Tactic:
congr
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s : Set σ
x : R
a :
  Eq (α := MvPolynomial σ R)
    (↑((AlgEquiv.symm (supportedEquivMvPolynomial s) : (a : MvPolynomial (↑s : Type u_1) R) → ↥(supported R s))
          ((C : (a : R) → MvPolynomial (↑s : Type u_1) R) x)) :
      MvPolynomial σ R)
    (↑((algebraMap R ↥(supported R s) : (a : R) → ↥(supported R s)) x) : MvPolynomial σ R)
⊢ Eq (α := ↥(supported R s))
    ((AlgEquiv.symm (supportedEquivMvPolynomial s) : (a : MvPolynomial (↑s : Type u_1) R) → ↥(supported R s))
        ((C : (a : R) → MvPolynomial (↑s : Type u_1) R) x) :
      ↥(supported R s))
    ((algebraMap R ↥(supported R s) : (a : R) → ↥(supported R s)) x : ↥(supported R s))

Tactic:
ext1
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s : Set σ
x : R
⊢ Eq (α := MvPolynomial σ R)
    (↑((AlgEquiv.symm (supportedEquivMvPolynomial s) : (a : MvPolynomial (↑s : Type u_1) R) → ↥(supported R s))
          ((C : (a : R) → MvPolynomial (↑s : Type u_1) R) x)) :
      MvPolynomial σ R)
    (↑((algebraMap R ↥(supported R s) : (a : R) → ↥(supported R s)) x) : MvPolynomial σ R)

Tactic:
simp [supportedEquivMvPolynomial, MvPolynomial.algebraMap_eq]

Premises used: MvPolynomial.algebraMap_eq, MvPolynomial.supportedEquivMvPolynomial
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s : Set σ
i : (↑s : Type u_1)
⊢ Eq (α := MvPolynomial σ R)
    (↑((AlgEquiv.symm (supportedEquivMvPolynomial s) : (a : MvPolynomial (↑s : Type u_1) R) → ↥(supported R s)) (X i)) :
      MvPolynomial σ R)
    (X (↑i : σ))

Tactic:
simp [supportedEquivMvPolynomial]

Premises used: MvPolynomial.supportedEquivMvPolynomial
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
p : MvPolynomial σ R
s : Set σ
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

Tactic:
rw [supported_eq_range_rename, AlgHom.mem_range]

Premises used: AlgHom.mem_range, MvPolynomial.supported_eq_range_rename
-- Module: Mathlib.Algebra.MvPolynomial.Supported
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
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
⊢ (∃ (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:
constructor
-- Module: Mathlib.Algebra.MvPolynomial.Supported
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

Tactic:
_root_.trans (Finset.coe_subset.2 (vars_rename _ _)) ?_

Premises used: Iff.mpr, trans, MvPolynomial.vars_rename, Finset.coe_subset
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s : Set σ
p : MvPolynomial.{u_1, u} { x : σ // x ∈ s } R
mp : (↑(Finset.image (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) p.vars) : Set σ) ⊆ s
⊢ (↑(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

Tactic:
refine _root_.trans (Finset.coe_subset.2 (vars_rename _ _)) ?_

Premises used: Iff.mpr, trans, MvPolynomial.vars_rename, Finset.coe_subset
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s : Set σ
p : MvPolynomial.{u_1, u} { x : σ // x ∈ s } R
⊢ (↑(Finset.image (Subtype.val (p := fun (x : σ) ↦ x ∈ s)) p.vars) : Set σ) ⊆ s

Tactic:
simp
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
p : MvPolynomial σ R
s : Set σ
hs : (↑p.vars : Set σ) ⊆ s
⊢ (↑p.vars : Set σ) ⊆ Set.range (ι := { x : σ // x ∈ s }) (Subtype.val (p := fun (x : σ) ↦ x ∈ s))

Tactic:
simpa
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
p : MvPolynomial σ R
s : Set σ
hs : (↑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:
exact exists_rename_eq_of_vars_subset_range p ((↑) : s → σ) Subtype.val_injective (by simpa)

Premises used: Subtype.val_injective, MvPolynomial.exists_rename_eq_of_vars_subset_range, Subtype.val
-- Module: Mathlib.Algebra.MvPolynomial.Supported
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
mpr 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
⊢ Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (supported R 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)

Premises used: Iff.mpr, trans, Subtype.val_injective, MvPolynomial.exists_rename_eq_of_vars_subset_range, AlgHom.mem_range, MvPolynomial.vars_rename, Subtype.val, MvPolynomial.supported_eq_range_rename, rfl, Finset.coe_subset
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s : Set σ
⊢ (↑(supported R s) : Set (MvPolynomial σ R)) = {p : MvPolynomial σ R | (↑p.vars : Set σ) ⊆ s}

Tactic:
Set.ext fun _ ↦ mem_supported

Premises used: Set.ext, MvPolynomial.mem_supported
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
p : MvPolynomial σ R
rw rw₁ : (↑p.vars : Set σ) ⊆ (↑p.vars : Set σ)
⊢ Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (supported R (↑p.vars : Set σ)) p

Tactic:
rw [mem_supported]

Premises used: MvPolynomial.mem_supported
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s : Set σ
⊢ Eq (α := Subalgebra R (MvPolynomial σ R)) (supported R s) (adjoin R (X '' s))

Tactic:
rfl

Premises used: MvPolynomial.supported, rfl
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
⊢ Eq (α := Subalgebra R (MvPolynomial σ R)) (supported R Set.univ) ⊤

Tactic:
simp [Algebra.eq_top_iff, mem_supported]

Premises used: MvPolynomial.mem_supported, Algebra.eq_top_iff
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
⊢ Eq (α := Subalgebra R (MvPolynomial σ R)) (supported R ∅) ⊥

Tactic:
simp [supported_eq_adjoin_X]

Premises used: MvPolynomial.supported_eq_adjoin_X
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s t : Set σ
st : s ⊆ t
⊢ LE.le (α := Subalgebra R (MvPolynomial σ R)) (supported R s) (supported R t)

Tactic:
Algebra.adjoin_mono (Set.image_mono st)

Premises used: Set.Mem, Set.image_mono, Algebra.adjoin_mono
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s : Set σ
inst_1 : Nontrivial R
i : σ
⊢ Membership.mem (γ := Subalgebra R (MvPolynomial σ R)) (supported R s) (X i) ↔ i ∈ s

Tactic:
simp [mem_supported]

Premises used: MvPolynomial.mem_supported
-- Module: Mathlib.Algebra.MvPolynomial.Supported
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
mpr : s ⊆ t → LE.le (α := Subalgebra R (MvPolynomial σ R)) (supported R s) (supported R t)
⊢ LE.le (α := Subalgebra R (MvPolynomial σ R)) (supported R s) (supported R t) ↔ s ⊆ t

Tactic:
constructor
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s t : Set σ
inst_1 : Nontrivial R
h : LE.le (α := Subalgebra R (MvPolynomial σ R)) (supported R s) (supported R t)
i : σ
⊢ i ∈ s → i ∈ t

Tactic:
simpa using @h (X i)
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s t : Set σ
inst_1 : Nontrivial R
⊢ s ⊆ t → LE.le (α := Subalgebra R (MvPolynomial σ R)) (supported R s) (supported R t)

Tactic:
supported_mono

Premises used: MvPolynomial.supported_mono
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
s t : Set σ
inst_1 : Nontrivial R
⊢ s ⊆ t → LE.le (α := Subalgebra R (MvPolynomial σ R)) (supported R s) (supported R t)

Tactic:
exact supported_mono

Premises used: MvPolynomial.supported_mono
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
R : Type u
inst : CommSemiring R
inst_1 : Nontrivial R
⊢ StrictMono (α := Set σ) (β := Subalgebra R (MvPolynomial σ R)) (supported R)

Tactic:
strictMono_of_le_iff_le fun _ _ ↦ supported_le_supported_iff.symm

Premises used: strictMono_of_le_iff_le, MvPolynomial.supported_le_supported_iff, Iff.symm
-- Module: Mathlib.Algebra.MvPolynomial.Supported
Goal:
σ : Type u_1
s : Set σ
R : Type u_2
inst : CommRing R
F : MvPolynomial σ ℤ
hF : (↑F.vars : Set σ) ⊆ s
⊢ ∃ (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

Premises used: AlgHom.mem_range, MvPolynomial.mem_supported, MvPolynomial.supported_eq_range_rename
-- Module: Mathlib.Algebra.MvPolynomial.Supported
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
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
⊢ ∃ (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
-- Module: Mathlib.Algebra.MvPolynomial.Supported
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
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)
⊢ ∃ (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:
use fun z ↦ aeval z F'

Premises used: MvPolynomial.aeval, DFunLike.coe