σ : Type u_1
τ : Type u_2
α : Type ?u.263211
R : Type u_3
S : Type ?u.263217
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
this : ↑(rename f) = Finsupp.mapDomain (Finsupp.mapDomain f)
⊢ Injective ↑(rename f)
σ : Type u_1
τ : Type u_2
α : Type ?u.263211
R : Type u_3
S : Type ?u.263217
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
⊢ Injective ↑(rename f)
have :
  (rename f : MvPolynomial σ R → MvPolynomial τ R) = Finsupp.mapDomain (Finsupp.mapDomain f) :=
  funext (rename_eq f)
σ : Type u_1
τ : Type u_2
α : Type ?u.263211
R : Type u_3
S : Type ?u.263217
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
this : ↑(rename f) = Finsupp.mapDomain (Finsupp.mapDomain f)
⊢ Injective (Finsupp.mapDomain (Finsupp.mapDomain f))
σ : Type u_1
τ : Type u_2
α : Type ?u.263211
R : Type u_3
S : Type ?u.263217
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
this : ↑(rename f) = Finsupp.mapDomain (Finsupp.mapDomain f)
⊢ Injective ↑(rename f)
rw [this]
no goals
σ : Type u_1
τ : Type u_2
α : Type ?u.263211
R : Type u_3
S : Type ?u.263217
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
this : ↑(rename f) = Finsupp.mapDomain (Finsupp.mapDomain f)
⊢ Injective (Finsupp.mapDomain (Finsupp.mapDomain f))
exact Finsupp.mapDomain_injective (Finsupp.mapDomain_injective hf)