-- Mathlib/LinearAlgebra/Dimension/FreeAndStrongRankCondition.lean
theorem lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank [Module.Free K V]
    [Module.Finite K V] : lift.{u} #V = lift.{v} #K ^ lift.{u} (Module.rank K V)

Proof state:
case intro.mk
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
this✝¹ : Nontrivial K
s : Type v
hs : Basis s K V
this✝ : Finite s
this : lift.{max u v, v} #V = lift.{v, max u v} #(s →₀ K)
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)

Tactic:
rwa [Finsupp.equivFunOnFinite.cardinal_eq, mk_arrow, hs.mk_eq_rank'', lift_power, lift_lift,
  lift_lift, lift_umax] at this

Result:
no goals

Proof state:
case intro.mk
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
this✝ : Nontrivial K
s : Type v
hs : Basis s K V
this : Finite s
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)

Tactic:
have := lift_mk_eq'.2 ⟨hs.repr.toEquiv⟩

Result:
case intro.mk
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
this✝¹ : Nontrivial K
s : Type v
hs : Basis s K V
this✝ : Finite s
this : lift.{max u v, v} #V = lift.{v, max u v} #(s →₀ K)
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)

Proof state:
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
this : Nontrivial K
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)

Tactic:
obtain ⟨s, hs⟩ := Module.Free.exists_basis (R := K) (M := V)

Result:
case intro.mk
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
this : Nontrivial K
s : Type v
hs : Basis s K V
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)

Proof state:
case intro.mk
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
this : Nontrivial K
s : Type v
hs : Basis s K V
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)

Tactic:
haveI : Finite s := by
  obtain ⟨t, ht⟩ := ‹Module.Finite K V›
  exact basis_finite_of_finite_spans _ t.finite_toSet ht hs

Result:
case intro.mk
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
this✝ : Nontrivial K
s : Type v
hs : Basis s K V
this : Finite s
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)

Proof state:
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
this : Nontrivial K
s : Type v
hs : Basis s K V
⊢ Finite s

Tactic:
obtain ⟨t, ht⟩ := ‹Module.Finite K V›

Result:
case mk.intro
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
this : Nontrivial K
s : Type v
hs : Basis s K V
t : Finset V
ht : span K ↑t = ⊤
⊢ Finite s

Proof state:
case mk.intro
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
this : Nontrivial K
s : Type v
hs : Basis s K V
t : Finset V
ht : span K ↑t = ⊤
⊢ Finite s

Tactic:
exact basis_finite_of_finite_spans _ t.finite_toSet ht hs

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)

Tactic:
haveI := nontrivial_of_invariantBasisNumber K

Result:
K : Type u
V : Type v
inst✝⁵ : Ring K
inst✝⁴ : StrongRankCondition K
inst✝³ : AddCommGroup V
inst✝² : Module K V
inst✝¹ : Free K V
inst✝ : Module.Finite K V
this : Nontrivial K
⊢ lift.{u, v} #V = lift.{v, u} #K ^ lift.{u, v} (Module.rank K V)