p : ℕ
R : Type ?u.19105
S : Type ?u.19108
T : Type ?u.19111
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
a₁✝ a₂✝ : 𝕎 α
h : mapFun f a₁✝ = mapFun f a₂✝
⊢ a₁✝ = a₂✝
p : ℕ
R : Type ?u.19105
S : Type ?u.19108
T : Type ?u.19111
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
⊢ Injective (mapFun f)
intros _ _ h
case h
p✝ : ℕ
R : Type ?u.19105
S : Type ?u.19108
T : Type ?u.19111
hp : Fact (Nat.Prime p✝)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
a₁✝ a₂✝ : WittVector p✝ α
h : mapFun f a₁✝ = mapFun f a₂✝
p : ℕ
⊢ coeff a₁✝ p = coeff a₂✝ p
p : ℕ
R : Type ?u.19105
S : Type ?u.19108
T : Type ?u.19111
hp : Fact (Nat.Prime p)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
a₁✝ a₂✝ : 𝕎 α
h : mapFun f a₁✝ = mapFun f a₂✝
⊢ a₁✝ = a₂✝
ext p
no goals
case h
p✝ : ℕ
R : Type ?u.19105
S : Type ?u.19108
T : Type ?u.19111
hp : Fact (Nat.Prime p✝)
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : CommRing T
α : Type u_1
β : Type u_2
f : α → β
hf : Injective f
a₁✝ a₂✝ : WittVector p✝ α
h : mapFun f a₁✝ = mapFun f a₂✝
p : ℕ
⊢ coeff a₁✝ p = coeff a₂✝ p
exact hf (congr_arg (fun x => coeff x p) h : _)