awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h : ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) < ℵ₀
⊢ span R (↑p : Set M) = p

Tactic:
simp
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h : ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) < ℵ₀
mp :
  ∀ (s : { s : Set M // span R s = p })
    (hs :
      Eq.{u + 2} (α := Cardinal.{u})
        ((fun (s : { s : Set M // span R s = p }) ↦ Cardinal.mk.{u} (↑(↑s : Set M) : Type u)) s)
        (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u))),
    ∃ (S : Set M), S.Finite ∧ span R S = p
⊢ ∃ (S : Set M), S.Finite ∧ span R S = p

Tactic:
obtain ⟨s, hs⟩ : ⨅ (s : {s : Set M // span R s = p}), #s ∈
      Set.range (fun (s : {s : Set M // span R s = p}) ↦ #s) := csInf_mem ⟨#p, ⟨⟨p, by simp⟩, rfl⟩⟩

Premises used: Cardinal.mk, Set.Elem, Set.range, Subtype.val, Set
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h : ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) < ℵ₀
s : { s : Set M // span R s = p }
hs :
  Eq.{u + 2} (α := Cardinal.{u})
    ((fun (s : { s : Set M // span R s = p }) ↦ Cardinal.mk.{u} (↑(↑s : Set M) : Type u)) s)
    (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u))
⊢ ∃ (S : Set M), S.Finite ∧ span R S = p

Tactic:
⟨s.1, ?_, s.2⟩

Premises used: And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h : ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) < ℵ₀
s : { s : Set M // span R s = p }
hs :
  Eq.{u + 2} (α := Cardinal.{u})
    ((fun (s : { s : Set M // span R s = p }) ↦ Cardinal.mk.{u} (↑(↑s : Set M) : Type u)) s)
    (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u))
mp : (↑s : Set M).Finite
⊢ ∃ (S : Set M), S.Finite ∧ span R S = p

Tactic:
refine ⟨s.1, ?_, s.2⟩
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
h : ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) < ℵ₀
s : { s : Set M // span R s = p }
hs :
  Eq.{u + 2} (α := Cardinal.{u})
    ((fun (s : { s : Set M // span R s = p }) ↦ Cardinal.mk.{u} (↑(↑s : Set M) : Type u)) s)
    (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u))
⊢ (↑s : Set M).Finite

Tactic:
simpa [← hs] using h
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
s : Set M
hs₁ : s.Finite
hs₂ : span R s = p
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ span R s = p) s hs₂) : Set M) : Type u) < ℵ₀

Tactic:
simpa
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
s : Set M
hs₁ : s.Finite
hs₂ : span R s = p
⊢ ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) < ℵ₀

Tactic:
exact (ciInf_le' _ ⟨s, hs₂⟩).trans_lt (by simpa)

Premises used: ciInf_le', LE.le.trans_lt
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
hp : ¬p.FG
⊢ p.spanFinrank = 0

Tactic:
toNat_eq_zero.2 ?_

Premises used: Iff.mpr, Submodule.spanFinrank, Cardinal.toNat_eq_zero
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
hp : ¬p.FG
refine : p.spanRank = 0 ∨ ℵ₀ ≤ p.spanRank
⊢ p.spanFinrank = 0

Tactic:
refine toNat_eq_zero.2 ?_

Premises used: Iff.mpr, Cardinal.toNat_eq_zero
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
hp : ¬p.FG
h : ℵ₀ ≤ p.spanRank
⊢ p.spanRank = 0 ∨ ℵ₀ ≤ p.spanRank

Tactic:
right
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
hp : ¬p.FG
h : ∀ (h : p.spanRank < ℵ₀), False
⊢ ℵ₀ ≤ p.spanRank

Tactic:
by_contra! h
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
hp : ¬p.FG
h : p.spanRank < ℵ₀
⊢ False

Tactic:
hp (spanRank_finite_iff_fg.1 h)

Premises used: Submodule.spanRank_finite_iff_fg, Iff.mp
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
hp : ¬p.FG
h : p.spanRank < ℵ₀
⊢ False

Tactic:
exact hp (spanRank_finite_iff_fg.1 h)

Premises used: Submodule.spanRank_finite_iff_fg, Iff.mp
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
rw : (↑((toNat : (a : Cardinal.{u}) → ℕ) p.spanRank) : Cardinal.{u}) = p.spanRank ↔ p.spanRank < ℵ₀
⊢ p.spanRank = (↑p.spanFinrank : Cardinal.{u}) ↔ p.FG

Tactic:
rw [spanFinrank, ← spanRank_finite_iff_fg, eq_comm]

Premises used: Submodule.spanRank_finite_iff_fg, eq_comm, Submodule.spanFinrank
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ (↑((toNat : (a : Cardinal.{u}) → ℕ) p.spanRank) : Cardinal.{u}) = p.spanRank ↔ p.spanRank < ℵ₀

Tactic:
cast_toNat_eq_iff_lt_aleph0

Premises used: Cardinal.cast_toNat_eq_iff_lt_aleph0
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
⊢ (↑((toNat : (a : Cardinal.{u}) → ℕ) p.spanRank) : Cardinal.{u}) = p.spanRank ↔ p.spanRank < ℵ₀

Tactic:
exact cast_toNat_eq_iff_lt_aleph0

Premises used: Cardinal.cast_toNat_eq_iff_lt_aleph0
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
fg : p.FG
⊢ p.spanRank = (↑p.spanFinrank : Cardinal.{u})

Tactic:
fg_iff_spanRank_eq_spanFinrank.mpr fg

Premises used: Submodule.fg_iff_spanRank_eq_spanFinrank, Iff.mpr
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
hp : p.FG
n : ℕ
⊢ p.spanRank < ℵ₀

Tactic:
simpa
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
s' : { s1 : Set M // Eq (α := Submodule R M) (span R s1) (span R s) } :=
  Subtype.mk (p := fun (s1 : Set M) ↦ Eq (α := Submodule R M) (span R s1) (span R s)) s ⋯
⊢ ⨅ (s_1 : { s_1 : Set M // Eq (α := Submodule R M) (span R s_1) (span R s) }), #(↑(↑s_1 : Set M) : Type u) ≤
    #(↑s : Type u)

Tactic:
ciInf_le' _ s'

Premises used: ciInf_le'
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
s' : { s1 : Set M // Eq (α := Submodule R M) (span R s1) (span R s) } :=
  Subtype.mk (p := fun (s1 : Set M) ↦ Eq (α := Submodule R M) (span R s1) (span R s)) s ⋯
⊢ ⨅ (s_1 : { s_1 : Set M // Eq (α := Submodule R M) (span R s_1) (span R s) }), #(↑(↑s_1 : Set M) : Type u) ≤
    #(↑s : Type u)

Tactic:
exact ciInf_le' _ s'

Premises used: ciInf_le'
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
⊢ spanRank (span R (Set.range v)) = #ι

Tactic:
le_antisymm (le_trans (spanRank_span_le_card _) mk_range_le) (le_ciInf fun x ↦ ?_)

Premises used: Submodule.spanRank_span_le_card, Cardinal.mk_range_le, le_ciInf, le_antisymm, le_trans
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
refine :
  ∀ (x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }), #ι ≤ #(↑(↑x : Set M) : Type u)
⊢ spanRank (span R (Set.range v)) = #ι

Tactic:
refine le_antisymm (le_trans (spanRank_span_le_card _) mk_range_le) (le_ciInf fun x ↦ ?_)

Premises used: Submodule.spanRank_span_le_card, Cardinal.mk_range_le, le_ciInf, le_antisymm, le_trans
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }
⊢ (↑x : Set M) ⊆
    Set.range (ι := ↥(span R (Set.range v)))
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x))

Tactic:
simp [← x.2]

Premises used: Subtype.property
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }
⊢ #(↑(↑x : Set M) : Type u) =
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)

Tactic:
have : #x.1 = #((Subtype.val : span R (.range v) → _) ⁻¹' x.1) :=
    (mk_preimage_of_injective_of_subset_range _ _ Subtype.val_injective (by simp [← x.2])).symm
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }
this :
  #(↑(↑x : Set M) : Type u) =
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)
rw :
  #ι ≤
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)
⊢ #ι ≤ #(↑(↑x : Set M) : Type u)

Tactic:
rw [this]
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }
this :
  #(↑(↑x : Set M) : Type u) =
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)
⊢ #ι ≤
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)

Tactic:
le_trans ?_ ((Module.Basis.span hs).le_span (R := R) (J := Subtype.val ⁻¹' x.1) ?_)

Premises used: Module.Basis.le_span, Module.Basis.span, le_trans
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }
this :
  #(↑(↑x : Set M) : Type u) =
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)
refine_1 : #ι ≤ #(↑(Set.range (ι := ι) (⇑(Module.Basis.span hs) : (a : ι) → ↥(span R (Set.range v)))) : Type u)
refine_2 :
  Eq (α := Submodule R ↥(span R (Set.range v)))
    (span R
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹' (↑x : Set M)))
    ⊤
⊢ #ι ≤
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)

Tactic:
refine le_trans ?_ ((Module.Basis.span hs).le_span (R := R) (J := Subtype.val ⁻¹' x.1) ?_)

Premises used: Module.Basis.le_span, Module.Basis.span, le_trans
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }
this :
  #(↑(↑x : Set M) : Type u) =
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)
refine_1 :
  Function.Injective.{u + 1, u + 1} (α := ι) (β := ↥(span R (Set.range v)))
    (⇑(Module.Basis.span hs) : (a : ι) → ↥(span R (Set.range v)))
⊢ #ι ≤ #(↑(Set.range (ι := ι) (⇑(Module.Basis.span hs) : (a : ι) → ↥(span R (Set.range v)))) : Type u)

Tactic:
rw [mk_range_eq]

Premises used: Cardinal.mk_range_eq
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }
this :
  #(↑(↑x : Set M) : Type u) =
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)
⊢ Function.Injective v

Tactic:
hv
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }
this :
  #(↑(↑x : Set M) : Type u) =
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)
h :
  Function.comp (β := ↥(span R (Set.range v)))
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x))
      (⇑(Module.Basis.span hs) : (a : ι) → ↥(span R (Set.range v))) =
    v
⊢ Function.Injective.{u + 1, u + 1} (α := ι) (β := M)
    (Function.comp (β := ↥(span R (Set.range v)))
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x))
      (⇑(Module.Basis.span hs) : (a : ι) → ↥(span R (Set.range v))))

Tactic:
convert! hv
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }
this :
  #(↑(↑x : Set M) : Type u) =
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)
h :
  ∀ (x : ι),
    Function.comp (β := ↥(span R (Set.range v)))
        (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x))
        (⇑(Module.Basis.span hs) : (a : ι) → ↥(span R (Set.range v))) x =
      v x
⊢ Function.comp (β := ↥(span R (Set.range v)))
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x))
      (⇑(Module.Basis.span hs) : (a : ι) → ↥(span R (Set.range v))) =
    v

Tactic:
ext
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }
this :
  #(↑(↑x : Set M) : Type u) =
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)
x_1 : ι
⊢ Function.comp (β := ↥(span R (Set.range v)))
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x))
      (⇑(Module.Basis.span hs) : (a : ι) → ↥(span R (Set.range v))) x_1 =
    v x_1

Tactic:
simp [Module.Basis.span_apply]

Premises used: Module.Basis.span_apply
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }
this :
  #(↑(↑x : Set M) : Type u) =
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)
⊢ Function.Injective.{u + 1, u + 1} (α := ι) (β := ↥(span R (Set.range v)))
    (⇑(Module.Basis.span hs) : (a : ι) → ↥(span R (Set.range v)))

Tactic:
exact .of_comp (f := Subtype.val) (by convert! hv; ext; simp [Module.Basis.span_apply])
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }
this :
  #(↑(↑x : Set M) : Type u) =
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)
refine_2 :
  Eq (α := Submodule R M)
    (map (M := ↥(span R (Set.range v))) (Submodule.subtype (span R (Set.range v)))
      (span R
        (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
          (↑x : Set M))))
    (map (M := ↥(span R (Set.range v))) (Submodule.subtype (span R (Set.range v))) ⊤)
⊢ Eq (α := Submodule R ↥(span R (Set.range v)))
    (span R
      (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹' (↑x : Set M)))
    ⊤

Tactic:
apply map_injective_of_injective (f := (span R _).subtype) (injective_subtype _)

Premises used: Submodule.injective_subtype, Submodule.map_injective_of_injective
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u
v : ι → M
hv : Function.Injective v
hs : LinearIndependent R v
x : { s : Set M // Eq (α := Submodule R M) (span R s) (span R (Set.range v)) }
this :
  #(↑(↑x : Set M) : Type u) =
    #(↑(Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
            (↑x : Set M)) :
        Type u)
⊢ Eq (α := Submodule R M)
    (map (M := ↥(span R (Set.range v))) (Submodule.subtype (span R (Set.range v)))
      (span R
        (Subtype.val (p := fun (x : M) ↦ Membership.mem (γ := Submodule R M) (span R (Set.range v)) x) ⁻¹'
          (↑x : Set M))))
    (map (M := ↥(span R (Set.range v))) (Submodule.subtype (span R (Set.range v))) ⊤)

Tactic:
simp [map_span, Set.image_preimage_eq_inter_range, Set.inter_eq_self_of_subset_left, ← x.2]

Premises used: Set.image_preimage_eq_inter_range, Submodule.map_span, Subtype.property, Set.inter_eq_self_of_subset_left
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
s : Set M
hs : LinearIndepOn R id s
⊢ spanRank (span R s) = #(↑s : Type u)

Tactic:
simp [← spanRank_span_range_of_linearIndependent Subtype.val_injective hs]

Premises used: Subtype.val_injective, Submodule.spanRank_span_range_of_linearIndependent
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
⊢ (↑((toNat : (a : Cardinal.{u}) → ℕ) (spanRank (span R s))) : ℕ∞) ≤
    (↑(↑toENat.toRingHom : Cardinal.{u} →* ℕ∞) : OneHom Cardinal.{u} ℕ∞).toFun (spanRank (span R s))

Tactic:
simp
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
⊢ LE.le (α := ℕ∞) ((↑((toNat : (a : Cardinal.{u}) → ℕ) (spanRank (span R s))) : ℕ∞) : ℕ∞)
    ((toENat : (a : Cardinal.{u}) → ℕ∞) #(↑s : Type u) : ℕ∞)

Tactic:
exact le_trans (by simp) (toENat.monotone' (spanRank_span_le_card (R := R) s))

Premises used: Submodule.spanRank_span_le_card, OrderRingHom.monotone', Cardinal.toENat, le_trans
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
hs : s.Finite
rw : LE.le (α := ℕ∞) (↑(spanFinrank (span R s)) : ℕ∞) (↑s.ncard : ℕ∞)
⊢ spanFinrank (span R s) ≤ s.ncard

Tactic:
rw [← Nat.cast_le (α := ℕ∞)]

Premises used: Nat.cast_le
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
hs : s.Finite
⊢ LE.le (α := ℕ∞) (↑(spanFinrank (span R s)) : ℕ∞) (↑s.ncard : ℕ∞)

Tactic:
le_trans (spanFinrank_span_le_encard _) hs.cast_ncard_eq.ge

Premises used: Eq.ge, Submodule.spanFinrank_span_le_encard, Set.Finite.cast_ncard_eq, le_trans
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
s : Set M
hs : s.Finite
⊢ LE.le (α := ℕ∞) (↑(spanFinrank (span R s)) : ℕ∞) (↑s.ncard : ℕ∞)

Tactic:
exact le_trans (spanFinrank_span_le_encard _) hs.cast_ncard_eq.ge

Premises used: Eq.ge, Submodule.spanFinrank_span_le_encard, Set.Finite.cast_ncard_eq, le_trans
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
obtain :
  ∀ (s : { s : Set M // span R s = p })
    (hs :
      Eq.{u + 2} (α := Cardinal.{u})
        ((fun (s : { s : Set M // span R s = p }) ↦ Cardinal.mk.{u} (↑(↑s : Set M) : Type u)) s)
        (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u))),
    ∃ (s : Set M), #(↑s : Type u) = ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) ∧ span R s = p
⊢ ∃ (s : Set M), #(↑s : Type u) = ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) ∧ span R s = p

Tactic:
obtain ⟨s, hs⟩ : ⨅ (s : {s : Set M // span R s = p}), #s ∈
    Set.range (fun (s : {s : Set M // span R s = p}) ↦ #s) := csInf_mem ⟨#p, ⟨⟨p, by simp⟩, rfl⟩⟩

Premises used: Cardinal.mk, Set.Elem, Set.range, Subtype.val, Set
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
s : { s : Set M // span R s = p }
hs :
  Eq.{u + 2} (α := Cardinal.{u})
    ((fun (s : { s : Set M // span R s = p }) ↦ Cardinal.mk.{u} (↑(↑s : Set M) : Type u)) s)
    (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u))
⊢ ∃ (s : Set M), #(↑s : Type u) = ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) ∧ span R s = p

Tactic:
⟨s.1, ⟨hs, s.2⟩⟩

Premises used: And.intro, Exists.intro, Subtype.val, Subtype.property
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
p : Submodule R M
s : { s : Set M // span R s = p }
hs :
  Eq.{u + 2} (α := Cardinal.{u})
    ((fun (s : { s : Set M // span R s = p }) ↦ Cardinal.mk.{u} (↑(↑s : Set M) : Type u)) s)
    (⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u))
⊢ ∃ (s : Set M), #(↑s : Type u) = ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) ∧ span R s = p

Tactic:
exact ⟨s.1, ⟨hs, s.2⟩⟩