awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ Eq (α := MvPolynomial α R)
    (eval₂ (RingHom.comp (β := MvPolynomial τ R) (eval₂Hom (algebraMap R (MvPolynomial α R)) fun (x : τ) ↦ X (g x)) C)
        (fun (x : σ) ↦ X (g (f x))) p :
      MvPolynomial α R)
    ((eval₂Hom (algebraMap R (MvPolynomial α R)) fun (x : σ) ↦ X (g (f x)) : (a : MvPolynomial σ R) → MvPolynomial α R)
        p :
      MvPolynomial α R)
have refine : Eq (α := R →+* MvPolynomial α R)
  (RingHom.comp (β := MvPolynomial τ R) (eval₂Hom (algebraMap R (MvPolynomial α R)) fun (x : τ) ↦ X (g x)) C)
  (algebraMap R (MvPolynomial α R))
Tactic: refine eval₂Hom_congr ?_ rfl rfl
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
inst : CommSemiring R
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ Eq (α := R →+* MvPolynomial α R)
    (RingHom.comp (β := MvPolynomial τ R) (eval₂Hom (algebraMap R (MvPolynomial α R)) fun (x : τ) ↦ X (g x)) C)
    (algebraMap R (MvPolynomial α R))
have a : ∀ (x : R),
  Eq (α := MvPolynomial α R)
    ((RingHom.comp (β := MvPolynomial τ R) (eval₂Hom (algebraMap R (MvPolynomial α R)) fun (x : τ) ↦ X (g x)) C :
          (a : R) → MvPolynomial α R)
        x :
      MvPolynomial α R)
    ((algebraMap R (MvPolynomial α R) : (a : R) → MvPolynomial α R) x : MvPolynomial α R)
Tactic: ext1
-- 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 : σ → τ
d : σ →₀ ℕ
r : R
⊢ Eq (α := MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((monomial d : (a : R) → MvPolynomial σ R) r) :
      MvPolynomial τ R)
    ((monomial (Finsupp.mapDomain f d) : (a : R) → MvPolynomial τ R) r : MvPolynomial τ R)
have rw : HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) r : MvPolynomial τ R)
    (d.prod fun (i : σ) (k : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) i) k : MvPolynomial τ R) =
  HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) r : MvPolynomial τ R)
    (d.prod fun (a : σ) (m : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) (X (f a)) m : MvPolynomial τ R)
Tactic: rw [rename, aeval_monomial, monomial_eq (s := Finsupp.mapDomain f d),
    Finsupp.prod_mapDomain_index, algebraMap_eq]
-- 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 : σ → τ
d : σ →₀ ℕ
r : R
rw :
  HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) r : MvPolynomial τ R)
      (d.prod fun (i : σ) (k : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) i) k : MvPolynomial τ R) =
    HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) r : MvPolynomial τ R)
      (d.prod fun (a : σ) (m : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) (X (f a)) m : MvPolynomial τ R)
⊢ Eq (α := MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((monomial d : (a : R) → MvPolynomial σ R) r) :
      MvPolynomial τ R)
    ((monomial (Finsupp.mapDomain f d) : (a : R) → MvPolynomial τ R) r : MvPolynomial τ R)
have h_zero : ∀ (b : τ), HPow.hPow (α := MvPolynomial τ R) (β := ℕ) (X b) 0 = 1
Tactic: rw [rename, aeval_monomial, monomial_eq (s := Finsupp.mapDomain f d),
    Finsupp.prod_mapDomain_index, algebraMap_eq]
-- 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 : σ → τ
d : σ →₀ ℕ
r : R
rw :
  HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) r : MvPolynomial τ R)
      (d.prod fun (i : σ) (k : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) i) k : MvPolynomial τ R) =
    HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) r : MvPolynomial τ R)
      (d.prod fun (a : σ) (m : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) (X (f a)) m : MvPolynomial τ R)
h_zero : ∀ (b : τ), HPow.hPow (α := MvPolynomial τ R) (β := ℕ) (X b) 0 = 1
⊢ Eq (α := MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) ((monomial d : (a : R) → MvPolynomial σ R) r) :
      MvPolynomial τ R)
    ((monomial (Finsupp.mapDomain f d) : (a : R) → MvPolynomial τ R) r : MvPolynomial τ R)
have h_add : ∀ (b : τ) (m₁ m₂ : ℕ),
  HPow.hPow (α := MvPolynomial τ R) (X b) (m₁ + m₂) =
    HPow.hPow (α := MvPolynomial τ R) (X b) m₁ * HPow.hPow (α := MvPolynomial τ R) (X b) m₂
Tactic: rw [rename, aeval_monomial, monomial_eq (s := Finsupp.mapDomain f d),
    Finsupp.prod_mapDomain_index, algebraMap_eq]
-- 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 : σ → τ
p : MvPolynomial σ R
⊢ (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
have simp_rw : (aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
Tactic: simp_rw [rename, aeval_def, eval₂, Finsupp.mapDomain, algebraMap_eq, comp_apply,
    X_pow_eq_monomial, ← monomial_finsupp_sum_index, ← single_eq_monomial, AddMonoidAlgebra.coeff]
-- 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 : σ → τ
p : MvPolynomial σ R
simp_rw : (aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
⊢ (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
have simp_rw₁ : eval₂ (algebraMap R (MvPolynomial τ R)) (X ∘ f) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
Tactic: simp_rw [rename, aeval_def, eval₂, Finsupp.mapDomain, algebraMap_eq, comp_apply,
    X_pow_eq_monomial, ← monomial_finsupp_sum_index, ← single_eq_monomial, AddMonoidAlgebra.coeff]
-- 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 : σ → τ
p : MvPolynomial σ R
simp_rw : (aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₁ : eval₂ (algebraMap R (MvPolynomial τ R)) (X ∘ f) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
⊢ (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
have simp_rw₂ : ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
    HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
      ((algebraMap R (MvPolynomial τ R) : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
      (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R)) =
  Finsupp.mapDomain (Finsupp.mapDomain f) p
Tactic: simp_rw [rename, aeval_def, eval₂, Finsupp.mapDomain, algebraMap_eq, comp_apply,
    X_pow_eq_monomial, ← monomial_finsupp_sum_index, ← single_eq_monomial, AddMonoidAlgebra.coeff]
-- 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 : σ → τ
p : MvPolynomial σ R
simp_rw : (aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₁ : eval₂ (algebraMap R (MvPolynomial τ R)) (X ∘ f) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₂ :
  ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
        ((algebraMap R (MvPolynomial τ R) : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R)) =
    Finsupp.mapDomain (Finsupp.mapDomain f) p
⊢ (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
have simp_rw₃ : Eq (α := MvPolynomial τ R)
  ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
    HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
      ((algebraMap R (MvPolynomial τ R) : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
      (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R))
  (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
Tactic: simp_rw [rename, aeval_def, eval₂, Finsupp.mapDomain, algebraMap_eq, comp_apply,
    X_pow_eq_monomial, ← monomial_finsupp_sum_index, ← single_eq_monomial, AddMonoidAlgebra.coeff]
-- 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 : σ → τ
p : MvPolynomial σ R
simp_rw : (aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₁ : eval₂ (algebraMap R (MvPolynomial τ R)) (X ∘ f) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₂ :
  ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
        ((algebraMap R (MvPolynomial τ R) : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R)) =
    Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₃ :
  Eq (α := MvPolynomial τ R)
    ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
        ((algebraMap R (MvPolynomial τ R) : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R))
    (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
⊢ (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
have simp_rw₄ : Eq (α := MvPolynomial τ R)
  ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
    HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
      (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R))
  (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
Tactic: simp_rw [rename, aeval_def, eval₂, Finsupp.mapDomain, algebraMap_eq, comp_apply,
    X_pow_eq_monomial, ← monomial_finsupp_sum_index, ← single_eq_monomial, AddMonoidAlgebra.coeff]
-- 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 : σ → τ
p : MvPolynomial σ R
simp_rw : (aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₁ : eval₂ (algebraMap R (MvPolynomial τ R)) (X ∘ f) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₂ :
  ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
        ((algebraMap R (MvPolynomial τ R) : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R)) =
    Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₃ :
  Eq (α := MvPolynomial τ R)
    ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
        ((algebraMap R (MvPolynomial τ R) : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R))
    (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
simp_rw₄ :
  Eq (α := MvPolynomial τ R)
    ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R))
    (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
⊢ (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
have simp_rw₅ : Eq (α := MvPolynomial τ R)
  ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
    HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
      (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) (X (f n)) e : MvPolynomial τ R))
  (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
Tactic: simp_rw [rename, aeval_def, eval₂, Finsupp.mapDomain, algebraMap_eq, comp_apply,
    X_pow_eq_monomial, ← monomial_finsupp_sum_index, ← single_eq_monomial, AddMonoidAlgebra.coeff]
-- 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 : σ → τ
p : MvPolynomial σ R
simp_rw : (aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₁ : eval₂ (algebraMap R (MvPolynomial τ R)) (X ∘ f) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₂ :
  ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
        ((algebraMap R (MvPolynomial τ R) : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R)) =
    Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₃ :
  Eq (α := MvPolynomial τ R)
    ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
        ((algebraMap R (MvPolynomial τ R) : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R))
    (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
simp_rw₄ :
  Eq (α := MvPolynomial τ R)
    ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R))
    (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
simp_rw₅ :
  Eq (α := MvPolynomial τ R)
    ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) (X (f n)) e : MvPolynomial τ R))
    (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
⊢ (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
have simp_rw₆ : Eq (α := MvPolynomial τ R)
  ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
    HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
      (s.prod fun (n : σ) (e : ℕ) ↦ (monomial (Finsupp.single (f n) e) : (a : R) → MvPolynomial τ R) 1 :
        MvPolynomial τ R))
  (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
Tactic: simp_rw [rename, aeval_def, eval₂, Finsupp.mapDomain, algebraMap_eq, comp_apply,
    X_pow_eq_monomial, ← monomial_finsupp_sum_index, ← single_eq_monomial, AddMonoidAlgebra.coeff]
-- 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 : σ → τ
p : MvPolynomial σ R
simp_rw : (aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₁ : eval₂ (algebraMap R (MvPolynomial τ R)) (X ∘ f) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₂ :
  ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
        ((algebraMap R (MvPolynomial τ R) : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R)) =
    Finsupp.mapDomain (Finsupp.mapDomain f) p
simp_rw₃ :
  Eq (α := MvPolynomial τ R)
    ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R)
        ((algebraMap R (MvPolynomial τ R) : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R))
    (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
simp_rw₄ :
  Eq (α := MvPolynomial τ R)
    ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) ((X ∘ f) n) e : MvPolynomial τ R))
    (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
simp_rw₅ :
  Eq (α := MvPolynomial τ R)
    ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ HPow.hPow (α := MvPolynomial τ R) (X (f n)) e : MvPolynomial τ R))
    (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
simp_rw₆ :
  Eq (α := MvPolynomial τ R)
    ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
      HMul.hMul (α := MvPolynomial τ R) (β := MvPolynomial τ R) ((C : (a : R) → MvPolynomial τ R) a : MvPolynomial τ R)
        (s.prod fun (n : σ) (e : ℕ) ↦ (monomial (Finsupp.single (f n) e) : (a : R) → MvPolynomial τ R) 1 :
          MvPolynomial τ R))
    (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
⊢ (rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
have simp_rw₇ : Eq (α := MvPolynomial τ R)
  ((AddMonoidAlgebra.coeff p).sum fun (s : σ →₀ ℕ) (a : R) ↦
    (monomial (s.sum fun (a : σ) ↦ Finsupp.single (f a)) : (a : R) → MvPolynomial τ R) a)
  (sum p fun (a : σ →₀ ℕ) ↦ Finsupp.single (a.sum fun (a : σ) ↦ Finsupp.single (f a)))
Tactic: simp_rw [rename, aeval_def, eval₂, Finsupp.mapDomain, algebraMap_eq, comp_apply,
    X_pow_eq_monomial, ← monomial_finsupp_sum_index, ← single_eq_monomial, AddMonoidAlgebra.coeff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (hypothesis)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
f : σ → τ
hf : Injective f
⊢ Injective (α := MvPolynomial σ R) (β := MvPolynomial τ R) (⇑(rename f) : (a : MvPolynomial σ R) → MvPolynomial τ R)
have this : Eq (α := (a : MvPolynomial σ R) → MvPolynomial τ R) (⇑(rename f) : (a : MvPolynomial σ R) → MvPolynomial τ R)
  (Finsupp.mapDomain (Finsupp.mapDomain f))
Tactic: have :
    (rename f : MvPolynomial σ R → MvPolynomial τ R) = Finsupp.mapDomain (Finsupp.mapDomain f) :=
    funext (rename_eq 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
this :
  Eq (α := (a : MvPolynomial σ R) → MvPolynomial τ R) (⇑(rename f) : (a : MvPolynomial σ R) → MvPolynomial τ R)
    (Finsupp.mapDomain (Finsupp.mapDomain f))
⊢ Injective (α := MvPolynomial σ R) (β := MvPolynomial τ R) (⇑(rename f) : (a : MvPolynomial σ R) → MvPolynomial τ R)
have rw : Injective (α := MvPolynomial σ R) (Finsupp.mapDomain (Finsupp.mapDomain f))
Tactic: rw [this]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
hf : Injective f
⊢ Eq (α := MvPolynomial τ R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
      (0 : MvPolynomial τ R) ↔
    p = 0
have rw : Eq (α := MvPolynomial τ R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
    ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) 0 : MvPolynomial τ R) ↔
  p = 0
Tactic: rw [← rename_zero f, (MvPolynomial.rename_injective _ hf).eq_iff]
-- Lean 4 proof step from Mathlib.Algebra.MvPolynomial.Rename (goal)
Goal:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst : CommSemiring R
p : MvPolynomial σ R
f : σ → τ
hf : Injective f
rw :
  Eq (α := MvPolynomial τ R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
      ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) 0 : MvPolynomial τ R) ↔
    p = 0
⊢ Eq (α := MvPolynomial τ R) ((rename f : (a : MvPolynomial σ R) → MvPolynomial τ R) p : MvPolynomial τ R)
      (0 : MvPolynomial τ R) ↔
    p = 0
have rw₁ : p = 0 ↔ p = 0
Tactic: rw [← rename_zero f, (MvPolynomial.rename_injective _ hf).eq_iff]
-- 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 : σ
⊢ Eq (α := MvPolynomial σ R)
    ((AlgHom.comp (killCompl hf) (rename f) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
    ((AlgHom.id R (MvPolynomial σ R) : (a : MvPolynomial σ R) → MvPolynomial σ R) (X i) : MvPolynomial σ R)
have dsimp : 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)
Tactic: dsimp
-- 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 : σ
⊢ 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)
  ((killCompl hf : (a : MvPolynomial τ R) → MvPolynomial σ R)
      ((aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X 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)
⊢ 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)
      ((aeval (X ∘ f) : (a : MvPolynomial σ R) → MvPolynomial τ R) (X 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]