awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
p q : MvPolynomial σ R
hp :
  Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
hq :
  Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) q : S₁)
⊢ Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) (p + q) : S₁)
have a : Membership.mem (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
  (HAdd.hAdd (α := S₁) (β := S₁) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
    ((aeval f : (a : MvPolynomial σ R) → S₁) q : S₁))
Tactic: rw [map_add]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
p : MvPolynomial σ R
n : σ
h :
  Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
⊢ Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) (p * X n) : S₁)
have a : Membership.mem (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
  (HMul.hMul (α := S₁) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) (f n))
Tactic: simp only [map_mul, aeval_X]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
p : MvPolynomial σ R
⊢ Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
have a : ∀ (a : R),
  Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) : S₁)
Tactic: induction p using induction_on with
    | C a => exact aeval_C f a ▸ Subsemiring.subset_closure (Or.inl (Set.mem_range_self a))
    | add p q hp hq => rw [map_add]; exact Subalgebra.add_mem _ hp hq
    | mul_X p n h =>
      simp only [map_mul, aeval_X]
      exact Subalgebra.mul_mem _ h (Algebra.subset_adjoin (Set.mem_range_self n))
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
p : MvPolynomial σ R
a :
  ∀ (a : R),
    Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
      ((aeval f : (a : MvPolynomial σ R) → S₁) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) : S₁)
⊢ Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
have a₁ : ∀ (p q : MvPolynomial σ R)
  (hp :
    Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
      ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁))
  (hq :
    Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
      ((aeval f : (a : MvPolynomial σ R) → S₁) q : S₁)),
  Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) (p + q) : S₁)
Tactic: induction p using induction_on with
    | C a => exact aeval_C f a ▸ Subsemiring.subset_closure (Or.inl (Set.mem_range_self a))
    | add p q hp hq => rw [map_add]; exact Subalgebra.add_mem _ hp hq
    | mul_X p n h =>
      simp only [map_mul, aeval_X]
      exact Subalgebra.mul_mem _ h (Algebra.subset_adjoin (Set.mem_range_self n))
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
p : MvPolynomial σ R
a :
  ∀ (a : R),
    Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
      ((aeval f : (a : MvPolynomial σ R) → S₁) ((C : (a : R) → MvPolynomial σ R) a : MvPolynomial σ R) : S₁)
a₁ :
  ∀ (p q : MvPolynomial σ R)
    (hp :
      Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
        ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁))
    (hq :
      Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
        ((aeval f : (a : MvPolynomial σ R) → S₁) q : S₁)),
    Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
      ((aeval f : (a : MvPolynomial σ R) → S₁) (p + q) : S₁)
⊢ Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
have a₂ : ∀ (p : MvPolynomial σ R) (n : σ)
  (h :
    Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
      ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)),
  Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
    ((aeval f : (a : MvPolynomial σ R) → S₁) (p * X n) : S₁)
Tactic: induction p using induction_on with
    | C a => exact aeval_C f a ▸ Subsemiring.subset_closure (Or.inl (Set.mem_range_self a))
    | add p q hp hq => rw [map_add]; exact Subalgebra.add_mem _ hp hq
    | mul_X p n h =>
      simp only [map_mul, aeval_X]
      exact Subalgebra.mul_mem _ h (Algebra.subset_adjoin (Set.mem_range_self n))
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
⊢ LE.le (α := Subalgebra R S₁) (Algebra.adjoin R (range f)) (AlgHom.range (aeval f))
have a : range f ⊆ (↑(AlgHom.range (aeval f)) : Set S₁)
Tactic: rw [Algebra.adjoin_le_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
i : σ
⊢ f i ∈ (↑(AlgHom.range (aeval f)) : Set S₁)
have w : MvPolynomial σ R
Tactic: use X i, by aesop
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
f : σ → S₁
i : σ
w : MvPolynomial σ R
⊢ f i ∈ (↑(AlgHom.range (aeval f)) : Set S₁)
have h : (AlgHom.toRingHom (aeval f) : (a : MvPolynomial σ R) → S₁) (X i) = f i
Tactic: use X i, by aesop
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
⊢ Eq (α := MvPolynomial σ R →+* S₂) (eval₂Hom f 0) (f.comp constantCoeff)
have hC : ∀ (x : R),
  Eq.{w + 1} (α := S₂) ((RingHom.comp (β := MvPolynomial σ R) (eval₂Hom f 0) C : (a : R) → S₂) x : S₂)
    ((RingHom.comp (β := MvPolynomial σ R) (f.comp constantCoeff) C : (a : R) → S₂) x : S₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
hC :
  ∀ (x : R),
    Eq.{w + 1} (α := S₂) ((RingHom.comp (β := MvPolynomial σ R) (eval₂Hom f 0) C : (a : R) → S₂) x : S₂)
      ((RingHom.comp (β := MvPolynomial σ R) (f.comp constantCoeff) C : (a : R) → S₂) x : S₂)
⊢ Eq (α := MvPolynomial σ R →+* S₂) (eval₂Hom f 0) (f.comp constantCoeff)
have hX : ∀ (i : σ),
  Eq.{w + 1} (α := S₂) ((eval₂Hom f 0 : (a : MvPolynomial σ R) → S₂) (X i) : S₂)
    ((f.comp constantCoeff : (a : MvPolynomial σ R) → S₂) (X i) : S₂)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
⊢ Eq.{w + 1} (α := S₂) ((eval₂Hom f g : (a : MvPolynomial σ R) → S₂) φ : S₂) (0 : S₂)
have rw : Eq.{w + 1} (α := S₂)
  (∑ x ∈ φ.support,
    (eval₂Hom f g : (a : MvPolynomial σ R) → S₂)
      ((monomial x : (a : R) → MvPolynomial σ R) (coeff x φ) : MvPolynomial σ R))
  0
Tactic: rw [φ.as_sum, map_sum]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
⊢ Eq.{w + 1} (α := S₂)
    (∑ x ∈ φ.support,
      (eval₂Hom f g : (a : MvPolynomial σ R) → S₂)
        ((monomial x : (a : R) → MvPolynomial σ R) (coeff x φ) : MvPolynomial σ R))
    0
have refine : ∀ (d : σ →₀ ℕ) (hd : d ∈ φ.support),
  Eq.{w + 1} (α := S₂)
    ((eval₂Hom f g : (a : MvPolynomial σ R) → S₂)
        ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R) :
      S₂)
    (0 : S₂)
Tactic: refine Finset.sum_eq_zero fun d hd => ?_
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
d : σ →₀ ℕ
hd : d ∈ φ.support
⊢ Eq.{w + 1} (α := S₂)
    ((eval₂Hom f g : (a : MvPolynomial σ R) → S₂)
        ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R) :
      S₂)
    (0 : S₂)
have obtain : ∀ (i : σ) (hi : i ∈ d.support) (hgi : g i = 0),
  Eq.{w + 1} (α := S₂)
    ((eval₂Hom f g : (a : MvPolynomial σ R) → S₂)
        ((monomial d : (a : R) → MvPolynomial σ R) (coeff d φ) : MvPolynomial σ R) :
      S₂)
    (0 : S₂)
Tactic: obtain ⟨i, hi, hgi⟩ : ∃ i ∈ d.support, g i = 0 := h d (Finsupp.mem_support_iff.mp hd)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₂
f : R →+* S₂
g : σ → S₂
φ : MvPolynomial σ R
h : ∀ (d : σ →₀ ℕ), coeff d φ ≠ 0 → ∃ i ∈ d.support, g i = 0
d : σ →₀ ℕ
hd : d ∈ φ.support
i : σ
hi : i ∈ d.support
hgi : g i = 0
⊢ HPow.hPow (β := ℕ) (g i) ((d : (a : σ) → ℕ) i : ℕ) = 0
have rw : Ne (α := ℕ) ((d : (a : σ) → ℕ) i : ℕ) (0 : ℕ)
Tactic: rw [hgi, zero_pow]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
s : Set S₁
⊢ Eq (α := Subalgebra R S₁) (Algebra.adjoin R s)
    (AlgHom.range (A := MvPolynomial.{v, u} { x : S₁ // x ∈ s } R) (aeval (Subtype.val (p := fun (x : S₁) ↦ x ∈ s))))
have rw : Eq (α := Subalgebra R S₁) (Algebra.adjoin R s)
  (Algebra.adjoin R (range (ι := { x : S₁ // x ∈ s }) (Subtype.val (p := fun (x : S₁) ↦ x ∈ s))))
Tactic: rw [← Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : Algebra R S₁
s : Set S₁
rw :
  Eq (α := Subalgebra R S₁) (Algebra.adjoin R s)
    (Algebra.adjoin R (range (ι := { x : S₁ // x ∈ s }) (Subtype.val (p := fun (x : S₁) ↦ x ∈ s))))
⊢ Eq (α := Subalgebra R S₁) (Algebra.adjoin R s)
    (AlgHom.range (A := MvPolynomial.{v, u} { x : S₁ // x ∈ s } R) (aeval (Subtype.val (p := fun (x : S₁) ↦ x ∈ s))))
have rw₁ : Eq (α := Subalgebra R S₁) (Algebra.adjoin R s) (Algebra.adjoin R s)
Tactic: rw [← Algebra.adjoin_range_eq_range_aeval, Subtype.range_coe]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
σ : Type u_1
S : Type u_2
inst : CommSemiring S
⊢ Eq (α := (X : σ → S) → MvPolynomial σ S →ₐ[S] S) (aevalTower (AlgHom.id S S)) aeval
have h : ∀ (x : σ → S) (i : σ),
  Eq.{u_2 + 1} (α := S) ((aevalTower (AlgHom.id S S) x : (a : MvPolynomial σ S) → S) (X i) : S)
    ((aeval x : (a : MvPolynomial σ S) → S) (X i) : S)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
σ : Type u_1
S : Type u_2
A : Type u_3
inst : CommSemiring S
inst_1 : CommSemiring A
inst_2 : Algebra S A
⊢ Eq (α := (X : σ → A) → MvPolynomial σ S →ₐ[S] A) (aevalTower (Algebra.ofId S A)) aeval
have h : ∀ (x : σ → A) (i : σ),
  Eq.{u_3 + 1} (α := A) ((aevalTower (Algebra.ofId S A) x : (a : MvPolynomial σ S) → A) (X i) : A)
    ((aeval x : (a : MvPolynomial σ S) → A) (X i) : A)
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
v : σ → S
hv : ∀ (i : σ), v i ∈ s
i : σ →₀ ℕ
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
have pos : ∀ (hi : i ∈ p.support), Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
Tactic: by_cases hi : i ∈ p.support
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
v : σ → S
hv : ∀ (i : σ), v i ∈ s
i : σ →₀ ℕ
pos : ∀ (hi : i ∈ p.support), Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
have neg : ∀ (hi : i ∉ p.support), Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
Tactic: by_cases hi : i ∈ p.support
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
v : σ → S
hv : ∀ (i : σ), v i ∈ s
i : σ →₀ ℕ
hi : i ∉ p.support
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
have neg : 0 ∈ s
Tactic: rw [MvPolynomial.notMem_support_iff.1 hi, f.map_zero]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f : R →+* S
p : MvPolynomial σ R
s : subS
hs : ∀ i ∈ p.support, Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
v : σ → S
hv : ∀ (i : σ), v i ∈ s
⊢ eval₂ f v p ∈ s
have hs₁ : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f : (a : R) → S) (coeff i p) : S)
Tactic: replace hs : ∀ i, f (p.coeff i) ∈ s := by
    intro i
    by_cases hi : i ∈ p.support
    · exact hs i hi
    · rw [MvPolynomial.notMem_support_iff.1 hi, f.map_zero]
      exact zero_mem s
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f_1 : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.support
h : b ≠ 0
ih :
  ∀ (hs : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)), eval₂ f_1 v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    Membership.mem.{u_2, u_3} (α := S) s
      ((f_1 : (a : R) → S)
          (coeff i
            (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) f)) :
        S)
⊢ eval₂ f_1 v (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) f) ∈ s
have monomial_add : HMul.hMul (α := S) (β := S) ((f_1 : (a : R) → S) b : S) (a.prod fun (n : σ) (e : ℕ) ↦ v n ^ e : S) + eval₂ f_1 v f ∈ s
Tactic: rw [eval₂_add, eval₂_monomial]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f_1 : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.support
h : b ≠ 0
ih :
  ∀ (hs : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)), eval₂ f_1 v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    Membership.mem.{u_2, u_3} (α := S) s
      ((f_1 : (a : R) → S)
          (coeff i
            (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) f)) :
        S)
⊢ HMul.hMul (α := S) (β := S) ((f_1 : (a : R) → S) b : S) (a.prod fun (n : σ) (e : ℕ) ↦ v n ^ e : S) + eval₂ f_1 v f ∈ s
have monomial_add : Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) b : S)
Tactic: refine add_mem (mul_mem ?_ <| prod_mem fun i _ => pow_mem (hv _) _) (ih fun i => ?_)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f_1 : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.support
h : b ≠ 0
ih :
  ∀ (hs : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)), eval₂ f_1 v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    Membership.mem.{u_2, u_3} (α := S) s
      ((f_1 : (a : R) → S)
          (coeff i
            (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) f)) :
        S)
monomial_add : Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) b : S)
⊢ HMul.hMul (α := S) (β := S) ((f_1 : (a : R) → S) b : S) (a.prod fun (n : σ) (e : ℕ) ↦ v n ^ e : S) + eval₂ f_1 v f ∈ s
have monomial_add₁ : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)
Tactic: refine add_mem (mul_mem ?_ <| prod_mem fun i _ => pow_mem (hv _) _) (ih fun i => ?_)
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f_1 : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.support
h : b ≠ 0
ih :
  ∀ (hs : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)), eval₂ f_1 v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    Membership.mem.{u_2, u_3} (α := S) s
      ((f_1 : (a : R) → S)
          (coeff i
            (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) f)) :
        S)
i : σ →₀ ℕ
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)
have this : Membership.mem.{u_2, u_3} (α := S) s
  ((f_1 : (a : R) → S)
      (coeff i (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) f)) :
    S)
Tactic: have := hs i
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (hypothesis)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f_1 : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.support
h : b ≠ 0
ih :
  ∀ (hs : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)), eval₂ f_1 v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    Membership.mem.{u_2, u_3} (α := S) s
      ((f_1 : (a : R) → S)
          (coeff i
            (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) f)) :
        S)
i : σ →₀ ℕ
this :
  Membership.mem.{u_2, u_3} (α := S) s
    ((f_1 : (a : R) → S)
        (coeff i
          (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) f)) :
      S)
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)
have this₁ : Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) ((if a = i then b else 0) + coeff i f) : S)
Tactic: rw [coeff_add, coeff_monomial] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f_1 : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.support
h : b ≠ 0
ih :
  ∀ (hs : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)), eval₂ f_1 v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    Membership.mem.{u_2, u_3} (α := S) s
      ((f_1 : (a : R) → S)
          (coeff i
            (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) f)) :
        S)
i : σ →₀ ℕ
this : Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) ((if a = i then b else 0) + coeff i f) : S)
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)
have pos : ∀ (h : a = i) (this : Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (b + coeff i f) : S)),
  Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)
Tactic: split_ifs at this with h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f_1 : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.support
h : b ≠ 0
ih :
  ∀ (hs : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)), eval₂ f_1 v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    Membership.mem.{u_2, u_3} (α := S) s
      ((f_1 : (a : R) → S)
          (coeff i
            (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) f)) :
        S)
i : σ →₀ ℕ
this : Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) ((if a = i then b else 0) + coeff i f) : S)
pos :
  ∀ (h : a = i) (this : Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (b + coeff i f) : S)),
    Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)
have neg : ∀ (h : ¬a = i) (this : Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (0 + coeff i f) : S)),
  Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)
Tactic: split_ifs at this with h
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
σ : Type u_1
inst : CommSemiring R
S : Type u_2
subS : Type u_3
inst_1 : CommSemiring S
inst_2 : SetLike subS S
inst_3 : SubsemiringClass subS S
f_1 : R →+* S
s : subS
v : σ → S
hv : ∀ (i : σ), v i ∈ s
a : σ →₀ ℕ
b : R
f : MvPolynomial σ R
ha : a ∉ f.support
h_1 : b ≠ 0
ih :
  ∀ (hs : ∀ (i : σ →₀ ℕ), Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)), eval₂ f_1 v f ∈ s
hs :
  ∀ (i : σ →₀ ℕ),
    Membership.mem.{u_2, u_3} (α := S) s
      ((f_1 : (a : R) → S)
          (coeff i
            (HAdd.hAdd (α := MvPolynomial σ R) ((monomial a : (a : R) → MvPolynomial σ R) b : MvPolynomial σ R) f)) :
        S)
i : σ →₀ ℕ
h : a = i
this : Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (b + coeff i f) : S)
⊢ Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff i f) : S)
have pos : ∀ (this : Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (b + coeff a f) : S)),
  Membership.mem.{u_2, u_3} (α := S) s ((f_1 : (a : R) → S) (coeff a f) : S)
Tactic: subst h
Cleared hypotheses: i, h, this