internlm/Lean-Github huggingface dataset:
Theorem: linearIndependent_restrict_pair_iff
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 ι✝
K : Type u_10
V : Type u_11
ι : Type u_12
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
i j : ι
f : ι → V
hij : i ≠ j
hi : f i ≠ 0
h : ¬f j = 0 ∧ ∀ (x : K), ¬x • f j = f i
h' : 0 • f i = f j
⊢ f j = 0
Tactic:
simp [← h']
Proof state after:
no goals
Theorem: linearIndependent.union_index
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 ι✝
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 ?_
Proof 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
Theorem: linearIndependent.union_index
Proof 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]
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 ι✝
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
Theorem: linearIndependent.union_index
Proof 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
Proof state after:
no goals
Theorem: linearIndependent.union_index
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 ι✝
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]
Proof 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
Theorem: linearIndependent.union_index
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 ι✝
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]
Proof 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
Theorem: linearIndependent.union_index
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 ι✝
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
Proof 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
Theorem: linearIndependent.union_index
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 ι✝
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⟩
Proof 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
Theorem: linearIndependent.union_index
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 ι✝
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))
Proof state after:
no goals
Theorem: linearIndependent.union_index
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 ι✝
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
Proof 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
Theorem: linearIndependent.union_index
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 ι✝
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
Proof 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
Theorem: linearIndependent.union_index
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 ι✝
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⟩
Proof 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
Theorem: linearIndependent.union_index
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 ι✝
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))]
Proof state after:
no goals
Theorem: linearIndependent.union_index
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 ι✝
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]
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'
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)
Theorem: linearIndependent.union_index
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 ι✝
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)
Proof state after:
no goals
Theorem: LinearIndependent.union_index'
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 ι✝
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 (⇑(span R (f '' s)).mkQ ∘ f))
⊢ LinearIndependent (ι := ↑(s ∪ t)) R ((s ∪ t).restrict f)
Tactic:
apply linearIndependent.union_index hs ht.of_comp
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'
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 (⇑(span R (f '' s)).mkQ ∘ f))
⊢ Disjoint (span R (f '' s)) (span R (f '' t))
Theorem: LinearIndependent.union_index'
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 ι✝
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 (⇑(span R (f '' s)).mkQ ∘ f))
⊢ Disjoint (span R (f '' s)) (span R (f '' t))
Tactic:
convert (Submodule.range_ker_disjoint ht).symm
Proof state after:
case h.e'_4
α : 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 (⇑(span R (f '' s)).mkQ ∘ f))
⊢ span R (f '' s) = LinearMap.ker (span R (f '' s)).mkQ

case h.e'_5.h.e'_6
α : 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 (⇑(span R (f '' s)).mkQ ∘ f))
⊢ f '' t = range fun x => f ↑x
Theorem: LinearIndependent.union_index'
Proof state before:
case h.e'_5.h.e'_6
α : 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 (⇑(span R (f '' s)).mkQ ∘ f))
⊢ f '' t = range fun x => f ↑x
Tactic:
aesop
Proof state after:
no goals
Theorem: LinearIndependent.union_index'
Proof state before:
case h.e'_4
α : 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 (⇑(span R (f '' s)).mkQ ∘ f))
⊢ span R (f '' s) = LinearMap.ker (span R (f '' s)).mkQ
Tactic:
simp
Proof state after:
no goals
Theorem: PartialEquiv.IsImage.restr_eq_restr_set
Proof state before:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
t : Set β
h : e.IsImage s t
⊢ h.restr = e.restr s
Tactic:
ext <;> simp
Proof state after:
no goals
Theorem: PartialEquiv.image_subset_target
Proof state before:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
hs : s ⊆ e.source
⊢ ↑e '' s ⊆ e.target
Tactic:
rw [← e.image_source_eq_target]
Proof state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
hs : s ⊆ e.source
⊢ ↑e '' s ⊆ ↑e '' e.source
Theorem: PartialEquiv.image_subset_target
Proof state before:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
hs : s ⊆ e.source
⊢ ↑e '' s ⊆ ↑e '' e.source
Tactic:
exact image_subset _ hs
Proof state after:
no goals
Theorem: PartialEquiv.symm_image_subset_source
Proof state before:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
hs : s ⊆ e.target
⊢ ↑e.symm '' s ⊆ e.source
Tactic:
rw [← e.symm_image_target_eq_source]
Proof state after:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
hs : s ⊆ e.target
⊢ ↑e.symm '' s ⊆ ↑e.symm '' e.target
Theorem: PartialEquiv.symm_image_subset_source
Proof state before:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set β
hs : s ⊆ e.target
⊢ ↑e.symm '' s ⊆ ↑e.symm '' e.target
Tactic:
exact image_subset _ hs
Proof state after:
no goals