Theorem: linearIndependent.union_index (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'
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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
⊢ LinearIndependent (ι := ↑(s ∪ t)) R ((s ∪ t).restrict f)
Tactic:
refine (linearIndependent_image ?_).2 ?_
State after:
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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
⊢ InjOn f (s ∪ t)

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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
⊢ LinearIndependent R fun (x : ↑(f '' (s ∪ t))) => ↑x

State before:
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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
⊢ LinearIndependent R fun (x : ↑(f '' (s ∪ t))) => ↑x
Tactic:
rw [image_union]
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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
⊢ LinearIndependent R fun (x : ↑(f '' s ∪ f '' t)) => ↑x

State before:
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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
⊢ LinearIndependent R fun (x : ↑(f '' s ∪ f '' t)) => ↑x
Tactic:
exact LinearIndependent.union hs.image ht.image hdj
State after:
no goals

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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
⊢ InjOn f (s ∪ t)
Tactic:
rw [injOn_union, and_iff_right <| injOn_iff_injective.2 hs.injective,
  and_iff_right <| injOn_iff_injective.2 ht.injective]
State after:
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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
⊢ ∀ x ∈ s, ∀ y ∈ t, f x ≠ f y

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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
⊢ Disjoint s t

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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
⊢ Disjoint s t
Tactic:
rw [disjoint_iff_forall_ne]
State after:
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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
⊢ ∀ ⦃a : ι⦄, a ∈ s → ∀ ⦃b : ι⦄, b ∈ t → a ≠ b

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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
⊢ ∀ ⦃a : ι⦄, a ∈ s → ∀ ⦃b : ι⦄, b ∈ t → a ≠ b
Tactic:
rintro i his _ hit rfl
State after:
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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
i : ι
his : i ∈ s
hit : i ∈ t
⊢ False

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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
i : ι
his : i ∈ s
hit : i ∈ t
⊢ False
Tactic:
apply hs.ne_zero ⟨i, his⟩
State after:
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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
i : ι
his : i ∈ s
hit : i ∈ t
⊢ s.restrict f ⟨i, his⟩ = 0

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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
i : ι
his : i ∈ s
hit : i ∈ t
⊢ s.restrict f ⟨i, his⟩ = 0
Tactic:
exact (Submodule.disjoint_def.1 hdj) (f i) (subset_span (mem_image_of_mem _ his))
  (subset_span (mem_image_of_mem _ hit))
State after:
no goals

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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
⊢ ∀ x ∈ s, ∀ y ∈ t, f x ≠ f y
Tactic:
intro x hx y hy he
State after:
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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
x : ι
hx : x ∈ s
y : ι
hy : y ∈ t
he : f x = f y
⊢ False

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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : Disjoint (span R (f '' s)) (span R (f '' t))
x : ι
hx : x ∈ s
y : ι
hy : y ∈ t
he : f x = f y
⊢ False
Tactic:
rw [Submodule.disjoint_def] at hdj
State after:
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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : ∀ x ∈ span R (f '' s), x ∈ span R (f '' t) → x = 0
x : ι
hx : x ∈ s
y : ι
hy : y ∈ t
he : f x = f y
⊢ False

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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : ∀ x ∈ span R (f '' s), x ∈ span R (f '' t) → x = 0
x : ι
hx : x ∈ s
y : ι
hy : y ∈ t
he : f x = f y
⊢ False
Tactic:
apply hs.ne_zero ⟨x,hx⟩
State after:
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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : ∀ x ∈ span R (f '' s), x ∈ span R (f '' t) → x = 0
x : ι
hx : x ∈ s
y : ι
hy : y ∈ t
he : f x = f y
⊢ s.restrict f ⟨x, hx⟩ = 0

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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : ∀ x ∈ span R (f '' s), x ∈ span R (f '' t) → x = 0
x : ι
hx : x ∈ s
y : ι
hy : y ∈ t
he : f x = f y
⊢ s.restrict f ⟨x, hx⟩ = 0
Tactic:
simp [hdj _ (subset_span (mem_image_of_mem _ hx))
  (by rw [he]; exact subset_span (mem_image_of_mem _ hy))]
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'
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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : ∀ x ∈ span R (f '' s), x ∈ span R (f '' t) → x = 0
x : ι
hx : x ∈ s
y : ι
hy : y ∈ t
he : f x = f y
⊢ f x ∈ span R (f '' t)
Tactic:
rw [he]
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'
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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : ∀ x ∈ span R (f '' s), x ∈ span R (f '' t) → x = 0
x : ι
hx : x ∈ s
y : ι
hy : y ∈ t
he : f x = f y
⊢ f y ∈ span R (f '' t)

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 ι✝
R : Type u_10
M : Type u_11
ι : Type u_12
inst✝² : Field R
inst✝¹ : AddCommGroup M
inst✝ : Module R M
s t : Set ι
f : ι → M
hs : LinearIndependent (ι := ↑s) R (s.restrict f)
ht : LinearIndependent (ι := ↑t) R (t.restrict f)
hdj : ∀ x ∈ span R (f '' s), x ∈ span R (f '' t) → x = 0
x : ι
hx : x ∈ s
y : ι
hy : y ∈ t
he : f x = f y
⊢ f y ∈ span R (f '' t)
Tactic:
exact subset_span (mem_image_of_mem _ hy)
State after:
no goals