-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem ext {f g : E →ₗ.[R] F} (h : f.domain = g.domain)
    (h' : ∀ ⦃x : E⦄ ⦃hf : x ∈ f.domain⦄ ⦃hg : x ∈ g.domain⦄, f ⟨x, hf⟩ = g ⟨x, hg⟩) : f = g

Proof state:
case mk.mk.e_toFun.h
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
f_dom : Submodule R E
f g : ↥f_dom →ₗ[R] F
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f }.domain⦄ ⦃hg : x ∈ { domain := f_dom, toFun := g }.domain⦄,
    ↑{ domain := f_dom, toFun := f } ⟨x, hf⟩ = ↑{ domain := f_dom, toFun := g } ⟨x, hg⟩
x : ↥f_dom
⊢ f x = g x

Tactic:
apply h'

Result:
no goals

Proof state:
case mk.mk.e_toFun.h
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
f_dom : Submodule R E
f g : ↥f_dom →ₗ[R] F
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f }.domain⦄ ⦃hg : x ∈ { domain := f_dom, toFun := g }.domain⦄,
    ↑{ domain := f_dom, toFun := f } ⟨x, hf⟩ = ↑{ domain := f_dom, toFun := g } ⟨x, hg⟩
⊢ ∀ (x : ↥f_dom), f x = g x

Tactic:
intro x

Result:
case mk.mk.e_toFun.h
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
f_dom : Submodule R E
f g : ↥f_dom →ₗ[R] F
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f }.domain⦄ ⦃hg : x ∈ { domain := f_dom, toFun := g }.domain⦄,
    ↑{ domain := f_dom, toFun := f } ⟨x, hf⟩ = ↑{ domain := f_dom, toFun := g } ⟨x, hg⟩
x : ↥f_dom
⊢ f x = g x

Proof state:
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
f_dom : Submodule R E
f g : ↥f_dom →ₗ[R] F
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f }.domain⦄ ⦃hg : x ∈ { domain := f_dom, toFun := g }.domain⦄,
    ↑{ domain := f_dom, toFun := f } ⟨x, hf⟩ = ↑{ domain := f_dom, toFun := g } ⟨x, hg⟩
⊢ { domain := f_dom, toFun := f } = { domain := f_dom, toFun := g }

Tactic:
congr

Result:
case mk.mk.e_toFun
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
f_dom : Submodule R E
f g : ↥f_dom →ₗ[R] F
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f }.domain⦄ ⦃hg : x ∈ { domain := f_dom, toFun := g }.domain⦄,
    ↑{ domain := f_dom, toFun := f } ⟨x, hf⟩ = ↑{ domain := f_dom, toFun := g } ⟨x, hg⟩
⊢ f = g

Proof state:
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
f_dom : Submodule R E
f : ↥f_dom →ₗ[R] F
g_dom : Submodule R E
g : ↥g_dom →ₗ[R] F
h : { domain := f_dom, toFun := f }.domain = { domain := g_dom, toFun := g }.domain
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f }.domain⦄ ⦃hg : x ∈ { domain := g_dom, toFun := g }.domain⦄,
    ↑{ domain := f_dom, toFun := f } ⟨x, hf⟩ = ↑{ domain := g_dom, toFun := g } ⟨x, hg⟩
⊢ { domain := f_dom, toFun := f } = { domain := g_dom, toFun := g }

Tactic:
obtain rfl : f_dom = g_dom := h

Result:
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
f_dom : Submodule R E
f g : ↥f_dom →ₗ[R] F
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f }.domain⦄ ⦃hg : x ∈ { domain := f_dom, toFun := g }.domain⦄,
    ↑{ domain := f_dom, toFun := f } ⟨x, hf⟩ = ↑{ domain := f_dom, toFun := g } ⟨x, hg⟩
⊢ { domain := f_dom, toFun := f } = { domain := f_dom, toFun := g }

Proof state:
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 : E →ₗ.[R] F
f_dom : Submodule R E
f : ↥f_dom →ₗ[R] F
h : { domain := f_dom, toFun := f }.domain = g.domain
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f }.domain⦄ ⦃hg : x ∈ g.domain⦄,
    ↑{ domain := f_dom, toFun := f } ⟨x, hf⟩ = ↑g ⟨x, hg⟩
⊢ { domain := f_dom, toFun := f } = g

Tactic:
rcases g with ⟨g_dom, g⟩

Result:
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
f_dom : Submodule R E
f : ↥f_dom →ₗ[R] F
g_dom : Submodule R E
g : ↥g_dom →ₗ[R] F
h : { domain := f_dom, toFun := f }.domain = { domain := g_dom, toFun := g }.domain
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f }.domain⦄ ⦃hg : x ∈ { domain := g_dom, toFun := g }.domain⦄,
    ↑{ domain := f_dom, toFun := f } ⟨x, hf⟩ = ↑{ domain := g_dom, toFun := g } ⟨x, hg⟩
⊢ { domain := f_dom, toFun := f } = { domain := g_dom, toFun := g }

Proof state:
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
f g : E →ₗ.[R] F
h : f.domain = g.domain
h' : ∀ ⦃x : E⦄ ⦃hf : x ∈ f.domain⦄ ⦃hg : x ∈ g.domain⦄, ↑f ⟨x, hf⟩ = ↑g ⟨x, hg⟩
⊢ f = g

Tactic:
rcases f with ⟨f_dom, f⟩

Result:
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 : E →ₗ.[R] F
f_dom : Submodule R E
f : ↥f_dom →ₗ[R] F
h : { domain := f_dom, toFun := f }.domain = g.domain
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f }.domain⦄ ⦃hg : x ∈ g.domain⦄,
    ↑{ domain := f_dom, toFun := f } ⟨x, hf⟩ = ↑g ⟨x, hg⟩
⊢ { domain := f_dom, toFun := f } = g

Proof state:
case mk.mk.e_toFun
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
f_dom : Submodule R E
f g : ↥f_dom →ₗ[R] F
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f }.domain⦄ ⦃hg : x ∈ { domain := f_dom, toFun := g }.domain⦄,
    ↑{ domain := f_dom, toFun := f } ⟨x, hf⟩ = ↑{ domain := f_dom, toFun := g } ⟨x, hg⟩
⊢ f = g

Tactic:
apply LinearMap.ext

Result:
case mk.mk.e_toFun.h
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
f_dom : Submodule R E
f g : ↥f_dom →ₗ[R] F
h' :
  ∀ ⦃x : E⦄ ⦃hf : x ∈ { domain := f_dom, toFun := f }.domain⦄ ⦃hg : x ∈ { domain := f_dom, toFun := g }.domain⦄,
    ↑{ domain := f_dom, toFun := f } ⟨x, hf⟩ = ↑{ domain := f_dom, toFun := g } ⟨x, hg⟩
⊢ ∀ (x : ↥f_dom), f x = g x