awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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)
⊢ #ι ≤ #(↑(Set.range (ι := ι) (⇑(Module.Basis.span hs) : (a : ι) → ↥(span R (Set.range v)))) : Type u)
have refine_1 : Function.Injective.{u + 1, u + 1} (α := ι) (β := ↥(span R (Set.range v)))
  (⇑(Module.Basis.span hs) : (a : ι) → ↥(span R (Set.range v)))
Tactic: rw [mk_range_eq]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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} (α := ι) (β := 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))))
have 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
Tactic: convert! hv
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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.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
have 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
Tactic: ext
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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 ↥(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)))
    ⊤
have 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))) ⊤)
Tactic: apply map_injective_of_injective (f := (span R _).subtype) (injective_subtype _)
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
⊢ spanFinrank (span R s) ≤ s.ncard
have rw : LE.le (α := ℕ∞) (↑(spanFinrank (span R s)) : ℕ∞) (↑s.ncard : ℕ∞)
Tactic: rw [← Nat.cast_le (α := ℕ∞)]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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), #(↑s : Type u) = ⨅ (s : { s : Set M // span R s = p }), #(↑(↑s : Set M) : Type u) ∧ span R s = p
have 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
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⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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), s.encard = (↑p.spanFinrank : ℕ∞) ∧ span R s = p
have 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
Tactic: obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_card_eq_spanRank p
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
have refine : s.encard = (↑p.spanFinrank : ℕ∞)
Tactic: refine ⟨s, ⟨?_, hs₂⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (hypothesis)
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.encard = (↑p.spanFinrank : ℕ∞)
have this : p.spanRank = (↑p.spanFinrank : Cardinal.{u})
Tactic: have := fg_iff_spanRank_eq_spanFinrank.mpr h
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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})
⊢ s.encard = (↑p.spanFinrank : ℕ∞)
have rw : Eq (α := ℕ∞) ((toENat : (a : Cardinal.{u}) → ℕ∞) (↑p.spanFinrank : Cardinal.{u}) : ℕ∞)
  ((↑((toNat : (a : Cardinal.{u}) → ℕ) (↑p.spanFinrank : Cardinal.{u})) : ℕ∞) : ℕ∞)
Tactic: rw [Set.encard, ENat.card, spanFinrank, hs₁, this]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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 : Finset M), s.card = p.spanFinrank ∧ span R (↑s : Set M) = p
have 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
Tactic: obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_encard_eq_spanFinrank h
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (hypothesis)
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 : Finset M), s.card = p.spanFinrank ∧ span R (↑s : Set M) = p
have s_f : s.Finite
Tactic: have s_f := Set.finite_of_encard_eq_coe hs₁
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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 : Finset M), s.card = p.spanFinrank ∧ span R (↑s : Set M) = p
have refine : s_f.toFinset (s := s).card = p.spanFinrank
Tactic: refine ⟨s_f.toFinset, ⟨?_, by simpa using hs₂⟩⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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}
⊢ lift.{v, u} p.spanRank ≤ a ↔ ∃ (s : Set M), lift.{v, u} #(↑s : Type u) ≤ a ∧ span R s = p
have mp : lift.{v, u} p.spanRank ≤ a → ∃ (s : Set M), lift.{v, u} #(↑s : Type u) ≤ a ∧ span R s = p
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
⊢ lift.{v, u} p.spanRank ≤ a ↔ ∃ (s : Set M), lift.{v, u} #(↑s : Type u) ≤ a ∧ span R s = p
have mpr : (∃ (s : Set M), lift.{v, u} #(↑s : Type u) ≤ a ∧ span R s = p) → lift.{v, u} p.spanRank ≤ a
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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), lift.{v, u} #(↑s : Type u) ≤ a ∧ span R s = p
have 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
Tactic: obtain ⟨s, ⟨hs₁, hs₂⟩⟩ := exists_span_set_card_eq_spanRank p
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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 ≤ a ↔ ∃ (s : Set M), #(↑s : Type u) ≤ a ∧ span R s = p
have h : p.spanRank = lift.{u, u} p.spanRank
Tactic: convert! lift_spanRank_le_iff_exists_span_set_card_le p (a := a)
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
⊢ p.spanRank ≤ a ↔ ∃ (s : Set M), #(↑s : Type u) ≤ a ∧ span R s = p
have h₁ : ∀ (x : Set M), #(↑x : Type u) = lift.{u, u} #(↑x : Type u)
Tactic: convert! lift_spanRank_le_iff_exists_span_set_card_le p (a := a)
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
I : Submodule R M
⊢ I.spanRank = 0 ↔ I = ⊥
have mp : I.spanRank = 0 → I = ⊥
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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 = ⊥
⊢ I.spanRank = 0 ↔ I = ⊥
have mpr : I = ⊥ → I.spanRank = 0
Tactic: constructor
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
⊢ I.spanRank ≤ 0
have rw : LE.le.{u + 1} (α := Cardinal.{u}) 0 0
Tactic: rw [h]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
⊢ I = ⊥
have mp : ∀ (s : Set M) (hs₁ : #(↑s : Type u) ≤ 0) (hs₂ : span R s = I), I = ⊥
Tactic: obtain ⟨s, ⟨hs₁, hs₂⟩⟩ :=
      (FG.spanRank_le_iff_exists_span_set_card_le I (a := 0)).mp (by rw [h])
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (hypothesis)
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
⊢ I = ⊥
have hs₃ : s = ∅
Tactic: simp only [nonpos_iff_eq_zero, mk_eq_zero_iff, Set.isEmpty_coe_sort] at hs₁
Cleared hypotheses: hs₁
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (hypothesis)
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.spanFinrank = 0
have this : Subsingleton M
Tactic: have := Module.subsingleton R M
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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.generators.ncard = p.spanFinrank
have rw : (↑p.spanFinrank : Cardinal.{u}) = p.spanRank
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]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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.generators.Finite
have rw : p.spanRank < ℵ₀
Tactic: rw [← Cardinal.lt_aleph0_iff_set_finite, Submodule.generators_card]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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 ⊆ (↑p : Set M)
have nth_rw : p.generators ⊆ (↑(span R p.generators) : Set M)
Tactic: nth_rw 2 [← span_generators p]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
⊢ (p ⊔ q).spanRank ≤ p.spanRank + q.spanRank
have apply : ∃ (s : Set M), #(↑s : Type u) ≤ p.spanRank + q.spanRank ∧ span R s = p ⊔ q
Tactic: apply (FG.spanRank_le_iff_exists_span_set_card_le (p ⊔ q)).mpr
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
⊢ ∃ (s : Set M), #(↑s : Type u) ≤ p.spanRank + q.spanRank ∧ span R s = p ⊔ q
have 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
Tactic: obtain ⟨sp, ⟨hp₁, rfl⟩⟩ := exists_span_set_card_eq_spanRank p
Cleared hypotheses: p
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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)
⊢ ∃ (s : Set M), #(↑s : Type u) ≤ spanRank (span R sp) + q.spanRank ∧ span R s = span R sp ⊔ q
have 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)
Tactic: obtain ⟨sq, ⟨hq₁, rfl⟩⟩ := exists_span_set_card_eq_spanRank q
Cleared hypotheses: q
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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 = 0 ↔ p = ⊥
have refine : ∀ (heq : p.spanFinrank = 0), p = ⊥
Tactic: refine ⟨fun heq ↦ ?_, fun h ↦ by simp [h]⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (hypothesis)
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 = ⊥
have heq₁ : p.generators = ∅
Tactic: rw [← Submodule.FG.generators_ncard h, Set.ncard_eq_zero h.finite_generators] at heq
Cleared hypotheses: heq
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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 = ∅
⊢ p = ⊥
have rw : Eq (α := Submodule R M) (span R p.generators) ⊥
Tactic: rw [← p.span_generators, heq, span_empty]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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) ⊥
⊢ p = ⊥
have rw₁ : Eq.{u + 1} (α := Submodule R M) (span R ∅) ⊥
Tactic: rw [← p.span_generators, heq, span_empty]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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 ∅) ⊥
⊢ p = ⊥
have rw₂ : Eq.{u + 1} (α := Submodule R M) ⊥ ⊥
Tactic: rw [← p.span_generators, heq, span_empty]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
have apply : spanFinrank (M := M) (R ∙ m) ≤ 1
Tactic: apply le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
⊢ spanFinrank (M := M) (R ∙ m) = 1
have apply₁ : 1 ≤ spanFinrank (M := M) (R ∙ m)
Tactic: apply le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
⊢ 1 ≤ spanFinrank (M := M) (R ∙ m)
have by_contra! : ∀ (this : spanFinrank (M := M) (R ∙ m) < 1), False
Tactic: by_contra!
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
⊢ Cardinal.lift.{u, v} (map f p).spanRank ≤ Cardinal.lift.{v, u} p.spanRank
have 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
Tactic: rw [← generators_card p, lift_spanRank_le_iff_exists_span_set_card_le]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
hp : p.FG
⊢ (map f p).spanFinrank ≤ p.spanFinrank
have rw : Cardinal.lift.{u, v} (map f p).spanRank ≤ Cardinal.lift.{v, u} p.spanRank
Tactic: rw [← (hp.map f).spanRank_le_iff, ← Cardinal.lift_le.{u}, Cardinal.lift_natCast,
    ← Cardinal.lift_natCast.{v}, ← hp.spanRank_eq_spanFinrank]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
hf : Function.Injective.{u + 1, v + 1} (α := M) (β := L) (⇑f : (a : M) → L)
p : Submodule R M
⊢ Cardinal.lift.{u, v} (map f p).spanRank = Cardinal.lift.{v, u} p.spanRank
have refine : Cardinal.lift.{v, u} p.spanRank ≤ Cardinal.lift.{u, v} (map f p).spanRank
Tactic: refine (lift_spanRank_map_le f p).antisymm ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
hf : Function.Injective.{u + 1, v + 1} (α := M) (β := L) (⇑f : (a : M) → L)
p : Submodule R M
⊢ Cardinal.lift.{v, u} p.spanRank ≤ Cardinal.lift.{u, v} (map f p).spanRank
have obtain : ∀ (s : Set L) (hs : Cardinal.mk (↑s : Type v) = (map f p).spanRank) (e : span S s = map f p),
  Cardinal.lift.{v, u} p.spanRank ≤ Cardinal.lift.{u, v} (map f p).spanRank
Tactic: obtain ⟨s, hs, e⟩ := (p.map f).exists_span_set_card_eq_spanRank
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
hf : Function.Injective.{u + 1, v + 1} (α := M) (β := L) (⇑f : (a : M) → L)
p : Submodule R M
s : Set L
hs : Cardinal.mk (↑s : Type v) = (map f p).spanRank
e : span S s = map f p
⊢ Cardinal.lift.{v, u} p.spanRank ≤ Cardinal.lift.{u, v} (map f p).spanRank
have obtain : ∀ (s : Set M) (hs : Cardinal.mk (↑((⇑f : (a : M) → L) '' s) : Type v) = (map f p).spanRank)
  (e : span S ((⇑f : (a : M) → L) '' s) = map f p),
  Cardinal.lift.{v, u} p.spanRank ≤ Cardinal.lift.{u, v} (map f p).spanRank
Tactic: obtain ⟨s, rfl⟩ : ∃ y, f '' y = s := Set.subset_range_iff_exists_image_eq.mp
    ((subset_span.trans e.le).trans LinearMap.map_le_range)
Cleared hypotheses: s, hs, e
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
hf : Function.Injective.{u + 1, v + 1} (α := M) (β := L) (⇑f : (a : M) → L)
p : Submodule R M
s : Set M
hs : Cardinal.mk (↑((⇑f : (a : M) → L) '' s) : Type v) = (map f p).spanRank
e : span S ((⇑f : (a : M) → L) '' s) = map f p
⊢ Cardinal.lift.{v, u} p.spanRank ≤ Cardinal.lift.{u, v} (map f p).spanRank
have obtain : ∀ (hs : Cardinal.mk (↑((⇑f : (a : M) → L) '' s) : Type v) = (map f (span R s)).spanRank)
  (e : span S ((⇑f : (a : M) → L) '' s) = map f (span R s)),
  Cardinal.lift.{v, u} (spanRank (span R s)) ≤ Cardinal.lift.{u, v} (map f (span R s)).spanRank
Tactic: obtain rfl : span R s = p := by simpa [(map_injective_of_injective hf).eq_iff] using e
Cleared hypotheses: p, hs, e
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
hf : Function.Injective.{u + 1, v + 1} (α := M) (β := L) (⇑f : (a : M) → L)
s : Set M
hs : Cardinal.mk (↑((⇑f : (a : M) → L) '' s) : Type v) = (map f (span R s)).spanRank
e : span S ((⇑f : (a : M) → L) '' s) = map f (span R s)
⊢ Cardinal.lift.{v, u} (spanRank (span R s)) ≤ Cardinal.lift.{u, v} (map f (span R s)).spanRank
have grw : Cardinal.lift.{v, u} (spanRank (span R s)) ≤ Cardinal.lift.{u, v} (Cardinal.mk (↑((⇑f : (a : M) → L) '' s) : Type v))
Tactic: grw [← hs, Cardinal.mk_image_eq_lift _ _ hf, Cardinal.lift_le, spanRank_span_le_card]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
hf : Function.Injective.{u + 1, v + 1} (α := M) (β := L) (⇑f : (a : M) → L)
s : Set M
hs : Cardinal.mk (↑((⇑f : (a : M) → L) '' s) : Type v) = (map f (span R s)).spanRank
e : span S ((⇑f : (a : M) → L) '' s) = map f (span R s)
grw :
  Cardinal.lift.{v, u} (spanRank (span R s)) ≤ Cardinal.lift.{u, v} (Cardinal.mk (↑((⇑f : (a : M) → L) '' s) : Type v))
⊢ Cardinal.lift.{v, u} (spanRank (span R s)) ≤ Cardinal.lift.{u, v} (map f (span R s)).spanRank
have grw₁ : Cardinal.lift.{v, u} (spanRank (span R s)) ≤ Cardinal.lift.{v, u} (Cardinal.mk (↑s : Type u))
Tactic: grw [← hs, Cardinal.mk_image_eq_lift _ _ hf, Cardinal.lift_le, spanRank_span_le_card]