case mk
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
b : ExtensionOf i f
a : N →ₗ.[R] Q
a_le : LinearMap.range i ≤ a.domain
e1 : ∀ (m : M), ↑f m = ↑a { val := ↑i m, property := (_ : ↑i m ∈ a.domain) }
domain_eq : { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain = b.domain
to_fun_eq :
  ∀ ⦃x : { x // x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain }⦄
    ⦃y : { x // x ∈ b.domain }⦄,
    ↑x = ↑y → ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap x = ↑b.toLinearPMap y
⊢ { toLinearPMap := a, le := a_le, is_extension := e1 } = b
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
domain_eq : a.domain = b.domain
to_fun_eq : ∀ ⦃x : { x // x ∈ a.domain }⦄ ⦃y : { x // x ∈ b.domain }⦄, ↑x = ↑y → ↑a.toLinearPMap x = ↑b.toLinearPMap y
⊢ a = b
rcases a with ⟨a, a_le, e1⟩
case mk.mk
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 : N →ₗ.[R] Q
a_le : LinearMap.range i ≤ a.domain
e1 : ∀ (m : M), ↑f m = ↑a { val := ↑i m, property := (_ : ↑i m ∈ a.domain) }
b : N →ₗ.[R] Q
b_le : LinearMap.range i ≤ b.domain
e2 : ∀ (m : M), ↑f m = ↑b { val := ↑i m, property := (_ : ↑i m ∈ b.domain) }
domain_eq :
  { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain =
    { toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap.domain
to_fun_eq :
  ∀ ⦃x : { x // x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain }⦄
    ⦃y : { x // x ∈ { toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap.domain }⦄,
    ↑x = ↑y →
      ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap x =
        ↑{ toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap y
⊢ { toLinearPMap := a, le := a_le, is_extension := e1 } = { toLinearPMap := b, le := b_le, is_extension := e2 }
case mk
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
b : ExtensionOf i f
a : N →ₗ.[R] Q
a_le : LinearMap.range i ≤ a.domain
e1 : ∀ (m : M), ↑f m = ↑a { val := ↑i m, property := (_ : ↑i m ∈ a.domain) }
domain_eq : { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain = b.domain
to_fun_eq :
  ∀ ⦃x : { x // x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain }⦄
    ⦃y : { x // x ∈ b.domain }⦄,
    ↑x = ↑y → ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap x = ↑b.toLinearPMap y
⊢ { toLinearPMap := a, le := a_le, is_extension := e1 } = b
rcases b with ⟨b, b_le, e2⟩
case mk.mk.e_toLinearPMap
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 : N →ₗ.[R] Q
a_le : LinearMap.range i ≤ a.domain
e1 : ∀ (m : M), ↑f m = ↑a { val := ↑i m, property := (_ : ↑i m ∈ a.domain) }
b : N →ₗ.[R] Q
b_le : LinearMap.range i ≤ b.domain
e2 : ∀ (m : M), ↑f m = ↑b { val := ↑i m, property := (_ : ↑i m ∈ b.domain) }
domain_eq :
  { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain =
    { toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap.domain
to_fun_eq :
  ∀ ⦃x : { x // x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain }⦄
    ⦃y : { x // x ∈ { toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap.domain }⦄,
    ↑x = ↑y →
      ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap x =
        ↑{ toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap y
⊢ a = b
case mk.mk
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 : N →ₗ.[R] Q
a_le : LinearMap.range i ≤ a.domain
e1 : ∀ (m : M), ↑f m = ↑a { val := ↑i m, property := (_ : ↑i m ∈ a.domain) }
b : N →ₗ.[R] Q
b_le : LinearMap.range i ≤ b.domain
e2 : ∀ (m : M), ↑f m = ↑b { val := ↑i m, property := (_ : ↑i m ∈ b.domain) }
domain_eq :
  { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain =
    { toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap.domain
to_fun_eq :
  ∀ ⦃x : { x // x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain }⦄
    ⦃y : { x // x ∈ { toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap.domain }⦄,
    ↑x = ↑y →
      ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap x =
        ↑{ toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap y
⊢ { toLinearPMap := a, le := a_le, is_extension := e1 } = { toLinearPMap := b, le := b_le, is_extension := e2 }
congr
no goals
case mk.mk.e_toLinearPMap
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 : N →ₗ.[R] Q
a_le : LinearMap.range i ≤ a.domain
e1 : ∀ (m : M), ↑f m = ↑a { val := ↑i m, property := (_ : ↑i m ∈ a.domain) }
b : N →ₗ.[R] Q
b_le : LinearMap.range i ≤ b.domain
e2 : ∀ (m : M), ↑f m = ↑b { val := ↑i m, property := (_ : ↑i m ∈ b.domain) }
domain_eq :
  { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain =
    { toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap.domain
to_fun_eq :
  ∀ ⦃x : { x // x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap.domain }⦄
    ⦃y : { x // x ∈ { toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap.domain }⦄,
    ↑x = ↑y →
      ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap x =
        ↑{ toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap y
⊢ a = b
exact LinearPMap.ext domain_eq to_fun_eq