[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
x : σ → R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x = x
[PROOFSTEP]
funext i
[GOAL]
case h
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
x : σ → R
i : σ
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x i = x i
[PROOFSTEP]
simp only [comap, AlgHom.id_apply, id.def, aeval_X]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) = id
[PROOFSTEP]
funext x
[GOAL]
case h
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
x : σ → R
⊢ comap (AlgHom.id R (MvPolynomial σ R)) x = id x
[PROOFSTEP]
exact comap_id_apply x
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
⊢ comap (AlgHom.comp g f) x = comap f (comap g x)
[PROOFSTEP]
funext i
[GOAL]
case h
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ comap (AlgHom.comp g f) x i = comap f (comap g x) i
[PROOFSTEP]
trans aeval x (aeval (fun i => g (X i)) (f (X i)))
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ comap (AlgHom.comp g f) x i = ↑(aeval x) (↑(aeval fun i => ↑g (X i)) (↑f (X i)))
[PROOFSTEP]
apply eval₂Hom_congr rfl rfl
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ ↑(AlgHom.comp g f) (X i) = ↑(aeval fun i => ↑g (X i)) (↑f (X i))
[PROOFSTEP]
rw [AlgHom.comp_apply]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ ↑g (↑f (X i)) = ↑(aeval fun i => ↑g (X i)) (↑f (X i))
[PROOFSTEP]
suffices g = aeval fun i => g (X i) by rw [← this]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
this : g = aeval fun i => ↑g (X i)
⊢ ↑g (↑f (X i)) = ↑(aeval fun i => ↑g (X i)) (↑f (X i))
[PROOFSTEP]
rw [← this]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ g = aeval fun i => ↑g (X i)
[PROOFSTEP]
exact aeval_unique g
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ ↑(aeval x) (↑(aeval fun i => ↑g (X i)) (↑f (X i))) = comap f (comap g x) i
[PROOFSTEP]
simp only [comap, aeval_eq_eval₂Hom, map_eval₂Hom, AlgHom.comp_apply]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ ↑(eval₂Hom (RingHom.comp (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R))) fun i =>
          ↑(eval₂Hom (algebraMap R R) x) (↑g (X i)))
      (↑f (X i)) =
    ↑(eval₂Hom (algebraMap R R) fun i => ↑(eval₂Hom (algebraMap R R) x) (↑g (X i))) (↑f (X i))
[PROOFSTEP]
refine' eval₂Hom_congr _ rfl rfl
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
⊢ RingHom.comp (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R)) = algebraMap R R
[PROOFSTEP]
ext r
[GOAL]
case a
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
i : σ
r : R
⊢ ↑(RingHom.comp (eval₂Hom (algebraMap R R) x) (algebraMap R (MvPolynomial υ R))) r = ↑(algebraMap R R) r
[PROOFSTEP]
apply aeval_C
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
⊢ comap (AlgHom.comp g f) = comap f ∘ comap g
[PROOFSTEP]
funext x
[GOAL]
case h
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R
g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R
x : υ → R
⊢ comap (AlgHom.comp g f) x = (comap f ∘ comap g) x
[PROOFSTEP]
exact comap_comp_apply _ _ _
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), ↑f φ = φ
x : σ → R
⊢ comap f x = x
[PROOFSTEP]
convert comap_id_apply x
[GOAL]
case h.e'_2.h.e'_5
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), ↑f φ = φ
x : σ → R
⊢ f = AlgHom.id R (MvPolynomial σ R)
[PROOFSTEP]
ext1 φ
[GOAL]
case h.e'_2.h.e'_5.hf
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R →ₐ[R] MvPolynomial σ R
hf : ∀ (φ : MvPolynomial σ R), ↑f φ = φ
x : σ → R
φ : σ
⊢ ↑f (X φ) = ↑(AlgHom.id R (MvPolynomial σ R)) (X φ)
[PROOFSTEP]
simp [hf, AlgHom.id_apply]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
x : τ → R
⊢ comap (rename f) x = x ∘ f
[PROOFSTEP]
funext
[GOAL]
case h
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
x : τ → R
x✝ : σ
⊢ comap (rename f) x x✝ = (x ∘ f) x✝
[PROOFSTEP]
simp [rename_X, comap_apply, aeval_X]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
⊢ Function.LeftInverse (comap ↑(AlgEquiv.symm f)) (comap ↑f)
[PROOFSTEP]
intro x
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : τ → R
⊢ comap (↑(AlgEquiv.symm f)) (comap (↑f) x) = x
[PROOFSTEP]
rw [← comap_comp_apply]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : τ → R
⊢ comap (AlgHom.comp ↑f ↑(AlgEquiv.symm f)) x = x
[PROOFSTEP]
apply comap_eq_id_of_eq_id
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : τ → R
⊢ ∀ (φ : MvPolynomial τ R), ↑(AlgHom.comp ↑f ↑(AlgEquiv.symm f)) φ = φ
[PROOFSTEP]
intro
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : τ → R
φ✝ : MvPolynomial τ R
⊢ ↑(AlgHom.comp ↑f ↑(AlgEquiv.symm f)) φ✝ = φ✝
[PROOFSTEP]
simp only [AlgHom.id_apply, AlgEquiv.comp_symm]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
⊢ Function.RightInverse (comap ↑(AlgEquiv.symm f)) (comap ↑f)
[PROOFSTEP]
intro x
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : σ → R
⊢ comap (↑f) (comap (↑(AlgEquiv.symm f)) x) = x
[PROOFSTEP]
rw [← comap_comp_apply]
[GOAL]
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : σ → R
⊢ comap (AlgHom.comp ↑(AlgEquiv.symm f) ↑f) x = x
[PROOFSTEP]
apply comap_eq_id_of_eq_id
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : σ → R
⊢ ∀ (φ : MvPolynomial σ R), ↑(AlgHom.comp ↑(AlgEquiv.symm f) ↑f) φ = φ
[PROOFSTEP]
intro
[GOAL]
case hf
σ : Type u_1
τ : Type u_2
υ : Type u_3
R : Type u_4
inst✝ : CommSemiring R
f : MvPolynomial σ R ≃ₐ[R] MvPolynomial τ R
x : σ → R
φ✝ : MvPolynomial σ R
⊢ ↑(AlgHom.comp ↑(AlgEquiv.symm f) ↑f) φ✝ = φ✝
[PROOFSTEP]
simp only [AlgHom.id_apply, AlgEquiv.symm_comp]
