[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p : MvPolynomial σ R
⊢ ↑(map f) (↑(rename g) p) = ↑(rename g) (↑(map f) p)
[PROOFSTEP]
apply
  MvPolynomial.induction_on p (fun a => by simp only [map_C, rename_C])
    (fun p q hp hq => by simp only [hp, hq, AlgHom.map_add, RingHom.map_add]) fun p n hp => by
    simp only [hp, rename_X, map_X, RingHom.map_mul, AlgHom.map_mul]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p : MvPolynomial σ R
a : R
⊢ ↑(map f) (↑(rename g) (↑C a)) = ↑(rename g) (↑(map f) (↑C a))
[PROOFSTEP]
simp only [map_C, rename_C]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p✝ p q : MvPolynomial σ R
hp : ↑(map f) (↑(rename g) p) = ↑(rename g) (↑(map f) p)
hq : ↑(map f) (↑(rename g) q) = ↑(rename g) (↑(map f) q)
⊢ ↑(map f) (↑(rename g) (p + q)) = ↑(rename g) (↑(map f) (p + q))
[PROOFSTEP]
simp only [hp, hq, AlgHom.map_add, RingHom.map_add]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
g : σ → τ
p✝ p : MvPolynomial σ R
n : σ
hp : ↑(map f) (↑(rename g) p) = ↑(rename g) (↑(map f) p)
⊢ ↑(map f) (↑(rename g) (p * X n)) = ↑(rename g) (↑(map f) (p * X n))
[PROOFSTEP]
simp only [hp, rename_X, map_X, RingHom.map_mul, AlgHom.map_mul]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ ↑(rename g) (eval₂ C (X ∘ f) p) = ↑(rename (g ∘ f)) p
[PROOFSTEP]
simp only [rename, aeval_eq_eval₂Hom]
  -- porting note: the Lean 3 proof of this was very fragile and included a nonterminal `simp`.
      -- Hopefully this is less prone to breaking
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ ↑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) (eval₂ C (X ∘ f) p) =
    ↑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f)) p
[PROOFSTEP]
rw [eval₂_comp_left (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) C (X ∘ f) p]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ eval₂ (RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) C)
      (↑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g)) ∘ X ∘ f) p =
    ↑(eval₂Hom (algebraMap R (MvPolynomial α R)) (X ∘ g ∘ f)) p
[PROOFSTEP]
simp only [(· ∘ ·), eval₂Hom_X', coe_eval₂Hom]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ eval₂ (RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)) C) (fun x => X (g (f x))) p =
    eval₂ (algebraMap R (MvPolynomial α R)) (fun x => X (g (f x))) p
[PROOFSTEP]
refine' eval₂Hom_congr _ rfl rfl
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
⊢ RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)) C = algebraMap R (MvPolynomial α R)
[PROOFSTEP]
ext1
[GOAL]
case a
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
g : τ → α
p : MvPolynomial σ R
x✝ : R
⊢ ↑(RingHom.comp (eval₂Hom (algebraMap R (MvPolynomial α R)) fun x => X (g x)) C) x✝ =
    ↑(algebraMap R (MvPolynomial α R)) x✝
[PROOFSTEP]
simp only [comp_apply, RingHom.coe_comp, eval₂Hom_C]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ ↑(rename f) (↑(monomial d) r) = ↑(monomial (Finsupp.mapDomain f d)) r
[PROOFSTEP]
rw [rename, aeval_monomial, monomial_eq (s := Finsupp.mapDomain f d), Finsupp.prod_mapDomain_index]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ (↑(algebraMap R (MvPolynomial τ R)) r * Finsupp.prod d fun i k => (X ∘ f) i ^ k) =
    ↑C r * Finsupp.prod d fun a m => X (f a) ^ m
[PROOFSTEP]
rfl
[GOAL]
case h_zero
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ ∀ (b : τ), X b ^ 0 = 1
[PROOFSTEP]
exact fun n => pow_zero _
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
d : σ →₀ ℕ
r : R
⊢ ∀ (b : τ) (m₁ m₂ : ℕ), X b ^ (m₁ + m₂) = X b ^ m₁ * X b ^ m₂
[PROOFSTEP]
exact fun n i₁ i₂ => pow_add _ _ _
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
p : MvPolynomial σ R
⊢ ↑(rename f) p = Finsupp.mapDomain (Finsupp.mapDomain f) p
[PROOFSTEP]
simp only [rename, aeval_def, eval₂, Finsupp.mapDomain, algebraMap_eq, comp_apply, X_pow_eq_monomial, ←
  monomial_finsupp_sum_index]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
p : MvPolynomial σ R
⊢ (sum p fun s a => ↑(monomial (sum s fun a b => Finsupp.single (f a) b)) a) =
    sum p fun a => Finsupp.single (sum a fun a => Finsupp.single (f a))
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
⊢ Injective ↑(rename f)
[PROOFSTEP]
have : (rename f : MvPolynomial σ R → MvPolynomial τ R) = Finsupp.mapDomain (Finsupp.mapDomain f) :=
  funext (rename_eq f)
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
this : ↑(rename f) = Finsupp.mapDomain (Finsupp.mapDomain f)
⊢ Injective ↑(rename f)
[PROOFSTEP]
rw [this]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
this : ↑(rename f) = Finsupp.mapDomain (Finsupp.mapDomain f)
⊢ Injective (Finsupp.mapDomain (Finsupp.mapDomain f))
[PROOFSTEP]
exact Finsupp.mapDomain_injective (Finsupp.mapDomain_injective hf)
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
i : σ
⊢ ↑(AlgHom.comp (killCompl hf) (rename f)) (X i) = ↑(AlgHom.id R (MvPolynomial σ R)) (X i)
[PROOFSTEP]
dsimp
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
i : σ
⊢ ↑(killCompl hf) (↑(rename f) (X i)) = X i
[PROOFSTEP]
rw [rename, killCompl, aeval_X, comp_apply, aeval_X, dif_pos, Equiv.ofInjective_symm_apply]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ ≃ τ
src✝ : MvPolynomial σ R →ₐ[R] MvPolynomial τ R := rename ↑f
p : MvPolynomial σ R
⊢ ↑(rename ↑f.symm) (↑(rename ↑f) p) = p
[PROOFSTEP]
rw [rename_rename, f.symm_comp_self, rename_id]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ ≃ τ
src✝ : MvPolynomial σ R →ₐ[R] MvPolynomial τ R := rename ↑f
p : MvPolynomial τ R
⊢ ↑(rename ↑f) (↑(rename ↑f.symm) p) = p
[PROOFSTEP]
rw [rename_rename, f.self_comp_symm, rename_id]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ eval₂ f g (↑(rename k) p) = eval₂ f (g ∘ k) p
[PROOFSTEP]
apply MvPolynomial.induction_on p
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ ∀ (a : R), eval₂ f g (↑(rename k) (↑C a)) = eval₂ f (g ∘ k) (↑C a)
[PROOFSTEP]
intros
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
a✝ : R
⊢ eval₂ f g (↑(rename k) (↑C a✝)) = eval₂ f (g ∘ k) (↑C a✝)
[PROOFSTEP]
simp [*]
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    eval₂ f g (↑(rename k) p) = eval₂ f (g ∘ k) p →
      eval₂ f g (↑(rename k) q) = eval₂ f (g ∘ k) q → eval₂ f g (↑(rename k) (p + q)) = eval₂ f (g ∘ k) (p + q)
[PROOFSTEP]
intros
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p p✝ q✝ : MvPolynomial σ R
a✝¹ : eval₂ f g (↑(rename k) p✝) = eval₂ f (g ∘ k) p✝
a✝ : eval₂ f g (↑(rename k) q✝) = eval₂ f (g ∘ k) q✝
⊢ eval₂ f g (↑(rename k) (p✝ + q✝)) = eval₂ f (g ∘ k) (p✝ + q✝)
[PROOFSTEP]
simp [*]
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    eval₂ f g (↑(rename k) p) = eval₂ f (g ∘ k) p → eval₂ f g (↑(rename k) (p * X n)) = eval₂ f (g ∘ k) (p * X n)
[PROOFSTEP]
intros
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g : τ → S
p p✝ : MvPolynomial σ R
n✝ : σ
a✝ : eval₂ f g (↑(rename k) p✝) = eval₂ f (g ∘ k) p✝
⊢ eval₂ f g (↑(rename k) (p✝ * X n✝)) = eval₂ f (g ∘ k) (p✝ * X n✝)
[PROOFSTEP]
simp [*]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ↑(rename k) (eval₂ C (g ∘ k) p) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) p)
[PROOFSTEP]
apply MvPolynomial.induction_on p
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ∀ (a : R), ↑(rename k) (eval₂ C (g ∘ k) (↑C a)) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) (↑C a))
[PROOFSTEP]
intros
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
a✝ : R
⊢ ↑(rename k) (eval₂ C (g ∘ k) (↑C a✝)) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) (↑C a✝))
[PROOFSTEP]
simp [*]
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    ↑(rename k) (eval₂ C (g ∘ k) p) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) p) →
      ↑(rename k) (eval₂ C (g ∘ k) q) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) q) →
        ↑(rename k) (eval₂ C (g ∘ k) (p + q)) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) (p + q))
[PROOFSTEP]
intros
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
p✝ q✝ : MvPolynomial σ R
a✝¹ : ↑(rename k) (eval₂ C (g ∘ k) p✝) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) p✝)
a✝ : ↑(rename k) (eval₂ C (g ∘ k) q✝) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) q✝)
⊢ ↑(rename k) (eval₂ C (g ∘ k) (p✝ + q✝)) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) (p✝ + q✝))
[PROOFSTEP]
simp [*]
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    ↑(rename k) (eval₂ C (g ∘ k) p) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) p) →
      ↑(rename k) (eval₂ C (g ∘ k) (p * X n)) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) (p * X n))
[PROOFSTEP]
intros
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
g : τ → MvPolynomial σ R
p✝ : MvPolynomial σ R
n✝ : σ
a✝ : ↑(rename k) (eval₂ C (g ∘ k) p✝) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) p✝)
⊢ ↑(rename k) (eval₂ C (g ∘ k) (p✝ * X n✝)) = eval₂ C (↑(rename k) ∘ g) (↑(rename k) (p✝ * X n✝))
[PROOFSTEP]
simp [*]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ↑(rename (Prod.mk j)) (eval₂ C g p) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) p
[PROOFSTEP]
apply MvPolynomial.induction_on p
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ∀ (a : R), ↑(rename (Prod.mk j)) (eval₂ C g (↑C a)) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) (↑C a)
[PROOFSTEP]
intros
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
a✝ : R
⊢ ↑(rename (Prod.mk j)) (eval₂ C g (↑C a✝)) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) (↑C a✝)
[PROOFSTEP]
simp [*]
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    ↑(rename (Prod.mk j)) (eval₂ C g p) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) p →
      ↑(rename (Prod.mk j)) (eval₂ C g q) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) q →
        ↑(rename (Prod.mk j)) (eval₂ C g (p + q)) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) (p + q)
[PROOFSTEP]
intros
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
p✝ q✝ : MvPolynomial σ R
a✝¹ : ↑(rename (Prod.mk j)) (eval₂ C g p✝) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) p✝
a✝ : ↑(rename (Prod.mk j)) (eval₂ C g q✝) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) q✝
⊢ ↑(rename (Prod.mk j)) (eval₂ C g (p✝ + q✝)) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) (p✝ + q✝)
[PROOFSTEP]
simp [*]
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    ↑(rename (Prod.mk j)) (eval₂ C g p) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) p →
      ↑(rename (Prod.mk j)) (eval₂ C g (p * X n)) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) (p * X n)
[PROOFSTEP]
intros
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p : MvPolynomial σ R
j : τ
g : σ → MvPolynomial σ R
p✝ : MvPolynomial σ R
n✝ : σ
a✝ : ↑(rename (Prod.mk j)) (eval₂ C g p✝) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) p✝
⊢ ↑(rename (Prod.mk j)) (eval₂ C g (p✝ * X n✝)) = eval₂ C (fun x => ↑(rename (Prod.mk j)) (g x)) (p✝ * X n✝)
[PROOFSTEP]
simp [*]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p✝ : MvPolynomial σ R
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ eval₂ f g (↑(rename (Prod.mk i)) p) = eval₂ f (fun j => g (i, j)) p
[PROOFSTEP]
apply MvPolynomial.induction_on p
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p✝ : MvPolynomial σ R
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ ∀ (a : R), eval₂ f g (↑(rename (Prod.mk i)) (↑C a)) = eval₂ f (fun j => g (i, j)) (↑C a)
[PROOFSTEP]
intros
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p✝ : MvPolynomial σ R
g : σ × τ → S
i : σ
p : MvPolynomial τ R
a✝ : R
⊢ eval₂ f g (↑(rename (Prod.mk i)) (↑C a✝)) = eval₂ f (fun j => g (i, j)) (↑C a✝)
[PROOFSTEP]
simp [*]
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p✝ : MvPolynomial σ R
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ ∀ (p q : MvPolynomial τ R),
    eval₂ f g (↑(rename (Prod.mk i)) p) = eval₂ f (fun j => g (i, j)) p →
      eval₂ f g (↑(rename (Prod.mk i)) q) = eval₂ f (fun j => g (i, j)) q →
        eval₂ f g (↑(rename (Prod.mk i)) (p + q)) = eval₂ f (fun j => g (i, j)) (p + q)
[PROOFSTEP]
intros
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p✝¹ : MvPolynomial σ R
g : σ × τ → S
i : σ
p p✝ q✝ : MvPolynomial τ R
a✝¹ : eval₂ f g (↑(rename (Prod.mk i)) p✝) = eval₂ f (fun j => g (i, j)) p✝
a✝ : eval₂ f g (↑(rename (Prod.mk i)) q✝) = eval₂ f (fun j => g (i, j)) q✝
⊢ eval₂ f g (↑(rename (Prod.mk i)) (p✝ + q✝)) = eval₂ f (fun j => g (i, j)) (p✝ + q✝)
[PROOFSTEP]
simp [*]
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p✝ : MvPolynomial σ R
g : σ × τ → S
i : σ
p : MvPolynomial τ R
⊢ ∀ (p : MvPolynomial τ R) (n : τ),
    eval₂ f g (↑(rename (Prod.mk i)) p) = eval₂ f (fun j => g (i, j)) p →
      eval₂ f g (↑(rename (Prod.mk i)) (p * X n)) = eval₂ f (fun j => g (i, j)) (p * X n)
[PROOFSTEP]
intros
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : R →+* S
k : σ → τ
g✝ : τ → S
p✝¹ : MvPolynomial σ R
g : σ × τ → S
i : σ
p p✝ : MvPolynomial τ R
n✝ : τ
a✝ : eval₂ f g (↑(rename (Prod.mk i)) p✝) = eval₂ f (fun j => g (i, j)) p✝
⊢ eval₂ f g (↑(rename (Prod.mk i)) (p✝ * X n✝)) = eval₂ f (fun j => g (i, j)) (p✝ * X n✝)
[PROOFSTEP]
simp [*]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∃ s q, p = ↑(rename Subtype.val) q
[PROOFSTEP]
classical
apply induction_on p
· intro r
  exact ⟨∅, C r, by rw [rename_C]⟩
· rintro p q ⟨s, p, rfl⟩ ⟨t, q, rfl⟩
  refine' ⟨s ∪ t, ⟨_, _⟩⟩
  ·
    refine' rename (Subtype.map id _) p + rename (Subtype.map id _) q <;>
      simp (config := { contextual := true }) only [id.def, true_or_iff, or_true_iff, Finset.mem_union, forall_true_iff]
  · simp only [rename_rename, AlgHom.map_add]
    rfl
· rintro p n ⟨s, p, rfl⟩
  refine' ⟨insert n s, ⟨_, _⟩⟩
  · refine' rename (Subtype.map id _) p * X ⟨n, s.mem_insert_self n⟩
    simp (config := { contextual := true }) only [id.def, or_true_iff, Finset.mem_insert, forall_true_iff]
  · simp only [rename_rename, rename_X, Subtype.coe_mk, AlgHom.map_mul]
    rfl
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∃ s q, p = ↑(rename Subtype.val) q
[PROOFSTEP]
apply induction_on p
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∀ (a : R), ∃ s q, ↑C a = ↑(rename Subtype.val) q
[PROOFSTEP]
intro r
[GOAL]
case h_C
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
r : R
⊢ ∃ s q, ↑C r = ↑(rename Subtype.val) q
[PROOFSTEP]
exact ⟨∅, C r, by rw [rename_C]⟩
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
r : R
⊢ ↑C r = ↑(rename Subtype.val) (↑C r)
[PROOFSTEP]
rw [rename_C]
[GOAL]
case h_add
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    (∃ s q, p = ↑(rename Subtype.val) q) →
      (∃ s q_1, q = ↑(rename Subtype.val) q_1) → ∃ s q_1, p + q = ↑(rename Subtype.val) q_1
[PROOFSTEP]
rintro p q ⟨s, p, rfl⟩ ⟨t, q, rfl⟩
[GOAL]
case h_add.intro.intro.intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ∃ s_1 q_1, ↑(rename Subtype.val) p + ↑(rename Subtype.val) q = ↑(rename Subtype.val) q_1
[PROOFSTEP]
refine' ⟨s ∪ t, ⟨_, _⟩⟩
[GOAL]
case h_add.intro.intro.intro.intro.refine'_1
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ MvPolynomial { x // x ∈ s ∪ t } R
[PROOFSTEP]
refine' rename (Subtype.map id _) p + rename (Subtype.map id _) q
[GOAL]
case h_add.intro.intro.intro.intro.refine'_1.refine'_1
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ∀ (a : σ), a ∈ s → id a ∈ s ∪ t
[PROOFSTEP]
simp (config := { contextual := true }) only [id.def, true_or_iff, or_true_iff, Finset.mem_union, forall_true_iff]
[GOAL]
case h_add.intro.intro.intro.intro.refine'_1.refine'_2
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ∀ (a : σ), a ∈ t → id a ∈ s ∪ t
[PROOFSTEP]
simp (config := { contextual := true }) only [id.def, true_or_iff, or_true_iff, Finset.mem_union, forall_true_iff]
[GOAL]
case h_add.intro.intro.intro.intro.refine'_2
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ↑(rename Subtype.val) p + ↑(rename Subtype.val) q =
    ↑(rename Subtype.val)
      (↑(rename (Subtype.map id (_ : ∀ (a : σ), a ∈ s → a ∈ s ∪ t))) p +
        ↑(rename (Subtype.map id (_ : ∀ (a : σ), a ∈ t → a ∈ s ∪ t))) q)
[PROOFSTEP]
simp only [rename_rename, AlgHom.map_add]
[GOAL]
case h_add.intro.intro.intro.intro.refine'_2
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
t : Finset σ
q : MvPolynomial { x // x ∈ t } R
⊢ ↑(rename Subtype.val) p + ↑(rename Subtype.val) q =
    ↑(rename (Subtype.val ∘ Subtype.map id (_ : ∀ (a : σ), a ∈ s → a ∈ s ∪ t))) p +
      ↑(rename (Subtype.val ∘ Subtype.map id (_ : ∀ (a : σ), a ∈ t → a ∈ s ∪ t))) q
[PROOFSTEP]
rfl
[GOAL]
case h_X
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ), (∃ s q, p = ↑(rename Subtype.val) q) → ∃ s q, p * X n = ↑(rename Subtype.val) q
[PROOFSTEP]
rintro p n ⟨s, p, rfl⟩
[GOAL]
case h_X.intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ∃ s_1 q, ↑(rename Subtype.val) p * X n = ↑(rename Subtype.val) q
[PROOFSTEP]
refine' ⟨insert n s, ⟨_, _⟩⟩
[GOAL]
case h_X.intro.intro.refine'_1
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ MvPolynomial { x // x ∈ insert n s } R
[PROOFSTEP]
refine' rename (Subtype.map id _) p * X ⟨n, s.mem_insert_self n⟩
[GOAL]
case h_X.intro.intro.refine'_1
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ∀ (a : σ), a ∈ s → id a ∈ insert n s
[PROOFSTEP]
simp (config := { contextual := true }) only [id.def, or_true_iff, Finset.mem_insert, forall_true_iff]
[GOAL]
case h_X.intro.intro.refine'_2
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑(rename Subtype.val) p * X n =
    ↑(rename Subtype.val)
      (↑(rename (Subtype.map id (_ : ∀ (a : σ), a ∈ s → a ∈ insert n s))) p *
        X { val := n, property := (_ : n ∈ insert n s) })
[PROOFSTEP]
simp only [rename_rename, rename_X, Subtype.coe_mk, AlgHom.map_mul]
[GOAL]
case h_X.intro.intro.refine'_2
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p✝ : MvPolynomial σ R
n : σ
s : Finset σ
p : MvPolynomial { x // x ∈ s } R
⊢ ↑(rename Subtype.val) p * X n =
    ↑(rename (Subtype.val ∘ Subtype.map id (_ : ∀ (a : σ), a ∈ s → a ∈ insert n s))) p * X n
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p₁ p₂ : MvPolynomial σ R
⊢ ∃ s q₁ q₂, p₁ = ↑(rename Subtype.val) q₁ ∧ p₂ = ↑(rename Subtype.val) q₂
[PROOFSTEP]
obtain ⟨s₁, q₁, rfl⟩ := exists_finset_rename p₁
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p₂ : MvPolynomial σ R
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
⊢ ∃ s q₁_1 q₂, ↑(rename Subtype.val) q₁ = ↑(rename Subtype.val) q₁_1 ∧ p₂ = ↑(rename Subtype.val) q₂
[PROOFSTEP]
obtain ⟨s₂, q₂, rfl⟩ := exists_finset_rename p₂
[GOAL]
case intro.intro.intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ∃ s q₁_1 q₂_1,
    ↑(rename Subtype.val) q₁ = ↑(rename Subtype.val) q₁_1 ∧ ↑(rename Subtype.val) q₂ = ↑(rename Subtype.val) q₂_1
[PROOFSTEP]
classical
use s₁ ∪ s₂
use rename (Set.inclusion <| s₁.subset_union_left s₂) q₁
use rename (Set.inclusion <| s₁.subset_union_right s₂) q₂
constructor
  -- porting note: was `<;> simp <;> rfl` but Lean couldn't infer the arguments
· rw [rename_rename (Set.inclusion <| s₁.subset_union_left s₂)]
  rfl
· rw [rename_rename (Set.inclusion <| s₁.subset_union_right s₂)]
  rfl
[GOAL]
case intro.intro.intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ∃ s q₁_1 q₂_1,
    ↑(rename Subtype.val) q₁ = ↑(rename Subtype.val) q₁_1 ∧ ↑(rename Subtype.val) q₂ = ↑(rename Subtype.val) q₂_1
[PROOFSTEP]
use s₁ ∪ s₂
[GOAL]
case h
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ∃ q₁_1 q₂_1,
    ↑(rename Subtype.val) q₁ = ↑(rename Subtype.val) q₁_1 ∧ ↑(rename Subtype.val) q₂ = ↑(rename Subtype.val) q₂_1
[PROOFSTEP]
use rename (Set.inclusion <| s₁.subset_union_left s₂) q₁
[GOAL]
case h
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ∃ q₂_1,
    ↑(rename Subtype.val) q₁ = ↑(rename Subtype.val) (↑(rename (inclusion (_ : s₁ ⊆ s₁ ∪ s₂))) q₁) ∧
      ↑(rename Subtype.val) q₂ = ↑(rename Subtype.val) q₂_1
[PROOFSTEP]
use rename (Set.inclusion <| s₁.subset_union_right s₂) q₂
[GOAL]
case h
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ↑(rename Subtype.val) q₁ = ↑(rename Subtype.val) (↑(rename (inclusion (_ : s₁ ⊆ s₁ ∪ s₂))) q₁) ∧
    ↑(rename Subtype.val) q₂ = ↑(rename Subtype.val) (↑(rename (inclusion (_ : s₂ ⊆ s₁ ∪ s₂))) q₂)
[PROOFSTEP]
constructor
  -- porting note: was `<;> simp <;> rfl` but Lean couldn't infer the arguments
[GOAL]
case h.left
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ↑(rename Subtype.val) q₁ = ↑(rename Subtype.val) (↑(rename (inclusion (_ : s₁ ⊆ s₁ ∪ s₂))) q₁)
[PROOFSTEP]
rw [rename_rename (Set.inclusion <| s₁.subset_union_left s₂)]
[GOAL]
case h.left
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ↑(rename Subtype.val) q₁ = ↑(rename (Subtype.val ∘ inclusion (_ : s₁ ⊆ s₁ ∪ s₂))) q₁
[PROOFSTEP]
rfl
[GOAL]
case h.right
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ↑(rename Subtype.val) q₂ = ↑(rename Subtype.val) (↑(rename (inclusion (_ : s₂ ⊆ s₁ ∪ s₂))) q₂)
[PROOFSTEP]
rw [rename_rename (Set.inclusion <| s₁.subset_union_right s₂)]
[GOAL]
case h.right
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s₁ : Finset σ
q₁ : MvPolynomial { x // x ∈ s₁ } R
s₂ : Finset σ
q₂ : MvPolynomial { x // x ∈ s₂ } R
⊢ ↑(rename Subtype.val) q₂ = ↑(rename (Subtype.val ∘ inclusion (_ : s₂ ⊆ s₁ ∪ s₂))) q₂
[PROOFSTEP]
rfl
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
p : MvPolynomial σ R
⊢ ∃ n f _hf q, p = ↑(rename f) q
[PROOFSTEP]
obtain ⟨s, q, rfl⟩ := exists_finset_rename p
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
⊢ ∃ n f _hf q_1, ↑(rename Subtype.val) q = ↑(rename f) q_1
[PROOFSTEP]
let n := Fintype.card { x // x ∈ s }
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
⊢ ∃ n f _hf q_1, ↑(rename Subtype.val) q = ↑(rename f) q_1
[PROOFSTEP]
let e := Fintype.equivFin { x // x ∈ s }
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
e : { x // x ∈ s } ≃ Fin (Fintype.card { x // x ∈ s }) := Fintype.equivFin { x // x ∈ s }
⊢ ∃ n f _hf q_1, ↑(rename Subtype.val) q = ↑(rename f) q_1
[PROOFSTEP]
refine' ⟨n, (↑) ∘ e.symm, Subtype.val_injective.comp e.symm.injective, rename e q, _⟩
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
e : { x // x ∈ s } ≃ Fin (Fintype.card { x // x ∈ s }) := Fintype.equivFin { x // x ∈ s }
⊢ ↑(rename Subtype.val) q = ↑(rename (Subtype.val ∘ ↑e.symm)) (↑(rename ↑e) q)
[PROOFSTEP]
rw [← rename_rename, rename_rename e]
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
s : Finset σ
q : MvPolynomial { x // x ∈ s } R
n : ℕ := Fintype.card { x // x ∈ s }
e : { x // x ∈ s } ≃ Fin (Fintype.card { x // x ∈ s }) := Fintype.equivFin { x // x ∈ s }
⊢ ↑(rename Subtype.val) q = ↑(rename Subtype.val) (↑(rename (↑e.symm ∘ ↑e)) q)
[PROOFSTEP]
simp only [Function.comp, Equiv.symm_apply_apply, rename_rename]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
c : ℤ →+* R
g : τ → R
p : MvPolynomial σ ℤ
⊢ eval₂ c (g ∘ f) p = eval₂ c g (↑(rename f) p)
[PROOFSTEP]
apply
  MvPolynomial.induction_on p (fun n => by simp only [eval₂_C, rename_C])
    (fun p q hp hq => by simp only [hp, hq, rename, eval₂_add, AlgHom.map_add]) fun p n hp => by
    simp only [eval₂_mul, hp, eval₂_X, comp_apply, map_mul, rename_X, eval₂_mul]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
c : ℤ →+* R
g : τ → R
p : MvPolynomial σ ℤ
n : ℤ
⊢ eval₂ c (g ∘ f) (↑C n) = eval₂ c g (↑(rename f) (↑C n))
[PROOFSTEP]
simp only [eval₂_C, rename_C]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
c : ℤ →+* R
g : τ → R
p✝ p q : MvPolynomial σ ℤ
hp : eval₂ c (g ∘ f) p = eval₂ c g (↑(rename f) p)
hq : eval₂ c (g ∘ f) q = eval₂ c g (↑(rename f) q)
⊢ eval₂ c (g ∘ f) (p + q) = eval₂ c g (↑(rename f) (p + q))
[PROOFSTEP]
simp only [hp, hq, rename, eval₂_add, AlgHom.map_add]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
c : ℤ →+* R
g : τ → R
p✝ p : MvPolynomial σ ℤ
n : σ
hp : eval₂ c (g ∘ f) p = eval₂ c g (↑(rename f) p)
⊢ eval₂ c (g ∘ f) (p * X n) = eval₂ c g (↑(rename f) (p * X n))
[PROOFSTEP]
simp only [eval₂_mul, hp, eval₂_X, comp_apply, map_mul, rename_X, eval₂_mul]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff (Finsupp.mapDomain f d) (↑(rename f) φ) = coeff d φ
[PROOFSTEP]
classical
apply
  φ.induction_on' (P := fun ψ => coeff (Finsupp.mapDomain f d) ((rename f) ψ) = coeff d ψ)
    -- Lean could no longer infer the motive
· intro u r
  rw [rename_monomial, coeff_monomial, coeff_monomial]
  simp only [(Finsupp.mapDomain_injective hf).eq_iff]
· intros
  simp only [*, AlgHom.map_add, coeff_add]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ coeff (Finsupp.mapDomain f d) (↑(rename f) φ) = coeff d φ
[PROOFSTEP]
apply
  φ.induction_on' (P := fun ψ => coeff (Finsupp.mapDomain f d) ((rename f) ψ) = coeff d ψ)
    -- Lean could no longer infer the motive
[GOAL]
case h1
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ∀ (u : σ →₀ ℕ) (a : R), coeff (Finsupp.mapDomain f d) (↑(rename f) (↑(monomial u) a)) = coeff d (↑(monomial u) a)
[PROOFSTEP]
intro u r
[GOAL]
case h1
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d u : σ →₀ ℕ
r : R
⊢ coeff (Finsupp.mapDomain f d) (↑(rename f) (↑(monomial u) r)) = coeff d (↑(monomial u) r)
[PROOFSTEP]
rw [rename_monomial, coeff_monomial, coeff_monomial]
[GOAL]
case h1
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d u : σ →₀ ℕ
r : R
⊢ (if Finsupp.mapDomain f u = Finsupp.mapDomain f d then r else 0) = if u = d then r else 0
[PROOFSTEP]
simp only [(Finsupp.mapDomain_injective hf).eq_iff]
[GOAL]
case h2
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
⊢ ∀ (p q : MvPolynomial σ R),
    coeff (Finsupp.mapDomain f d) (↑(rename f) p) = coeff d p →
      coeff (Finsupp.mapDomain f d) (↑(rename f) q) = coeff d q →
        coeff (Finsupp.mapDomain f d) (↑(rename f) (p + q)) = coeff d (p + q)
[PROOFSTEP]
intros
[GOAL]
case h2
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
hf : Injective f
φ : MvPolynomial σ R
d : σ →₀ ℕ
p✝ q✝ : MvPolynomial σ R
a✝¹ : coeff (Finsupp.mapDomain f d) (↑(rename f) p✝) = coeff d p✝
a✝ : coeff (Finsupp.mapDomain f d) (↑(rename f) q✝) = coeff d q✝
⊢ coeff (Finsupp.mapDomain f d) (↑(rename f) (p✝ + q✝)) = coeff d (p✝ + q✝)
[PROOFSTEP]
simp only [*, AlgHom.map_add, coeff_add]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ coeff d (↑(rename f) φ) = 0
[PROOFSTEP]
classical
rw [rename_eq, ← not_mem_support_iff]
intro H
replace H := mapDomain_support H
rw [Finset.mem_image] at H 
obtain ⟨u, hu, rfl⟩ := H
specialize h u rfl
simp at h hu 
contradiction
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ coeff d (↑(rename f) φ) = 0
[PROOFSTEP]
rw [rename_eq, ← not_mem_support_iff]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ ¬d ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
[PROOFSTEP]
intro H
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : d ∈ support (Finsupp.mapDomain (Finsupp.mapDomain f) φ)
⊢ False
[PROOFSTEP]
replace H := mapDomain_support H
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : d ∈ Finset.image (Finsupp.mapDomain f) φ.support
⊢ False
[PROOFSTEP]
rw [Finset.mem_image] at H 
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
H : ∃ a, a ∈ φ.support ∧ Finsupp.mapDomain f a = d
⊢ False
[PROOFSTEP]
obtain ⟨u, hu, rfl⟩ := H
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.support
h : ∀ (u_1 : σ →₀ ℕ), Finsupp.mapDomain f u_1 = Finsupp.mapDomain f u → coeff u_1 φ = 0
⊢ False
[PROOFSTEP]
specialize h u rfl
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
hu : u ∈ φ.support
h : coeff u φ = 0
⊢ False
[PROOFSTEP]
simp at h hu 
[GOAL]
case intro.intro
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
u : σ →₀ ℕ
h : coeff u φ = 0
hu : ¬↑φ u = 0
⊢ False
[PROOFSTEP]
contradiction
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : coeff d (↑(rename f) φ) ≠ 0
⊢ ∃ u, Finsupp.mapDomain f u = d ∧ coeff u φ ≠ 0
[PROOFSTEP]
contrapose! h
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f : σ → τ
φ : MvPolynomial σ R
d : τ →₀ ℕ
h : ∀ (u : σ →₀ ℕ), Finsupp.mapDomain f u = d → coeff u φ = 0
⊢ coeff d (↑(rename f) φ) = 0
[PROOFSTEP]
apply coeff_rename_eq_zero _ _ _ h
[GOAL]
σ : Type u_1
τ✝ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ↑constantCoeff (↑(rename f) φ) = ↑constantCoeff φ
[PROOFSTEP]
apply φ.induction_on
[GOAL]
case h_C
σ : Type u_1
τ✝ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (a : R), ↑constantCoeff (↑(rename f) (↑C a)) = ↑constantCoeff (↑C a)
[PROOFSTEP]
intro a
[GOAL]
case h_C
σ : Type u_1
τ✝ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
a : R
⊢ ↑constantCoeff (↑(rename f) (↑C a)) = ↑constantCoeff (↑C a)
[PROOFSTEP]
simp only [constantCoeff_C, rename_C]
[GOAL]
case h_add
σ : Type u_1
τ✝ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (p q : MvPolynomial σ R),
    ↑constantCoeff (↑(rename f) p) = ↑constantCoeff p →
      ↑constantCoeff (↑(rename f) q) = ↑constantCoeff q → ↑constantCoeff (↑(rename f) (p + q)) = ↑constantCoeff (p + q)
[PROOFSTEP]
intro p q hp hq
[GOAL]
case h_add
σ : Type u_1
τ✝ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_6
f : σ → τ
φ p q : MvPolynomial σ R
hp : ↑constantCoeff (↑(rename f) p) = ↑constantCoeff p
hq : ↑constantCoeff (↑(rename f) q) = ↑constantCoeff q
⊢ ↑constantCoeff (↑(rename f) (p + q)) = ↑constantCoeff (p + q)
[PROOFSTEP]
simp only [hp, hq, RingHom.map_add, AlgHom.map_add]
[GOAL]
case h_X
σ : Type u_1
τ✝ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_6
f : σ → τ
φ : MvPolynomial σ R
⊢ ∀ (p : MvPolynomial σ R) (n : σ),
    ↑constantCoeff (↑(rename f) p) = ↑constantCoeff p →
      ↑constantCoeff (↑(rename f) (p * X n)) = ↑constantCoeff (p * X n)
[PROOFSTEP]
intro p n hp
[GOAL]
case h_X
σ : Type u_1
τ✝ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
τ : Type u_6
f : σ → τ
φ p : MvPolynomial σ R
n : σ
hp : ↑constantCoeff (↑(rename f) p) = ↑constantCoeff p
⊢ ↑constantCoeff (↑(rename f) (p * X n)) = ↑constantCoeff (p * X n)
[PROOFSTEP]
simp only [hp, rename_X, constantCoeff_X, RingHom.map_mul, AlgHom.map_mul]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
p : MvPolynomial σ R
f : σ → τ
inst✝ : DecidableEq τ
h : Injective f
⊢ support (↑(rename f) p) = Finset.image (Finsupp.mapDomain f) (support p)
[PROOFSTEP]
rw [rename_eq]
[GOAL]
σ : Type u_1
τ : Type u_2
α : Type u_3
R : Type u_4
S : Type u_5
inst✝² : CommSemiring R
inst✝¹ : CommSemiring S
p : MvPolynomial σ R
f : σ → τ
inst✝ : DecidableEq τ
h : Injective f
⊢ support (Finsupp.mapDomain (Finsupp.mapDomain f) p) = Finset.image (Finsupp.mapDomain f) (support p)
[PROOFSTEP]
exact Finsupp.mapDomain_support_of_injective (mapDomain_injective h) _
