-- Mathlib/Algebra/Module/Injective.lean
theorem ExtensionOf.ext {a b : ExtensionOf i f} (domain_eq : a.domain = b.domain)
    (to_fun_eq : ∀ ⦃x : N⦄ ⦃ha : x ∈ a.domain⦄ ⦃hb : x ∈ b.domain⦄,
      a.toLinearPMap ⟨x, ha⟩ = b.toLinearPMap ⟨x, hb⟩) :
    a = b

Proof state:
case mk
R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
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 ⟨i m, ⋯⟩
domain_eq : { toLinearPMap := a, le := a_le, is_extension := e1 }.domain = b.domain
to_fun_eq :
  ∀ ⦃x : N⦄ ⦃ha : x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.domain⦄ ⦃hb : x ∈ b.domain⦄,
    ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap ⟨x, ha⟩ = ↑b.toLinearPMap ⟨x, hb⟩
⊢ { toLinearPMap := a, le := a_le, is_extension := e1 } = b

Tactic:
rcases b with ⟨b, b_le, e2⟩

Result:
case mk.mk
R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
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 ⟨i m, ⋯⟩
b : N →ₗ.[R] Q
b_le : LinearMap.range i ≤ b.domain
e2 : ∀ (m : M), f m = ↑b ⟨i m, ⋯⟩
domain_eq :
  { toLinearPMap := a, le := a_le, is_extension := e1 }.domain =
    { toLinearPMap := b, le := b_le, is_extension := e2 }.domain
to_fun_eq :
  ∀ ⦃x : N⦄ ⦃ha : x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.domain⦄
    ⦃hb : x ∈ { toLinearPMap := b, le := b_le, is_extension := e2 }.domain⦄,
    ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap ⟨x, ha⟩ =
      ↑{ toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap ⟨x, hb⟩
⊢ { toLinearPMap := a, le := a_le, is_extension := e1 } = { toLinearPMap := b, le := b_le, is_extension := e2 }

Proof state:
R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
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 : N⦄ ⦃ha : x ∈ a.domain⦄ ⦃hb : x ∈ b.domain⦄, ↑a.toLinearPMap ⟨x, ha⟩ = ↑b.toLinearPMap ⟨x, hb⟩
⊢ a = b

Tactic:
rcases a with ⟨a, a_le, e1⟩

Result:
case mk
R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
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 ⟨i m, ⋯⟩
domain_eq : { toLinearPMap := a, le := a_le, is_extension := e1 }.domain = b.domain
to_fun_eq :
  ∀ ⦃x : N⦄ ⦃ha : x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.domain⦄ ⦃hb : x ∈ b.domain⦄,
    ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap ⟨x, ha⟩ = ↑b.toLinearPMap ⟨x, hb⟩
⊢ { toLinearPMap := a, le := a_le, is_extension := e1 } = b

Proof state:
case mk.mk
R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
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 ⟨i m, ⋯⟩
b : N →ₗ.[R] Q
b_le : LinearMap.range i ≤ b.domain
e2 : ∀ (m : M), f m = ↑b ⟨i m, ⋯⟩
domain_eq :
  { toLinearPMap := a, le := a_le, is_extension := e1 }.domain =
    { toLinearPMap := b, le := b_le, is_extension := e2 }.domain
to_fun_eq :
  ∀ ⦃x : N⦄ ⦃ha : x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.domain⦄
    ⦃hb : x ∈ { toLinearPMap := b, le := b_le, is_extension := e2 }.domain⦄,
    ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap ⟨x, ha⟩ =
      ↑{ toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap ⟨x, hb⟩
⊢ { toLinearPMap := a, le := a_le, is_extension := e1 } = { toLinearPMap := b, le := b_le, is_extension := e2 }

Tactic:
congr

Result:
case mk.mk.e_toLinearPMap
R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
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 ⟨i m, ⋯⟩
b : N →ₗ.[R] Q
b_le : LinearMap.range i ≤ b.domain
e2 : ∀ (m : M), f m = ↑b ⟨i m, ⋯⟩
domain_eq :
  { toLinearPMap := a, le := a_le, is_extension := e1 }.domain =
    { toLinearPMap := b, le := b_le, is_extension := e2 }.domain
to_fun_eq :
  ∀ ⦃x : N⦄ ⦃ha : x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.domain⦄
    ⦃hb : x ∈ { toLinearPMap := b, le := b_le, is_extension := e2 }.domain⦄,
    ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap ⟨x, ha⟩ =
      ↑{ toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap ⟨x, hb⟩
⊢ a = b

Proof state:
case mk.mk.e_toLinearPMap
R : Type u
inst✝⁶ : Ring R
Q : Type v
inst✝⁵ : AddCommGroup Q
inst✝⁴ : Module R Q
M : Type u_1
N : Type u_2
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 ⟨i m, ⋯⟩
b : N →ₗ.[R] Q
b_le : LinearMap.range i ≤ b.domain
e2 : ∀ (m : M), f m = ↑b ⟨i m, ⋯⟩
domain_eq :
  { toLinearPMap := a, le := a_le, is_extension := e1 }.domain =
    { toLinearPMap := b, le := b_le, is_extension := e2 }.domain
to_fun_eq :
  ∀ ⦃x : N⦄ ⦃ha : x ∈ { toLinearPMap := a, le := a_le, is_extension := e1 }.domain⦄
    ⦃hb : x ∈ { toLinearPMap := b, le := b_le, is_extension := e2 }.domain⦄,
    ↑{ toLinearPMap := a, le := a_le, is_extension := e1 }.toLinearPMap ⟨x, ha⟩ =
      ↑{ toLinearPMap := b, le := b_le, is_extension := e2 }.toLinearPMap ⟨x, hb⟩
⊢ a = b

Tactic:
exact LinearPMap.ext domain_eq to_fun_eq

Result:
no goals