Theorem: Polynomial.hom_congr_vars (FormalSnarksProject/ToMathlib/OptionEquivRight.lean)

State before:
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : R[X] →+* S
hC : f₁.comp C = f₂.comp C
hv : f₁ X = f₂ X
⊢ f₁ = f₂
Tactic:
ext p
State after:
case h₁.a
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : R[X] →+* S
hC : f₁.comp C = f₂.comp C
hv : f₁ X = f₂ X
p : R
⊢ (f₁.comp C) p = (f₂.comp C) p

case h₂
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : R[X] →+* S
hC : f₁.comp C = f₂.comp C
hv : f₁ X = f₂ X
⊢ f₁ X = f₂ X

State before:
case h₁.a
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : R[X] →+* S
hC : f₁.comp C = f₂.comp C
hv : f₁ X = f₂ X
p : R
⊢ (f₁.comp C) p = (f₂.comp C) p

case h₂
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : R[X] →+* S
hC : f₁.comp C = f₂.comp C
hv : f₁ X = f₂ X
⊢ f₁ X = f₂ X
Tactic:
exact congrFun (congrArg DFunLike.coe hC) p
State after:
case h₂
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : R[X] →+* S
hC : f₁.comp C = f₂.comp C
hv : f₁ X = f₂ X
⊢ f₁ X = f₂ X

State before:
case h₂
R : Type u
S : Type v
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S
f₁ f₂ : R[X] →+* S
hC : f₁.comp C = f₂.comp C
hv : f₁ X = f₂ X
⊢ f₁ X = f₂ X
Tactic:
exact hv
State after:
no goals