no goals
R : Type u
inst✝⁶ : Ring R
Q : TypeMax
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M N : Type (max u v)
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
i : M →ₗ[R] N
f : M →ₗ[R] Q
a b : ExtensionOf i f
r : a = b
x y : { x // x ∈ a.domain }
h : ↑x = ↑y
⊢ x = y
exact_mod_cast h