case mk
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.20860
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : E →ₗ.[R] F
f_dom : Submodule R E
f : { x // x ∈ f_dom } →ₗ[R] F
h : { domain := f_dom, toFun := f }.domain = g.domain
h' :
  ∀ ⦃x : { x // x ∈ { domain := f_dom, toFun := f }.domain }⦄ ⦃y : { x // x ∈ g.domain }⦄,
    ↑x = ↑y → ↑{ domain := f_dom, toFun := f } x = ↑g y
⊢ { domain := f_dom, toFun := f } = g
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.20860
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f g : E →ₗ.[R] F
h : f.domain = g.domain
h' : ∀ ⦃x : { x // x ∈ f.domain }⦄ ⦃y : { x // x ∈ g.domain }⦄, ↑x = ↑y → ↑f x = ↑g y
⊢ f = g
rcases f with ⟨f_dom, f⟩
case mk.mk
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.20860
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f_dom : Submodule R E
f : { x // x ∈ f_dom } →ₗ[R] F
g_dom : Submodule R E
g : { x // x ∈ g_dom } →ₗ[R] F
h : { domain := f_dom, toFun := f }.domain = { domain := g_dom, toFun := g }.domain
h' :
  ∀ ⦃x : { x // x ∈ { domain := f_dom, toFun := f }.domain }⦄ ⦃y : { x // x ∈ { domain := g_dom, toFun := g }.domain }⦄,
    ↑x = ↑y → ↑{ domain := f_dom, toFun := f } x = ↑{ domain := g_dom, toFun := g } y
⊢ { domain := f_dom, toFun := f } = { domain := g_dom, toFun := g }
case mk
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.20860
inst✝¹ : AddCommGroup G
inst✝ : Module R G
g : E →ₗ.[R] F
f_dom : Submodule R E
f : { x // x ∈ f_dom } →ₗ[R] F
h : { domain := f_dom, toFun := f }.domain = g.domain
h' :
  ∀ ⦃x : { x // x ∈ { domain := f_dom, toFun := f }.domain }⦄ ⦃y : { x // x ∈ g.domain }⦄,
    ↑x = ↑y → ↑{ domain := f_dom, toFun := f } x = ↑g y
⊢ { domain := f_dom, toFun := f } = g
rcases g with ⟨g_dom, g⟩
case mk.mk
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.20860
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f_dom : Submodule R E
f g : { x // x ∈ f_dom } →ₗ[R] F
h' :
  ∀ ⦃x : { x // x ∈ { domain := f_dom, toFun := f }.domain }⦄ ⦃y : { x // x ∈ { domain := f_dom, toFun := g }.domain }⦄,
    ↑x = ↑y → ↑{ domain := f_dom, toFun := f } x = ↑{ domain := f_dom, toFun := g } y
⊢ { domain := f_dom, toFun := f } = { domain := f_dom, toFun := g }
case mk.mk
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.20860
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f_dom : Submodule R E
f : { x // x ∈ f_dom } →ₗ[R] F
g_dom : Submodule R E
g : { x // x ∈ g_dom } →ₗ[R] F
h : { domain := f_dom, toFun := f }.domain = { domain := g_dom, toFun := g }.domain
h' :
  ∀ ⦃x : { x // x ∈ { domain := f_dom, toFun := f }.domain }⦄ ⦃y : { x // x ∈ { domain := g_dom, toFun := g }.domain }⦄,
    ↑x = ↑y → ↑{ domain := f_dom, toFun := f } x = ↑{ domain := g_dom, toFun := g } y
⊢ { domain := f_dom, toFun := f } = { domain := g_dom, toFun := g }
obtain rfl : f_dom = g_dom := h
case mk.mk
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.20860
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f_dom : Submodule R E
f : { x // x ∈ f_dom } →ₗ[R] F
h' :
  ∀ ⦃x y : { x // x ∈ { domain := f_dom, toFun := f }.domain }⦄,
    ↑x = ↑y → ↑{ domain := f_dom, toFun := f } x = ↑{ domain := f_dom, toFun := f } y
⊢ { domain := f_dom, toFun := f } = { domain := f_dom, toFun := f }
case mk.mk
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.20860
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f_dom : Submodule R E
f g : { x // x ∈ f_dom } →ₗ[R] F
h' :
  ∀ ⦃x : { x // x ∈ { domain := f_dom, toFun := f }.domain }⦄ ⦃y : { x // x ∈ { domain := f_dom, toFun := g }.domain }⦄,
    ↑x = ↑y → ↑{ domain := f_dom, toFun := f } x = ↑{ domain := f_dom, toFun := g } y
⊢ { domain := f_dom, toFun := f } = { domain := f_dom, toFun := g }
obtain rfl : f = g := LinearMap.ext fun x => h' rfl
no goals
case mk.mk
R : Type u_1
inst✝⁶ : Ring R
E : Type u_2
inst✝⁵ : AddCommGroup E
inst✝⁴ : Module R E
F : Type u_3
inst✝³ : AddCommGroup F
inst✝² : Module R F
G : Type ?u.20860
inst✝¹ : AddCommGroup G
inst✝ : Module R G
f_dom : Submodule R E
f : { x // x ∈ f_dom } →ₗ[R] F
h' :
  ∀ ⦃x y : { x // x ∈ { domain := f_dom, toFun := f }.domain }⦄,
    ↑x = ↑y → ↑{ domain := f_dom, toFun := f } x = ↑{ domain := f_dom, toFun := f } y
⊢ { domain := f_dom, toFun := f } = { domain := f_dom, toFun := f }
rfl