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 : p.FG
obtain :
  ∀ (s : Set M) (hs₁ : #(↑s : Type u) = p.spanRank) (hs₂ : span R s = p),
    ∃ (s : Set M), s.encard = (↑p.spanFinrank : ℕ∞) ∧ span R s = p
⊢ ∃ (s : Set M), s.encard = (↑p.spanFinrank : ℕ∞) ∧ span R s = p

Tactic:
obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_card_eq_spanRank p

Premises used: Submodule.exists_span_set_card_eq_spanRank
-- 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 : p.FG
s : Set M
hs₁ : #(↑s : Type u) = p.spanRank
hs₂ : span R s = p
⊢ ∃ (s : Set M), s.encard = (↑p.spanFinrank : ℕ∞) ∧ span R s = p

Tactic:
⟨s, ⟨?_, hs₂⟩⟩

Premises used: And.intro, Exists.intro
-- 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 : p.FG
s : Set M
hs₁ : #(↑s : Type u) = p.spanRank
hs₂ : span R s = p
refine : s.encard = (↑p.spanFinrank : ℕ∞)
⊢ ∃ (s : Set M), s.encard = (↑p.spanFinrank : ℕ∞) ∧ span R s = p

Tactic:
refine ⟨s, ⟨?_, hs₂⟩⟩
-- 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 : p.FG
s : Set M
hs₁ : #(↑s : Type u) = p.spanRank
hs₂ : span R s = p
⊢ p.spanRank = (↑p.spanFinrank : Cardinal.{u})

Tactic:
have := fg_iff_spanRank_eq_spanFinrank.mpr 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
h : p.FG
s : Set M
hs₁ : #(↑s : Type u) = p.spanRank
hs₂ : span R s = p
this : p.spanRank = (↑p.spanFinrank : Cardinal.{u})
rw :
  Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) (↑p.spanFinrank : Cardinal.{u}) : ℕ∞)
    ((↑((toNat : (a : Cardinal.{u}) → ℕ) (↑p.spanFinrank : Cardinal.{u})) : ℕ∞) : ℕ∞)
⊢ s.encard = (↑p.spanFinrank : ℕ∞)

Tactic:
rw [Set.encard, ENat.card, spanFinrank, hs₁, this]

Premises used: Set.encard, Submodule.spanFinrank, ENat.card
-- 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 : p.FG
s : Set M
hs₁ : #(↑s : Type u) = p.spanRank
hs₂ : span R s = p
this : p.spanRank = (↑p.spanFinrank : Cardinal.{u})
⊢ Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) (↑p.spanFinrank : Cardinal.{u}) : ℕ∞)
    ((↑((toNat : (a : Cardinal.{u}) → ℕ) (↑p.spanFinrank : Cardinal.{u})) : ℕ∞) : ℕ∞)

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 : p.FG
obtain :
  ∀ (s : Set M) (hs₁ : s.encard = (↑p.spanFinrank : ℕ∞)) (hs₂ : span R s = p),
    ∃ (s : Finset M), s.card = p.spanFinrank ∧ span R (↑s : Set M) = p
⊢ ∃ (s : Finset M), s.card = p.spanFinrank ∧ span R (↑s : Set M) = p

Tactic:
obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_encard_eq_spanFinrank h

Premises used: Submodule.FG.exists_span_set_encard_eq_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
h : p.FG
s : Set M
hs₁ : s.encard = (↑p.spanFinrank : ℕ∞)
hs₂ : span R s = p
⊢ s.Finite

Tactic:
have s_f := Set.finite_of_encard_eq_coe hs₁
-- 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 : p.FG
s : Set M
hs₁ : s.encard = (↑p.spanFinrank : ℕ∞)
hs₂ : span R s = p
s_f : s.Finite
⊢ span R (↑(s_f.toFinset (s := s)) : Set M) = p

Tactic:
simpa using hs₂
-- 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 : p.FG
s : Set M
hs₁ : s.encard = (↑p.spanFinrank : ℕ∞)
hs₂ : span R s = p
s_f : s.Finite
refine : s_f.toFinset (s := s).card = p.spanFinrank
⊢ ∃ (s : Finset M), s.card = p.spanFinrank ∧ span R (↑s : Set M) = p

Tactic:
refine ⟨s_f.toFinset, ⟨?_, by simpa using hs₂⟩⟩
-- 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 : p.FG
s : Set M
hs₁ : s.encard = (↑p.spanFinrank : ℕ∞)
hs₂ : span R s = p
s_f : s.Finite
⊢ s_f.toFinset (s := s).card = p.spanFinrank

Tactic:
simpa [s_f.encard_eq_coe_toFinset_card, ENat.coe_inj] using hs₁

Premises used: ENat.coe_inj, Set.Finite.encard_eq_coe_toFinset_card
-- 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
a : Cardinal.{max u v}
mp : lift.{v, u} p.spanRank ≤ a → ∃ (s : Set M), lift.{v, u} #(↑s : Type u) ≤ a ∧ span R s = p
mpr : (∃ (s : Set M), lift.{v, u} #(↑s : Type u) ≤ a ∧ span R s = p) → lift.{v, u} p.spanRank ≤ a
⊢ lift.{v, u} p.spanRank ≤ a ↔ ∃ (s : Set M), lift.{v, u} #(↑s : Type u) ≤ a ∧ span R s = p

Tactic:
constructor
-- 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
a : Cardinal.{max u v}
h : lift.{v, u} p.spanRank ≤ a
mp :
  ∀ (s : Set M) (hs₁ : #(↑s : Type u) = p.spanRank) (hs₂ : span R s = p),
    ∃ (s : Set M), lift.{v, u} #(↑s : Type u) ≤ a ∧ span R s = p
⊢ ∃ (s : Set M), lift.{v, u} #(↑s : Type u) ≤ a ∧ span R s = p

Tactic:
obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_card_eq_spanRank p

Premises used: Submodule.exists_span_set_card_eq_spanRank
-- 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
a : Cardinal.{max u v}
h : lift.{v, u} p.spanRank ≤ a
s : Set M
hs₁ : #(↑s : Type u) = p.spanRank
hs₂ : span R s = p
⊢ ∃ (s : Set M), lift.{v, u} #(↑s : Type u) ≤ a ∧ span R s = p

Tactic:
⟨s, ⟨hs₁ ▸ h, hs₂⟩⟩

Premises used: Eq.rec, And.intro, Exists.intro, Eq.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
p : Submodule R M
a : Cardinal.{max u v}
h : lift.{v, u} p.spanRank ≤ a
s : Set M
hs₁ : #(↑s : Type u) = p.spanRank
hs₂ : span R s = p
⊢ ∃ (s : Set M), lift.{v, u} #(↑s : Type u) ≤ a ∧ span R s = p

Tactic:
exact ⟨s, ⟨hs₁ ▸ h, hs₂⟩⟩
-- 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
a : Cardinal.{max u v}
⊢ (∃ (s : Set M), lift.{v, u} #(↑s : Type u) ≤ a ∧ span R s = p) → lift.{v, u} p.spanRank ≤ a

Tactic:
fun ⟨s, ⟨h₁, h₂⟩⟩ ↦ h₂.symm ▸ (Cardinal.lift_le.mpr (spanRank_span_le_card s)).trans h₁

Premises used: Iff.mpr, Submodule.spanRank_span_le_card, Cardinal.lift, Eq.rec, _private.0.Submodule.lift_spanRank_le_iff_exists_span_set_card_le.match_1, LE.le, LE.le.trans, Eq.symm, Cardinal.lift_le, Submodule.spanRank
-- 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
a : Cardinal.{max u v}
⊢ (∃ (s : Set M), lift.{v, u} #(↑s : Type u) ≤ a ∧ span R s = p) → lift.{v, u} p.spanRank ≤ a

Tactic:
exact fun ⟨s, ⟨h₁, h₂⟩⟩ ↦ h₂.symm ▸ (Cardinal.lift_le.mpr (spanRank_span_le_card s)).trans 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
a : Cardinal.{u}
⊢ lift.{u, u} p.spanRank ≤ a ↔ ∃ (s : Set M), lift.{u, u} #(↑s : Type u) ≤ a ∧ span R s = p

Tactic:
lift_spanRank_le_iff_exists_span_set_card_le p (a := a)

Premises used: Submodule.lift_spanRank_le_iff_exists_span_set_card_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
p : Submodule R M
a : Cardinal.{u}
h : p.spanRank = lift.{u, u} p.spanRank
h₁ : ∀ (x : Set M), #(↑x : Type u) = lift.{u, u} #(↑x : Type u)
⊢ p.spanRank ≤ a ↔ ∃ (s : Set M), #(↑s : Type u) ≤ a ∧ span R s = p

Tactic:
convert! lift_spanRank_le_iff_exists_span_set_card_le p (a := a)

Premises used: Submodule.lift_spanRank_le_iff_exists_span_set_card_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
p : Submodule R M
a : Cardinal.{u}
⊢ p.spanRank = lift.{u, u} p.spanRank

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
a : Cardinal.{u}
x : Set M
⊢ #(↑x : Type u) = lift.{u, u} #(↑x : Type u)

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
I : Submodule R M
mp : I.spanRank = 0 → I = ⊥
mpr : I = ⊥ → I.spanRank = 0
⊢ I.spanRank = 0 ↔ I = ⊥

Tactic:
constructor
-- 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
I : Submodule R M
h : I.spanRank = 0
rw rw₁ : LE.le.{u + 1} (α := Cardinal.{u}) 0 0
⊢ I.spanRank ≤ 0

Tactic:
rw [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
I : Submodule R M
h : I.spanRank = 0
mp : ∀ (s : Set M) (hs₁ : #(↑s : Type u) ≤ 0) (hs₂ : span R s = I), I = ⊥
⊢ I = ⊥

Tactic:
obtain ⟨s, ⟨hs₁, hs₂⟩⟩ :=
      (FG.spanRank_le_iff_exists_span_set_card_le I (a := 0)).mp (by rw [h])

Premises used: Iff.mp, Submodule.FG.spanRank_le_iff_exists_span_set_card_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
I : Submodule R M
h : I.spanRank = 0
s : Set M
hs₁ : #(↑s : Type u) ≤ 0
hs₂ : span R s = I
⊢ s = ∅

Tactic:
simp only [nonpos_iff_eq_zero, mk_eq_zero_iff, Set.isEmpty_coe_sort] at hs₁

Premises used: Set.isEmpty_coe_sort, Cardinal.mk_eq_zero_iff, nonpos_iff_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
I : Submodule R M
h : I.spanRank = 0
s : Set M
hs₂ : span R s = I
hs₁ : s = ∅
⊢ I = ⊥

Tactic:
simp_all
-- 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
⊢ Eq.{u + 1} (α := Submodule R M) (span R ∅) ⊥

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
⊢ #(↑(↑(Subtype.mk (p := fun (s : Set M) ↦ Eq (α := Submodule R M) (span R s) ⊥) ∅ ⋯) : Set M) : Type u) = 0

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
⊢ Eq.{u + 2} (α := Cardinal.{u})
    (⨅ (s : { s : Set M // Eq (α := Submodule R M) (span R s) ⊥ }), #(↑(↑s : Set M) : Type u)) 0

Tactic:
exact Cardinal.iInf_eq_zero_iff.mpr (Or.inr ⟨⟨∅, by simp⟩, by simp⟩)

Premises used: Iff.mpr, Exists.intro, Cardinal.iInf_eq_zero_iff, Or.inr
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
inst : Semiring R
⊢ spanRank (R := R) (M := R) ⊥ = 0

Tactic:
Submodule.spanRank_eq_zero_iff_eq_bot.mpr rfl

Premises used: Iff.mpr, Submodule.spanRank_eq_zero_iff_eq_bot, rfl
-- 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
⊢ spanFinrank.{u, u_1} (R := R) (M := M) ⊥ = 0

Tactic:
simp [spanFinrank]

Premises used: 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
inst_3 : Subsingleton R
p : Submodule R M
⊢ p.spanRank = 0

Tactic:
simp [nontriviality]
-- 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 : Subsingleton R
p : Submodule R M
⊢ Subsingleton M

Tactic:
have := Module.subsingleton R M
-- 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 : Subsingleton R
p : Submodule R M
this : Subsingleton M
⊢ p.spanFinrank = 0

Tactic:
simp [Submodule.eq_bot_of_subsingleton]

Premises used: Submodule.eq_bot_of_subsingleton
-- 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
⊢ #(↑p.generators : Type u) = p.spanRank

Tactic:
(Classical.choose_spec (exists_span_set_card_eq_spanRank p)).1

Premises used: Submodule.exists_span_set_card_eq_spanRank, Submodule.generators, Classical.choose_spec, And.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
p : Submodule R M
h : p.FG
rw : (↑p.spanFinrank : Cardinal.{u}) = p.spanRank
⊢ p.generators.ncard = p.spanFinrank

Tactic:
rw [← Nat.cast_inj (R := Cardinal), ← fg_iff_spanRank_eq_spanFinrank.mpr h, Set.ncard, Set.encard,
     ENat.card, generators_card, toNat_toENat, ← spanFinrank]

Premises used: Submodule.fg_iff_spanRank_eq_spanFinrank, Iff.mpr, Submodule.generators_card, Set.encard, Nat.cast_inj, Cardinal.toNat_toENat, Submodule.spanFinrank, Set.ncard, ENat.card
-- 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 : p.FG
⊢ (↑p.spanFinrank : Cardinal.{u}) = p.spanRank

Tactic:
(fg_iff_spanRank_eq_spanFinrank.mpr h).symm

Premises used: Submodule.fg_iff_spanRank_eq_spanFinrank, Iff.mpr, Eq.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
p : Submodule R M
h : p.FG
⊢ (↑p.spanFinrank : Cardinal.{u}) = p.spanRank

Tactic:
exact (fg_iff_spanRank_eq_spanFinrank.mpr h).symm

Premises used: Submodule.fg_iff_spanRank_eq_spanFinrank, Iff.mpr, Eq.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
p : Submodule R M
hp : p.FG
rw : p.spanRank < ℵ₀
⊢ p.generators.Finite

Tactic:
rw [← Cardinal.lt_aleph0_iff_set_finite, Submodule.generators_card]

Premises used: Submodule.generators_card, Cardinal.lt_aleph0_iff_set_finite
-- 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.spanRank < ℵ₀

Tactic:
spanRank_finite_iff_fg.mpr hp

Premises used: Iff.mpr, Submodule.spanRank_finite_iff_fg
-- 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.spanRank < ℵ₀

Tactic:
exact spanRank_finite_iff_fg.mpr hp

Premises used: Iff.mpr, Submodule.spanRank_finite_iff_fg
-- 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
⊢ span R p.generators = p

Tactic:
(Classical.choose_spec (exists_span_set_card_eq_spanRank p)).2

Premises used: Submodule.exists_span_set_card_eq_spanRank, Submodule.generators, Classical.choose_spec, And.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
nth_rw : p.generators ⊆ (↑(span R p.generators) : Set M)
⊢ p.generators ⊆ (↑p : Set M)

Tactic:
nth_rw 2 [← span_generators p]

Premises used: Submodule.span_generators
-- 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
⊢ p.generators ⊆ (↑(span R p.generators) : Set M)

Tactic:
subset_span (s := generators p)

Premises used: Submodule.subset_span
-- 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
⊢ p.generators ⊆ (↑(span R p.generators) : Set M)

Tactic:
exact subset_span (s := generators p)

Premises used: Submodule.subset_span
-- 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 q : Submodule R M
apply : ∃ (s : Set M), #(↑s : Type u) ≤ p.spanRank + q.spanRank ∧ span R s = p ⊔ q
⊢ (p ⊔ q).spanRank ≤ p.spanRank + q.spanRank

Tactic:
apply (FG.spanRank_le_iff_exists_span_set_card_le (p ⊔ q)).mpr

Premises used: Iff.mpr, Max.max, Submodule.FG.spanRank_le_iff_exists_span_set_card_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
p q : Submodule R M
obtain :
  ∀ (sp : Set M) (hp₁ : #(↑sp : Type u) = spanRank (span R sp)),
    ∃ (s : Set M), #(↑s : Type u) ≤ spanRank (span R sp) + q.spanRank ∧ span R s = span R sp ⊔ q
⊢ ∃ (s : Set M), #(↑s : Type u) ≤ p.spanRank + q.spanRank ∧ span R s = p ⊔ q

Tactic:
obtain ⟨sp, ⟨hp₁, rfl⟩⟩ := exists_span_set_card_eq_spanRank p

Premises used: Submodule.exists_span_set_card_eq_spanRank, rfl
-- 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
q : Submodule R M
sp : Set M
hp₁ : #(↑sp : Type u) = spanRank (span R sp)
obtain :
  ∀ (sq : Set M) (hq₁ : #(↑sq : Type u) = spanRank (span R sq)),
    ∃ (s : Set M),
      #(↑s : Type u) ≤ spanRank (span R sp) + spanRank (span R sq) ∧
        Eq (α := Submodule R M) (span R s) (span R sp ⊔ span R sq)
⊢ ∃ (s : Set M), #(↑s : Type u) ≤ spanRank (span R sp) + q.spanRank ∧ span R s = span R sp ⊔ q

Tactic:
obtain ⟨sq, ⟨hq₁, rfl⟩⟩ := exists_span_set_card_eq_spanRank q

Premises used: Submodule.exists_span_set_card_eq_spanRank, sq, rfl
-- 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
sp : Set M
hp₁ : #(↑sp : Type u) = spanRank (span R sp)
sq : Set M
hq₁ : #(↑sq : Type u) = spanRank (span R sq)
⊢ ∃ (s : Set M),
    #(↑s : Type u) ≤ spanRank (span R sp) + spanRank (span R sq) ∧
      Eq (α := Submodule R M) (span R s) (span R sp ⊔ span R sq)

Tactic:
⟨sp ∪ sq, ⟨hp₁ ▸ hq₁ ▸ (Cardinal.mk_union_le sp sq), span_union sp sq⟩⟩

Premises used: Eq.rec, Submodule.span_union, And.intro, Exists.intro, Union.union, Cardinal.mk_union_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
sp : Set M
hp₁ : #(↑sp : Type u) = spanRank (span R sp)
sq : Set M
hq₁ : #(↑sq : Type u) = spanRank (span R sq)
⊢ ∃ (s : Set M),
    #(↑s : Type u) ≤ spanRank (span R sp) + spanRank (span R sq) ∧
      Eq (α := Submodule R M) (span R s) (span R sp ⊔ span R sq)

Tactic:
exact ⟨sp ∪ sq, ⟨hp₁ ▸ hq₁ ▸ (Cardinal.mk_union_le sp sq), span_union sp sq⟩⟩
-- 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_1 : p.FG
h : p = ⊥
⊢ p.spanFinrank = 0

Tactic:
simp [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
h : p.FG
refine : ∀ (heq : p.spanFinrank = 0), p = ⊥
⊢ p.spanFinrank = 0 ↔ p = ⊥

Tactic:
refine ⟨fun heq ↦ ?_, fun h ↦ by simp [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
h : p.FG
heq : p.spanFinrank = 0
⊢ p.generators = ∅

Tactic:
rw [← Submodule.FG.generators_ncard h, Set.ncard_eq_zero h.finite_generators] at heq

Premises used: Set.ncard_eq_zero, Submodule.FG.generators_ncard, Submodule.FG.finite_generators
-- 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 : p.FG
heq : p.generators = ∅
rw : Eq (α := Submodule R M) (span R p.generators) ⊥
rw₁ : Eq.{u + 1} (α := Submodule R M) (span R ∅) ⊥
rw₂ rw₃ : Eq.{u + 1} (α := Submodule R M) ⊥ ⊥
⊢ p = ⊥

Tactic:
rw [← p.span_generators, heq, span_empty]

Premises used: Submodule.span_empty, Submodule.span_generators
-- 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
m : M
hm : m ≠ 0
apply : spanFinrank (M := M) (R ∙ m) ≤ 1
apply₁ : 1 ≤ spanFinrank (M := M) (R ∙ m)
⊢ spanFinrank (M := M) (R ∙ m) = 1

Tactic:
apply le_antisymm ?_ ?_

Premises used: le_antisymm
-- 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
m : M
hm : m ≠ 0
⊢ Set.Finite (α := M) {m}

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
m : M
hm : m ≠ 0
⊢ Set.ncard (α := M) {m} ≤ 1

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
m : M
hm : m ≠ 0
⊢ spanFinrank (M := M) (R ∙ m) ≤ 1

Tactic:
exact le_trans (Submodule.spanFinrank_span_le_ncard_of_finite (by simp)) (by simp)

Premises used: Submodule.spanFinrank_span_le_ncard_of_finite, 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
m : M
hm : m ≠ 0
by_contra! : ∀ (this : spanFinrank (M := M) (R ∙ m) < 1), False
⊢ 1 ≤ spanFinrank (M := M) (R ∙ m)

Tactic:
by_contra!
-- 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
m : M
hm : m ≠ 0
this : spanFinrank (M := M) (R ∙ m) < 1
⊢ False

Tactic:
simp [Submodule.spanFinrank_eq_zero_iff_eq_bot (fg_span_singleton m), hm] at this

Premises used: Submodule.fg_span_singleton, Submodule.spanFinrank_eq_zero_iff_eq_bot
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
S : Type u_2
M : Type u
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : AddCommMonoid M
inst_3 : Module R M
L : Type v
inst_4 : AddCommMonoid L
inst_5 : Module S L
inst_6 : RingHomSurjective σ
f : M →ₛₗ[σ] L
p : Submodule R M
rw :
  ∃ (s : Set L),
    Cardinal.lift.{u, v} (Cardinal.mk (↑s : Type v)) ≤ Cardinal.lift.{v, u} (Cardinal.mk (↑p.generators : Type u)) ∧
      span S s = map f p
⊢ Cardinal.lift.{u, v} (map f p).spanRank ≤ Cardinal.lift.{v, u} p.spanRank

Tactic:
rw [← generators_card p, lift_spanRank_le_iff_exists_span_set_card_le]

Premises used: Submodule.generators_card, Submodule.lift_spanRank_le_iff_exists_span_set_card_le
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
S : Type u_2
M : Type u
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : AddCommMonoid M
inst_3 : Module R M
L : Type v
inst_4 : AddCommMonoid L
inst_5 : Module S L
inst_6 : RingHomSurjective σ
f : M →ₛₗ[σ] L
p : Submodule R M
⊢ map f p ≤ span S ((⇑f : (a : M) → L) '' p.generators)

Tactic:
simp [span_generators]

Premises used: Submodule.span_generators
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
S : Type u_2
M : Type u
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : AddCommMonoid M
inst_3 : Module R M
L : Type v
inst_4 : AddCommMonoid L
inst_5 : Module S L
inst_6 : RingHomSurjective σ
f : M →ₛₗ[σ] L
p : Submodule R M
⊢ ∃ (s : Set L),
    Cardinal.lift.{u, v} (Cardinal.mk (↑s : Type v)) ≤ Cardinal.lift.{v, u} (Cardinal.mk (↑p.generators : Type u)) ∧
      span S s = map f p

Tactic:
exact ⟨f '' p.generators, Cardinal.mk_image_le_lift, le_antisymm (span_le.2 (fun n ⟨m, hm, h⟩ ↦
    ⟨m, span_generators p ▸ subset_span hm, h⟩)) (by simp [span_generators])⟩
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
S : Type u_2
M N : Type u
inst : Semiring R
inst_1 : Semiring S
σ : R →+* S
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : AddCommMonoid N
inst_5 : Module S N
inst_6 : RingHomSurjective σ
f : M →ₛₗ[σ] N
p : Submodule R M
⊢ (map f p).spanRank ≤ p.spanRank

Tactic:
simpa using lift_spanRank_map_le f p

Premises used: Submodule.lift_spanRank_map_le