case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
n : ℕ
⊢ coeff (↑(map f) (teichmullerFun p r)) n = coeff (teichmullerFun p (↑f r)) n
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
⊢ ↑(map f) (teichmullerFun p r) = teichmullerFun p (↑f r)
ext n
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
⊢ coeff (↑(map f) (teichmullerFun p r)) Nat.zero = coeff (teichmullerFun p (↑f r)) Nat.zero

case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
n✝ : ℕ
⊢ coeff (↑(map f) (teichmullerFun p r)) (Nat.succ n✝) = coeff (teichmullerFun p (↑f r)) (Nat.succ n✝)
case h
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
n : ℕ
⊢ coeff (↑(map f) (teichmullerFun p r)) n = coeff (teichmullerFun p (↑f r)) n
cases n
no goals
case h.zero
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
⊢ coeff (↑(map f) (teichmullerFun p r)) Nat.zero = coeff (teichmullerFun p (↑f r)) Nat.zero
rfl
no goals
case h.succ
p : ℕ
R : Type u_1
S : Type u_2
hp : Fact (Nat.Prime p)
inst✝¹ : CommRing R
inst✝ : CommRing S
f : R →+* S
r : R
n✝ : ℕ
⊢ coeff (↑(map f) (teichmullerFun p r)) (Nat.succ n✝) = coeff (teichmullerFun p (↑f r)) (Nat.succ n✝)
exact f.map_zero