[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : Module.rank K V = ↑n
⊢ finrank K V = n
[PROOFSTEP]
apply_fun toNat at h 
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : ↑toNat (Module.rank K V) = ↑toNat ↑n
⊢ finrank K V = n
[PROOFSTEP]
rw [toNat_cast] at h 
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : ↑toNat (Module.rank K V) = n
⊢ finrank K V = n
[PROOFSTEP]
exact_mod_cast h
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : Module.rank K V ≤ ↑n
⊢ finrank K V ≤ n
[PROOFSTEP]
rwa [← Cardinal.toNat_le_iff_le_of_lt_aleph0, toNat_cast] at h 
[GOAL]
case hc
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : Module.rank K V ≤ ↑n
⊢ Module.rank K V < ℵ₀
[PROOFSTEP]
exact h.trans_lt (nat_lt_aleph0 n)
[GOAL]
case hd
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : Module.rank K V ≤ ↑n
⊢ ↑n < ℵ₀
[PROOFSTEP]
exact nat_lt_aleph0 n
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : Module.rank K V < ↑n
⊢ finrank K V < n
[PROOFSTEP]
rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_cast] at h 
[GOAL]
case hc
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : Module.rank K V < ↑n
⊢ Module.rank K V < ℵ₀
[PROOFSTEP]
exact h.trans (nat_lt_aleph0 n)
[GOAL]
case hd
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : Module.rank K V < ↑n
⊢ ↑n < ℵ₀
[PROOFSTEP]
exact nat_lt_aleph0 n
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : n < finrank K V
⊢ ↑n < Module.rank K V
[PROOFSTEP]
rwa [← Cardinal.toNat_lt_iff_lt_of_lt_aleph0, toNat_cast]
[GOAL]
case hc
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : n < finrank K V
⊢ ↑n < ℵ₀
[PROOFSTEP]
exact nat_lt_aleph0 n
[GOAL]
case hd
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : n < finrank K V
⊢ Module.rank K V < ℵ₀
[PROOFSTEP]
contrapose! h
[GOAL]
case hd
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : ℵ₀ ≤ Module.rank K V
⊢ finrank K V ≤ n
[PROOFSTEP]
rw [finrank, Cardinal.toNat_apply_of_aleph0_le h]
[GOAL]
case hd
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
n : ℕ
h : ℵ₀ ≤ Module.rank K V
⊢ 0 ≤ n
[PROOFSTEP]
exact n.zero_le
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
h : 1 < finrank K V
⊢ 1 < Module.rank K V
[PROOFSTEP]
simpa using lt_rank_of_lt_finrank h
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
h : lift (Module.rank K V) ≤ lift (Module.rank K V₂)
h' : Module.rank K V₂ < ℵ₀
⊢ finrank K V ≤ finrank K V₂
[PROOFSTEP]
simpa only [toNat_lift] using toNat_le_of_le_of_lt_aleph0 (lift_lt_aleph0.mpr h') h
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : Nontrivial K
inst✝ : NoZeroSMulDivisors K V
n : ℕ
hn : finrank K V = Nat.succ n
⊢ 0 < finrank (?m.108424 hn) V
[PROOFSTEP]
rw [hn]
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : Nontrivial K
inst✝ : NoZeroSMulDivisors K V
n : ℕ
hn : finrank K V = Nat.succ n
⊢ 0 < Nat.succ n
[PROOFSTEP]
exact n.succ_pos
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : Nontrivial K
inst✝ : NoZeroSMulDivisors K V
h : Subsingleton V
⊢ finrank K V = 0
[PROOFSTEP]
by_contra h0
[GOAL]
K : Type u
V : Type v
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : Nontrivial K
inst✝ : NoZeroSMulDivisors K V
h : Subsingleton V
h0 : ¬finrank K V = 0
⊢ False
[PROOFSTEP]
obtain ⟨x, y, hxy⟩ := nontrivial_of_finrank_pos (Nat.pos_of_ne_zero h0)
[GOAL]
case mk.intro.intro
K : Type u
V : Type v
inst✝⁶ : Ring K
inst✝⁵ : AddCommGroup V
inst✝⁴ : Module K V
V₂ : Type v'
inst✝³ : AddCommGroup V₂
inst✝² : Module K V₂
inst✝¹ : Nontrivial K
inst✝ : NoZeroSMulDivisors K V
h : Subsingleton V
h0 : ¬finrank K V = 0
x y : V
hxy : x ≠ y
⊢ False
[PROOFSTEP]
exact hxy (Subsingleton.elim _ _)
[GOAL]
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : StrongRankCondition K
ι : Type w
b : Finset ι
h : Basis { x // x ∈ b } K V
⊢ finrank K V = Finset.card b
[PROOFSTEP]
rw [finrank_eq_card_basis h, Fintype.card_coe]
[GOAL]
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : StrongRankCondition K
⊢ Module.rank K K = ↑1
[PROOFSTEP]
simp
[GOAL]
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : AddCommGroup V
inst✝³ : Module K V
V₂ : Type v'
inst✝² : AddCommGroup V₂
inst✝¹ : Module K V₂
inst✝ : StrongRankCondition K
n : ℕ
⊢ finrank K (Fin n → K) = n
[PROOFSTEP]
simp
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : ∀ (s : Set V), Basis (↑s) K V → ¬Set.Finite s
⊢ finrank K V = 0
[PROOFSTEP]
obtain ⟨_, ⟨b⟩⟩ := (Module.free_iff_set K V).mp ‹_›
[GOAL]
case intro.intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : ∀ (s : Set V), Basis (↑s) K V → ¬Set.Finite s
w✝ : Set V
b : Basis (↑w✝) K V
⊢ finrank K V = 0
[PROOFSTEP]
exact dif_neg fun rank_lt => h _ b (b.finite_index_of_rank_lt_aleph0 rank_lt)
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : ∀ (s : Finset V), Basis (↑↑s) K V → False
s : Set V
b : Basis (↑s) K V
hs : Set.Finite s
⊢ Basis (↑↑(Set.Finite.toFinset hs)) K V
[PROOFSTEP]
convert b
[GOAL]
case h.e'_1.h.e'_2
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : StrongRankCondition K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : Free K V
h : ∀ (s : Finset V), Basis (↑↑s) K V → False
s : Set V
b : Basis (↑s) K V
hs : Set.Finite s
⊢ ↑(Set.Finite.toFinset hs) = s
[PROOFSTEP]
simp
[GOAL]
K : Type u
V : Type v
inst✝⁹ : Ring K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
V₂ : Type v'
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module K V₂
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M ≃ₗ[R] M₂
⊢ finrank R M = finrank R M₂
[PROOFSTEP]
unfold finrank
[GOAL]
K : Type u
V : Type v
inst✝⁹ : Ring K
inst✝⁸ : AddCommGroup V
inst✝⁷ : Module K V
V₂ : Type v'
inst✝⁶ : AddCommGroup V₂
inst✝⁵ : Module K V₂
R : Type u_1
M : Type u_2
M₂ : Type u_3
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₂
inst✝¹ : Module R M
inst✝ : Module R M₂
f : M ≃ₗ[R] M₂
⊢ ↑toNat (Module.rank R M) = ↑toNat (Module.rank R M₂)
[PROOFSTEP]
rw [← Cardinal.toNat_lift, f.lift_rank_eq, Cardinal.toNat_lift]
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V →ₗ[K] V₂
hf : Injective ↑f
⊢ finrank K { x // x ∈ range f } = finrank K V
[PROOFSTEP]
rw [(LinearEquiv.ofInjective f hf).finrank_eq]
[GOAL]
K : Type u
V : Type v
inst✝² : Ring K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ finrank K { x // x ∈ ⊤ } = finrank K V
[PROOFSTEP]
unfold finrank
[GOAL]
K : Type u
V : Type v
inst✝² : Ring K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
⊢ ↑toNat (Module.rank K { x // x ∈ ⊤ }) = ↑toNat (Module.rank K V)
[PROOFSTEP]
simp [rank_top]
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
s t : Submodule K V
le : s ≤ t
lt : finrank K { x // x ∈ s } < finrank K { x // x ∈ t }
h : s = t
⊢ finrank K { x // x ∈ s } = finrank K { x // x ∈ t }
[PROOFSTEP]
rw [h]
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
s : Submodule K V
lt : finrank K { x // x ∈ s } < finrank K V
⊢ s < ⊤
[PROOFSTEP]
rw [← finrank_top K V] at lt 
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
V₂ : Type v'
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
s : Submodule K V
lt : finrank K { x // x ∈ s } < finrank K { x // x ∈ ⊤ }
⊢ s < ⊤
[PROOFSTEP]
exact lt_of_le_of_finrank_lt_finrank le_top lt
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Set V
inst✝ : Fintype ↑s
⊢ Module.rank K { x // x ∈ span K s } ≤ ↑(Finset.card (Set.toFinset s))
[PROOFSTEP]
simpa using rank_span_le (K := K) s
[GOAL]
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
⊢ Finset.card (Set.toFinset ↑s) = Finset.card s
[PROOFSTEP]
simp
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ Set.finrank K (Set.range b) ≤ Fintype.card ι
[PROOFSTEP]
classical
refine (finrank_span_le_card _).trans ?_
rw [Set.toFinset_range]
exact Finset.card_image_le
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ Set.finrank K (Set.range b) ≤ Fintype.card ι
[PROOFSTEP]
refine (finrank_span_le_card _).trans ?_
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ Finset.card (Set.toFinset (Set.range b)) ≤ Fintype.card ι
[PROOFSTEP]
rw [Set.toFinset_range]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ Finset.card (Finset.image b Finset.univ) ≤ Fintype.card ι
[PROOFSTEP]
exact Finset.card_image_le
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hb : LinearIndependent K b
⊢ Module.rank K { x // x ∈ span K (Set.range b) } = ↑(Fintype.card ι)
[PROOFSTEP]
have : Module.rank K (span K (Set.range b)) = #(Set.range b) := rank_span hb
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hb : LinearIndependent K b
this : Module.rank K { x // x ∈ span K (Set.range b) } = #↑(Set.range b)
⊢ Module.rank K { x // x ∈ span K (Set.range b) } = ↑(Fintype.card ι)
[PROOFSTEP]
rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast, lift_eq_nat_iff] at this 
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Set V
inst✝ : Fintype ↑s
hs : LinearIndependent K Subtype.val
⊢ Module.rank K { x // x ∈ span K s } = ↑(Finset.card (Set.toFinset s))
[PROOFSTEP]
have : Module.rank K (span K s) = #s := rank_span_set hs
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
s : Set V
inst✝ : Fintype ↑s
hs : LinearIndependent K Subtype.val
this : Module.rank K { x // x ∈ span K s } = #↑s
⊢ Module.rank K { x // x ∈ span K s } = ↑(Finset.card (Set.toFinset s))
[PROOFSTEP]
rwa [Cardinal.mk_fintype, ← Set.toFinset_card] at this 
[GOAL]
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : LinearIndependent K Subtype.val
⊢ finrank K { x // x ∈ span K ↑s } = Finset.card s
[PROOFSTEP]
convert finrank_span_set_eq_card (s : Set V) hs
[GOAL]
case h.e'_3.h.e'_2
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : LinearIndependent K Subtype.val
⊢ s = Set.toFinset ↑s
[PROOFSTEP]
ext
[GOAL]
case h.e'_3.h.e'_2.a
K : Type u
V : Type v
inst✝² : DivisionRing K
inst✝¹ : AddCommGroup V
inst✝ : Module K V
s : Finset V
hs : LinearIndependent K Subtype.val
a✝ : V
⊢ a✝ ∈ s ↔ a✝ ∈ Set.toFinset ↑s
[PROOFSTEP]
simp
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
⊢ g i = 0
[PROOFSTEP]
classical
by_contra gx_ne_zero
refine'
  not_le_of_gt (span_lt_top_of_card_lt_finrank (show (b '' (Set.univ \ { i })).toFinset.card < finrank K V from _)) _
·
  calc
    (b '' (Set.univ \ { i })).toFinset.card = ((Set.univ \ { i }).toFinset.image b).card := by
      rw [Set.toFinset_card, Fintype.card_ofFinset]
    _ ≤ (Set.univ \ { i }).toFinset.card := Finset.card_image_le
    _ = (Finset.univ.erase i).card := (congr_arg Finset.card (Finset.ext (by simp [and_comm])))
    _ < Finset.univ.card := (Finset.card_erase_lt_of_mem (Finset.mem_univ i))
    _ = finrank K V := card_eq
refine' spans.trans (span_le.mpr _)
rintro _
  ⟨j, rfl, rfl⟩
      -- The case that `j ≠ i` is easy because `b j ∈ b '' (univ \ {i})`.
by_cases j_eq : j = i
swap
· refine' subset_span ⟨j, (Set.mem_diff _).mpr ⟨Set.mem_univ _, _⟩, rfl⟩
  exact mt Set.mem_singleton_iff.mp j_eq
rw [j_eq, SetLike.mem_coe, show b i = -((g i)⁻¹ • (s.erase i).sum fun j => g j • b j) from _]
· refine' neg_mem (smul_mem _ _ (sum_mem fun k hk => _))
  obtain ⟨k_ne_i, _⟩ := Finset.mem_erase.mp hk
  refine' smul_mem _ _ (subset_span ⟨k, _, rfl⟩)
  simp_all only [Set.mem_univ, Set.mem_diff, Set.mem_singleton_iff]
    -- To show `b i` is a weighted sum of the other `b j`s, we'll rewrite this sum
        -- to have the form of the assumption `dependent`.
apply eq_neg_of_add_eq_zero_left
calc
  (b i + (g i)⁻¹ • (s.erase i).sum fun j => g j • b j) = (g i)⁻¹ • (g i • b i + (s.erase i).sum fun j => g j • b j) :=
    by rw [smul_add, ← mul_smul, inv_mul_cancel gx_ne_zero, one_smul]
  _ = (g i)⁻¹ • (0 : V) := (congr_arg _ ?_)
  _ = 0 :=
    smul_zero
      _
        -- And then it's just a bit of manipulation with finite sums.
rwa [← Finset.insert_erase i_mem_s, Finset.sum_insert (Finset.not_mem_erase _ _)] at dependent 
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
⊢ g i = 0
[PROOFSTEP]
by_contra gx_ne_zero
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ False
[PROOFSTEP]
refine'
  not_le_of_gt (span_lt_top_of_card_lt_finrank (show (b '' (Set.univ \ { i })).toFinset.card < finrank K V from _)) _
[GOAL]
case refine'_1
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ Finset.card (Set.toFinset (b '' (Set.univ \ {i}))) < finrank K V
[PROOFSTEP]
calc
  (b '' (Set.univ \ { i })).toFinset.card = ((Set.univ \ { i }).toFinset.image b).card := by
    rw [Set.toFinset_card, Fintype.card_ofFinset]
  _ ≤ (Set.univ \ { i }).toFinset.card := Finset.card_image_le
  _ = (Finset.univ.erase i).card := (congr_arg Finset.card (Finset.ext (by simp [and_comm])))
  _ < Finset.univ.card := (Finset.card_erase_lt_of_mem (Finset.mem_univ i))
  _ = finrank K V := card_eq
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ Finset.card (Set.toFinset (b '' (Set.univ \ {i}))) = Finset.card (Finset.image b (Set.toFinset (Set.univ \ {i})))
[PROOFSTEP]
rw [Set.toFinset_card, Fintype.card_ofFinset]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ ∀ (a : ι), a ∈ Set.toFinset (Set.univ \ {i}) ↔ a ∈ Finset.erase Finset.univ i
[PROOFSTEP]
simp [and_comm]
[GOAL]
case refine'_2
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ ⊤ ≤ span K (b '' (Set.univ \ {i}))
[PROOFSTEP]
refine' spans.trans (span_le.mpr _)
[GOAL]
case refine'_2
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
⊢ Set.range b ⊆ ↑(span K (b '' (Set.univ \ {i})))
[PROOFSTEP]
rintro _
  ⟨j, rfl, rfl⟩
      -- The case that `j ≠ i` is easy because `b j ∈ b '' (univ \ {i})`.
[GOAL]
case refine'_2.intro.refl
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
⊢ b j ∈ ↑(span K (b '' (Set.univ \ {i})))
[PROOFSTEP]
by_cases j_eq : j = i
[GOAL]
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ b j ∈ ↑(span K (b '' (Set.univ \ {i})))
case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : ¬j = i
⊢ b j ∈ ↑(span K (b '' (Set.univ \ {i})))
[PROOFSTEP]
swap
[GOAL]
case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : ¬j = i
⊢ b j ∈ ↑(span K (b '' (Set.univ \ {i})))
[PROOFSTEP]
refine' subset_span ⟨j, (Set.mem_diff _).mpr ⟨Set.mem_univ _, _⟩, rfl⟩
[GOAL]
case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : ¬j = i
⊢ ¬j ∈ {i}
[PROOFSTEP]
exact mt Set.mem_singleton_iff.mp j_eq
[GOAL]
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ b j ∈ ↑(span K (b '' (Set.univ \ {i})))
[PROOFSTEP]
rw [j_eq, SetLike.mem_coe, show b i = -((g i)⁻¹ • (s.erase i).sum fun j => g j • b j) from _]
[GOAL]
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ -((g i)⁻¹ • Finset.sum (Finset.erase s i) fun j => g j • b j) ∈ span K (b '' (Set.univ \ {i}))
[PROOFSTEP]
refine' neg_mem (smul_mem _ _ (sum_mem fun k hk => _))
[GOAL]
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
k : ι
hk : k ∈ Finset.erase s i
⊢ g k • b k ∈ span K (b '' (Set.univ \ {i}))
[PROOFSTEP]
obtain ⟨k_ne_i, _⟩ := Finset.mem_erase.mp hk
[GOAL]
case pos.intro
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
k : ι
hk : k ∈ Finset.erase s i
k_ne_i : k ≠ i
right✝ : k ∈ s
⊢ g k • b k ∈ span K (b '' (Set.univ \ {i}))
[PROOFSTEP]
refine' smul_mem _ _ (subset_span ⟨k, _, rfl⟩)
[GOAL]
case pos.intro
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
k : ι
hk : k ∈ Finset.erase s i
k_ne_i : k ≠ i
right✝ : k ∈ s
⊢ k ∈ Set.univ \ {i}
[PROOFSTEP]
simp_all only [Set.mem_univ, Set.mem_diff, Set.mem_singleton_iff]
  -- To show `b i` is a weighted sum of the other `b j`s, we'll rewrite this sum
      -- to have the form of the assumption `dependent`.
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ b i = -((g i)⁻¹ • Finset.sum (Finset.erase s i) fun j => g j • b j)
[PROOFSTEP]
apply eq_neg_of_add_eq_zero_left
[GOAL]
case h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ (b i + (g i)⁻¹ • Finset.sum (Finset.erase s i) fun j => g j • b j) = 0
[PROOFSTEP]
calc
  (b i + (g i)⁻¹ • (s.erase i).sum fun j => g j • b j) = (g i)⁻¹ • (g i • b i + (s.erase i).sum fun j => g j • b j) :=
    by rw [smul_add, ← mul_smul, inv_mul_cancel gx_ne_zero, one_smul]
  _ = (g i)⁻¹ • (0 : V) := (congr_arg _ ?_)
  _ = 0 :=
    smul_zero
      _
        -- And then it's just a bit of manipulation with finite sums.
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ (b i + (g i)⁻¹ • Finset.sum (Finset.erase s i) fun j => g j • b j) =
    (g i)⁻¹ • (g i • b i + Finset.sum (Finset.erase s i) fun j => g j • b j)
[PROOFSTEP]
rw [smul_add, ← mul_smul, inv_mul_cancel gx_ne_zero, one_smul]
[GOAL]
case h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
spans : ⊤ ≤ span K (Set.range b)
card_eq : Fintype.card ι = finrank K V
s : Finset ι
g : ι → K
dependent : (Finset.sum s fun i => g i • b i) = 0
i : ι
i_mem_s : i ∈ s
gx_ne_zero : ¬g i = 0
j : ι
j_eq : j = i
⊢ (g i • b i + Finset.sum (Finset.erase s i) fun j => g j • b j) = 0
[PROOFSTEP]
rwa [← Finset.insert_erase i_mem_s, Finset.sum_insert (Finset.not_mem_erase _ _)] at dependent 
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ LinearIndependent K b ↔ Fintype.card ι = Set.finrank K (Set.range b)
[PROOFSTEP]
constructor
[GOAL]
case mp
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ LinearIndependent K b → Fintype.card ι = Set.finrank K (Set.range b)
[PROOFSTEP]
intro h
[GOAL]
case mp
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
h : LinearIndependent K b
⊢ Fintype.card ι = Set.finrank K (Set.range b)
[PROOFSTEP]
exact (finrank_span_eq_card h).symm
[GOAL]
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ Fintype.card ι = Set.finrank K (Set.range b) → LinearIndependent K b
[PROOFSTEP]
intro hc
[GOAL]
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
⊢ LinearIndependent K b
[PROOFSTEP]
let f := Submodule.subtype (span K (Set.range b))
[GOAL]
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
⊢ LinearIndependent K b
[PROOFSTEP]
let b' : ι → span K (Set.range b) := fun i => ⟨b i, mem_span.2 fun p hp => hp (Set.mem_range_self _)⟩
[GOAL]
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
⊢ LinearIndependent K b
[PROOFSTEP]
have hs : ⊤ ≤ span K (Set.range b') := by
  intro x
  have h : span K (f '' Set.range b') = map f (span K (Set.range b')) := span_image f
  have hf : f '' Set.range b' = Set.range b := by
    ext x
    simp [Set.mem_image, Set.mem_range]
  rw [hf] at h 
  have hx : (x : V) ∈ span K (Set.range b) := x.property
  conv at hx =>
    arg 2
    rw [h]
  simpa [mem_map] using hx
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
⊢ ⊤ ≤ span K (Set.range b')
[PROOFSTEP]
intro x
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
[PROOFSTEP]
have h : span K (f '' Set.range b') = map f (span K (Set.range b')) := span_image f
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (↑f '' Set.range b') = Submodule.map f (span K (Set.range b'))
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
[PROOFSTEP]
have hf : f '' Set.range b' = Set.range b := by
  ext x
  simp [Set.mem_image, Set.mem_range]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (↑f '' Set.range b') = Submodule.map f (span K (Set.range b'))
⊢ ↑f '' Set.range b' = Set.range b
[PROOFSTEP]
ext x
[GOAL]
case h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x✝ : { x // x ∈ span K (Set.range b) }
h : span K (↑f '' Set.range b') = Submodule.map f (span K (Set.range b'))
x : V
⊢ x ∈ ↑f '' Set.range b' ↔ x ∈ Set.range b
[PROOFSTEP]
simp [Set.mem_image, Set.mem_range]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (↑f '' Set.range b') = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
[PROOFSTEP]
rw [hf] at h 
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
[PROOFSTEP]
have hx : (x : V) ∈ span K (Set.range b) := x.property
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
hx : ↑x ∈ span K (Set.range b)
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
[PROOFSTEP]
conv at hx =>
  arg 2
  rw [h]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
hx : ↑x ∈ span K (Set.range b)
| ↑x ∈ span K (Set.range b)
[PROOFSTEP]
  arg 2
  rw [h]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
hx : ↑x ∈ span K (Set.range b)
| ↑x ∈ span K (Set.range b)
[PROOFSTEP]
  arg 2
  rw [h]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
hx : ↑x ∈ span K (Set.range b)
| ↑x ∈ span K (Set.range b)
[PROOFSTEP]
arg 2
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
hx : ↑x ∈ span K (Set.range b)
| span K (Set.range b)
[PROOFSTEP]
rw [h]
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
x : { x // x ∈ span K (Set.range b) }
h : span K (Set.range b) = Submodule.map f (span K (Set.range b'))
hf : ↑f '' Set.range b' = Set.range b
hx : ↑x ∈ Submodule.map f (span K (Set.range b'))
⊢ x ∈ ⊤ → x ∈ span K (Set.range b')
[PROOFSTEP]
simpa [mem_map] using hx
[GOAL]
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
hs : ⊤ ≤ span K (Set.range b')
⊢ LinearIndependent K b
[PROOFSTEP]
have hi : LinearMap.ker f = ⊥ := ker_subtype _
[GOAL]
case mpr
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
hc : Fintype.card ι = Set.finrank K (Set.range b)
f : { x // x ∈ span K (Set.range b) } →ₗ[K] V := Submodule.subtype (span K (Set.range b))
b' : ι → { x // x ∈ span K (Set.range b) } := fun i => { val := b i, property := (_ : b i ∈ span K (Set.range b)) }
hs : ⊤ ≤ span K (Set.range b')
hi : LinearMap.ker f = ⊥
⊢ LinearIndependent K b
[PROOFSTEP]
convert (linearIndependent_of_top_le_span_of_card_eq_finrank hs hc).map' _ hi
[GOAL]
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Fintype ι
b : ι → V
⊢ LinearIndependent K b ↔ Fintype.card ι ≤ Set.finrank K (Set.range b)
[PROOFSTEP]
rw [linearIndependent_iff_card_eq_finrank_span, finrank_range_le_card.le_iff_eq]
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
n : v ≠ 0
h : ∀ (w : V), ∃ c, c • v = w
⊢ finrank K V = 1
[PROOFSTEP]
haveI := nontrivial_of_invariantBasisNumber K
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
n : v ≠ 0
h : ∀ (w : V), ∃ c, c • v = w
this : Nontrivial K
⊢ finrank K V = 1
[PROOFSTEP]
obtain ⟨b⟩ := (Basis.basis_singleton_iff.{u} PUnit).mpr ⟨v, n, h⟩
[GOAL]
case intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
n : v ≠ 0
h : ∀ (w : V), ∃ c, c • v = w
this : Nontrivial K
b : Basis PUnit K V
⊢ finrank K V = 1
[PROOFSTEP]
rw [finrank_eq_card_basis b, Fintype.card_punit]
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
h : ∀ (w : V), ∃ c, c • v = w
⊢ finrank K V ≤ 1
[PROOFSTEP]
haveI := nontrivial_of_invariantBasisNumber K
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
h : ∀ (w : V), ∃ c, c • v = w
this : Nontrivial K
⊢ finrank K V ≤ 1
[PROOFSTEP]
rcases eq_or_ne v 0 with (rfl | hn)
[GOAL]
case inl
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
⊢ finrank K V ≤ 1
[PROOFSTEP]
haveI :=
  subsingleton_of_forall_eq (0 : V) fun w => by
    obtain ⟨c, rfl⟩ := h w
    simp
[GOAL]
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
w : V
⊢ w = 0
[PROOFSTEP]
obtain ⟨c, rfl⟩ := h w
[GOAL]
case intro
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
c : K
⊢ c • 0 = 0
[PROOFSTEP]
simp
[GOAL]
case inl
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this✝ : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
this : Subsingleton V
⊢ finrank K V ≤ 1
[PROOFSTEP]
rw [finrank_zero_of_subsingleton]
[GOAL]
case inl
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
this✝ : Nontrivial K
h : ∀ (w : V), ∃ c, c • 0 = w
this : Subsingleton V
⊢ 0 ≤ 1
[PROOFSTEP]
exact zero_le_one
[GOAL]
case inr
K : Type u
V : Type v
inst✝⁴ : Ring K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : NoZeroSMulDivisors K V
inst✝ : StrongRankCondition K
v : V
h : ∀ (w : V), ∃ c, c • v = w
this : Nontrivial K
hn : v ≠ 0
⊢ finrank K V ≤ 1
[PROOFSTEP]
exact (finrank_eq_one v hn h).le
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : CommRing F
inst✝¹ : Ring E
inst✝ : Algebra F E
⊢ Module.rank F { x // x ∈ ⊤ } = Module.rank F { x // x ∈ ⊤ }
[PROOFSTEP]
rw [← Algebra.top_toSubmodule]
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : CommRing F
inst✝¹ : Ring E
inst✝ : Algebra F E
⊢ Module.rank F { x // x ∈ ⊤ } = Module.rank F { x // x ∈ ↑Subalgebra.toSubmodule ⊤ }
[PROOFSTEP]
rfl
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : CommRing F
inst✝¹ : Ring E
inst✝ : Algebra F E
⊢ finrank F { x // x ∈ ⊤ } = finrank F { x // x ∈ ⊤ }
[PROOFSTEP]
rw [← Algebra.top_toSubmodule]
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : CommRing F
inst✝¹ : Ring E
inst✝ : Algebra F E
⊢ finrank F { x // x ∈ ⊤ } = finrank F { x // x ∈ ↑Subalgebra.toSubmodule ⊤ }
[PROOFSTEP]
rfl
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : CommRing F
inst✝¹ : Ring E
inst✝ : Algebra F E
⊢ Module.rank F { x // x ∈ ⊤ } = Module.rank F E
[PROOFSTEP]
rw [subalgebra_top_rank_eq_submodule_top_rank]
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝² : CommRing F
inst✝¹ : Ring E
inst✝ : Algebra F E
⊢ Module.rank F { x // x ∈ ⊤ } = Module.rank F E
[PROOFSTEP]
exact _root_.rank_top F E
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
⊢ Module.rank F { x // x ∈ span F {1} } = 1
[PROOFSTEP]
letI := Module.nontrivial F E
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
this : Nontrivial F := Module.nontrivial F E
⊢ Module.rank F { x // x ∈ span F {1} } = 1
[PROOFSTEP]
rw [rank_span_set]
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
this : Nontrivial F := Module.nontrivial F E
⊢ #↑{1} = 1
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
this : Nontrivial F := Module.nontrivial F E
⊢ LinearIndependent F fun x => ↑x
[PROOFSTEP]
exacts [mk_singleton _, linearIndependent_singleton one_ne_zero]
[GOAL]
K : Type u
V : Type v
F : Type u_1
E : Type u_2
inst✝⁵ : CommRing F
inst✝⁴ : Ring E
inst✝³ : Algebra F E
inst✝² : StrongRankCondition F
inst✝¹ : NoZeroSMulDivisors F E
inst✝ : Nontrivial E
⊢ Module.rank F { x // x ∈ ⊥ } = ↑1
[PROOFSTEP]
simp
