Theorem: optionEquivRight_comp_to_MvPolynomial_Option (FormalSnarksProject/ToMathlib/OptionEquivRight.lean)

State before:
F V : Type
inst✝ : Field F
⊢ (optionEquivRight F V).toRingEquiv.toRingHom.comp (to_MvPolynomial_Option V) = C
Tactic:
apply Polynomial.hom_congr_vars
State after:
case hC
F V : Type
inst✝ : Field F
⊢ ((optionEquivRight F V).toRingEquiv.toRingHom.comp (to_MvPolynomial_Option V)).comp Polynomial.C = C.comp Polynomial.C

case hv
F V : Type
inst✝ : Field F
⊢ ((optionEquivRight F V).toRingEquiv.toRingHom.comp (to_MvPolynomial_Option V)) Polynomial.X = C Polynomial.X

State before:
case hC
F V : Type
inst✝ : Field F
⊢ ((optionEquivRight F V).toRingEquiv.toRingHom.comp (to_MvPolynomial_Option V)).comp Polynomial.C = C.comp Polynomial.C
Tactic:
simp only [AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe, AlgEquiv.toRingEquiv_toRingHom]
State after:
case hC
F V : Type
inst✝ : Field F
⊢ ((↑(optionEquivRight F V)).comp (to_MvPolynomial_Option V)).comp Polynomial.C = C.comp Polynomial.C

State before:
case hC
F V : Type
inst✝ : Field F
⊢ ((↑(optionEquivRight F V)).comp (to_MvPolynomial_Option V)).comp Polynomial.C = C.comp Polynomial.C
Tactic:
rw [RingHom.comp_assoc]
State after:
case hC
F V : Type
inst✝ : Field F
⊢ (↑(optionEquivRight F V)).comp ((to_MvPolynomial_Option V).comp Polynomial.C) = C.comp Polynomial.C

State before:
case hC
F V : Type
inst✝ : Field F
⊢ (↑(optionEquivRight F V)).comp ((to_MvPolynomial_Option V).comp Polynomial.C) = C.comp Polynomial.C
Tactic:
rw [@RingHom.ext_iff]
State after:
case hC
F V : Type
inst✝ : Field F
⊢ ∀ (x : F), ((↑(optionEquivRight F V)).comp ((to_MvPolynomial_Option V).comp Polynomial.C)) x = (C.comp Polynomial.C) x

State before:
case hC
F V : Type
inst✝ : Field F
⊢ ∀ (x : F), ((↑(optionEquivRight F V)).comp ((to_MvPolynomial_Option V).comp Polynomial.C)) x = (C.comp Polynomial.C) x
Tactic:
intro x
State after:
case hC
F V : Type
inst✝ : Field F
x : F
⊢ ((↑(optionEquivRight F V)).comp ((to_MvPolynomial_Option V).comp Polynomial.C)) x = (C.comp Polynomial.C) x

State before:
case hC
F V : Type
inst✝ : Field F
x : F
⊢ ((↑(optionEquivRight F V)).comp ((to_MvPolynomial_Option V).comp Polynomial.C)) x = (C.comp Polynomial.C) x
Tactic:
simp [to_MvPolynomial_Option_C]
State after:
no goals

State before:
case hv
F V : Type
inst✝ : Field F
⊢ ((optionEquivRight F V).toRingEquiv.toRingHom.comp (to_MvPolynomial_Option V)) Polynomial.X = C Polynomial.X
Tactic:
simp only [AlgEquiv.toRingEquiv_eq_coe, RingEquiv.toRingHom_eq_coe,
  AlgEquiv.toRingEquiv_toRingHom, RingHom.coe_comp, RingHom.coe_coe, Function.comp_apply]
State after:
case hv
F V : Type
inst✝ : Field F
⊢ (optionEquivRight F V) ((to_MvPolynomial_Option V) Polynomial.X) = C Polynomial.X

State before:
case hv
F V : Type
inst✝ : Field F
⊢ (optionEquivRight F V) ((to_MvPolynomial_Option V) Polynomial.X) = C Polynomial.X
Tactic:
rw [to_MvPolynomial_Option_X]
State after:
case hv
F V : Type
inst✝ : Field F
⊢ (optionEquivRight F V) (X none) = C Polynomial.X

State before:
case hv
F V : Type
inst✝ : Field F
⊢ (optionEquivRight F V) (X none) = C Polynomial.X
Tactic:
simp only [MvPolynomial.optionEquivRight_X_none]
State after:
no goals