K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : ¬(#κ) ≤ (#ι)
⊢ False
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
⊢ (#κ) ≤ (#ι)
by_contra h
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
⊢ False
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : ¬(#κ) ≤ (#ι)
⊢ False
rw [not_le, ← Cardinal.mk_finset_of_infinite ι] at h
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
⊢ False
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
⊢ False
let Φ := fun k : κ => (b.repr (v k)).support
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
⊢ False
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
⊢ False
obtain ⟨s, w : Infinite ↑(Φ ⁻¹' {s})⟩ := Cardinal.exists_infinite_fiber Φ h (by infer_instance)
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := fun k => v ↑k
⊢ False
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
⊢ False
let v' := fun k : Φ ⁻¹' {s} => v k
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := fun k => v ↑k
i' : LinearIndependent R v'
⊢ False
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := fun k => v ↑k
⊢ False
have i' : LinearIndependent R v' := i.comp _ Subtype.val_injective
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := fun k => v ↑k
i' : LinearIndependent R v'
w' : Fintype ↑(Φ ⁻¹' {s})
⊢ False
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := fun k => v ↑k
i' : LinearIndependent R v'
⊢ False
have w' : Fintype (Φ ⁻¹' {s}) := by
  apply linearIndependentFintypeOfLeSpanFintype v' i' (s.image b)
  rintro m ⟨⟨p, ⟨rfl⟩⟩, rfl⟩
  simp only [SetLike.mem_coe, Subtype.coe_mk, Finset.coe_image]
  apply Basis.mem_span_repr_support
no goals
case intro
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := fun k => v ↑k
i' : LinearIndependent R v'
w' : Fintype ↑(Φ ⁻¹' {s})
⊢ False
exact w.false
no goals
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
⊢ Infinite (Finset ι)
infer_instance
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := fun k => v ↑k
i' : LinearIndependent R v'
⊢ range v' ≤ ↑(span R ↑(Finset.image (↑b) s))
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := fun k => v ↑k
i' : LinearIndependent R v'
⊢ Fintype ↑(Φ ⁻¹' {s})
apply linearIndependentFintypeOfLeSpanFintype v' i' (s.image b)
case intro.mk.refl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
p : κ
w : Infinite ↑(Φ ⁻¹' {Φ p})
v' : ↑(Φ ⁻¹' {Φ p}) → M := fun k => v ↑k
i' : LinearIndependent R v'
⊢ v' { val := p, property := (_ : Φ p = Φ p) } ∈ ↑(span R ↑(Finset.image (↑b) (Φ p)))
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
s : Finset ι
w : Infinite ↑(Φ ⁻¹' {s})
v' : ↑(Φ ⁻¹' {s}) → M := fun k => v ↑k
i' : LinearIndependent R v'
⊢ range v' ≤ ↑(span R ↑(Finset.image (↑b) s))
rintro m ⟨⟨p, ⟨rfl⟩⟩, rfl⟩
case intro.mk.refl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
p : κ
w : Infinite ↑(Φ ⁻¹' {Φ p})
v' : ↑(Φ ⁻¹' {Φ p}) → M := fun k => v ↑k
i' : LinearIndependent R v'
⊢ v p ∈ span R (↑b '' ↑(↑b.repr (v p)).support)
case intro.mk.refl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
p : κ
w : Infinite ↑(Φ ⁻¹' {Φ p})
v' : ↑(Φ ⁻¹' {Φ p}) → M := fun k => v ↑k
i' : LinearIndependent R v'
⊢ v' { val := p, property := (_ : Φ p = Φ p) } ∈ ↑(span R ↑(Finset.image (↑b) (Φ p)))
simp only [SetLike.mem_coe, Subtype.coe_mk, Finset.coe_image]
no goals
case intro.mk.refl
K : Type u
V V₁ V₂ V₃ : Type v
V' V'₁ : Type v'
V'' : Type v''
ι✝ : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type ?u.357987
R : Type u
inst✝⁴ : Ring R
inst✝³ : StrongRankCondition R
M : Type v
inst✝² : AddCommGroup M
inst✝¹ : Module R M
ι : Type u_1
b : Basis ι R M
inst✝ : Infinite ι
κ : Type u_1
v : κ → M
i : LinearIndependent R v
h : (#Finset ι) < (#κ)
Φ : κ → Finset ι := fun k => (↑b.repr (v k)).support
p : κ
w : Infinite ↑(Φ ⁻¹' {Φ p})
v' : ↑(Φ ⁻¹' {Φ p}) → M := fun k => v ↑k
i' : LinearIndependent R v'
⊢ v p ∈ span R (↑b '' ↑(↑b.repr (v p)).support)
apply Basis.mem_span_repr_support