-- Mathlib/LinearAlgebra/Dimension/Free.lean
theorem nonempty_linearEquiv_of_lift_rank_eq
    (cnd : Cardinal.lift.{v'} (Module.rank R M) = Cardinal.lift.{v} (Module.rank R M')) :
    Nonempty (M ≃ₗ[R] M')

Proof state:
R : Type u
M : Type v
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Free R M'
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
β : Type v'
B' : Basis β R M'
⊢ lift.{v', v} #α = lift.{v, v'} #β

Tactic:
rw [B.mk_eq_rank'', cnd, B'.mk_eq_rank'']

Result:
no goals

Proof state:
R : Type u
M : Type v
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Free R M'
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
⊢ Nonempty (M ≃ₗ[R] M')

Tactic:
obtain ⟨⟨α, B⟩⟩ := Module.Free.exists_basis (R := R) (M := M)

Result:
case intro.mk
R : Type u
M : Type v
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Free R M'
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
⊢ Nonempty (M ≃ₗ[R] M')

Proof state:
case intro.mk.intro.mk
R : Type u
M : Type v
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Free R M'
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
β : Type v'
B' : Basis β R M'
this : lift.{v', v} #α = lift.{v, v'} #β
⊢ Nonempty (M ≃ₗ[R] M')

Tactic:
exact (Cardinal.lift_mk_eq.{v, v', 0}.1 this).map (B.equiv B')

Result:
no goals

Proof state:
case intro.mk
R : Type u
M : Type v
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Free R M'
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
⊢ Nonempty (M ≃ₗ[R] M')

Tactic:
obtain ⟨⟨β, B'⟩⟩ := Module.Free.exists_basis (R := R) (M := M')

Result:
case intro.mk.intro.mk
R : Type u
M : Type v
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Free R M'
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
β : Type v'
B' : Basis β R M'
⊢ Nonempty (M ≃ₗ[R] M')

Proof state:
case intro.mk.intro.mk
R : Type u
M : Type v
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Free R M'
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
β : Type v'
B' : Basis β R M'
⊢ Nonempty (M ≃ₗ[R] M')

Tactic:
have : Cardinal.lift.{v', v} #α = Cardinal.lift.{v, v'} #β := by
  rw [B.mk_eq_rank'', cnd, B'.mk_eq_rank'']

Result:
case intro.mk.intro.mk
R : Type u
M : Type v
M' : Type v'
inst✝⁷ : Semiring R
inst✝⁶ : StrongRankCondition R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
inst✝³ : Free R M
inst✝² : AddCommMonoid M'
inst✝¹ : Module R M'
inst✝ : Free R M'
cnd : lift.{v', v} (Module.rank R M) = lift.{v, v'} (Module.rank R M')
α : Type v
B : Basis α R M
β : Type v'
B' : Basis β R M'
this : lift.{v', v} #α = lift.{v, v'} #β
⊢ Nonempty (M ≃ₗ[R] M')