-- 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_2.intro.intro.intro.intro.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 = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ LinearMap.ker f
⊢ f (s + t) ∈ LinearMap.range (f.domRestrict S)

Tactic:
exact ⟨⟨s, hs⟩, by simp [LinearMap.mem_ker.1 ht]⟩

Result:
no goals

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 : S ⊔ LinearMap.ker f = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ LinearMap.ker f
⊢ (f.domRestrict S) ⟨s, hs⟩ = f (s + t)

Tactic:
simp [LinearMap.mem_ker.1 ht]

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.domRestrict S) = LinearMap.range f

Tactic:
refine le_antisymm (LinearMap.range_domRestrict_le_range f S) ?_

Result:
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)

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
⊢ ⊤ ≤ S ⊔ LinearMap.ker f

Tactic:
intro x _

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 ∈ ⊤
⊢ x ∈ S ⊔ LinearMap.ker f

Proof state:
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)

Tactic:
obtain ⟨s, hs, t, ht, rfl⟩ : ∃ s, s ∈ S ∧ ∃ t, t ∈ LinearMap.ker f ∧ s + t = y :=
  Submodule.mem_sup.1 (by simp [h])

Result:
case refine_2.intro.intro.intro.intro.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 = ⊤
s : M
hs : s ∈ S
t : M
ht : t ∈ LinearMap.ker f
⊢ f (s + t) ∈ 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
⊢ LinearMap.range (f.domRestrict S) = LinearMap.range f ↔ S ⊔ LinearMap.ker f = ⊤

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩

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
⊢ S ⊔ LinearMap.ker f = ⊤

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.domRestrict S) = LinearMap.range 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 ∈ ⊤
⊢ x ∈ S ⊔ LinearMap.ker f

Tactic:
have : f x ∈ LinearMap.range f := LinearMap.mem_range_self f x

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
⊢ 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
⊢ S ⊔ LinearMap.ker f = ⊤

Tactic:
rw [eq_top_iff]

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
⊢ ⊤ ≤ S ⊔ LinearMap.ker f

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 : S ⊔ LinearMap.ker f = ⊤
y : M
⊢ y ∈ S ⊔ LinearMap.ker f

Tactic:
simp [h]

Result:
no goals

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.domRestrict S)
⊢ x ∈ S ⊔ LinearMap.ker f

Tactic:
obtain ⟨y, hy⟩ : ∃ y : S, f.domRestrict S y = f x := this

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
⊢ x ∈ S ⊔ LinearMap.ker f