Theorem: linearIndependent_sUnion_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
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]
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)

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)
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

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
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)

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
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)

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
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
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
State after:
no goals