-- Mathlib/LinearAlgebra/Span/Basic.lean
lemma biSup_comap_eq_top_of_range_eq_biSup
    {R R₂ : Type*} [Ring R] [Ring R₂] {τ₁₂ : R →+* R₂} [RingHomSurjective τ₁₂]
    [Module R M] [Module R₂ M₂] {ι : Type*} (s : Set ι) (hs : s.Nonempty)
    (p : ι → Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (hf : LinearMap.range f = ⨆ i ∈ s, p i) :
    ⨆ i ∈ s, (p i).comap f = ⊤

Proof state:
M : Type u_4
M₂ : Type u_5
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
R : Type u_9
R₂ : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring R₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
ι : Type u_11
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : LinearMap.range f = ⨆ i ∈ s, p i
⊢ ⨆ i ∈ s, comap f (p i) = ⊤

Tactic:
suffices ⨆ i ∈ s, (p i).comap (LinearMap.range f).subtype = ⊤ by
  rw [← biSup_comap_eq_top_of_surjective s hs _ this _ f.surjective_rangeRestrict]; rfl

Result:
M : Type u_4
M₂ : Type u_5
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
R : Type u_9
R₂ : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring R₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
ι : Type u_11
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : LinearMap.range f = ⨆ i ∈ s, p i
⊢ ⨆ i ∈ s, comap (LinearMap.range f).subtype (p i) = ⊤

Proof state:
M : Type u_4
M₂ : Type u_5
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
R : Type u_9
R₂ : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring R₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
ι : Type u_11
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : LinearMap.range f = ⨆ i ∈ s, p i
⊢ ⨆ i ∈ s, comap (LinearMap.range f).subtype (p i) = ⊤

Tactic:
exact hf ▸ biSup_comap_subtype_eq_top s p

Result:
no goals

Proof state:
M : Type u_4
M₂ : Type u_5
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
R : Type u_9
R₂ : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring R₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
ι : Type u_11
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : LinearMap.range f = ⨆ i ∈ s, p i
this : ⨆ i ∈ s, comap (LinearMap.range f).subtype (p i) = ⊤
⊢ ⨆ i ∈ s, comap f (p i) = ⨆ i ∈ s, comap f.rangeRestrict (comap (LinearMap.range f).subtype (p i))

Tactic:
rfl

Result:
no goals

Proof state:
M : Type u_4
M₂ : Type u_5
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
R : Type u_9
R₂ : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring R₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
ι : Type u_11
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : LinearMap.range f = ⨆ i ∈ s, p i
this : ⨆ i ∈ s, comap (LinearMap.range f).subtype (p i) = ⊤
⊢ ⨆ i ∈ s, comap f (p i) = ⊤

Tactic:
rw [← biSup_comap_eq_top_of_surjective s hs _ this _ f.surjective_rangeRestrict]

Result:
M : Type u_4
M₂ : Type u_5
inst✝⁶ : AddCommGroup M
inst✝⁵ : AddCommGroup M₂
R : Type u_9
R₂ : Type u_10
inst✝⁴ : Ring R
inst✝³ : Ring R₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
inst✝¹ : Module R M
inst✝ : Module R₂ M₂
ι : Type u_11
s : Set ι
hs : s.Nonempty
p : ι → Submodule R₂ M₂
f : M →ₛₗ[τ₁₂] M₂
hf : LinearMap.range f = ⨆ i ∈ s, p i
this : ⨆ i ∈ s, comap (LinearMap.range f).subtype (p i) = ⊤
⊢ ⨆ i ∈ s, comap f (p i) = ⨆ i ∈ s, comap f.rangeRestrict (comap (LinearMap.range f).subtype (p i))