-- Mathlib/LinearAlgebra/Span/Basic.lean
@[simp]
lemma biSup_comap_subtype_eq_top {ι : Type*} (s : Set ι) (p : ι → Submodule R M) :
    ⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype = ⊤

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
⊢ ∀ i ∈ s, map (⨆ i ∈ s, p i).subtype (comap (⨆ i ∈ s, p i).subtype (p i)) = p i

Tactic:
intro i hi

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
i : ι
hi : i ∈ s
⊢ map (⨆ i ∈ s, p i).subtype (comap (⨆ i ∈ s, p i).subtype (p i)) = p i

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
⊢ ⟨x, hx⟩ ∈ ⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i)

Tactic:
suffices x ∈ (⨆ i ∈ s, (p i).comap (⨆ i ∈ s, p i).subtype).map (⨆ i ∈ s, (p i)).subtype by
  obtain ⟨y, hy, rfl⟩ := Submodule.mem_map.mp this
  exact hy

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
⊢ x ∈ map (⨆ i ∈ s, p i).subtype (⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i))

Proof state:
case intro.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ y : ↥(⨆ i ∈ s, p i)
hy : y ∈ ⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i)
hx : (⨆ i ∈ s, p i).subtype y ∈ ⨆ i ∈ s, p i
x✝ : ⟨(⨆ i ∈ s, p i).subtype y, hx⟩ ∈ ⊤
this : (⨆ i ∈ s, p i).subtype y ∈ map (⨆ i ∈ s, p i).subtype (⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i))
⊢ ⟨(⨆ i ∈ s, p i).subtype y, hx⟩ ∈ ⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i)

Tactic:
exact hy

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
⊢ ⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i) = ⊤

Tactic:
refine eq_top_iff.mpr fun ⟨x, hx⟩ _ ↦ ?_

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
⊢ ⟨x, hx⟩ ∈ ⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i)

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
i : ι
hi : i ∈ s
⊢ map (⨆ i ∈ s, p i).subtype (comap (⨆ i ∈ s, p i).subtype (p i)) = p i

Tactic:
rw [map_comap_eq, range_subtype, inf_eq_right]

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
i : ι
hi : i ∈ s
⊢ p i ≤ ⨆ i ∈ s, p i

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
⊢ x ∈ map (⨆ i ∈ s, p i).subtype (⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i))

Tactic:
suffices ∀ i ∈ s, (comap (⨆ i ∈ s, p i).subtype (p i)).map (⨆ i ∈ s, p i).subtype = p i by
  simpa only [map_iSup, biSup_congr this]

Result:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
⊢ ∀ i ∈ s, map (⨆ i ∈ s, p i).subtype (comap (⨆ i ∈ s, p i).subtype (p i)) = p i

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
i : ι
hi : i ∈ s
⊢ p i ≤ ⨆ i ∈ s, p i

Tactic:
exact le_biSup p hi

Result:
no goals

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
this : x ∈ map (⨆ i ∈ s, p i).subtype (⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i))
⊢ ⟨x, hx⟩ ∈ ⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i)

Tactic:
obtain ⟨y, hy, rfl⟩ := Submodule.mem_map.mp this

Result:
case intro.intro
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ y : ↥(⨆ i ∈ s, p i)
hy : y ∈ ⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i)
hx : (⨆ i ∈ s, p i).subtype y ∈ ⨆ i ∈ s, p i
x✝ : ⟨(⨆ i ∈ s, p i).subtype y, hx⟩ ∈ ⊤
this : (⨆ i ∈ s, p i).subtype y ∈ map (⨆ i ∈ s, p i).subtype (⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i))
⊢ ⟨(⨆ i ∈ s, p i).subtype y, hx⟩ ∈ ⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i)

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
ι : Type u_9
s : Set ι
p : ι → Submodule R M
x✝¹ : ↥(⨆ i ∈ s, p i)
x : M
hx : x ∈ ⨆ i ∈ s, p i
x✝ : ⟨x, hx⟩ ∈ ⊤
this : ∀ i ∈ s, map (⨆ i ∈ s, p i).subtype (comap (⨆ i ∈ s, p i).subtype (p i)) = p i
⊢ x ∈ map (⨆ i ∈ s, p i).subtype (⨆ i ∈ s, comap (⨆ i ∈ s, p i).subtype (p i))

Tactic:
simpa only [map_iSup, biSup_congr this]

Result:
no goals