α : Type u_1
β : Type u_2
γ : Type ?u.251410
ι : Type ?u.251413
M : Type u_3
M' : Type ?u.251419
N : Type ?u.251422
P : Type ?u.251425
G : Type ?u.251428
H : Type ?u.251431
R : Type ?u.251434
S : Type ?u.251437
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
⊢ v₁ = v₂
α : Type u_1
β : Type u_2
γ : Type ?u.251410
ι : Type ?u.251413
M : Type u_3
M' : Type ?u.251419
N : Type ?u.251422
P : Type ?u.251425
G : Type ?u.251428
H : Type ?u.251431
R : Type ?u.251434
S : Type ?u.251437
inst✝ : AddCommMonoid M
v v₁ v₂ : α →₀ M
f : α → β
hf : Injective f
⊢ Injective (mapDomain f)
intro v₁ v₂ eq
case h
α : Type u_1
β : Type u_2
γ : Type ?u.251410
ι : Type ?u.251413
M : Type u_3
M' : Type ?u.251419
N : Type ?u.251422
P : Type ?u.251425
G : Type ?u.251428
H : Type ?u.251431
R : Type ?u.251434
S : Type ?u.251437
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ ↑v₁ a = ↑v₂ a
α : Type u_1
β : Type u_2
γ : Type ?u.251410
ι : Type ?u.251413
M : Type u_3
M' : Type ?u.251419
N : Type ?u.251422
P : Type ?u.251425
G : Type ?u.251428
H : Type ?u.251431
R : Type ?u.251434
S : Type ?u.251437
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
⊢ v₁ = v₂
ext a
case h
α : Type u_1
β : Type u_2
γ : Type ?u.251410
ι : Type ?u.251413
M : Type u_3
M' : Type ?u.251419
N : Type ?u.251422
P : Type ?u.251425
G : Type ?u.251428
H : Type ?u.251431
R : Type ?u.251434
S : Type ?u.251437
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
this : ↑(mapDomain f v₁) (f a) = ↑(mapDomain f v₂) (f a)
⊢ ↑v₁ a = ↑v₂ a
case h
α : Type u_1
β : Type u_2
γ : Type ?u.251410
ι : Type ?u.251413
M : Type u_3
M' : Type ?u.251419
N : Type ?u.251422
P : Type ?u.251425
G : Type ?u.251428
H : Type ?u.251431
R : Type ?u.251434
S : Type ?u.251437
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ ↑v₁ a = ↑v₂ a
have : mapDomain f v₁ (f a) = mapDomain f v₂ (f a) := by rw [eq]
no goals
case h
α : Type u_1
β : Type u_2
γ : Type ?u.251410
ι : Type ?u.251413
M : Type u_3
M' : Type ?u.251419
N : Type ?u.251422
P : Type ?u.251425
G : Type ?u.251428
H : Type ?u.251431
R : Type ?u.251434
S : Type ?u.251437
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
this : ↑(mapDomain f v₁) (f a) = ↑(mapDomain f v₂) (f a)
⊢ ↑v₁ a = ↑v₂ a
rwa [mapDomain_apply hf, mapDomain_apply hf] at this
no goals
α : Type u_1
β : Type u_2
γ : Type ?u.251410
ι : Type ?u.251413
M : Type u_3
M' : Type ?u.251419
N : Type ?u.251422
P : Type ?u.251425
G : Type ?u.251428
H : Type ?u.251431
R : Type ?u.251434
S : Type ?u.251437
inst✝ : AddCommMonoid M
v v₁✝ v₂✝ : α →₀ M
f : α → β
hf : Injective f
v₁ v₂ : α →₀ M
eq : mapDomain f v₁ = mapDomain f v₂
a : α
⊢ ↑(mapDomain f v₁) (f a) = ↑(mapDomain f v₂) (f a)
rw [eq]