-- Mathlib/LinearAlgebra/Span/Basic.lean
lemma _root_.LinearMap.range_domRestrict_eq_range_iff {f : M →ₛₗ[τ₁₂] M₂} {S : Submodule R M} :
    LinearMap.range (f.domRestrict S) = LinearMap.range f ↔ S ⊔ (LinearMap.ker f) = ⊤

Proof state:
case refine_1.intro
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : LinearMap.range (f.domRestrict S) = LinearMap.range f
x : M
a✝ : x ∈ ⊤
y : ↥S
hy : (f.domRestrict S) y = f x
⊢ x ∈ S ⊔ LinearMap.ker f

Tactic:
have : (y : M) + (x - y) ∈ S ⊔ (LinearMap.ker f) := Submodule.add_mem_sup y.2 (by simp [← hy])

Result:
case refine_1.intro
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : LinearMap.range (f.domRestrict S) = LinearMap.range f
x : M
a✝ : x ∈ ⊤
y : ↥S
hy : (f.domRestrict S) y = f x
this : ↑y + (x - ↑y) ∈ S ⊔ LinearMap.ker f
⊢ x ∈ S ⊔ LinearMap.ker f

Proof state:
case refine_1
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : LinearMap.range (f.domRestrict S) = LinearMap.range f
x : M
a✝ : x ∈ ⊤
this : f x ∈ LinearMap.range f
⊢ x ∈ S ⊔ LinearMap.ker f

Tactic:
rw [← h] at this

Result:
case refine_1
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : LinearMap.range (f.domRestrict S) = LinearMap.range f
x : M
a✝ : x ∈ ⊤
this : f x ∈ LinearMap.range (f.domRestrict S)
⊢ x ∈ S ⊔ LinearMap.ker f

Proof state:
case refine_1.intro
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : LinearMap.range (f.domRestrict S) = LinearMap.range f
x : M
a✝ : x ∈ ⊤
y : ↥S
hy : (f.domRestrict S) y = f x
this : ↑y + (x - ↑y) ∈ S ⊔ LinearMap.ker f
⊢ x ∈ S ⊔ LinearMap.ker f

Tactic:
simpa using this

Result:
no goals

Proof state:
case refine_2
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : S ⊔ LinearMap.ker f = ⊤
⊢ LinearMap.range f ≤ LinearMap.range (f.domRestrict S)

Tactic:
rintro x ⟨y, rfl⟩

Result:
case refine_2.intro
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : S ⊔ LinearMap.ker f = ⊤
y : M
⊢ f y ∈ LinearMap.range (f.domRestrict S)

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_4
M₂ : Type u_5
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝ : RingHomSurjective τ₁₂
f : M →ₛₗ[τ₁₂] M₂
S : Submodule R M
h : LinearMap.range (f.domRestrict S) = LinearMap.range f
x : M
a✝ : x ∈ ⊤
y : ↥S
hy : (f.domRestrict S) y = f x
⊢ x - ↑y ∈ LinearMap.ker f

Tactic:
simp [← hy]

Result:
no goals