internlm/Lean-Github huggingface dataset:
Theorem: linearIndependent_iUnion_of_directed'
Proof 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
Proof 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))
Theorem: linearIndependent_iUnion_of_directed'
Proof 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
Proof 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))
Theorem: linearIndependent_iUnion_of_directed'
Proof 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)
Proof 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))
Theorem: linearIndependent_iUnion_of_directed'
Proof 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) ?_
Proof 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)
Theorem: linearIndependent_iUnion_of_directed'
Proof 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
Proof state after:
no goals
Theorem: linearIndependent_iUnion_of_directed'
Proof 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]
Proof 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)
Theorem: linearIndependent_iUnion_of_directed'
Proof 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
Proof state after:
no goals
Theorem: linearIndependent_iUnion_of_directed'
Proof 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 ↦ ?_)
Proof 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
Theorem: linearIndependent_iUnion_of_directed'
Proof 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
Proof 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
Theorem: linearIndependent_iUnion_of_directed'
Proof 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
Proof state after:
no goals
Theorem: linearIndependent_iUnion_of_directed'
Proof 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
Proof state after:
no goals
Theorem: linearIndependent_sUnion_of_directed'
Proof 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
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : Set (Set ι)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ c ∈ s, LinearIndependent (ι := ↑c) R (c.restrict f)
⊢ LinearIndependent (ι := ↑(⋃₀ s)) R ((⋃₀ s).restrict f)
Tactic:
rw [sUnion_eq_iUnion]
Proof 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
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : Set (Set ι)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ c ∈ s, LinearIndependent (ι := ↑c) R (c.restrict f)
⊢ LinearIndependent (ι := ↑(⋃ i, ↑i)) R ((⋃ i, ↑i).restrict f)
Theorem: linearIndependent_sUnion_of_directed'
Proof 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
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : Set (Set ι)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ c ∈ s, LinearIndependent (ι := ↑c) R (c.restrict f)
⊢ LinearIndependent (ι := ↑(⋃ i, ↑i)) R ((⋃ i, ↑i).restrict f)
Tactic:
apply linearIndependent_iUnion_of_directed' _ _ _ (by aesop)
Proof 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
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : Set (Set ι)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ c ∈ s, LinearIndependent (ι := ↑c) R (c.restrict f)
⊢ Directed (fun x x_1 => x ⊆ x_1) fun j => ↑j
Theorem: linearIndependent_sUnion_of_directed'
Proof 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
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : Set (Set ι)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ c ∈ s, LinearIndependent (ι := ↑c) R (c.restrict f)
⊢ Directed (fun x x_1 => x ⊆ x_1) fun j => ↑j
Tactic:
rintro x y
Proof 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
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : Set (Set ι)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ c ∈ s, LinearIndependent (ι := ↑c) R (c.restrict f)
x y : ↑s
⊢ ∃ z,
    (fun x x_1 => x ⊆ x_1) ((fun j => ↑j) x) ((fun j => ↑j) z) ∧
      (fun x x_1 => x ⊆ x_1) ((fun j => ↑j) y) ((fun j => ↑j) z)
Theorem: linearIndependent_sUnion_of_directed'
Proof 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
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : Set (Set ι)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ c ∈ s, LinearIndependent (ι := ↑c) R (c.restrict f)
x y : ↑s
⊢ ∃ z,
    (fun x x_1 => x ⊆ x_1) ((fun j => ↑j) x) ((fun j => ↑j) z) ∧
      (fun x x_1 => x ⊆ x_1) ((fun j => ↑j) y) ((fun j => ↑j) z)
Tactic:
specialize hs x x.prop y y.prop
Proof 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
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : Set (Set ι)
h : ∀ c ∈ s, LinearIndependent (ι := ↑c) R (c.restrict f)
x y : ↑s
hs : ∃ z ∈ s, (fun x x_1 => x ⊆ x_1) (↑x) z ∧ (fun x x_1 => x ⊆ x_1) (↑y) z
⊢ ∃ z,
    (fun x x_1 => x ⊆ x_1) ((fun j => ↑j) x) ((fun j => ↑j) z) ∧
      (fun x x_1 => x ⊆ x_1) ((fun j => ↑j) y) ((fun j => ↑j) z)
Theorem: linearIndependent_sUnion_of_directed'
Proof 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
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : Set (Set ι)
h : ∀ c ∈ s, LinearIndependent (ι := ↑c) R (c.restrict f)
x y : ↑s
hs : ∃ z ∈ s, (fun x x_1 => x ⊆ x_1) (↑x) z ∧ (fun x x_1 => x ⊆ x_1) (↑y) z
⊢ ∃ z,
    (fun x x_1 => x ⊆ x_1) ((fun j => ↑j) x) ((fun j => ↑j) z) ∧
      (fun x x_1 => x ⊆ x_1) ((fun j => ↑j) y) ((fun j => ↑j) z)
Tactic:
aesop
Proof state after:
no goals
Theorem: linearIndependent_sUnion_of_directed'
Proof 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
inst✝² : DivisionRing R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
f : ι → M
s : Set (Set ι)
hs : DirectedOn (fun x x_1 => x ⊆ x_1) s
h : ∀ c ∈ s, LinearIndependent (ι := ↑c) R (c.restrict f)
⊢ ∀ (j : ↑s), LinearIndependent (ι := ↑↑j) R ((↑j).restrict f)
Tactic:
aesop
Proof state after:
no goals
Theorem: exists_linearIndependent_extension'
Proof 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'
K : Type u_7
V : Type u_8
ι : Type u_9
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
s₀ s t : Set ι
hli : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
⊢ ∃ s, s₀ ⊆ s ∧ s ⊆ t ∧ f '' t ⊆ ↑(span K (f '' s)) ∧ LinearIndependent (ι := ↑s) K (s.restrict f)
Tactic:
have hzorn := zorn_subset_nonempty {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent K (r.restrict f)}
  ?_ s₀ ⟨Subset.rfl, hs₀t, hli⟩
Proof state after:
case refine_2
α : 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'
K : Type u_7
V : Type u_8
ι : Type u_9
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
s₀ s t : Set ι
hli : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
hzorn :
  ∃ m ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)},
    s₀ ⊆ m ∧ ∀ a ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, m ⊆ a → a = m
⊢ ∃ s, s₀ ⊆ s ∧ s ⊆ t ∧ f '' t ⊆ ↑(span K (f '' s)) ∧ LinearIndependent (ι := ↑s) K (s.restrict f)

case refine_1
α : 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'
K : Type u_7
V : Type u_8
ι : Type u_9
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
s₀ s t : Set ι
hli : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
⊢ ∀ c ⊆ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)},
    IsChain (fun x x_1 => x ⊆ x_1) c →
      c.Nonempty → ∃ ub ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, ∀ s ∈ c, s ⊆ ub
Theorem: exists_linearIndependent_extension'
Proof state before:
case refine_1
α : 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'
K : Type u_7
V : Type u_8
ι : Type u_9
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
s₀ s t : Set ι
hli : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
⊢ ∀ c ⊆ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)},
    IsChain (fun x x_1 => x ⊆ x_1) c →
      c.Nonempty → ∃ ub ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, ∀ s ∈ c, s ⊆ ub
Tactic:
rintro c hcss hchain ⟨r, hr⟩
Proof state after:
case refine_1.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'
K : Type u_7
V : Type u_8
ι : Type u_9
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
s₀ s t : Set ι
hli : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
c : Set (Set ι)
hcss : c ⊆ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
r : Set ι
hr : r ∈ c
⊢ ∃ ub ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, ∀ s ∈ c, s ⊆ ub
Theorem: exists_linearIndependent_extension'
Proof state before:
case refine_1.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'
K : Type u_7
V : Type u_8
ι : Type u_9
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
s₀ s t : Set ι
hli : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
c : Set (Set ι)
hcss : c ⊆ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
r : Set ι
hr : r ∈ c
⊢ ∃ ub ∈ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}, ∀ s ∈ c, s ⊆ ub
Tactic:
refine ⟨⋃₀ c, ⟨(hcss hr).1.trans <| subset_sUnion_of_mem hr,
  sUnion_subset fun t' ht'c ↦ (hcss ht'c).2.1,?_⟩, fun _ ↦ subset_sUnion_of_mem⟩
Proof state after:
case refine_1.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'
K : Type u_7
V : Type u_8
ι : Type u_9
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
s₀ s t : Set ι
hli : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
c : Set (Set ι)
hcss : c ⊆ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
r : Set ι
hr : r ∈ c
⊢ LinearIndependent (ι := ↑(⋃₀ c)) K ((⋃₀ c).restrict f)
Theorem: exists_linearIndependent_extension'
Proof state before:
case refine_1.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'
K : Type u_7
V : Type u_8
ι : Type u_9
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
f : ι → V
s₀ s t : Set ι
hli : LinearIndependent (ι := ↑s₀) K (s₀.restrict f)
hs₀t : s₀ ⊆ t
c : Set (Set ι)
hcss : c ⊆ {r | s₀ ⊆ r ∧ r ⊆ t ∧ LinearIndependent (ι := ↑r) K (r.restrict f)}
hchain : IsChain (fun x x_1 => x ⊆ x_1) c
r : Set ι
hr : r ∈ c
⊢ LinearIndependent (ι := ↑(⋃₀ c)) K ((⋃₀ c).restrict f)
Tactic:
apply linearIndependent_sUnion_of_directed' _ _ (IsChain.directedOn hchain)
  (fun s hs ↦ (hcss hs).2.2)
Proof state after:
no goals