p : ℕ
R : Type u_1
S : Type ?u.90078
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℤ
⊢ ↑(map (MvPolynomial.map (Int.castRingHom ℚ))) (teichmullerFun p (x * y)) =
    ↑(map (MvPolynomial.map (Int.castRingHom ℚ))) (teichmullerFun p x * teichmullerFun p y)
p : ℕ
R : Type u_1
S : Type ?u.90078
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℤ
⊢ teichmullerFun p (x * y) = teichmullerFun p x * teichmullerFun p y
refine' map_injective (MvPolynomial.map (Int.castRingHom ℚ))
  (MvPolynomial.map_injective _ Int.cast_injective) _
no goals
p : ℕ
R : Type u_1
S : Type ?u.90078
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
x y : MvPolynomial R ℤ
⊢ ↑(map (MvPolynomial.map (Int.castRingHom ℚ))) (teichmullerFun p (x * y)) =
    ↑(map (MvPolynomial.map (Int.castRingHom ℚ))) (teichmullerFun p x * teichmullerFun p y)
simp only [teichmuller_mul_aux₁, map_teichmullerFun, RingHom.map_mul]