no goals
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : _root_.Finite ι
b : Basis ι K V
⊢ lift (Module.rank K V) = Module.rank K (Dual K V)
classical
  cases nonempty_fintype ι
  have := LinearEquiv.lift_rank_eq b.toDualEquiv
  rw [Cardinal.lift_umax.{u₂,u₁}] at this
  rw [this, ← Cardinal.lift_umax]
  apply Cardinal.lift_id
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : _root_.Finite ι
b : Basis ι K V
val✝ : Fintype ι
⊢ lift (Module.rank K V) = Module.rank K (Dual K V)
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : _root_.Finite ι
b : Basis ι K V
⊢ lift (Module.rank K V) = Module.rank K (Dual K V)
cases nonempty_fintype ι
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : _root_.Finite ι
b : Basis ι K V
val✝ : Fintype ι
this : lift (Module.rank K V) = lift (Module.rank K (Dual K V))
⊢ lift (Module.rank K V) = Module.rank K (Dual K V)
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : _root_.Finite ι
b : Basis ι K V
val✝ : Fintype ι
⊢ lift (Module.rank K V) = Module.rank K (Dual K V)
have := LinearEquiv.lift_rank_eq b.toDualEquiv
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : _root_.Finite ι
b : Basis ι K V
val✝ : Fintype ι
this : lift (Module.rank K V) = lift (Module.rank K (Dual K V))
⊢ lift (Module.rank K V) = Module.rank K (Dual K V)
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : _root_.Finite ι
b : Basis ι K V
val✝ : Fintype ι
this : lift (Module.rank K V) = lift (Module.rank K (Dual K V))
⊢ lift (Module.rank K V) = Module.rank K (Dual K V)
rw [Cardinal.lift_umax.{u₂,u₁}] at this
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : _root_.Finite ι
b : Basis ι K V
val✝ : Fintype ι
this : lift (Module.rank K V) = lift (Module.rank K (Dual K V))
⊢ lift (Module.rank K (Dual K V)) = Module.rank K (Dual K V)
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : _root_.Finite ι
b : Basis ι K V
val✝ : Fintype ι
this : lift (Module.rank K V) = lift (Module.rank K (Dual K V))
⊢ lift (Module.rank K V) = Module.rank K (Dual K V)
rw [this, ← Cardinal.lift_umax]
no goals
case intro
R : Type u
M : Type v
K : Type u₁
V : Type u₂
ι : Type w
inst✝³ : CommRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
inst✝ : _root_.Finite ι
b : Basis ι K V
val✝ : Fintype ι
this : lift (Module.rank K V) = lift (Module.rank K (Dual K V))
⊢ lift (Module.rank K (Dual K V)) = Module.rank K (Dual K V)
apply Cardinal.lift_id