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₁
f : R →+* S₁
p : MvPolynomial σ S₁
n : σ
ih :
  ∀ (hx : (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
    Membership.mem (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) p
hx : (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
⊢ Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) (p * X n)
have refine_2 : ∀ (q : MvPolynomial σ R)
  (ih :
    ∀
      (hx :
        (↑(coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q)) : Set S₁) ⊆
          range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
      Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
        (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁))
  (hx :
    (↑(coeffs.{v, u_1} (σ := σ) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q)) : Set S₁) ⊆
      range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
  Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    (HMul.hMul (α := MvPolynomial σ S₁) (β := MvPolynomial σ S₁)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁) (X n))
Tactic: obtain ⟨q, rfl⟩ := ih hx
Cleared hypotheses: p, ih, hx
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (hypothesis)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
a : σ →₀ ℕ
s : S₁
p : MvPolynomial σ S₁
ha : a ∉ p.support
hs : s ≠ 0
hp :
  ∀ (hx : (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
    Membership.mem (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) p
ih :
  ∀
    (hx :
      (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : Set S₁) ⊆
        range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
    Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
      ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)
hx :
  (↑(HAdd.hAdd (α := MvPolynomial σ S₁) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁) p).coeffs :
      Set S₁) ⊆
    range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
⊢ Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    (HAdd.hAdd (α := MvPolynomial σ S₁) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁) p)
have hx₁ : (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s) ∪ p.coeffs) : Set S₁) ⊆
  range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
Tactic: rw [coeffs_add (disjoint_support_monomial ha hs)] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (hypothesis)
Goal:
R : Type u
S₁ : Type v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
a : σ →₀ ℕ
s : S₁
p : MvPolynomial σ S₁
ha : a ∉ p.support
hs : s ≠ 0
hp :
  ∀ (hx : (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
    Membership.mem (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) p
ih :
  ∀
    (hx :
      (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : Set S₁) ⊆
        range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
    Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
      ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)
hx :
  (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s) ∪ p.coeffs) : Set S₁) ⊆
    range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
⊢ Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    (HAdd.hAdd (α := MvPolynomial σ S₁) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁) p)
have hx₁ : (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : Set S₁) ⊆
    range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁) ∧
  (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
Tactic: simp only [Finset.coe_union, Set.union_subset_iff] at hx
Cleared hypotheses: hx
-- 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₁
f : R →+* S₁
a : σ →₀ ℕ
s : S₁
p : MvPolynomial σ S₁
ha : a ∉ p.support
hs : s ≠ 0
hp :
  ∀ (hx : (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
    Membership.mem (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) p
ih :
  ∀
    (hx :
      (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : Set S₁) ⊆
        range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
    Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
      ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)
hx :
  (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : Set S₁) ⊆
      range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁) ∧
    (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
⊢ Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    (HAdd.hAdd (α := MvPolynomial σ S₁) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁) p)
have refine_2 : ∀ (q : MvPolynomial σ R)
  (hq :
    Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁)
      ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)),
  Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    (HAdd.hAdd (α := MvPolynomial σ S₁) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁) p)
Tactic: obtain ⟨q, hq⟩ := ih hx.1
-- 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₁
f : R →+* S₁
a : σ →₀ ℕ
s : S₁
p : MvPolynomial σ S₁
ha : a ∉ p.support
hs : s ≠ 0
hp :
  ∀ (hx : (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
    Membership.mem (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) p
ih :
  ∀
    (hx :
      (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : Set S₁) ⊆
        range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
    Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
      ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)
hx :
  (↑(coeffs.{v, u_1} (σ := σ) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s)) : Set S₁) ⊆
      range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁) ∧
    (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
q : MvPolynomial σ R
hq :
  Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁)
    ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁)
⊢ Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    (HAdd.hAdd (α := MvPolynomial σ S₁) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁) p)
have refine_2 : ∀ (u : MvPolynomial σ R) (hu : (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) u = p),
  Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    (HAdd.hAdd (α := MvPolynomial σ S₁) ((monomial a : (a : S₁) → MvPolynomial σ S₁) s : MvPolynomial σ S₁) p)
Tactic: obtain ⟨u, hu⟩ := hp hx.2
-- 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₁
f : R →+* S₁
x : MvPolynomial σ S₁
hx : (↑x.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
⊢ Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) x
have refine_2 : ∀ (a : S₁)
  (hx :
    (↑(coeffs.{v, u_1} (σ := σ) ((C : (a : S₁) → MvPolynomial σ S₁) a)) : Set S₁) ⊆
      range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
  Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
    ((C : (a : S₁) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
Tactic: induction x using induction_on'' with
    | C a =>
      by_cases h : a = 0
      · subst h
        exact ⟨0, by simp⟩
      · simp only [coeffs_C, h, reduceIte, Finset.coe_singleton, Set.singleton_subset_iff] at hx
        obtain ⟨b, rfl⟩ := hx
        exact ⟨C b, by simp⟩
    | mul_X p n ih =>
      rw [coeffs_mul_X] at hx
      obtain ⟨q, rfl⟩ := ih hx
      exact ⟨q * X n, by simp⟩
    | monomial_add a s p ha hs hp ih =>
      rw [coeffs_add (disjoint_support_monomial ha hs)] at hx
      simp only [Finset.coe_union, Set.union_subset_iff] at hx
      obtain ⟨q, hq⟩ := ih hx.1
      obtain ⟨u, hu⟩ := hp hx.2
      exact ⟨q + u, by simp [hq, hu]⟩
Cleared hypotheses: x, hx
-- 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₁
f : R →+* S₁
x : MvPolynomial σ S₁
hx : (↑x.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
refine_2 :
  ∀ (a : S₁)
    (hx :
      (↑(coeffs.{v, u_1} (σ := σ) ((C : (a : S₁) → MvPolynomial σ S₁) a)) : Set S₁) ⊆
        range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
    Membership.mem (α := MvPolynomial σ S₁) (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁))
      ((C : (a : S₁) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
⊢ Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) x
have refine_2₁ : ∀ (p : MvPolynomial σ S₁) (n : σ)
  (ih :
    ∀ (hx : (↑p.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
      Membership.mem (γ := Set (MvPolynomial σ S₁))
        (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) p)
  (hx : (↑(p * X n).coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
  Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) (p * X n)
Tactic: induction x using induction_on'' with
    | C a =>
      by_cases h : a = 0
      · subst h
        exact ⟨0, by simp⟩
      · simp only [coeffs_C, h, reduceIte, Finset.coe_singleton, Set.singleton_subset_iff] at hx
        obtain ⟨b, rfl⟩ := hx
        exact ⟨C b, by simp⟩
    | mul_X p n ih =>
      rw [coeffs_mul_X] at hx
      obtain ⟨q, rfl⟩ := ih hx
      exact ⟨q * X n, by simp⟩
    | monomial_add a s p ha hs hp ih =>
      rw [coeffs_add (disjoint_support_monomial ha hs)] at hx
      simp only [Finset.coe_union, Set.union_subset_iff] at hx
      obtain ⟨q, hq⟩ := ih hx.1
      obtain ⟨u, hu⟩ := hp hx.2
      exact ⟨q + u, by simp [hq, hu]⟩
Cleared hypotheses: x, hx
-- 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₁
f : R →+* S₁
x : MvPolynomial σ S₁
⊢ Membership.mem (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) x ↔
    (↑x.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
have refine_1 : ∀
  (hx :
    Membership.mem (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) x),
  (↑x.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
Tactic: classical
  refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
  · obtain ⟨p, rfl⟩ := hx
    exact subset_trans (coe_coeffs_map f p) (by simp)
  · induction x using induction_on'' with
    | C a =>
      by_cases h : a = 0
      · subst h
        exact ⟨0, by simp⟩
      · simp only [coeffs_C, h, reduceIte, Finset.coe_singleton, Set.singleton_subset_iff] at hx
        obtain ⟨b, rfl⟩ := hx
        exact ⟨C b, by simp⟩
    | mul_X p n ih =>
      rw [coeffs_mul_X] at hx
      obtain ⟨q, rfl⟩ := ih hx
      exact ⟨q * X n, by simp⟩
    | monomial_add a s p ha hs hp ih =>
      rw [coeffs_add (disjoint_support_monomial ha hs)] at hx
      simp only [Finset.coe_union, Set.union_subset_iff] at hx
      obtain ⟨q, hq⟩ := ih hx.1
      obtain ⟨u, hu⟩ := hp hx.2
      exact ⟨q + u, by simp [hq, hu]⟩
-- 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₁
f : R →+* S₁
x : MvPolynomial σ S₁
refine_1 :
  ∀
    (hx :
      Membership.mem (γ := Set (MvPolynomial σ S₁))
        (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) x),
    (↑x.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
⊢ Membership.mem (γ := Set (MvPolynomial σ S₁))
      (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) x ↔
    (↑x.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)
have refine_2 : ∀ (hx : (↑x.coeffs : Set S₁) ⊆ range.{v, u + 1} (ι := R) (⇑f : (a : R) → S₁)),
  Membership.mem (γ := Set (MvPolynomial σ S₁))
    (range (ι := MvPolynomial σ R) (⇑(map f) : (a : MvPolynomial σ R) → MvPolynomial σ S₁)) x
Tactic: classical
  refine ⟨fun hx ↦ ?_, fun hx ↦ ?_⟩
  · obtain ⟨p, rfl⟩ := hx
    exact subset_trans (coe_coeffs_map f p) (by simp)
  · induction x using induction_on'' with
    | C a =>
      by_cases h : a = 0
      · subst h
        exact ⟨0, by simp⟩
      · simp only [coeffs_C, h, reduceIte, Finset.coe_singleton, Set.singleton_subset_iff] at hx
        obtain ⟨b, rfl⟩ := hx
        exact ⟨C b, by simp⟩
    | mul_X p n ih =>
      rw [coeffs_mul_X] at hx
      obtain ⟨q, rfl⟩ := ih hx
      exact ⟨q * X n, by simp⟩
    | monomial_add a s p ha hs hp ih =>
      rw [coeffs_add (disjoint_support_monomial ha hs)] at hx
      simp only [Finset.coe_union, Set.union_subset_iff] at hx
      obtain ⟨q, hq⟩ := ih hx.1
      obtain ⟨u, hu⟩ := hp hx.2
      exact ⟨q + u, by simp [hq, hu]⟩
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : Algebra R S₁
inst_4 : Algebra R S₂
f : S₁ →ₐ[R] S₂
⊢ Eq (α := Submodule R (MvPolynomial σ S₂))
    ((Subalgebra.toSubmodule : (a : Subalgebra R (MvPolynomial σ S₂)) → Submodule R (MvPolynomial σ S₂))
        (AlgHom.range (mapAlgHom f)) :
      Submodule R (MvPolynomial σ S₂))
    (coeffsIn σ ((Subalgebra.toSubmodule : (a : Subalgebra R S₂) → Submodule R S₂) f.range) :
      Submodule R (MvPolynomial σ S₂))
have simp : range (ι := MvPolynomial σ S₁) (⇑(mapAlgHom f) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) =
  (↑(coeffsIn σ ((Subalgebra.toSubmodule : (a : Subalgebra R S₂) → Submodule R S₂) f.range)) : Set (MvPolynomial σ S₂))
Tactic: simp only [← SetLike.coe_set_eq, Subalgebra.coe_toSubmodule, AlgHom.coe_range]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : Algebra R S₁
inst_4 : Algebra R S₂
f : S₁ →ₐ[R] S₂
⊢ range (ι := MvPolynomial σ S₁) (⇑(mapAlgHom f) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) =
    (↑(coeffsIn σ ((Subalgebra.toSubmodule : (a : Subalgebra R S₂) → Submodule R S₂) f.range)) :
      Set (MvPolynomial σ S₂))
have h : ∀ (x : MvPolynomial σ S₂),
  Membership.mem (γ := Set (MvPolynomial σ S₂))
      (range (ι := MvPolynomial σ S₁) (⇑(mapAlgHom f) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂)) x ↔
    x ∈
      (↑(coeffsIn σ ((Subalgebra.toSubmodule : (a : Subalgebra R S₂) → Submodule R S₂) f.range)) :
        Set (MvPolynomial σ S₂))
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
inst_2 : CommSemiring S₂
inst_3 : Algebra R S₁
inst_4 : Algebra R S₂
f : S₁ →ₐ[R] S₂
x : MvPolynomial σ S₂
⊢ Membership.mem (γ := Set (MvPolynomial σ S₂))
      (range (ι := MvPolynomial σ S₁) (⇑(mapAlgHom f) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂)) x ↔
    x ∈
      (↑(coeffsIn σ ((Subalgebra.toSubmodule : (a : Subalgebra R S₂) → Submodule R S₂) f.range)) :
        Set (MvPolynomial σ S₂))
have h : (↑x.coeffs : Set S₂) ⊆ range.{w, v + 1} (ι := S₁) (⇑(↑f : S₁ →+* S₂) : (a : S₁) → S₂) ↔
  (↑x.coeffs : Set S₂) ⊆
    (↑((Subalgebra.toSubmodule : (a : Subalgebra R S₂) → Submodule R S₂) f.range : Submodule R S₂) : Set S₂)
Tactic: erw [mem_range_map_iff_coeffs_subset, mem_coeffsIn_iff_coeffs_subset]
-- 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₁
φ : MvPolynomial σ R →ₐ[R] S₁
⊢ φ = aeval (comp (β := MvPolynomial σ R) (⇑φ : (a : MvPolynomial σ R) → S₁) X)
have hf : ∀ (i : σ),
  Eq.{v + 1} (α := S₁) ((φ : (a : MvPolynomial σ R) → S₁) (X i) : S₁)
    ((aeval (comp (β := MvPolynomial σ R) (⇑φ : (a : MvPolynomial σ R) → S₁) X) : (a : MvPolynomial σ R) → S₁) (X i) :
      S₁)
Tactic: ext i
-- 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₁
B : Type u_2
inst_3 : CommSemiring B
inst_4 : Algebra R B
φ : S₁ →ₐ[R] B
⊢ φ.comp (aeval f) = aeval fun (i : σ) ↦ (φ : (a : S₁) → B) (f i)
have hf : ∀ (i : σ),
  Eq.{u_2 + 1} (α := B) ((φ.comp (aeval f) : (a : MvPolynomial σ R) → B) (X i) : B)
    ((aeval fun (i : σ) ↦ (φ : (a : S₁) → B) (f i) : (a : MvPolynomial σ R) → B) (X i) : B)
Tactic: ext i
-- 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₁
B : Type u_2
inst_3 : CommSemiring B
inst_4 : Algebra R B
φ : S₁ →ₐ[R] B
p : MvPolynomial σ R
⊢ Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
    ((aeval fun (i : σ) ↦ (φ : (a : S₁) → B) (f i) : (a : MvPolynomial σ R) → B) p : B)
have rw : Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
  ((φ.comp (aeval f) : (a : MvPolynomial σ R) → B) p : B)
Tactic: rw [← comp_aeval, AlgHom.coe_comp, comp_apply]
-- 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₁
B : Type u_2
inst_3 : CommSemiring B
inst_4 : Algebra R B
φ : S₁ →ₐ[R] B
p : MvPolynomial σ R
rw :
  Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
    ((φ.comp (aeval f) : (a : MvPolynomial σ R) → B) p : B)
⊢ Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
    ((aeval fun (i : σ) ↦ (φ : (a : S₁) → B) (f i) : (a : MvPolynomial σ R) → B) p : B)
have rw₁ : Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
  (comp (β := S₁) (⇑φ : (a : S₁) → B) (⇑(aeval f) : (a : MvPolynomial σ R) → S₁) p : B)
Tactic: rw [← comp_aeval, AlgHom.coe_comp, comp_apply]
-- 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₁
B : Type u_2
inst_3 : CommSemiring B
inst_4 : Algebra R B
φ : S₁ →ₐ[R] B
p : MvPolynomial σ R
rw :
  Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
    ((φ.comp (aeval f) : (a : MvPolynomial σ R) → B) p : B)
rw₁ :
  Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
    (comp (β := S₁) (⇑φ : (a : S₁) → B) (⇑(aeval f) : (a : MvPolynomial σ R) → S₁) p : B)
⊢ Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
    ((aeval fun (i : σ) ↦ (φ : (a : S₁) → B) (f i) : (a : MvPolynomial σ R) → B) p : B)
have rw₂ : Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
  ((φ : (a : S₁) → B) ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
Tactic: rw [← comp_aeval, AlgHom.coe_comp, comp_apply]
-- 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₁
B : Type u_2
inst_3 : CommSemiring B
g : σ → S₁
φ : S₁ →+* B
p : MvPolynomial σ R
⊢ Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval g : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
    ((eval₂Hom (φ.comp (algebraMap R S₁)) fun (i : σ) ↦ (φ : (a : S₁) → B) (g i) : (a : MvPolynomial σ R) → B) p : B)
have rw : Eq.{u_2 + 1} (α := B) ((φ : (a : S₁) → B) ((aeval g : (a : MvPolynomial σ R) → S₁) p : S₁) : B)
  ((φ.comp (eval₂Hom (algebraMap R S₁) g) : (a : MvPolynomial σ R) → B) p : B)
Tactic: rw [← comp_eval₂Hom]
-- 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₁
⊢ Eq (α := Subalgebra R S₁) (AlgHom.range (aeval f)) (Algebra.adjoin R (range f))
have a : LE.le (α := Subalgebra R S₁) (AlgHom.range (aeval f)) (Algebra.adjoin R (range f))
Tactic: apply le_antisymm
-- 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₁
a : LE.le (α := Subalgebra R S₁) (AlgHom.range (aeval f)) (Algebra.adjoin R (range f))
⊢ Eq (α := Subalgebra R S₁) (AlgHom.range (aeval f)) (Algebra.adjoin R (range f))
have a₁ : LE.le (α := Subalgebra R S₁) (Algebra.adjoin R (range f)) (AlgHom.range (aeval f))
Tactic: apply le_antisymm
-- 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))
    ((AlgHom.toRingHom (aeval f) : (a : MvPolynomial σ R) → S₁) p : S₁)
have a : Membership.mem (α := S₁) (γ := Subalgebra R S₁) (Algebra.adjoin R (range f))
  ((aeval f : (a : MvPolynomial σ R) → S₁) p : S₁)
Tactic: simp only [AlgHom.toRingHom_eq_coe, RingHom.coe_coe]