case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : FiniteDimensional K V
⊢ span K (Set.range b) = ⊤

case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : ¬FiniteDimensional K V
⊢ span K (Set.range b) = ⊤
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
⊢ span K (Set.range b) = ⊤
by_cases fin : FiniteDimensional K V
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : FiniteDimensional K V
⊢ span K (Set.range b) = ⊤
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : FiniteDimensional K V
⊢ span K (Set.range b) = ⊤
replace fin : FiniteDimensional _ _ := fin
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : FiniteDimensional K V
ne_top : ¬span K (Set.range b) = ⊤
⊢ False
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : FiniteDimensional K V
⊢ span K (Set.range b) = ⊤
by_contra ne_top
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : FiniteDimensional K V
ne_top : ¬span K (Set.range b) = ⊤
lt_top : span K (Set.range b) < ⊤
⊢ False
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : FiniteDimensional K V
ne_top : ¬span K (Set.range b) = ⊤
⊢ False
have lt_top : span K (Set.range b) < ⊤ := lt_of_le_of_ne le_top ne_top
no goals
case pos
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : FiniteDimensional K V
ne_top : ¬span K (Set.range b) = ⊤
lt_top : span K (Set.range b) < ⊤
⊢ False
exact ne_of_lt (Submodule.finrank_lt lt_top)
  (_root_.trans (finrank_span_eq_card lin_ind) card_eq)
case neg.h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : ¬FiniteDimensional K V
⊢ False
case neg
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : ¬FiniteDimensional K V
⊢ span K (Set.range b) = ⊤
exfalso
case neg.h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : ¬FiniteDimensional K V
⊢ 0 = Fintype.card ι
case neg.h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : ¬FiniteDimensional K V
⊢ False
apply ne_of_lt (Fintype.card_pos_iff.mpr hι)
case neg.h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : ¬FiniteDimensional K V
⊢ Fintype.card ι = 0
case neg.h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : ¬FiniteDimensional K V
⊢ 0 = Fintype.card ι
symm
case neg.h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : ¬IsNoetherian K V
⊢ Fintype.card ι = 0
case neg.h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : ¬FiniteDimensional K V
⊢ Fintype.card ι = 0
replace fin := (not_iff_not.2 IsNoetherian.iff_fg).2 fin
no goals
case neg.h
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
hι : Nonempty ι
inst✝ : Fintype ι
b : ι → V
lin_ind : LinearIndependent K b
card_eq : Fintype.card ι = finrank K V
fin : ¬IsNoetherian K V
⊢ Fintype.card ι = 0
calc
  Fintype.card ι = finrank K V := card_eq
  _ = 0 := dif_neg (mt IsNoetherian.iff_rank_lt_aleph0.mpr fin)