awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
η : Type u₁'
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : Fintype η
rw :
  (↑(Fintype.card η) : Cardinal.{max u₁' u}) * lift.{u₁', u} (Module.rank R R) =
    (↑(Fintype.card η) : Cardinal.{max u u₁'})
rw₁ : (↑(Fintype.card η) : Cardinal.{max u₁' u}) * lift.{u₁', u} 1 = (↑(Fintype.card η) : Cardinal.{max u u₁'})
rw₂ :
  HMul.hMul (α := Cardinal.{max u₁' u}) (↑(Fintype.card η) : Cardinal.{max u₁' u}) 1 =
    (↑(Fintype.card η) : Cardinal.{max u u₁'})
rw₃ rw₄ :
  Eq (α := Cardinal.{max u u₁'}) (↑(Fintype.card η) : Cardinal.{max u₁' u}) (↑(Fintype.card η) : Cardinal.{max u u₁'})
⊢ Module.rank R (η → R) = (↑(Fintype.card η) : Cardinal.{max u u₁'})

Tactic:
rw [rank_fun_eq_lift_mul, rank_self, Cardinal.lift_one, mul_one]

Premises used: Module.rank_self, Cardinal.lift_one, mul_one, rank_fun_eq_lift_mul
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
n : ℕ
⊢ Module.rank R (Fin n → R) = (↑n : Cardinal.{u})

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
η : Type u₁'
inst : Semiring R
inst_1 : StrongRankCondition R
inst_2 : Fintype η
⊢ finrank R (η → R) = Fintype.card η

Tactic:
finrank_eq_of_rank_eq rank_fun'

Premises used: Module.finrank_eq_of_rank_eq, rank_fun'
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
inst : Semiring R
inst_1 : StrongRankCondition R
n : ℕ
⊢ finrank R (Fin n → R) = n

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R M
inst_6 : StrongRankCondition R
inst_7 : Free R M
inst_8 : (i : η) → AddCommMonoid (φ i)
inst_9 : (i : η) → Module.{u, u_1} R (φ i)
inst_10 : ∀ (i : η), Free.{u, u_1} R (φ i)
inst_11 : Fintype η
n : ℕ
hn : Module.rank R M = (↑n : Cardinal.{v})
⊢ Nontrivial R

Tactic:
haveI := nontrivial_of_invariantBasisNumber R
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R M
inst_6 : StrongRankCondition R
inst_7 : Free R M
inst_8 : (i : η) → AddCommMonoid (φ i)
inst_9 : (i : η) → Module.{u, u_1} R (φ i)
inst_10 : ∀ (i : η), Free.{u, u_1} R (φ i)
inst_11 : Fintype η
n : ℕ
hn : Module.rank R M = (↑n : Cardinal.{v})
this : Nontrivial R
⊢ lift.{u, v} (↑n : Cardinal.{v}) = lift.{v, u} (↑n : Cardinal.{u})

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R M
inst_6 : StrongRankCondition R
inst_7 : Free R M
inst_8 : (i : η) → AddCommMonoid (φ i)
inst_9 : (i : η) → Module.{u, u_1} R (φ i)
inst_10 : ∀ (i : η), Free.{u, u_1} R (φ i)
inst_11 : Fintype η
n : ℕ
hn : Module.rank R M = (↑n : Cardinal.{v})
this : Nontrivial R
⊢ lift.{u, v} (↑n : Cardinal.{v}) = lift.{v, u} (↑n : Cardinal.{u})

Tactic:
have : Cardinal.lift.{u} (n : Cardinal.{v}) = Cardinal.lift.{v} (n : Cardinal.{u}) := by simp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R M
inst_6 : StrongRankCondition R
inst_7 : Free R M
inst_8 : (i : η) → AddCommMonoid (φ i)
inst_9 : (i : η) → Module.{u, u_1} R (φ i)
inst_10 : ∀ (i : η), Free.{u, u_1} R (φ i)
inst_11 : Fintype η
n : ℕ
hn : Module.rank R M = (↑n : Cardinal.{v})
this_1 : Nontrivial R
this : lift.{u, v} (↑n : Cardinal.{v}) = lift.{v, u} (↑n : Cardinal.{u})
⊢ lift.{u, v} (Module.rank R M) = lift.{u, v} (↑n : Cardinal.{v})

Tactic:
have hn := Cardinal.lift_inj.{v, u}.2 hn
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R M
inst_6 : StrongRankCondition R
inst_7 : Free R M
inst_8 : (i : η) → AddCommMonoid (φ i)
inst_9 : (i : η) → Module.{u, u_1} R (φ i)
inst_10 : ∀ (i : η), Free.{u, u_1} R (φ i)
inst_11 : Fintype η
n : ℕ
hn_1 : Module.rank R M = (↑n : Cardinal.{v})
this_1 : Nontrivial R
this : lift.{u, v} (↑n : Cardinal.{v}) = lift.{v, u} (↑n : Cardinal.{u})
hn : lift.{u, v} (Module.rank R M) = lift.{u, v} (↑n : Cardinal.{v})
⊢ lift.{u, v} (Module.rank R M) = lift.{v, u} (↑n : Cardinal.{u})

Tactic:
rw [this] at hn
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R M
inst_6 : StrongRankCondition R
inst_7 : Free R M
inst_8 : (i : η) → AddCommMonoid (φ i)
inst_9 : (i : η) → Module.{u, u_1} R (φ i)
inst_10 : ∀ (i : η), Free.{u, u_1} R (φ i)
inst_11 : Fintype η
n : ℕ
hn_1 : Module.rank R M = (↑n : Cardinal.{v})
this_1 : Nontrivial R
this : lift.{u, v} (↑n : Cardinal.{v}) = lift.{v, u} (↑n : Cardinal.{u})
hn : lift.{u, v} (Module.rank R M) = lift.{v, u} (↑n : Cardinal.{u})
⊢ lift.{u, v} (Module.rank R M) = lift.{v, u} (Module.rank R (Fin n → R))

Tactic:
rw [← @rank_fin_fun R _ _ n] at hn

Premises used: rank_fin_fun
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R M
inst_6 : StrongRankCondition R
inst_7 : Free R M
inst_8 : (i : η) → AddCommMonoid (φ i)
inst_9 : (i : η) → Module.{u, u_1} R (φ i)
inst_10 : ∀ (i : η), Free.{u, u_1} R (φ i)
inst_11 : Fintype η
n : ℕ
hn_1 : Module.rank R M = (↑n : Cardinal.{v})
this_1 : Nontrivial R
this : lift.{u, v} (↑n : Cardinal.{v}) = lift.{v, u} (↑n : Cardinal.{u})
hn : lift.{u, v} (Module.rank R M) = lift.{v, u} (Module.rank R (Fin n → R))
⊢ Free R (Fin n → R)

Tactic:
haveI : Module.Free R (Fin n → R) := Module.Free.pi _ _
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
M₁ : Type v
ι : Type w
ι' : Type w'
η : Type u₁'
φ : η → Type u_1
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : AddCommMonoid M₁
inst_5 : Module R M
inst_6 : StrongRankCondition R
inst_7 : Free R M
inst_8 : (i : η) → AddCommMonoid (φ i)
inst_9 : (i : η) → Module.{u, u_1} R (φ i)
inst_10 : ∀ (i : η), Free.{u, u_1} R (φ i)
inst_11 : Fintype η
n : ℕ
hn_1 : Module.rank R M = (↑n : Cardinal.{v})
this_1 : Nontrivial R
this_2 : lift.{u, v} (↑n : Cardinal.{v}) = lift.{v, u} (↑n : Cardinal.{u})
hn : lift.{u, v} (Module.rank R M) = lift.{v, u} (Module.rank R (Fin n → R))
this : Free R (Fin n → R)
⊢ M ≃ₗ[R] Fin n → R

Tactic:
exact Classical.choice (nonempty_linearEquiv_of_lift_rank_eq hn)

Premises used: Classical.choice, nonempty_linearEquiv_of_lift_rank_eq
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : StrongRankCondition R
inst_6 : StrongRankCondition S
inst_7 : Module S M
inst_8 : Module S M'
inst_9 : Free S M'
inst_10 : Algebra S R
inst_11 : IsScalarTower S R M
inst_12 : Free R M
obtain :
  ∀ (fst : Type v) (bM : Basis fst R M),
    Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')

Tactic:
obtain ⟨⟨_, bM⟩⟩ := Module.Free.exists_basis (R := R) (M := M)

Premises used: Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : StrongRankCondition R
inst_6 : StrongRankCondition S
inst_7 : Module S M
inst_8 : Module S M'
inst_9 : Free S M'
inst_10 : Algebra S R
inst_11 : IsScalarTower S R M
inst_12 : Free R M
fst : Type v
bM : Basis fst R M
obtain :
  ∀ (fst : Type v') (bN : Basis fst S M'),
    Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')

Tactic:
obtain ⟨⟨_, bN⟩⟩ := Module.Free.exists_basis (R := S) (M := M')

Premises used: Module.Free.exists_basis
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : StrongRankCondition R
inst_6 : StrongRankCondition S
inst_7 : Module S M
inst_8 : Module S M'
inst_9 : Free S M'
inst_10 : Algebra S R
inst_11 : IsScalarTower S R M
inst_12 : Free R M
fst : Type v
bM : Basis fst R M
fst_1 : Type v'
bN : Basis fst_1 S M'
rw : Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} #fst * Cardinal.lift.{v, v'} (Module.rank S M')
rw₁ : Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} #fst * Cardinal.lift.{v, v'} #fst_1
rw₂ : #(fst × fst_1) = Cardinal.lift.{v', v} #fst * Cardinal.lift.{v, v'} #fst_1
rw₃ rw₄ :
  Cardinal.lift.{v', v} #fst * Cardinal.lift.{v, v'} #fst_1 = Cardinal.lift.{v', v} #fst * Cardinal.lift.{v, v'} #fst_1
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')

Tactic:
rw [← bM.mk_eq_rank'', ← bN.mk_eq_rank'', ← (bM.tensorProduct bN).mk_eq_rank'', Cardinal.mk_prod]

Premises used: Module.Basis.tensorProduct, Module.Basis.mk_eq_rank'', Cardinal.mk_prod
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
S : Type u'
M M₁ : Type v
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M₁
inst_4 : Module R M
inst_5 : StrongRankCondition R
inst_6 : StrongRankCondition S
inst_7 : Module S M
inst_8 : Module S M₁
inst_9 : Free S M₁
inst_10 : Algebra S R
inst_11 : IsScalarTower S R M
inst_12 : Free R M
⊢ Module.rank R (M ⊗[S] M₁) = Module.rank R M * Module.rank S M₁

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
S : Type u'
M' : Type v'
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M'
inst_3 : StrongRankCondition R
inst_4 : StrongRankCondition S
inst_5 : Module S M'
inst_6 : Free S M'
inst_7 : Algebra S R
⊢ Module.rank R (R ⊗[S] M') = Cardinal.lift.{u, v'} (Module.rank S M')

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
S : Type u'
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M
inst_3 : AddCommMonoid M'
inst_4 : Module R M
inst_5 : StrongRankCondition R
inst_6 : StrongRankCondition S
inst_7 : Module S M
inst_8 : Module S M'
inst_9 : Free S M'
inst_10 : Algebra S R
inst_11 : IsScalarTower S R M
inst_12 : Free R M
⊢ finrank R (M ⊗[S] M') = finrank R M * finrank S M'

Tactic:
simp [finrank]

Premises used: Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
S : Type u'
M' : Type v'
inst : Semiring R
inst_1 : CommSemiring S
inst_2 : AddCommMonoid M'
inst_3 : StrongRankCondition R
inst_4 : StrongRankCondition S
inst_5 : Module S M'
inst_6 : Free S M'
inst_7 : Algebra S R
⊢ finrank R (R ⊗[S] M') = finrank S M'

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s t : Submodule R M
le : s ≤ t
lt : finrank.{u, v} R ↥s < finrank.{u, v} R ↥t
h : s = t
rw rw₁ : finrank.{u, v} R ↥t = finrank.{u, v} R ↥t
⊢ finrank.{u, v} R ↥s = finrank.{u, v} R ↥t

Tactic:
rw [h]
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Submodule R M
lt : finrank.{u, v} R ↥s < finrank R M
⊢ finrank.{u, v} R ↥s < finrank.{u, v} R ↥⊤

Tactic:
rw [← finrank_top R M] at lt

Premises used: finrank_top
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Submodule R M
lt : finrank.{u, v} R ↥s < finrank.{u, v} R ↥⊤
⊢ s < ⊤

Tactic:
lt_of_le_of_finrank_lt_finrank le_top lt

Premises used: Submodule.lt_of_le_of_finrank_lt_finrank, le_top
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Submodule R M
lt : finrank.{u, v} R ↥s < finrank.{u, v} R ↥⊤
⊢ s < ⊤

Tactic:
exact lt_of_le_of_finrank_lt_finrank le_top lt

Premises used: Submodule.lt_of_le_of_finrank_lt_finrank, le_top
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Module.Finite R M
s : Submodule R M
⊢ finrank.{u, v} R ↥s ≤ finrank R M

Tactic:
toNat_le_toNat (Submodule.rank_le s) (rank_lt_aleph0 _ _)

Premises used: Submodule.rank_le, Cardinal.toNat_le_toNat, Module.rank_lt_aleph0, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
M' : Type v'
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid M'
inst_3 : Module R M
inst_4 : StrongRankCondition R
inst_5 : Module R M'
f : M →ₗ[R] M'
p : Submodule R M
inst_6 : Module.Finite.{u, v} R ↥p
⊢ finrank.{u, v'} R ↥(map f p) ≤ finrank.{u, v} R ↥p

Tactic:
finrank_le_finrank_of_rank_le_rank (lift_rank_map_le _ _) (rank_lt_aleph0 _ _)

Premises used: lift_rank_map_le, Module.finrank_le_finrank_of_rank_le_rank, Module.rank_lt_aleph0
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s t : Submodule R M
inst_4 : Module.Finite.{u, v} R ↥t
hst : s ≤ t
⊢ finrank.{u, v} R ↥s ≤ finrank.{u, v} R ↥t

Tactic:
Cardinal.toNat_le_toNat (Submodule.rank_mono hst) (rank_lt_aleph0 R ↥t)

Premises used: Membership.mem, Subtype, Submodule.rank_mono, Cardinal.toNat_le_toNat, Module.rank_lt_aleph0, Module.finrank
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Set M
rw :
  lift.{max u v, v}
      (Module.rank R
        ↥(LinearMap.range (M := Finsupp.{v, u} { x : M // x ∈ s } R)
            (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))) ≤
    lift.{max u v, v} #(↑s : Type v)
⊢ Module.rank R ↥(span R s) ≤ #(↑s : Type v)

Tactic:
rw [Finsupp.span_eq_range_linearCombination, ← lift_strictMono.le_iff_le]

Premises used: Finsupp.span_eq_range_linearCombination, Cardinal.lift_strictMono, StrictMono.le_iff_le
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Set M
⊢ lift.{max u v, v}
      (Module.rank R
        ↥(LinearMap.range (M := Finsupp.{v, u} { x : M // x ∈ s } R)
            (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))) ≤
    lift.{max u v, v} #(↑s : Type v)

Tactic:
(lift_rank_range_le _).trans ?_

Premises used: LE.le.trans, lift_rank_range_le
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Set M
refine : lift.{v, max u v} (Module.rank R (Finsupp.{v, u} { x : M // x ∈ s } R)) ≤ lift.{max u v, v} #(↑s : Type v)
⊢ lift.{max u v, v}
      (Module.rank R
        ↥(LinearMap.range (M := Finsupp.{v, u} { x : M // x ∈ s } R)
            (Finsupp.linearCombination R (Subtype.val (p := fun (x : M) ↦ x ∈ s))))) ≤
    lift.{max u v, v} #(↑s : Type v)

Tactic:
refine (lift_rank_range_le _).trans ?_

Premises used: LE.le.trans, lift_rank_range_le
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Set M
rw : lift.{v, max u v} (lift.{u, v} #{ x : M // x ∈ s }) ≤ lift.{max u v, v} #(↑s : Type v)
⊢ lift.{v, max u v} (Module.rank R (Finsupp.{v, u} { x : M // x ∈ s } R)) ≤ lift.{max u v, v} #(↑s : Type v)

Tactic:
rw [rank_finsupp_self]

Premises used: rank_finsupp_self
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Set M
⊢ lift.{v, max u v} (lift.{u, v} #{ x : M // x ∈ s }) ≤ lift.{max u v, v} #(↑s : Type v)

Tactic:
simp only [lift_lift, le_refl]

Premises used: le_refl, Cardinal.lift_lift
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Finset M
⊢ Module.rank R ↥(span R (↑s : Set M)) ≤ (↑s.card : Cardinal.{v})

Tactic:
simpa using rank_span_le (s : Set M)

Premises used: rank_span_le, SetLike.coe
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Finset M
⊢ Module.rank R ↥(span R (↑s : Set M)) < ℵ₀

Tactic:
(rank_span_finset_le s).trans_lt natCast_lt_aleph0

Premises used: rank_span_finset_le, Cardinal.natCast_lt_aleph0, LE.le.trans_lt
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Set M
inst_4 : Fintype (↑s : Type v)
⊢ Module.rank R ↥(span R s) ≤ (↑s.toFinset.card : Cardinal.{v})

Tactic:
simpa using rank_span_le (R := R) s

Premises used: rank_span_le
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Finset M
⊢ (↑s : Set M).toFinset.card = s.card

Tactic:
simp
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
b : ι → M
⊢ Set.finrank R (range b) ≤ Fintype.card ι

Tactic:
(finrank_span_le_card _).trans ?_

Premises used: finrank_span_le_card, Set.finrank, LE.le.trans
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
b : ι → M
refine : (range b).toFinset.card ≤ Fintype.card ι
⊢ Set.finrank R (range b) ≤ Fintype.card ι

Tactic:
refine (finrank_span_le_card _).trans ?_

Premises used: finrank_span_le_card, LE.le.trans
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
b : ι → M
rw : (Finset.image b Finset.univ).card ≤ Fintype.card ι
⊢ (range b).toFinset.card ≤ Fintype.card ι

Tactic:
rw [Set.toFinset_range]

Premises used: Set.toFinset_range
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
b : ι → M
⊢ (Finset.image b Finset.univ).card ≤ Fintype.card ι

Tactic:
Finset.card_image_le

Premises used: Fintype.card, Finset.card_image_le
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
b : ι → M
⊢ (Finset.image b Finset.univ).card ≤ Fintype.card ι

Tactic:
exact Finset.card_image_le

Premises used: Finset.card_image_le
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : Type u_2
inst_4 : Fintype ι
b : ι → M
refine : (range b).toFinset.card ≤ Fintype.card ι
refine₁ : (Finset.image b Finset.univ).card ≤ Fintype.card ι
⊢ Set.finrank R (range b) ≤ Fintype.card ι

Tactic:
classical
  refine (finrank_span_le_card _).trans ?_
  rw [Set.toFinset_range]
  exact Finset.card_image_le

Premises used: Set.toFinset_range, finrank_span_le_card, Finset.card_image_le, LE.le.trans
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Nontrivial R
ι : Type u_2
inst_5 : Fintype ι
b : ι → M
hb : LinearIndependent R b
⊢ Module.rank R ↥(span R (range b)) = #(↑(range b) : Type v)

Tactic:
have : Module.rank R (span R (Set.range b)) = #(Set.range b) := rank_span hb
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Nontrivial R
ι : Type u_2
inst_5 : Fintype ι
b : ι → M
hb : LinearIndependent R b
this : Module.rank R ↥(span R (range b)) = #(↑(range b) : Type v)
rwa :
  ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = lift.{u_2, v} #(↑(range b) : Type v)),
    Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
rwa₁ :
  ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = lift.{v, u_2} #ι),
    Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
rwa₂ :
  ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = lift.{v, u_2} (↑(Fintype.card ι) : Cardinal.{u_2})),
    Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
rwa₃ :
  ∀ (this : lift.{u_2, v} (Module.rank R ↥(span R (range b))) = (↑(Fintype.card ι) : Cardinal.{max u_2 v})),
    Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
rwa₄ rwa₅ rwa₆ rwa₇ :
  ∀ (this : Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})),
    Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})
⊢ Module.rank R ↥(span R (range b)) = (↑(Fintype.card ι) : Cardinal.{v})

Tactic:
rwa [← lift_inj, mk_range_eq_of_injective hb.injective, Cardinal.mk_fintype, lift_natCast,
        lift_eq_nat_iff] at this

Premises used: Cardinal.mk_range_eq_of_injective, LinearIndependent.injective, Cardinal.mk_fintype, Cardinal.lift_inj, Cardinal.lift_natCast, Cardinal.lift_eq_nat_iff
-- Module: Mathlib.LinearAlgebra.Dimension.Constructions
Goal:
R : Type u
M : Type v
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
s : Set M
inst_4 : Fintype (↑s : Type v)
hs : LinearIndepOn R id s
⊢ Module.rank R ↥(span R s) = #(↑s : Type v)

Tactic:
have : Module.rank R (span R s) = #s := rank_span_set hs