awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
⊢ (φ ^ n).vars ⊆ φ.vars
have zero : (HPow.hPow (β := ℕ) φ 0).vars ⊆ φ.vars
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ']
    apply Finset.Subset.trans (vars_mul _ _)
    exact Finset.union_subset (Finset.Subset.refl _) ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
zero : (HPow.hPow (β := ℕ) φ 0).vars ⊆ φ.vars
⊢ (φ ^ n).vars ⊆ φ.vars
have succ : ∀ (n : ℕ) (ih : (φ ^ n).vars ⊆ φ.vars), (φ ^ (n + 1)).vars ⊆ φ.vars
Tactic: induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ']
    apply Finset.Subset.trans (vars_mul _ _)
    exact Finset.union_subset (Finset.Subset.refl _) ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
⊢ (φ ^ n).vars ⊆ φ.vars
have zero : (HPow.hPow (β := ℕ) φ 0).vars ⊆ φ.vars
Tactic: classical
  induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ']
    apply Finset.Subset.trans (vars_mul _ _)
    exact Finset.union_subset (Finset.Subset.refl _) ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
φ : MvPolynomial σ R
n : ℕ
zero : (HPow.hPow (β := ℕ) φ 0).vars ⊆ φ.vars
⊢ (φ ^ n).vars ⊆ φ.vars
have succ : ∀ (n : ℕ) (ih : (φ ^ n).vars ⊆ φ.vars), (φ ^ (n + 1)).vars ⊆ φ.vars
Tactic: classical
  induction n with
  | zero => simp
  | succ n ih =>
    rw [pow_succ']
    apply Finset.Subset.trans (vars_mul _ _)
    exact Finset.union_subset (Finset.Subset.refl _) ih
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq σ
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
hs : a ∉ s
hsub : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ s, f i)) (s.biUnion fun (i : ι) ↦ (f i).vars)
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ insert a s, f i))
    ((insert a s).biUnion fun (i : ι) ↦ (f i).vars)
have insert : (f a * ∏ i ∈ s, f i).vars ⊆ (f a).vars ∪ s.biUnion fun (i : ι) ↦ (f i).vars
Tactic: simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq σ
f : ι → MvPolynomial σ R
a : ι
s : Finset ι
hs : a ∉ s
hsub : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ s, f i)) (s.biUnion fun (i : ι) ↦ (f i).vars)
⊢ (f a * ∏ i ∈ s, f i).vars ⊆ (f a).vars ∪ s.biUnion fun (i : ι) ↦ (f i).vars
have insert : (f a).vars ∪ vars.{u, u_1} (R := R) (∏ i ∈ s, f i) ⊆ (f a).vars ∪ s.biUnion fun (i : ι) ↦ (f i).vars
Tactic: apply Finset.Subset.trans (vars_mul _ _)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ s, f i)) (s.biUnion fun (i : ι) ↦ (f i).vars)
have empty : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ ∅, f i)) (Finset.biUnion ∅ fun (i : ι) ↦ (f i).vars)
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ hs hsub =>
    simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
    apply Finset.Subset.trans (vars_mul _ _)
    exact Finset.union_subset_union (Finset.Subset.refl _) hsub
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
empty : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ ∅, f i)) (Finset.biUnion ∅ fun (i : ι) ↦ (f i).vars)
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ s, f i)) (s.biUnion fun (i : ι) ↦ (f i).vars)
have insert : ∀ (a : ι) (s : Finset ι) (hs : a ∉ s)
  (hsub : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ s, f i)) (s.biUnion fun (i : ι) ↦ (f i).vars)),
  Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ insert a s, f i))
    ((insert a s).biUnion fun (i : ι) ↦ (f i).vars)
Tactic: induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ hs hsub =>
    simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
    apply Finset.Subset.trans (vars_mul _ _)
    exact Finset.union_subset_union (Finset.Subset.refl _) hsub
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ s, f i)) (s.biUnion fun (i : ι) ↦ (f i).vars)
have empty : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ ∅, f i)) (Finset.biUnion ∅ fun (i : ι) ↦ (f i).vars)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ hs hsub =>
    simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
    apply Finset.Subset.trans (vars_mul _ _)
    exact Finset.union_subset_union (Finset.Subset.refl _) hsub
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
inst_1 : DecidableEq σ
s : Finset ι
f : ι → MvPolynomial σ R
empty : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ ∅, f i)) (Finset.biUnion ∅ fun (i : ι) ↦ (f i).vars)
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ s, f i)) (s.biUnion fun (i : ι) ↦ (f i).vars)
have insert : ∀ (a : ι) (s : Finset ι) (hs : a ∉ s)
  (hsub : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ s, f i)) (s.biUnion fun (i : ι) ↦ (f i).vars)),
  Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∏ i ∈ insert a s, f i))
    ((insert a s).biUnion fun (i : ι) ↦ (f i).vars)
Tactic: classical
  induction s using Finset.induction_on with
  | empty => simp
  | insert _ _ hs hsub =>
    simp only [hs, Finset.biUnion_insert, Finset.prod_insert, not_false_iff]
    apply Finset.Subset.trans (vars_mul _ _)
    exact Finset.union_subset_union (Finset.Subset.refl _) hsub
Cleared hypotheses: s
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
σ : Type u_1
A : Type u_3
inst : CommRing A
inst_1 : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
⊢ (HMul.hMul (α := MvPolynomial σ A) ((C : (a : A) → MvPolynomial σ A) a : MvPolynomial σ A) φ).vars = φ.vars
have h : ∀ (i : σ),
  i ∈ (HMul.hMul (α := MvPolynomial σ A) ((C : (a : A) → MvPolynomial σ A) a : MvPolynomial σ A) φ).vars ↔ i ∈ φ.vars
Tactic: ext1 i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
σ : Type u_1
A : Type u_3
inst : CommRing A
inst_1 : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ i ∈ (HMul.hMul (α := MvPolynomial σ A) ((C : (a : A) → MvPolynomial σ A) a : MvPolynomial σ A) φ).vars ↔ i ∈ φ.vars
have h : (∃ (d : σ →₀ ℕ),
    coeff d (HMul.hMul (α := MvPolynomial σ A) ((C : (a : A) → MvPolynomial σ A) a : MvPolynomial σ A) φ) ≠ 0 ∧
      i ∈ d.support) ↔
  ∃ (d : σ →₀ ℕ), coeff d φ ≠ 0 ∧ i ∈ d.support
Tactic: simp only [mem_vars_iff_mem_support, mem_support_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
σ : Type u_1
A : Type u_3
inst : CommRing A
inst_1 : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
⊢ (∃ (d : σ →₀ ℕ),
      coeff d (HMul.hMul (α := MvPolynomial σ A) ((C : (a : A) → MvPolynomial σ A) a : MvPolynomial σ A) φ) ≠ 0 ∧
        i ∈ d.support) ↔
    ∃ (d : σ →₀ ℕ), coeff d φ ≠ 0 ∧ i ∈ d.support
have h : ∀ (a_1 : σ →₀ ℕ),
  coeff a_1 (HMul.hMul (α := MvPolynomial σ A) ((C : (a : A) → MvPolynomial σ A) a : MvPolynomial σ A) φ) ≠ 0 ∧
      i ∈ a_1.support ↔
    coeff a_1 φ ≠ 0 ∧ i ∈ a_1.support
Tactic: apply exists_congr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
σ : Type u_1
A : Type u_3
inst : CommRing A
inst_1 : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
d : σ →₀ ℕ
⊢ coeff d (HMul.hMul (α := MvPolynomial σ A) ((C : (a : A) → MvPolynomial σ A) a : MvPolynomial σ A) φ) ≠ 0 ∧
      i ∈ d.support ↔
    coeff d φ ≠ 0 ∧ i ∈ d.support
have h : a * coeff d φ ≠ 0 ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
Tactic: rw [coeff_C_mul, mul_ne_zero_iff, eq_true ha, true_and]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
σ : Type u_1
A : Type u_3
inst : CommRing A
inst_1 : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
d : σ →₀ ℕ
h : a * coeff d φ ≠ 0 ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
⊢ coeff d (HMul.hMul (α := MvPolynomial σ A) ((C : (a : A) → MvPolynomial σ A) a : MvPolynomial σ A) φ) ≠ 0 ∧
      i ∈ d.support ↔
    coeff d φ ≠ 0 ∧ i ∈ d.support
have h₁ : (a ≠ 0 ∧ coeff d φ ≠ 0) ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
Tactic: rw [coeff_C_mul, mul_ne_zero_iff, eq_true ha, true_and]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
σ : Type u_1
A : Type u_3
inst : CommRing A
inst_1 : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
d : σ →₀ ℕ
h : a * coeff d φ ≠ 0 ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
h₁ : (a ≠ 0 ∧ coeff d φ ≠ 0) ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
⊢ coeff d (HMul.hMul (α := MvPolynomial σ A) ((C : (a : A) → MvPolynomial σ A) a : MvPolynomial σ A) φ) ≠ 0 ∧
      i ∈ d.support ↔
    coeff d φ ≠ 0 ∧ i ∈ d.support
have h₂ : (True ∧ coeff d φ ≠ 0) ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
Tactic: rw [coeff_C_mul, mul_ne_zero_iff, eq_true ha, true_and]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
σ : Type u_1
A : Type u_3
inst : CommRing A
inst_1 : NoZeroDivisors A
a : A
ha : a ≠ 0
φ : MvPolynomial σ A
i : σ
d : σ →₀ ℕ
h : a * coeff d φ ≠ 0 ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
h₁ : (a ≠ 0 ∧ coeff d φ ≠ 0) ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
h₂ : (True ∧ coeff d φ ≠ 0) ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
⊢ coeff d (HMul.hMul (α := MvPolynomial σ A) ((C : (a : A) → MvPolynomial σ A) a : MvPolynomial σ A) φ) ≠ 0 ∧
      i ∈ d.support ↔
    coeff d φ ≠ 0 ∧ i ∈ d.support
have h₃ : coeff d φ ≠ 0 ∧ i ∈ d.support ↔ coeff d φ ≠ 0 ∧ i ∈ d.support
Tactic: rw [coeff_C_mul, mul_ne_zero_iff, eq_true ha, true_and]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
a : ι
s : Finset ι
has : a ∉ s
hsum : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ s, φ i)) (s.biUnion fun (i : ι) ↦ (φ i).vars)
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ insert a s, φ i))
    ((insert a s).biUnion fun (i : ι) ↦ (φ i).vars)
have insert : (φ a + ∑ x ∈ s, φ x).vars ⊆ (φ a).vars ∪ s.biUnion fun (i : ι) ↦ (φ i).vars
Tactic: rw [Finset.biUnion_insert, Finset.sum_insert has]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ t, φ i)) (t.biUnion fun (i : ι) ↦ (φ i).vars)
have empty : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ ∅, φ i)) (Finset.biUnion ∅ fun (i : ι) ↦ (φ i).vars)
Tactic: induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ has hsum =>
    rw [Finset.biUnion_insert, Finset.sum_insert has]
    refine Finset.Subset.trans
      (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) ?_)
    assumption
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
empty : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ ∅, φ i)) (Finset.biUnion ∅ fun (i : ι) ↦ (φ i).vars)
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ t, φ i)) (t.biUnion fun (i : ι) ↦ (φ i).vars)
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (hsum : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ s, φ i)) (s.biUnion fun (i : ι) ↦ (φ i).vars)),
  Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ insert a s, φ i))
    ((insert a s).biUnion fun (i : ι) ↦ (φ i).vars)
Tactic: induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ has hsum =>
    rw [Finset.biUnion_insert, Finset.sum_insert has]
    refine Finset.Subset.trans
      (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) ?_)
    assumption
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ t, φ i)) (t.biUnion fun (i : ι) ↦ (φ i).vars)
have empty : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ ∅, φ i)) (Finset.biUnion ∅ fun (i : ι) ↦ (φ i).vars)
Tactic: classical
  induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ has hsum =>
    rw [Finset.biUnion_insert, Finset.sum_insert has]
    refine Finset.Subset.trans
      (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) ?_)
    assumption
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
empty : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ ∅, φ i)) (Finset.biUnion ∅ fun (i : ι) ↦ (φ i).vars)
⊢ Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ t, φ i)) (t.biUnion fun (i : ι) ↦ (φ i).vars)
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (hsum : Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ s, φ i)) (s.biUnion fun (i : ι) ↦ (φ i).vars)),
  Subset.{u_1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ insert a s, φ i))
    ((insert a s).biUnion fun (i : ι) ↦ (φ i).vars)
Tactic: classical
  induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ has hsum =>
    rw [Finset.biUnion_insert, Finset.sum_insert has]
    refine Finset.Subset.trans
      (vars_add_subset _ _) (Finset.union_subset_union (Finset.Subset.refl _) ?_)
    assumption
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Finset σ) Disjoint fun (i : ι) ↦ (φ i).vars)
a : ι
s : Finset ι
has : a ∉ s
hsum : Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ s, φ i)) (s.biUnion fun (i : ι) ↦ (φ i).vars)
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ insert a s, φ i))
    ((insert a s).biUnion fun (i : ι) ↦ (φ i).vars)
have insert : Disjoint (φ a).vars (vars.{u, u_1} (R := R) (∑ x ∈ s, φ x))
Tactic: rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
h : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint.{u_1} (α := Finset σ) ((fun (i : ι) ↦ (φ i).vars) i) ((fun (i : ι) ↦ (φ i).vars) j)
a : ι
s : Finset ι
has : a ∉ s
hsum : Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ s, φ i)) (s.biUnion fun (i : ι) ↦ (φ i).vars)
⊢ Disjoint (φ a).vars (vars.{u, u_1} (R := R) (∑ x ∈ s, φ x))
have insert : ∀ (h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ a ∈ (φ i).vars, ∀ b ∈ (φ j).vars, a ≠ b),
  ∀ a_1 ∈ (φ a).vars, ∀ (b : σ), Membership.mem (γ := Finset σ) (vars.{u, u_1} (R := R) (∑ x ∈ s, φ x)) b → a_1 ≠ b
Tactic: simp only [Finset.disjoint_iff_ne] 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
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Finset σ) Disjoint fun (i : ι) ↦ (φ i).vars)
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ t, φ i)) (t.biUnion fun (i : ι) ↦ (φ i).vars)
have empty : Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ ∅, φ i)) (Finset.biUnion ∅ fun (i : ι) ↦ (φ i).vars)
Tactic: induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ has hsum =>
    rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
    unfold Pairwise onFun at h
    simp only [Finset.disjoint_iff_ne] at h ⊢
    grind
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Finset σ) Disjoint fun (i : ι) ↦ (φ i).vars)
empty : Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ ∅, φ i)) (Finset.biUnion ∅ fun (i : ι) ↦ (φ i).vars)
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ t, φ i)) (t.biUnion fun (i : ι) ↦ (φ i).vars)
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (hsum : Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ s, φ i)) (s.biUnion fun (i : ι) ↦ (φ i).vars)),
  Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ insert a s, φ i))
    ((insert a s).biUnion fun (i : ι) ↦ (φ i).vars)
Tactic: induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ has hsum =>
    rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
    unfold Pairwise onFun at h
    simp only [Finset.disjoint_iff_ne] at h ⊢
    grind
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Finset σ) Disjoint fun (i : ι) ↦ (φ i).vars)
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ t, φ i)) (t.biUnion fun (i : ι) ↦ (φ i).vars)
have empty : Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ ∅, φ i)) (Finset.biUnion ∅ fun (i : ι) ↦ (φ i).vars)
Tactic: classical
  induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ has hsum =>
    rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
    unfold Pairwise onFun at h
    simp only [Finset.disjoint_iff_ne] at h ⊢
    grind
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst_1 : DecidableEq σ
h : Pairwise.{u_3} (α := ι) (onFun.{u_3 + 1, u_1 + 1, 1} (β := Finset σ) Disjoint fun (i : ι) ↦ (φ i).vars)
empty : Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ ∅, φ i)) (Finset.biUnion ∅ fun (i : ι) ↦ (φ i).vars)
⊢ Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ t, φ i)) (t.biUnion fun (i : ι) ↦ (φ i).vars)
have insert : ∀ (a : ι) (s : Finset ι) (has : a ∉ s)
  (hsum : Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ s, φ i)) (s.biUnion fun (i : ι) ↦ (φ i).vars)),
  Eq.{u_1 + 1} (α := Finset σ) (vars.{u, u_1} (R := R) (∑ i ∈ insert a s, φ i))
    ((insert a s).biUnion fun (i : ι) ↦ (φ i).vars)
Tactic: classical
  induction t using Finset.induction_on with
  | empty => simp
  | insert _ _ has hsum =>
    rw [Finset.biUnion_insert, Finset.sum_insert has, vars_add_of_disjoint, hsum]
    unfold Pairwise onFun at h
    simp only [Finset.disjoint_iff_ne] at h ⊢
    grind
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
e : ℕ
r : R
he : e ≠ 0
hr : r ≠ 0
⊢ Eq (α := Finset σ) (vars.{u, u_1} (R := R) ((monomial (Finsupp.single i e) : (a : R) → MvPolynomial σ R) r)) {i}
have rw : Finsupp.support (Finsupp.single i e) = {i}
Tactic: rw [vars_monomial hr, Finsupp.support_single _ he]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
i : σ
e : ℕ
r : R
he : e ≠ 0
hr : r ≠ 0
rw : Finsupp.support (Finsupp.single i e) = {i}
⊢ Eq (α := Finset σ) (vars.{u, u_1} (R := R) ((monomial (Finsupp.single i e) : (a : R) → MvPolynomial σ R) r)) {i}
have rw₁ : Eq (α := Finset σ) {i} {i}
Tactic: rw [vars_monomial hr, Finsupp.support_single _ he]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : DecidableEq σ
⊢ p.vars = p.support.biUnion Finsupp.support
have h : ∀ (i : σ), i ∈ p.vars ↔ i ∈ p.support.biUnion Finsupp.support
Tactic: ext i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : DecidableEq σ
i : σ
⊢ i ∈ p.vars ↔ i ∈ p.support.biUnion Finsupp.support
have h : (∃ d ∈ p.support, i ∈ d.support) ↔ i ∈ p.support.biUnion Finsupp.support
Tactic: rw [mem_vars_iff_mem_support, Finset.mem_biUnion]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
p : MvPolynomial σ R
inst_1 : DecidableEq σ
i : σ
h : (∃ d ∈ p.support, i ∈ d.support) ↔ i ∈ p.support.biUnion Finsupp.support
⊢ i ∈ p.vars ↔ i ∈ p.support.biUnion Finsupp.support
have h₁ : (∃ d ∈ p.support, i ∈ d.support) ↔ ∃ a ∈ p.support, i ∈ a.support
Tactic: rw [mem_vars_iff_mem_support, Finset.mem_biUnion]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
| ((eval₂Hom f g : (a : MvPolynomial σ R) → S) p : S)
have rw : ((eval₂Hom f g : (a : MvPolynomial σ R) → S) (∑ v ∈ p.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p)) :
  S)
Tactic: rw [p.as_sum]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
⊢ Eq.{v + 1} (α := S) ((eval₂Hom f g : (a : MvPolynomial σ R) → S) p : S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
have conv_lhs : Eq.{v + 1} (α := S)
  ((eval₂Hom f g : (a : MvPolynomial σ R) → S)
      (∑ v ∈ p.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p)) :
    S)
  ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
Tactic: conv_lhs => rw [p.as_sum]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Variables (goal)
Goal:
R : Type u
S : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S
f : R →+* S
g : σ → S
p : MvPolynomial σ R
hp : ∀ i ∈ p.vars, g i = 0
⊢ Eq.{v + 1} (α := S)
    ((eval₂Hom f g : (a : MvPolynomial σ R) → S)
        (∑ v ∈ p.support, (monomial v : (a : R) → MvPolynomial σ R) (coeff v p)) :
      S)
    ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
have simp : Eq.{v + 1} (α := S)
  (∑ x ∈ p.support,
      HMul.hMul (α := S) (β := S) ((f : (a : R) → S) (coeff x p) : S) (x.prod fun (i : σ) (k : ℕ) ↦ g i ^ k : S) :
    S)
  ((f : (a : R) → S) ((constantCoeff : (a : MvPolynomial σ R) → R) p : R) : S)
Tactic: simp only [map_sum, eval₂Hom_monomial]