-- Mathlib/Algebra/MvPolynomial/Comap.lean
theorem comap_comp_apply (f : MvPolynomial σ R →ₐ[R] MvPolynomial τ R)
    (g : MvPolynomial τ R →ₐ[R] MvPolynomial υ R) (x : υ → R) :
    comap (g.comp f) x = comap f (comap g x)

Proof state:
σ : 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)

Tactic:
exact aeval_unique g

Result:
no goals

Proof state:
σ : 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))

Tactic:
suffices g = aeval fun i => g (X i) by rw [← this]

Result:
σ : 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)

Proof state:
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 (g.comp f) x i = comap f (comap g x) i

Tactic:
trans aeval x (aeval (fun i => g (X i)) (f (X i)))

Result:
σ : 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 (g.comp f) x i = (aeval x) ((aeval fun i => g (X i)) (f (X i)))

σ : 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

Proof state:
σ : 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 (g.comp f) x i = (aeval x) ((aeval fun i => g (X i)) (f (X i)))

Tactic:
apply eval₂Hom_congr rfl rfl

Result:
σ : 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.comp f) (X i) = (aeval fun i => g (X i)) (f (X i))

Proof state:
σ : 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))

Tactic:
rw [← this]

Result:
no goals

Proof state:
σ : 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

Tactic:
simp only [comap, aeval_eq_eval₂Hom, map_eval₂Hom, AlgHom.comp_apply]

Result:
σ : 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 ((eval₂Hom (algebraMap R R) x).comp (algebraMap R (MvPolynomial υ R))) fun i =>
        (eval₂Hom (algebraMap R R) x) (g (X i)))
      (f (X i)) =
    (eval₂Hom (algebraMap R R) (comap g x)) (f (X i))

Proof state:
σ : 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.comp f) (X i) = (aeval fun i => g (X i)) (f (X i))

Tactic:
rw [AlgHom.comp_apply]

Result:
σ : 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))

Proof state:
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
⊢ ((eval₂Hom (algebraMap R R) x).comp (algebraMap R (MvPolynomial υ R))) r = (algebraMap R R) r

Tactic:
apply aeval_C

Result:
no goals

Proof state:
σ : 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 ((eval₂Hom (algebraMap R R) x).comp (algebraMap R (MvPolynomial υ R))) fun i =>
        (eval₂Hom (algebraMap R R) x) (g (X i)))
      (f (X i)) =
    (eval₂Hom (algebraMap R R) (comap g x)) (f (X i))

Tactic:
refine eval₂Hom_congr ?_ rfl rfl

Result:
σ : 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 (algebraMap R R) x).comp (algebraMap R (MvPolynomial υ R)) = algebraMap R R

Proof state:
σ : 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 (algebraMap R R) x).comp (algebraMap R (MvPolynomial υ R)) = algebraMap R R

Tactic:
ext r

Result:
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
⊢ ((eval₂Hom (algebraMap R R) x).comp (algebraMap R (MvPolynomial υ R))) r = (algebraMap R R) r

Proof state:
σ : 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 (g.comp f) x = comap f (comap g x)

Tactic:
funext i

Result:
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 (g.comp f) x i = comap f (comap g x) i