Theorem: linearIndependent_iUnion_of_directed' (Matroid/ForMathlib/LinearAlgebra/LinearIndependent.lean)

State before:
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
⊢ LinearIndependent (ι := ↑(⋃ j, s j)) R ((⋃ j, s j).restrict f)
Tactic:
obtain (h_empt | hne) := isEmpty_or_nonempty η
State after:
case inl
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
h_empt : IsEmpty η
⊢ LinearIndependent (ι := ↑(⋃ j, s j)) R ((⋃ j, s j).restrict f)

case inr
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
⊢ LinearIndependent (ι := ↑(⋃ j, s j)) R ((⋃ j, s j).restrict f)

State before:
case inr
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
⊢ LinearIndependent (ι := ↑(⋃ j, s j)) R ((⋃ j, s j).restrict f)
Tactic:
apply linearIndependent_of_finite_index _ (fun t ht ↦ ?_)
State after:
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
⊢ LinearIndependent (ι := ↑t) R (t.restrict ((⋃ j, s j).restrict f))

State before:
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
⊢ LinearIndependent (ι := ↑t) R (t.restrict ((⋃ j, s j).restrict f))
Tactic:
obtain ⟨I,hIfin, hI⟩ :=
  finite_subset_iUnion (ht.image Subtype.val) (Subtype.coe_image_subset (⋃ j, s j) t)
State after:
case intro.intro
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
⊢ LinearIndependent (ι := ↑t) R (t.restrict ((⋃ j, s j).restrict f))

State before:
case intro.intro
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
⊢ LinearIndependent (ι := ↑t) R (t.restrict ((⋃ j, s j).restrict f))
Tactic:
obtain ⟨z, hz⟩ := hs.finset_le hIfin.toFinset
State after:
case intro.intro.intro
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
z : η
hz : ∀ i ∈ hIfin.toFinset, s i ⊆ s z
⊢ LinearIndependent (ι := ↑t) R (t.restrict ((⋃ j, s j).restrict f))

State before:
case intro.intro.intro
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
z : η
hz : ∀ i ∈ hIfin.toFinset, s i ⊆ s z
⊢ LinearIndependent (ι := ↑t) R (t.restrict ((⋃ j, s j).restrict f))
Tactic:
have hss : Subtype.val '' t ⊆ s z := by
  refine hI.trans (iUnion_subset fun i j h ↦ ?_)
  simp only [mem_iUnion, exists_prop] at h
  exact hz i (by simpa using h.1) h.2
State after:
case intro.intro.intro
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
z : η
hz : ∀ i ∈ hIfin.toFinset, s i ⊆ s z
hss : Subtype.val '' t ⊆ s z
⊢ LinearIndependent (ι := ↑t) R (t.restrict ((⋃ j, s j).restrict f))

State before:
case intro.intro.intro
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
z : η
hz : ∀ i ∈ hIfin.toFinset, s i ⊆ s z
hss : Subtype.val '' t ⊆ s z
⊢ LinearIndependent (ι := ↑t) R (t.restrict ((⋃ j, s j).restrict f))
Tactic:
set emb : t → s z := (inclusion hss) ∘ (imageFactorization Subtype.val t)
State after:
case intro.intro.intro
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
z : η
hz : ∀ i ∈ hIfin.toFinset, s i ⊆ s z
hss : Subtype.val '' t ⊆ s z
emb : ↑t → ↑(s z) := Set.inclusion hss ∘ imageFactorization Subtype.val t
⊢ LinearIndependent (ι := ↑t) R (t.restrict ((⋃ j, s j).restrict f))

State before:
case intro.intro.intro
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
z : η
hz : ∀ i ∈ hIfin.toFinset, s i ⊆ s z
hss : Subtype.val '' t ⊆ s z
emb : ↑t → ↑(s z) := Set.inclusion hss ∘ imageFactorization Subtype.val t
⊢ LinearIndependent (ι := ↑t) R (t.restrict ((⋃ j, s j).restrict f))
Tactic:
refine (h z).comp emb <| Function.Injective.comp (inclusion_injective hss) ?_
State after:
case intro.intro.intro
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
z : η
hz : ∀ i ∈ hIfin.toFinset, s i ⊆ s z
hss : Subtype.val '' t ⊆ s z
emb : ↑t → ↑(s z) := Set.inclusion hss ∘ imageFactorization Subtype.val t
⊢ Injective (imageFactorization Subtype.val t)

State before:
case intro.intro.intro
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
z : η
hz : ∀ i ∈ hIfin.toFinset, s i ⊆ s z
hss : Subtype.val '' t ⊆ s z
emb : ↑t → ↑(s z) := Set.inclusion hss ∘ imageFactorization Subtype.val t
⊢ Injective (imageFactorization Subtype.val t)
Tactic:
exact Subtype.val_injective.injOn.imageFactorization_injective
State after:
no goals

State before:
case inl
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
h_empt : IsEmpty η
⊢ LinearIndependent (ι := ↑(⋃ j, s j)) R ((⋃ j, s j).restrict f)
Tactic:
rw [iUnion_of_empty s]
State after:
case inl
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
h_empt : IsEmpty η
⊢ LinearIndependent (ι := ↑∅) R (∅.restrict f)

State before:
case inl
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
h_empt : IsEmpty η
⊢ LinearIndependent (ι := ↑∅) R (∅.restrict f)
Tactic:
apply linearIndependent_empty_type
State after:
no goals

State before:
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
z : η
hz : ∀ i ∈ hIfin.toFinset, s i ⊆ s z
⊢ Subtype.val '' t ⊆ s z
Tactic:
refine hI.trans (iUnion_subset fun i j h ↦ ?_)
State after:
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h✝ : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
z : η
hz : ∀ i ∈ hIfin.toFinset, s i ⊆ s z
i : η
j : ι
h : j ∈ ⋃ (_ : i ∈ I), s i
⊢ j ∈ s z

State before:
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h✝ : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
z : η
hz : ∀ i ∈ hIfin.toFinset, s i ⊆ s z
i : η
j : ι
h : j ∈ ⋃ (_ : i ∈ I), s i
⊢ j ∈ s z
Tactic:
simp only [mem_iUnion, exists_prop] at h
State after:
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h✝ : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
z : η
hz : ∀ i ∈ hIfin.toFinset, s i ⊆ s z
i : η
j : ι
h : i ∈ I ∧ j ∈ s i
⊢ j ∈ s z

State before:
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h✝ : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
z : η
hz : ∀ i ∈ hIfin.toFinset, s i ⊆ s z
i : η
j : ι
h : i ∈ I ∧ j ∈ s i
⊢ j ∈ s z
Tactic:
exact hz i (by simpa using h.1) h.2
State after:
no goals

State before:
α : Type u_1
ι✝ : Type u_2
W : Type u_3
W' : Type u_4
M✝ : Type u_5
R✝ : Type u_6
inst✝⁴ : AddCommGroup W
inst✝³ : AddCommGroup W'
R : Type u_7
M : Type u_8
ι : Type u_9
η : Type u_10
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : η → Set ι
hs : Directed (fun x x_1 => x ⊆ x_1) s
h✝ : ∀ (j : η), LinearIndependent (ι := ↑(s j)) R ((s j).restrict f)
hne : Nonempty η
t : Set ↑(⋃ j, s j)
ht : t.Finite
I : Set η
hIfin : I.Finite
hI : Subtype.val '' t ⊆ ⋃ i ∈ I, s i
z : η
hz : ∀ i ∈ hIfin.toFinset, s i ⊆ s z
i : η
j : ι
h : i ∈ I ∧ j ∈ s i
⊢ i ∈ hIfin.toFinset
Tactic:
simpa using h.1
State after:
no goals