awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p_1 p : MvPolynomial S₂ R
s : S₂
hp :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p) :
      MvPolynomial S₃ S₁)
mul_X :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p * eval₂ C g (X s)) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X s)) :
      MvPolynomial S₃ S₁)
mul_X₁ :
  HMul.hMul (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p) : MvPolynomial S₃ S₁)
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (X s)) : MvPolynomial S₃ S₁) =
    eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X s))
⊢ Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (p * X s)) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X s)) :
      MvPolynomial S₃ S₁)
have mul_X₂ : HMul.hMul (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p))
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (X s)) : MvPolynomial S₃ S₁) =
  eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
    ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X s))
Tactic: rw [eval₂_mul, (map f).map_mul, hp, (map f).map_mul, map_X, eval₂_mul, eval₂_X, eval₂_X,
      comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
R : Type u
S₁ : Type v
S₂ : Type w
S₃ : Type x
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
g : S₂ → MvPolynomial S₃ R
p_1 p : MvPolynomial S₂ R
s : S₂
hp :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p) :
      MvPolynomial S₃ S₁)
mul_X :
  Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p * eval₂ C g (X s)) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X s)) :
      MvPolynomial S₃ S₁)
mul_X₁ :
  HMul.hMul (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g p) : MvPolynomial S₃ S₁)
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (X s)) : MvPolynomial S₃ S₁) =
    eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X s))
mul_X₂ :
  HMul.hMul (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
      (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p))
      ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (X s)) : MvPolynomial S₃ S₁) =
    eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X s))
⊢ Eq (α := MvPolynomial S₃ S₁)
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (p * X s)) : MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
        ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (p * X s)) :
      MvPolynomial S₃ S₁)
have mul_X₃ : HMul.hMul (α := MvPolynomial S₃ S₁) (β := MvPolynomial S₃ S₁)
    (eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p))
    ((map f : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) (eval₂ C g (X s)) : MvPolynomial S₃ S₁) =
  eval₂ C ((⇑(map f) : (a : MvPolynomial S₃ R) → MvPolynomial S₃ S₁) ∘ g)
    (HMul.hMul (α := MvPolynomial S₂ S₁) (β := MvPolynomial S₂ S₁)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) p : MvPolynomial S₂ S₁)
      ((map f : (a : MvPolynomial S₂ R) → MvPolynomial S₂ S₁) (X s) : MvPolynomial S₂ S₁))
Tactic: rw [eval₂_mul, (map f).map_mul, hp, (map f).map_mul, map_X, eval₂_mul, eval₂_X, eval₂_X,
      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₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
p : MvPolynomial ι R
⊢ eval₂ (RingHom.comp (map f) C) h p = eval₂ C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) p)
have C : ∀ (a : R),
  eval₂ (RingHom.comp (map f) C) h ((C : (a : R) → MvPolynomial ι R) a) =
    eval₂ C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) ((C : (a : R) → MvPolynomial ι R) a))
Tactic: induction p using MvPolynomial.induction_on
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₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
p : MvPolynomial ι R
C :
  ∀ (a : R),
    eval₂ (RingHom.comp (map f) MvPolynomial.C) h ((MvPolynomial.C : (a : R) → MvPolynomial ι R) a) =
      eval₂ MvPolynomial.C h
        ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) ((MvPolynomial.C : (a : R) → MvPolynomial ι R) a))
⊢ eval₂ (RingHom.comp (map f) MvPolynomial.C) h p =
    eval₂ MvPolynomial.C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) p)
have add : ∀ (p q : MvPolynomial ι R),
  eval₂ (RingHom.comp (map f) MvPolynomial.C) h p =
      eval₂ MvPolynomial.C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) p) →
    eval₂ (RingHom.comp (map f) MvPolynomial.C) h q =
        eval₂ MvPolynomial.C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) q) →
      eval₂ (RingHom.comp (map f) MvPolynomial.C) h (p + q) =
        eval₂ MvPolynomial.C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) (p + q))
Tactic: induction p using MvPolynomial.induction_on
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₁
ι : Type u_2
f : R →+* S₁
h : ι → MvPolynomial σ S₁
p : MvPolynomial ι R
C :
  ∀ (a : R),
    eval₂ (RingHom.comp (map f) MvPolynomial.C) h ((MvPolynomial.C : (a : R) → MvPolynomial ι R) a) =
      eval₂ MvPolynomial.C h
        ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) ((MvPolynomial.C : (a : R) → MvPolynomial ι R) a))
add :
  ∀ (p q : MvPolynomial ι R),
    eval₂ (RingHom.comp (map f) MvPolynomial.C) h p =
        eval₂ MvPolynomial.C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) p) →
      eval₂ (RingHom.comp (map f) MvPolynomial.C) h q =
          eval₂ MvPolynomial.C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) q) →
        eval₂ (RingHom.comp (map f) MvPolynomial.C) h (p + q) =
          eval₂ MvPolynomial.C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) (p + q))
⊢ eval₂ (RingHom.comp (map f) MvPolynomial.C) h p =
    eval₂ MvPolynomial.C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) p)
have mul_X : ∀ (p : MvPolynomial ι R) (n : ι),
  eval₂ (RingHom.comp (map f) MvPolynomial.C) h p =
      eval₂ MvPolynomial.C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) p) →
    eval₂ (RingHom.comp (map f) MvPolynomial.C) h (p * X n) =
      eval₂ MvPolynomial.C h ((map f : (a : MvPolynomial ι R) → MvPolynomial ι S₁) (p * X n))
Tactic: induction p using MvPolynomial.induction_on
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
S₁ : Type v
σ : Type u_1
inst : CommSemiring S₁
S₂ : Type u_2
inst_1 : CommSemiring S₂
q : S₁ →+* S₂
g : σ → S₁
p : MvPolynomial σ S₁
⊢ Eq.{u_2 + 1} (α := S₂) ((q : (a : S₁) → S₂) ((eval g : (a : MvPolynomial σ S₁) → S₁) p : S₁) : S₂)
    ((eval ((⇑q : (a : S₁) → S₂) ∘ g) : (a : MvPolynomial σ S₂) → S₂)
        ((map q : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) p : MvPolynomial σ S₂) :
      S₂)
have rw : (q : (a : S₁) → S₂) ((eval g : (a : MvPolynomial σ S₁) → S₁) p : S₁) = eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) p
Tactic: rw [← eval₂_eq_eval_map, ← eval₂_id, eval₂_comp_right, map_id]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
S₁ : Type v
σ : Type u_1
inst : CommSemiring S₁
S₂ : Type u_2
inst_1 : CommSemiring S₂
q : S₁ →+* S₂
g : σ → S₁
p : MvPolynomial σ S₁
rw : (q : (a : S₁) → S₂) ((eval g : (a : MvPolynomial σ S₁) → S₁) p : S₁) = eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) p
⊢ Eq.{u_2 + 1} (α := S₂) ((q : (a : S₁) → S₂) ((eval g : (a : MvPolynomial σ S₁) → S₁) p : S₁) : S₂)
    ((eval ((⇑q : (a : S₁) → S₂) ∘ g) : (a : MvPolynomial σ S₂) → S₂)
        ((map q : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) p : MvPolynomial σ S₂) :
      S₂)
have rw₁ : (q : (a : S₁) → S₂) (eval₂ (RingHom.id S₁) g p) = eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) p
Tactic: rw [← eval₂_eq_eval_map, ← eval₂_id, eval₂_comp_right, map_id]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
S₁ : Type v
σ : Type u_1
inst : CommSemiring S₁
S₂ : Type u_2
inst_1 : CommSemiring S₂
q : S₁ →+* S₂
g : σ → S₁
p : MvPolynomial σ S₁
rw : (q : (a : S₁) → S₂) ((eval g : (a : MvPolynomial σ S₁) → S₁) p : S₁) = eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) p
rw₁ : (q : (a : S₁) → S₂) (eval₂ (RingHom.id S₁) g p) = eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) p
⊢ Eq.{u_2 + 1} (α := S₂) ((q : (a : S₁) → S₂) ((eval g : (a : MvPolynomial σ S₁) → S₁) p : S₁) : S₂)
    ((eval ((⇑q : (a : S₁) → S₂) ∘ g) : (a : MvPolynomial σ S₂) → S₂)
        ((map q : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) p : MvPolynomial σ S₂) :
      S₂)
have rw₂ : eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) ((map (RingHom.id S₁) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₁) p) =
  eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) p
Tactic: rw [← eval₂_eq_eval_map, ← eval₂_id, eval₂_comp_right, map_id]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Eval (goal)
Goal:
S₁ : Type v
σ : Type u_1
inst : CommSemiring S₁
S₂ : Type u_2
inst_1 : CommSemiring S₂
q : S₁ →+* S₂
g : σ → S₁
p : MvPolynomial σ S₁
rw : (q : (a : S₁) → S₂) ((eval g : (a : MvPolynomial σ S₁) → S₁) p : S₁) = eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) p
rw₁ : (q : (a : S₁) → S₂) (eval₂ (RingHom.id S₁) g p) = eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) p
rw₂ :
  eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) ((map (RingHom.id S₁) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₁) p) =
    eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) p
⊢ Eq.{u_2 + 1} (α := S₂) ((q : (a : S₁) → S₂) ((eval g : (a : MvPolynomial σ S₁) → S₁) p : S₁) : S₂)
    ((eval ((⇑q : (a : S₁) → S₂) ∘ g) : (a : MvPolynomial σ S₂) → S₂)
        ((map q : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) p : MvPolynomial σ S₂) :
      S₂)
have rw₃ : eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) p = eval₂ q ((⇑q : (a : S₁) → S₂) ∘ g) p
Tactic: rw [← eval₂_eq_eval_map, ← eval₂_id, eval₂_comp_right, map_id]
-- 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 σ R
⊢ ∀ (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
      ((f : (a : R) → S₁) (coeff m p) : S₁)
have C : ∀ (a : R) (m : σ →₀ ℕ),
  Eq.{v + 1} (α := S₁)
    (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((C : (a : R) → MvPolynomial σ R) a)) : S₁)
    ((f : (a : R) → S₁) (coeff m ((C : (a : R) → MvPolynomial σ R) a)) : S₁)
Tactic: apply MvPolynomial.induction_on 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₁
f : R →+* S₁
p : MvPolynomial σ R
C :
  ∀ (a : R) (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁)
      (coeff m
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        S₁)
      ((f : (a : R) → S₁) (coeff m ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) : S₁)
⊢ ∀ (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
      ((f : (a : R) → S₁) (coeff m p) : S₁)
have add : ∀ (p q : MvPolynomial σ R),
  (∀ (m : σ →₀ ℕ),
      Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
        ((f : (a : R) → S₁) (coeff m p) : S₁)) →
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q) : S₁)
          ((f : (a : R) → S₁) (coeff m q) : S₁)) →
      ∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q)) : S₁)
          ((f : (a : R) → S₁) (coeff m (p + q)) : S₁)
Tactic: apply MvPolynomial.induction_on 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₁
f : R →+* S₁
p : MvPolynomial σ R
C :
  ∀ (a : R) (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁)
      (coeff m
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        S₁)
      ((f : (a : R) → S₁) (coeff m ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) : S₁)
add :
  ∀ (p q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
          ((f : (a : R) → S₁) (coeff m p) : S₁)) →
      (∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q) : S₁)
            ((f : (a : R) → S₁) (coeff m q) : S₁)) →
        ∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q)) : S₁)
            ((f : (a : R) → S₁) (coeff m (p + q)) : S₁)
⊢ ∀ (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
      ((f : (a : R) → S₁) (coeff m p) : S₁)
have mul_X : ∀ (p : MvPolynomial σ R) (n : σ),
  (∀ (m : σ →₀ ℕ),
      Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
        ((f : (a : R) → S₁) (coeff m p) : S₁)) →
    ∀ (m : σ →₀ ℕ),
      Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X n)) : S₁)
        ((f : (a : R) → S₁) (coeff m (p * X n)) : S₁)
Tactic: apply MvPolynomial.induction_on 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₁
f : R →+* S₁
r : R
m : σ →₀ ℕ
⊢ Eq.{v + 1} (α := S₁)
    (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((C : (a : R) → MvPolynomial σ R) r)) : S₁)
    ((f : (a : R) → S₁) (coeff m ((C : (a : R) → MvPolynomial σ R) r)) : S₁)
have C : Eq.{v + 1} (α := S₁) (coeff m ((C : (a : S₁) → MvPolynomial σ S₁) ((f : (a : R) → S₁) r)) : S₁)
  ((f : (a : R) → S₁) (coeff m ((C : (a : R) → MvPolynomial σ R) r)) : S₁)
Tactic: simp_rw [map_C, coeff_C, apply_ite f, f.map_zero]
-- 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₁
r : R
m : σ →₀ ℕ
C :
  Eq.{v + 1} (α := S₁) (coeff m ((MvPolynomial.C : (a : S₁) → MvPolynomial σ S₁) ((f : (a : R) → S₁) r)) : S₁)
    ((f : (a : R) → S₁) (coeff m ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r)) : S₁)
⊢ Eq.{v + 1} (α := S₁)
    (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r)) :
      S₁)
    ((f : (a : R) → S₁) (coeff m ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r)) : S₁)
have C₁ : Eq.{v + 1} (α := S₁) (if 0 = m then (f : (a : R) → S₁) r else 0 : S₁) ((f : (a : R) → S₁) (if 0 = m then r else 0) : S₁)
Tactic: simp_rw [map_C, coeff_C, apply_ite f, f.map_zero]
-- 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₁
r : R
m : σ →₀ ℕ
C :
  Eq.{v + 1} (α := S₁) (coeff m ((MvPolynomial.C : (a : S₁) → MvPolynomial σ S₁) ((f : (a : R) → S₁) r)) : S₁)
    ((f : (a : R) → S₁) (coeff m ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r)) : S₁)
C₁ :
  Eq.{v + 1} (α := S₁) (if 0 = m then (f : (a : R) → S₁) r else 0 : S₁)
    ((f : (a : R) → S₁) (if 0 = m then r else 0) : S₁)
⊢ Eq.{v + 1} (α := S₁)
    (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r)) :
      S₁)
    ((f : (a : R) → S₁) (coeff m ((MvPolynomial.C : (a : R) → MvPolynomial σ R) r)) : S₁)
have C₂ : Eq.{v + 1} (α := S₁) (if 0 = m then (f : (a : R) → S₁) r else 0 : S₁)
  (if 0 = m then (f : (a : R) → S₁) r else (f : (a : R) → S₁) 0 : S₁)
Tactic: simp_rw [map_C, coeff_C, apply_ite f, f.map_zero]
-- 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 σ R
⊢ ∀ (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
      ((f : (a : R) → S₁) (coeff m p) : S₁)
have C : ∀ (a : R) (m : σ →₀ ℕ),
  Eq.{v + 1} (α := S₁)
    (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((C : (a : R) → MvPolynomial σ R) a)) : S₁)
    ((f : (a : R) → S₁) (coeff m ((C : (a : R) → MvPolynomial σ R) a)) : S₁)
Tactic: classical
  apply MvPolynomial.induction_on p <;> clear p
  · intro r m
    simp_rw [map_C, coeff_C, apply_ite f, f.map_zero]
  · intro p q hp hq m
    simp only [hp, hq, (map f).map_add, coeff_add, f.map_add]
  · intro p i hp m
    simp only [(map f).map_mul, map_X, hp, coeff_mul_X', f.map_zero, apply_ite f]
-- 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 σ R
C :
  ∀ (a : R) (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁)
      (coeff m
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        S₁)
      ((f : (a : R) → S₁) (coeff m ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) : S₁)
⊢ ∀ (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
      ((f : (a : R) → S₁) (coeff m p) : S₁)
have add : ∀ (p q : MvPolynomial σ R),
  (∀ (m : σ →₀ ℕ),
      Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
        ((f : (a : R) → S₁) (coeff m p) : S₁)) →
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q) : S₁)
          ((f : (a : R) → S₁) (coeff m q) : S₁)) →
      ∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q)) : S₁)
          ((f : (a : R) → S₁) (coeff m (p + q)) : S₁)
Tactic: classical
  apply MvPolynomial.induction_on p <;> clear p
  · intro r m
    simp_rw [map_C, coeff_C, apply_ite f, f.map_zero]
  · intro p q hp hq m
    simp only [hp, hq, (map f).map_add, coeff_add, f.map_add]
  · intro p i hp m
    simp only [(map f).map_mul, map_X, hp, coeff_mul_X', f.map_zero, apply_ite f]
-- 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 σ R
C :
  ∀ (a : R) (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁)
      (coeff m
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) :
        S₁)
      ((f : (a : R) → S₁) (coeff m ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)) : S₁)
add :
  ∀ (p q : MvPolynomial σ R),
    (∀ (m : σ →₀ ℕ),
        Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
          ((f : (a : R) → S₁) (coeff m p) : S₁)) →
      (∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q) : S₁)
            ((f : (a : R) → S₁) (coeff m q) : S₁)) →
        ∀ (m : σ →₀ ℕ),
          Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q)) : S₁)
            ((f : (a : R) → S₁) (coeff m (p + q)) : S₁)
⊢ ∀ (m : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
      ((f : (a : R) → S₁) (coeff m p) : S₁)
have mul_X : ∀ (p : MvPolynomial σ R) (n : σ),
  (∀ (m : σ →₀ ℕ),
      Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) : S₁)
        ((f : (a : R) → S₁) (coeff m p) : S₁)) →
    ∀ (m : σ →₀ ℕ),
      Eq.{v + 1} (α := S₁) (coeff m ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X n)) : S₁)
        ((f : (a : R) → S₁) (coeff m (p * X n)) : S₁)
Tactic: classical
  apply MvPolynomial.induction_on p <;> clear p
  · intro r m
    simp_rw [map_C, coeff_C, apply_ite f, f.map_zero]
  · intro p q hp hq m
    simp only [hp, hq, (map f).map_add, coeff_add, f.map_add]
  · intro p i hp m
    simp only [(map f).map_mul, map_X, hp, coeff_mul_X', f.map_zero, apply_ite f]
-- 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₁
⊢ Eq (α := MvPolynomial σ R →+* MvPolynomial σ S₁) (map f) (eval₂Hom (RingHom.comp C f) X)
have hC : ∀ (a : R) (x : σ →₀ ℕ),
  Eq.{v + 1} (α := S₁) (coeff x ((RingHom.comp (map f) C : (a : R) → MvPolynomial σ S₁) a))
    (coeff x ((RingHom.comp (eval₂Hom (RingHom.comp C f) X) C : (a : R) → MvPolynomial σ S₁) a))
Tactic: ext a 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₁
f : R →+* S₁
hC :
  ∀ (a : R) (x : σ →₀ ℕ),
    Eq.{v + 1} (α := S₁) (coeff x ((RingHom.comp (map f) C : (a : R) → MvPolynomial σ S₁) a))
      (coeff x ((RingHom.comp (eval₂Hom (RingHom.comp C f) X) C : (a : R) → MvPolynomial σ S₁) a))
⊢ Eq (α := MvPolynomial σ R →+* MvPolynomial σ S₁) (map f) (eval₂Hom (RingHom.comp C f) X)
have hX : ∀ (a : σ) (x : σ →₀ ℕ),
  Eq.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (X a)))
    (coeff x ((eval₂Hom (RingHom.comp C f) X : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (X a)))
Tactic: ext a 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₁
f : R →+* S₁
hf : Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
p q : MvPolynomial σ R
h :
  Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁)
    ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁)
⊢ p = q
have simp : ∀ (h : ∀ (m : σ →₀ ℕ), Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) (coeff m p) : S₁) ((f : (a : R) → S₁) (coeff m q) : S₁))
  (m : σ →₀ ℕ), coeff m p = coeff m q
Tactic: simp only [MvPolynomial.ext_iff, coeff_map] at h ⊢
Cleared hypotheses: h