-- Mathlib/LinearAlgebra/Span/Basic.lean
lemma linearMap_eq_iff_of_span_eq_top (f g : M →ₗ[R] N)
    {S : Set M} (hM : span R S = ⊤) :
    f = g ↔ ∀ (s : S), f s = g s

Proof state:
case h.e'_1.a.mpr
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
h : f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype
⊢ f = g

Tactic:
ext x

Result:
case h.e'_1.a.mpr.h
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
h : f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype
x : M
⊢ f x = g x

Proof state:
case h.e'_1.a.mp
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
⊢ f = g → f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype

Tactic:
rintro rfl

Result:
case h.e'_1.a.mp
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
⊢ f ∘ₗ ⊤.subtype = f ∘ₗ ⊤.subtype

Proof state:
case h.e'_1.a.mpr.h
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
h : f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype
x : M
⊢ f x = g x

Tactic:
exact DFunLike.congr_fun h ⟨x, by simp⟩

Result:
no goals

Proof state:
case h.e'_1.a
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
⊢ f = g ↔ f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype

Tactic:
constructor

Result:
case h.e'_1.a.mp
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
⊢ f = g → f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype

case h.e'_1.a.mpr
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
⊢ f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype → f = g

Proof state:
case h.e'_1.a.mp
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
⊢ f ∘ₗ ⊤.subtype = f ∘ₗ ⊤.subtype

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
h : f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype
x : M
⊢ x ∈ ⊤

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
⊢ f = g ↔ ∀ (s : ↑S), f ↑s = g ↑s

Tactic:
convert linearMap_eq_iff_of_eq_span (f.comp (Submodule.subtype _))
  (g.comp (Submodule.subtype _)) hM.symm

Result:
case h.e'_1.a
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
⊢ f = g ↔ f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype

Proof state:
case h.e'_1.a.mpr
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
⊢ f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype → f = g

Tactic:
intro h

Result:
case h.e'_1.a.mpr
R : Type u_1
M : Type u_4
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
N : Type u_9
inst✝¹ : AddCommMonoid N
inst✝ : Module R N
f g : M →ₗ[R] N
S : Set M
hM : span R S = ⊤
h : f ∘ₗ ⊤.subtype = g ∘ₗ ⊤.subtype
⊢ f = g