awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
inst_5 : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
⊢ Infinite M

Tactic:
have : Infinite M := infinite_iff.mpr <| lift_le.mp <| le_trans (by simp) h_lt.le
-- Module: Mathlib.LinearAlgebra.Dimension.Free
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
inst_5 : Infinite R
h_lt : lift.{v, u} #R < lift.{u, v} #M
this : Infinite M
⊢ lift.{max u v, v} #M = lift.{v, max u v} #(Finsupp.{v, u} (ChooseBasisIndex R M) R)

Tactic:
have h : lift #M = lift #(ChooseBasisIndex R M →₀ R) := lift_mk_eq'.mpr ⟨(chooseBasis R M).repr⟩