-- Mathlib/Algebra/DirectSum/Module.lean
lemma isInternal_biSup_submodule_of_iSupIndep {A : ι → Submodule R M} (s : Set ι)
    (h : iSupIndep <| fun i : s ↦ A i) :
    IsInternal <| fun (i : s) ↦ (A i).comap (⨆ i ∈ s, A i).subtype

Proof state:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
⊢ iSupIndep fun i => Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)

Tactic:
suffices (e ∘ fun i : s ↦ (A i).comap p.subtype) = fun i ↦ ⟨A i, hp i i.property⟩ by
  rw [← iSupIndep_map_orderIso_iff e, this]
  exact .of_coe_Iic_comp h

Result:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
⊢ (⇑e ∘ fun i => Submodule.comap p.subtype (A ↑i)) = fun i => ⟨A ↑i, ⋯⟩

Proof state:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
this : (⇑e ∘ fun i => Submodule.comap p.subtype (A ↑i)) = fun i => ⟨A ↑i, ⋯⟩
⊢ iSupIndep fun i => ⟨A ↑i, ⋯⟩

Tactic:
exact .of_coe_Iic_comp h

Result:
no goals

Proof state:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
this : (⇑e ∘ fun i => Submodule.comap p.subtype (A ↑i)) = fun i => ⟨A ↑i, ⋯⟩
⊢ iSupIndep fun i => Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)

Tactic:
rw [← iSupIndep_map_orderIso_iff e, this]

Result:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
this : (⇑e ∘ fun i => Submodule.comap p.subtype (A ↑i)) = fun i => ⟨A ↑i, ⋯⟩
⊢ iSupIndep fun i => ⟨A ↑i, ⋯⟩

Proof state:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
⊢ (⇑e ∘ fun i => Submodule.comap p.subtype (A ↑i)) = fun i => ⟨A ↑i, ⋯⟩

Tactic:
ext i m

Result:
case h.a.h
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
i : ↑s
m : M
⊢ m ∈ ↑((⇑e ∘ fun i => Submodule.comap p.subtype (A ↑i)) i) ↔ m ∈ ↑⟨A ↑i, ⋯⟩

Proof state:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
⊢ ⨆ i, Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i) = ⊤

Tactic:
simp [iSup_subtype]

Result:
no goals

Proof state:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
⊢ iSupIndep fun i => Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)

Tactic:
let e : Submodule R p ≃o Set.Iic p := p.mapIic

Result:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
⊢ iSupIndep fun i => Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)

Proof state:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
⊢ IsInternal fun i => Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)

Tactic:
refine (isInternal_submodule_iff_iSupIndep_and_iSup_eq_top _).mpr ⟨?_, by simp [iSup_subtype]⟩

Result:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
⊢ iSupIndep fun i => Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)

Proof state:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
⊢ iSupIndep fun i => Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)

Tactic:
have hp : ∀ i ∈ s, A i ≤ p := fun i hi ↦ le_biSup A hi

Result:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
⊢ iSupIndep fun i => Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)

Proof state:
case h.a.h
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
i : ↑s
m : M
⊢ m ∈ Submodule.map p.subtype (Submodule.comap p.subtype (A ↑i)) ↔ m ∈ ↑⟨A ↑i, ⋯⟩

Tactic:
rw [Submodule.map_comap_subtype, inf_of_le_right (hp i i.property)]

Result:
no goals

Proof state:
case h.a.h
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
i : ↑s
m : M
⊢ m ∈ ↑((⇑e ∘ fun i => Submodule.comap p.subtype (A ↑i)) i) ↔ m ∈ ↑⟨A ↑i, ⋯⟩

Tactic:
change m ∈ ((A i).comap p.subtype).map p.subtype ↔ _

Result:
case h.a.h
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
hp : ∀ i ∈ s, A i ≤ p
e : Submodule R ↥p ≃o ↑(Set.Iic p) := p.mapIic
i : ↑s
m : M
⊢ m ∈ Submodule.map p.subtype (Submodule.comap p.subtype (A ↑i)) ↔ m ∈ ↑⟨A ↑i, ⋯⟩

Proof state:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
⊢ iSupIndep fun i => Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)

Tactic:
let p := ⨆ i ∈ s, A i

Result:
R : Type u
inst✝² : Ring R
ι : Type v
dec_ι : DecidableEq ι
M : Type u_1
inst✝¹ : AddCommGroup M
inst✝ : Module R M
A : ι → Submodule R M
s : Set ι
h : iSupIndep fun i => A ↑i
p : Submodule R M := ⨆ i ∈ s, A i
⊢ iSupIndep fun i => Submodule.comap (⨆ i ∈ s, A i).subtype (A ↑i)