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₁
hf : Surjective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
i : σ →₀ ℕ
fr : S₁
⊢ ∃ (a : MvPolynomial σ R),
    Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
      ((monomial i : (a : S₁) → MvPolynomial σ S₁) fr : MvPolynomial σ S₁)
have monomial : ∀ (r : R),
  ∃ (a : MvPolynomial σ R),
    Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
      ((monomial i : (a : S₁) → MvPolynomial σ S₁) ((f : (a : R) → S₁) r) : MvPolynomial σ S₁)
Tactic: obtain ⟨r, rfl⟩ := hf fr
Cleared hypotheses: fr
-- 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 : Surjective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
a b : MvPolynomial σ S₁
ha : ∃ (a_1 : MvPolynomial σ R), (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a_1 = a
hb : ∃ (a : MvPolynomial σ R), (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a = b
⊢ ∃ (a_1 : MvPolynomial σ R), (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a_1 = a + b
have add : ∀ (a : MvPolynomial σ R),
  ∃ (a_1 : MvPolynomial σ R),
    (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a_1 =
      HAdd.hAdd (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a : MvPolynomial σ S₁) b
Tactic: obtain ⟨a, rfl⟩ := ha
Cleared hypotheses: a, ha
-- 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 : Surjective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
b : MvPolynomial σ S₁
hb : ∃ (a : MvPolynomial σ R), (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a = b
a : MvPolynomial σ R
⊢ ∃ (a_1 : MvPolynomial σ R),
    (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a_1 =
      HAdd.hAdd (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a : MvPolynomial σ S₁) b
have add : ∀ (b : MvPolynomial σ R),
  ∃ (a_1 : MvPolynomial σ R),
    (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a_1 =
      HAdd.hAdd (α := MvPolynomial σ S₁) (β := MvPolynomial σ S₁)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) b : MvPolynomial σ S₁)
Tactic: obtain ⟨b, rfl⟩ := hb
Cleared hypotheses: b, hb
-- 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 : Surjective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
p : MvPolynomial σ S₁
⊢ ∃ (a : MvPolynomial σ R), (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a = p
have monomial : ∀ (i : σ →₀ ℕ) (fr : S₁),
  ∃ (a : MvPolynomial σ R),
    Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
      ((monomial i : (a : S₁) → MvPolynomial σ S₁) fr : MvPolynomial σ S₁)
Tactic: induction p using MvPolynomial.induction_on' with
  | monomial i fr =>
    obtain ⟨r, rfl⟩ := hf fr
    exact ⟨monomial i r, map_monomial _ _ _⟩
  | add a b ha hb =>
    obtain ⟨a, rfl⟩ := ha
    obtain ⟨b, rfl⟩ := hb
    exact ⟨a + b, map_add _ _ _⟩
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₁
f : R →+* S₁
hf : Surjective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
p : MvPolynomial σ S₁
monomial :
  ∀ (i : σ →₀ ℕ) (fr : S₁),
    ∃ (a : MvPolynomial σ R),
      Eq (α := MvPolynomial σ S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a : MvPolynomial σ S₁)
        ((MvPolynomial.monomial i : (a : S₁) → MvPolynomial σ S₁) fr : MvPolynomial σ S₁)
⊢ ∃ (a : MvPolynomial σ R), (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a = p
have add : ∀ (a b : MvPolynomial σ S₁)
  (ha : ∃ (a_1 : MvPolynomial σ R), (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a_1 = a)
  (hb : ∃ (a : MvPolynomial σ R), (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a = b),
  ∃ (a_1 : MvPolynomial σ R), (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) a_1 = a + b
Tactic: induction p using MvPolynomial.induction_on' with
  | monomial i fr =>
    obtain ⟨r, rfl⟩ := hf fr
    exact ⟨monomial i r, map_monomial _ _ _⟩
  | add a b ha hb =>
    obtain ⟨a, rfl⟩ := ha
    obtain ⟨b, rfl⟩ := hb
    exact ⟨a + b, map_add _ _ _⟩
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₁
f : R →+* S₁
g : S₁ →+* R
hf : LeftInverse.{v + 1, u + 1} (α := S₁) (β := R) (⇑f : (a : R) → S₁) (⇑g : (a : S₁) → R)
X : MvPolynomial σ S₁
⊢ (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((map g : (a : MvPolynomial σ S₁) → MvPolynomial σ R) X) = X
have rw : (map (f.comp g) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₁) X = X
Tactic: rw [map_map, (RingHom.ext hf : f.comp g = RingHom.id _), 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₁
g : S₁ →+* R
hf : LeftInverse.{v + 1, u + 1} (α := S₁) (β := R) (⇑f : (a : R) → S₁) (⇑g : (a : S₁) → R)
X : MvPolynomial σ S₁
rw : (map (f.comp g) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₁) X = X
⊢ (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((map g : (a : MvPolynomial σ S₁) → MvPolynomial σ R) X) = X
have rw₁ : (map (RingHom.id S₁) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₁) X = X
Tactic: rw [map_map, (RingHom.ext hf : f.comp g = RingHom.id _), 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₁
g : S₁ →+* R
hf : LeftInverse.{v + 1, u + 1} (α := S₁) (β := R) (⇑f : (a : R) → S₁) (⇑g : (a : S₁) → R)
X : MvPolynomial σ S₁
rw : (map (f.comp g) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₁) X = X
rw₁ : (map (RingHom.id S₁) : (a : MvPolynomial σ S₁) → MvPolynomial σ S₁) X = X
⊢ (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((map g : (a : MvPolynomial σ S₁) → MvPolynomial σ R) X) = X
have rw₂ : X = X
Tactic: rw [map_map, (RingHom.ext hf : f.comp g = RingHom.id _), 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₁
g : σ → S₁
p : MvPolynomial σ R
⊢ (eval g : (a : MvPolynomial σ S₁) → S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁) =
    eval₂ f g p
have C : ∀ (a : R),
  (eval g : (a : MvPolynomial σ S₁) → S₁)
      ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((C : (a : R) → MvPolynomial σ R) a) : MvPolynomial σ S₁) =
    eval₂ f g ((C : (a : R) → MvPolynomial σ R) a)
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₁
g : σ → S₁
p : MvPolynomial σ R
C :
  ∀ (a : R),
    (eval g : (a : MvPolynomial σ S₁) → S₁)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) :
          MvPolynomial σ S₁) =
      eval₂ f g ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
⊢ (eval g : (a : MvPolynomial σ S₁) → S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁) =
    eval₂ f g p
have add : ∀ (p q : MvPolynomial σ R),
  (eval g : (a : MvPolynomial σ S₁) → S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁) =
      eval₂ f g p →
    (eval g : (a : MvPolynomial σ S₁) → S₁)
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁) =
        eval₂ f g q →
      (eval g : (a : MvPolynomial σ S₁) → S₁)
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q) : MvPolynomial σ S₁) =
        eval₂ f g (p + q)
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₁
g : σ → S₁
p : MvPolynomial σ R
C :
  ∀ (a : R),
    (eval g : (a : MvPolynomial σ S₁) → S₁)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a) :
          MvPolynomial σ S₁) =
      eval₂ f g ((MvPolynomial.C : (a : R) → MvPolynomial σ R) a)
add :
  ∀ (p q : MvPolynomial σ R),
    (eval g : (a : MvPolynomial σ S₁) → S₁)
          ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁) =
        eval₂ f g p →
      (eval g : (a : MvPolynomial σ S₁) → S₁)
            ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) q : MvPolynomial σ S₁) =
          eval₂ f g q →
        (eval g : (a : MvPolynomial σ S₁) → S₁)
            ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p + q) : MvPolynomial σ S₁) =
          eval₂ f g (p + q)
⊢ (eval g : (a : MvPolynomial σ S₁) → S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁) =
    eval₂ f g p
have mul_X : ∀ (p : MvPolynomial σ R) (n : σ),
  (eval g : (a : MvPolynomial σ S₁) → S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p : MvPolynomial σ S₁) =
      eval₂ f g p →
    (eval g : (a : MvPolynomial σ S₁) → S₁)
        ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (p * X n) : MvPolynomial σ S₁) =
      eval₂ f g (p * X n)
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₁
g : σ → R
p : MvPolynomial σ R
⊢ (f : (a : R) → S₁) ((eval g : (a : MvPolynomial σ R) → R) p : R) = eval₂ f ((⇑f : (a : R) → S₁) ∘ g) p
have rw : (f : (a : R) → S₁)
    ((eval g : (a : MvPolynomial σ R) → R)
        ((map (RingHom.id R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) :
      R) =
  eval₂ f ((⇑f : (a : R) → S₁) ∘ g) ((map (RingHom.id R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p)
Tactic: rw [← p.map_id, eval_map, eval₂_comp_right]
-- 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₁
g : σ → R
p : MvPolynomial σ R
rw :
  (f : (a : R) → S₁)
      ((eval g : (a : MvPolynomial σ R) → R)
          ((map (RingHom.id R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R) =
    eval₂ f ((⇑f : (a : R) → S₁) ∘ g) ((map (RingHom.id R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p)
⊢ (f : (a : R) → S₁) ((eval g : (a : MvPolynomial σ R) → R) p : R) = eval₂ f ((⇑f : (a : R) → S₁) ∘ g) p
have rw₁ : (f : (a : R) → S₁) (eval₂ (RingHom.id R) g p) =
  eval₂ f ((⇑f : (a : R) → S₁) ∘ g) ((map (RingHom.id R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p)
Tactic: rw [← p.map_id, eval_map, eval₂_comp_right]
-- 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₁
g : σ → R
p : MvPolynomial σ R
rw :
  (f : (a : R) → S₁)
      ((eval g : (a : MvPolynomial σ R) → R)
          ((map (RingHom.id R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p : MvPolynomial σ R) :
        R) =
    eval₂ f ((⇑f : (a : R) → S₁) ∘ g) ((map (RingHom.id R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p)
rw₁ :
  (f : (a : R) → S₁) (eval₂ (RingHom.id R) g p) =
    eval₂ f ((⇑f : (a : R) → S₁) ∘ g) ((map (RingHom.id R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p)
⊢ (f : (a : R) → S₁) ((eval g : (a : MvPolynomial σ R) → R) p : R) = eval₂ f ((⇑f : (a : R) → S₁) ∘ g) p
have rw₂ : eval₂ f ((⇑f : (a : R) → S₁) ∘ g) ((map (RingHom.id R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p) =
  eval₂ f ((⇑f : (a : R) → S₁) ∘ g) ((map (RingHom.id R) : (a : MvPolynomial σ R) → MvPolynomial σ R) p)
Tactic: rw [← p.map_id, eval_map, eval₂_comp_right]
-- 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₂
f : R →+* S₁
g : σ → S₂
φ : S₁ →+* S₂
p : MvPolynomial σ R
⊢ eval₂ φ g ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) = eval₂ (φ.comp f) g p
have rw : (eval g : (a : MvPolynomial σ S₂) → S₂)
    ((map φ : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) :
      MvPolynomial σ S₂) =
  eval₂ (φ.comp f) g p
Tactic: rw [← eval_map, ← eval_map, map_map]
-- 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₂
f : R →+* S₁
g : σ → S₂
φ : S₁ →+* S₂
p : MvPolynomial σ R
rw :
  (eval g : (a : MvPolynomial σ S₂) → S₂)
      ((map φ : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) :
        MvPolynomial σ S₂) =
    eval₂ (φ.comp f) g p
⊢ eval₂ φ g ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) = eval₂ (φ.comp f) g p
have rw₁ : Eq.{w + 1} (α := S₂)
  ((eval g : (a : MvPolynomial σ S₂) → S₂)
      ((map φ : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) :
        MvPolynomial σ S₂) :
    S₂)
  ((eval g : (a : MvPolynomial σ S₂) → S₂)
      ((map (φ.comp f) : (a : MvPolynomial σ R) → MvPolynomial σ S₂) p : MvPolynomial σ S₂) :
    S₂)
Tactic: rw [← eval_map, ← eval_map, map_map]
-- 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₂
f : R →+* S₁
g : σ → S₂
φ : S₁ →+* S₂
p : MvPolynomial σ R
rw :
  (eval g : (a : MvPolynomial σ S₂) → S₂)
      ((map φ : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) :
        MvPolynomial σ S₂) =
    eval₂ (φ.comp f) g p
rw₁ :
  Eq.{w + 1} (α := S₂)
    ((eval g : (a : MvPolynomial σ S₂) → S₂)
        ((map φ : (a : MvPolynomial σ S₁) → MvPolynomial σ S₂)
            ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) :
          MvPolynomial σ S₂) :
      S₂)
    ((eval g : (a : MvPolynomial σ S₂) → S₂)
        ((map (φ.comp f) : (a : MvPolynomial σ R) → MvPolynomial σ S₂) p : MvPolynomial σ S₂) :
      S₂)
⊢ eval₂ φ g ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) = eval₂ (φ.comp f) g p
have rw₂ : Eq.{w + 1} (α := S₂)
  ((eval g : (a : MvPolynomial σ S₂) → S₂)
      ((map (φ.comp f) : (a : MvPolynomial σ R) → MvPolynomial σ S₂) p : MvPolynomial σ S₂) :
    S₂)
  ((eval g : (a : MvPolynomial σ S₂) → S₂)
      ((map (φ.comp f) : (a : MvPolynomial σ R) → MvPolynomial σ S₂) p : MvPolynomial σ S₂) :
    S₂)
Tactic: rw [← eval_map, ← eval_map, map_map]
-- 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 →+* S₁) (RingHom.comp constantCoeff (map f)) (f.comp constantCoeff)
have hC : ∀ (x : R),
  Eq.{v + 1} (α := S₁)
    ((RingHom.comp (β := MvPolynomial σ R) (RingHom.comp constantCoeff (map f)) 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 v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
hC :
  ∀ (x : R),
    Eq.{v + 1} (α := S₁)
      ((RingHom.comp (β := MvPolynomial σ R) (RingHom.comp constantCoeff (map f)) C : (a : R) → S₁) x : S₁)
      ((RingHom.comp (β := MvPolynomial σ R) (f.comp constantCoeff) C : (a : R) → S₁) x : S₁)
⊢ Eq (α := MvPolynomial σ R →+* S₁) (RingHom.comp constantCoeff (map f)) (f.comp constantCoeff)
have hX : ∀ (i : σ),
  Eq.{v + 1} (α := S₁) ((RingHom.comp constantCoeff (map f) : (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 v
σ : Type u_1
inst : CommSemiring R
inst_1 : CommSemiring S₁
f : R →+* S₁
p : MvPolynomial σ R
⊢ support.{v, u_1} (R := S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) ⊆ p.support
have simp : ∀ ⦃x : σ →₀ ℕ⦄,
  Ne.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0 → coeff x p ≠ 0
Tactic: simp only [Finset.subset_iff, mem_support_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₁
f : R →+* S₁
p : MvPolynomial σ R
x : σ →₀ ℕ
hx : Ne.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0
⊢ coeff x p ≠ 0
have contrapose : ∀ (hx : coeff x p = 0), Eq.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0
Tactic: contrapose 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₁
p : MvPolynomial σ R
x : σ →₀ ℕ
hx : coeff x p = 0
⊢ Eq.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0
have rw : Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) (coeff x p) : S₁) (0 : S₁)
Tactic: rw [coeff_map, hx, 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
x : σ →₀ ℕ
hx : coeff x p = 0
rw : Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) (coeff x p) : S₁) (0 : S₁)
⊢ Eq.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0
have rw₁ : Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) 0 : S₁) (0 : S₁)
Tactic: rw [coeff_map, hx, 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
x : σ →₀ ℕ
hx : coeff x p = 0
rw : Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) (coeff x p) : S₁) (0 : S₁)
rw₁ : Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) 0 : S₁) (0 : S₁)
⊢ Eq.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0
have rw₂ : Eq.{v + 1} (α := S₁) 0 0
Tactic: rw [coeff_map, hx, 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₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
⊢ support.{v, u_1} (R := S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) = p.support
have H₁ : support.{v, u_1} (R := S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) ⊆ p.support
Tactic: apply Finset.Subset.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₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
H₁ : support.{v, u_1} (R := S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) ⊆ p.support
⊢ support.{v, u_1} (R := S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p) = p.support
have H₂ : p.support ⊆ support.{v, u_1} (R := S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)
Tactic: apply Finset.Subset.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₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
⊢ p.support ⊆ support.{v, u_1} (R := S₁) ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)
have H₂ : ∀ ⦃x : σ →₀ ℕ⦄,
  coeff x p ≠ 0 → Ne.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0
Tactic: simp only [Finset.subset_iff, mem_support_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₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
x : σ →₀ ℕ
hx : coeff x p ≠ 0
⊢ Ne.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0
have H₂ : ∀ (hx : Eq.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0), coeff x p = 0
Tactic: contrapose 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₁
p : MvPolynomial σ R
f : R →+* S₁
hf : Injective.{u + 1, v + 1} (α := R) (β := S₁) (⇑f : (a : R) → S₁)
x : σ →₀ ℕ
hx : Eq.{v + 1} (α := S₁) (coeff x ((map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) p)) 0
⊢ coeff x p = 0
have hx₁ : Eq.{v + 1} (α := S₁) ((f : (a : R) → S₁) (coeff x p) : S₁) ((f : (a : R) → S₁) 0 : S₁)
Tactic: rw [coeff_map, ← f.map_zero] 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₁
q : R →+* S₁
r : R
hr : ∀ (r' : R), Eq.{v + 1} (α := S₁) ((q : (a : R) → S₁) r' : S₁) (0 : S₁) ↔ r ∣ r'
φ : MvPolynomial σ R
⊢ (C : (a : R) → MvPolynomial σ R) r ∣ φ ↔
    Eq (α := MvPolynomial σ S₁) ((map q : (a : MvPolynomial σ R) → MvPolynomial σ S₁) φ : MvPolynomial σ S₁)
      (0 : MvPolynomial σ S₁)
have rw : (∀ (i : σ →₀ ℕ), r ∣ coeff i φ) ↔
  ∀ (m : σ →₀ ℕ), Eq.{v + 1} (α := S₁) (coeff m ((map q : (a : MvPolynomial σ R) → MvPolynomial σ S₁) φ)) (coeff m 0)
Tactic: rw [C_dvd_iff_dvd_coeff, MvPolynomial.ext_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₁
f : R →+* S₁
g : S₁ → R
hg : g 0 = 0
φ : MvPolynomial σ S₁
⊢ (map f : (a : MvPolynomial σ R) → MvPolynomial σ S₁) (mapRange g hg φ) = φ ↔
    ∀ (d : σ →₀ ℕ), (f : (a : R) → S₁) (g (coeff d φ)) = coeff d φ
have simp_rw : (∀ (m : σ →₀ ℕ), (f : (a : R) → S₁) (coeff m (mapRange g hg φ)) = coeff m φ) ↔
  ∀ (d : σ →₀ ℕ), (f : (a : R) → S₁) (g (coeff d φ)) = coeff d φ
Tactic: simp_rw [MvPolynomial.ext_iff, coeff_map]