awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
i : σ
rw :
  Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₁ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : τ) ↦
            if h : i ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) i h))
            else 0 :
          (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
have rw₂ : Eq (α := MvPolynomial σ R)
  ((aeval fun (i : τ) ↦
          if h : i ∈ range f then
            X
              (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) i h))
          else 0 :
        (a : MvPolynomial τ R) → MvPolynomial σ R)
      ((X ∘ f) i) :
    MvPolynomial σ R)
  (X i : MvPolynomial σ R)
Tactic: rw [rename, killCompl, aeval_X, comp_apply, aeval_X, dif_pos ⟨i, rfl⟩,
      Equiv.ofInjective_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
i : σ
rw :
  Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₁ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : τ) ↦
            if h : i ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) i h))
            else 0 :
          (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₂ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : τ) ↦
            if h : i ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) i h))
            else 0 :
          (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((X ∘ f) i) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
have rw₃ : Eq (α := MvPolynomial σ R)
  ((aeval fun (i : τ) ↦
          if h : i ∈ range f then
            X
              (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) i h))
          else 0 :
        (a : MvPolynomial τ R) → MvPolynomial σ R)
      (X (f i)) :
    MvPolynomial σ R)
  (X i : MvPolynomial σ R)
Tactic: rw [rename, killCompl, aeval_X, comp_apply, aeval_X, dif_pos ⟨i, rfl⟩,
      Equiv.ofInjective_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
i : σ
rw :
  Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₁ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : τ) ↦
            if h : i ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) i h))
            else 0 :
          (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₂ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : τ) ↦
            if h : i ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) i h))
            else 0 :
          (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((X ∘ f) i) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₃ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : τ) ↦
            if h : i ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) i h))
            else 0 :
          (a : MvPolynomial τ R) → MvPolynomial σ R)
        (X (f i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
have rw₄ : Eq (α := MvPolynomial σ R)
  (if h : f i ∈ range f then
    X
      (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
        (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) (f i) h))
  else 0)
  (X i)
Tactic: rw [rename, killCompl, aeval_X, comp_apply, aeval_X, dif_pos ⟨i, rfl⟩,
      Equiv.ofInjective_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
i : σ
rw :
  Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₁ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : τ) ↦
            if h : i ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) i h))
            else 0 :
          (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₂ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : τ) ↦
            if h : i ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) i h))
            else 0 :
          (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((X ∘ f) i) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₃ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : τ) ↦
            if h : i ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) i h))
            else 0 :
          (a : MvPolynomial τ R) → MvPolynomial σ R)
        (X (f i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₄ :
  Eq (α := MvPolynomial σ R)
    (if h : f i ∈ range f then
      X
        (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
          (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) (f i) h))
    else 0)
    (X i)
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
have rw₅ : Eq (α := MvPolynomial σ R)
  (X
      (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
        (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) (f i) sorry)) :
    MvPolynomial σ R)
  (X i : MvPolynomial σ R)
Tactic: rw [rename, killCompl, aeval_X, comp_apply, aeval_X, dif_pos ⟨i, rfl⟩,
      Equiv.ofInjective_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
i : σ
rw :
  Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₁ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : τ) ↦
            if h : i ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) i h))
            else 0 :
          (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₂ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : τ) ↦
            if h : i ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) i h))
            else 0 :
          (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((X ∘ f) i) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₃ :
  Eq (α := MvPolynomial σ R)
    ((aeval fun (i : τ) ↦
            if h : i ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) i h))
            else 0 :
          (a : MvPolynomial τ R) → MvPolynomial σ R)
        (X (f i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
rw₄ :
  Eq (α := MvPolynomial σ R)
    (if h : f i ∈ range f then
      X
        (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
          (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) (f i) h))
    else 0)
    (X i)
rw₅ :
  Eq (α := MvPolynomial σ R)
    (X
        (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
          (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) (f i) ⋯)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) (X i)) :
      MvPolynomial σ R)
    (X i : MvPolynomial σ R)
have rw₆ : Eq (α := MvPolynomial σ R) (X i) (X i)
Tactic: rw [rename, killCompl, aeval_X, comp_apply, aeval_X, dif_pos ⟨i, rfl⟩,
      Equiv.ofInjective_symm_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
⊢ Eq (α := MvPolynomial σ S)
    ((killCompl hf : (a : MvPolynomial τ S) → MvPolynomial σ S)
        ((map φ : (a : MvPolynomial τ R) → MvPolynomial τ S) p) :
      MvPolynomial σ S)
    ((map φ : (a : MvPolynomial σ R) → MvPolynomial σ S)
        ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) p) :
      MvPolynomial σ S)
have simp : Eq (α := MvPolynomial σ S)
  ((RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) :
        (a : MvPolynomial τ R) → MvPolynomial σ S)
      p :
    MvPolynomial σ S)
  ((RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R) :
        (a : MvPolynomial τ R) → MvPolynomial σ S)
      p :
    MvPolynomial σ S)
Tactic: simp only [← AlgHom.coe_toRingHom, ← RingHom.comp_apply]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
⊢ Eq (α := MvPolynomial σ S)
    ((RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        p :
      MvPolynomial σ S)
    ((RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        p :
      MvPolynomial σ S)
have e_a : RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) =
  RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R)
Tactic: congr
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
⊢ RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) =
    RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R)
have e_a : ∀ (i : R) (n : σ →₀ ℕ),
  Eq.{u_5 + 1} (α := S)
    (coeff n
      ((RingHom.comp (RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ)) C :
          (a : R) → MvPolynomial σ S)
        i))
    (coeff n
      ((RingHom.comp (RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R)) C :
          (a : R) → MvPolynomial σ S)
        i))
Tactic: ext i n
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
e_a :
  ∀ (i : R) (n : σ →₀ ℕ),
    Eq.{u_5 + 1} (α := S)
      (coeff n
        ((RingHom.comp (RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ)) C :
            (a : R) → MvPolynomial σ S)
          i))
      (coeff n
        ((RingHom.comp (RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R)) C :
            (a : R) → MvPolynomial σ S)
          i))
⊢ RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) =
    RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R)
have e_a₁ : ∀ (i : τ) (n : σ →₀ ℕ),
  Eq.{u_5 + 1} (α := S)
    (coeff n
      ((RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        (X i)))
    (coeff n
      ((RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        (X i)))
Tactic: ext i n
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
i : τ
n : σ →₀ ℕ
⊢ Eq.{u_5 + 1} (α := S)
    (coeff n
      ((RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        (X i)))
    (coeff n
      ((RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        (X i)))
have pos : ∀ (h : i ∈ range f),
  Eq.{u_5 + 1} (α := S)
    (coeff n
      ((RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        (X i)))
    (coeff n
      ((RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        (X i)))
Tactic: by_cases h : i ∈ Set.range f
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
S : Type u_5
inst : CommSemiring R
inst_1 : CommSemiring S
f : σ → τ
hf : Injective f
φ : R →+* S
p : MvPolynomial τ R
i : τ
n : σ →₀ ℕ
pos :
  ∀ (h : i ∈ range f),
    Eq.{u_5 + 1} (α := S)
      (coeff n
        ((RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) :
            (a : MvPolynomial τ R) → MvPolynomial σ S)
          (X i)))
      (coeff n
        ((RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R) :
            (a : MvPolynomial τ R) → MvPolynomial σ S)
          (X i)))
⊢ Eq.{u_5 + 1} (α := S)
    (coeff n
      ((RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        (X i)))
    (coeff n
      ((RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        (X i)))
have neg : ∀ (h : i ∉ range f),
  Eq.{u_5 + 1} (α := S)
    (coeff n
      ((RingHom.comp (↑(killCompl hf) : MvPolynomial τ S →+* MvPolynomial σ S) (map φ) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        (X i)))
    (coeff n
      ((RingHom.comp (map φ) (↑(killCompl hf) : MvPolynomial τ R →+* MvPolynomial σ R) :
          (a : MvPolynomial τ R) → MvPolynomial σ S)
        (X i)))
Tactic: by_cases h : i ∈ Set.range f
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
a : τ
ha : a ∈ s.support
hs : a ∉ range f
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)
have rw : HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
    ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
    (∏ a ∈ s.support,
        HPow.hPow (α := MvPolynomial σ R) (β := ℕ)
          (if h : a ∈ range f then
            X
              (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) a h))
          else 0)
          ((s : (a : τ) → ℕ) a : ℕ) :
      MvPolynomial σ R) =
  0
Tactic: rw [killCompl, aeval_monomial, Finsupp.prod]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
a : τ
ha : a ∈ s.support
hs : a ∉ range f
⊢ HMul.hMul (α := MvPolynomial σ R) (β := MvPolynomial σ R)
      ((algebraMap R (MvPolynomial σ R) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
      (∏ a ∈ s.support,
          HPow.hPow (α := MvPolynomial σ R) (β := ℕ)
            (if h : a ∈ range f then
              X
                (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
                  (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) a h))
            else 0)
            ((s : (a : τ) → ℕ) a : ℕ) :
        MvPolynomial σ R) =
    0
have h : Eq (α := MvPolynomial σ R)
  (∏ a ∈ s.support,
    HPow.hPow (α := MvPolynomial σ R) (β := ℕ)
      (if h : a ∈ range f then
        X
          (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
            (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) a h))
      else 0)
      ((s : (a : τ) → ℕ) a : ℕ))
  0
Tactic: apply mul_eq_zero_of_right
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
a : τ
ha : a ∈ s.support
hs : a ∉ range f
⊢ Eq (α := MvPolynomial σ R)
    (∏ a ∈ s.support,
      HPow.hPow (α := MvPolynomial σ R) (β := ℕ)
        (if h : a ∈ range f then
          X
            (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
              (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) a h))
        else 0)
        ((s : (a : τ) → ℕ) a : ℕ))
    0
have h : HPow.hPow (α := MvPolynomial σ R) (β := ℕ)
    (if h : a ∈ range f then
      X
        (((Equiv.ofInjective f hf).symm : (a : (↑(range f) : Type u_2)) → σ)
          (Subtype.mk (p := fun (x : τ) ↦ x ∈ range f) a h))
    else 0)
    ((s : (a : τ) → ℕ) a : ℕ) =
  0
Tactic: apply Finset.prod_eq_zero ha
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
hs : (↑s.support : Set τ) ⊆ range f
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    ((monomial (Finsupp.comapDomain f s ⋯) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
have nth_rw : Eq (α := MvPolynomial σ R)
  ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
      ((monomial (Finsupp.mapDomain f (Finsupp.comapDomain f s sorry)) : (a : R) → MvPolynomial τ R) c) :
    MvPolynomial σ R)
  ((monomial (Finsupp.comapDomain f s sorry) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
Tactic: nth_rw 1 [← s.mapDomain_comapDomain f hf hs, killCompl_monomial_mapDomain]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
hs : (↑s.support : Set τ) ⊆ range f
nth_rw :
  Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
        ((monomial (Finsupp.mapDomain f (Finsupp.comapDomain f s ⋯)) : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    ((monomial (Finsupp.comapDomain f s ⋯) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    ((monomial (Finsupp.comapDomain f s ⋯) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
have nth_rw₁ : Eq (α := MvPolynomial σ R) ((monomial (Finsupp.comapDomain f s sorry) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
  ((monomial (Finsupp.comapDomain f s sorry) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
Tactic: nth_rw 1 [← s.mapDomain_comapDomain f hf hs, killCompl_monomial_mapDomain]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
inst_1 : Decidable ((↑s.support : Set τ) ⊆ range f)
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    (if (↑s.support : Set τ) ⊆ range f then (monomial (Finsupp.comapDomain f s ⋯) : (a : R) → MvPolynomial σ R) c
      else 0 :
      MvPolynomial σ R)
have pos : ∀ (h : (↑s.support : Set τ) ⊆ range f),
  Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    ((monomial (Finsupp.comapDomain f s sorry) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
s : τ →₀ ℕ
c : R
inst_1 : Decidable ((↑s.support : Set τ) ⊆ range f)
pos :
  ∀ (h : (↑s.support : Set τ) ⊆ range f),
    Eq (α := MvPolynomial σ R)
      ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
        MvPolynomial σ R)
      ((monomial (Finsupp.comapDomain f s ⋯) : (a : R) → MvPolynomial σ R) c : MvPolynomial σ R)
⊢ Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    (if (↑s.support : Set τ) ⊆ range f then (monomial (Finsupp.comapDomain f s ⋯) : (a : R) → MvPolynomial σ R) c
      else 0 :
      MvPolynomial σ R)
have neg : ∀ (h : ¬(↑s.support : Set τ) ⊆ range f),
  Eq (α := MvPolynomial σ R)
    ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R) ((monomial s : (a : R) → MvPolynomial τ R) c) :
      MvPolynomial σ R)
    (0 : MvPolynomial σ R)
Tactic: split_ifs with h