awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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))
grw₁ : Cardinal.lift.{v, u} (spanRank (span R s)) ≤ Cardinal.lift.{v, u} (Cardinal.mk (↑s : Type u))
⊢ Cardinal.lift.{v, u} (spanRank (span R s)) ≤ Cardinal.lift.{u, v} (map f (span R s)).spanRank
have grw₂ : spanRank (span R s) ≤ Cardinal.mk (↑s : Type u)
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))
grw₁ : Cardinal.lift.{v, u} (spanRank (span R s)) ≤ Cardinal.lift.{v, u} (Cardinal.mk (↑s : Type u))
grw₂ : spanRank (span R s) ≤ Cardinal.mk (↑s : Type u)
⊢ Cardinal.lift.{v, u} (spanRank (span R s)) ≤ Cardinal.lift.{u, v} (map f (span R s)).spanRank
have grw₃ : Cardinal.mk (↑s : Type u) ≤ Cardinal.mk (↑s : Type u)
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)
p : Submodule R M
⊢ (map f p).spanFinrank = p.spanFinrank
have rw : (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (map f p).spanRank = p.spanFinrank
Tactic: rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v},
    ← Cardinal.toNat_lift.{v, u}, lift_spanRank_map_eq_of_injective f hf p]
-- 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
rw : (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (map f p).spanRank = p.spanFinrank
⊢ (map f p).spanFinrank = p.spanFinrank
have rw₁ : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (map f p).spanRank : ℕ)
  ((Cardinal.toNat : (a : Cardinal.{u}) → ℕ) p.spanRank : ℕ)
Tactic: rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v},
    ← Cardinal.toNat_lift.{v, u}, lift_spanRank_map_eq_of_injective f hf p]
-- 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
rw : (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (map f p).spanRank = p.spanFinrank
rw₁ :
  Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (map f p).spanRank : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{u}) → ℕ) p.spanRank : ℕ)
⊢ (map f p).spanFinrank = p.spanFinrank
have rw₂ : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{max u v}) → ℕ) (Cardinal.lift.{u, v} (map f p).spanRank) : ℕ)
  ((Cardinal.toNat : (a : Cardinal.{u}) → ℕ) p.spanRank : ℕ)
Tactic: rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v},
    ← Cardinal.toNat_lift.{v, u}, lift_spanRank_map_eq_of_injective f hf p]
-- 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
rw : (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (map f p).spanRank = p.spanFinrank
rw₁ :
  Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (map f p).spanRank : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{u}) → ℕ) p.spanRank : ℕ)
rw₂ :
  Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{max u v}) → ℕ) (Cardinal.lift.{u, v} (map f p).spanRank) : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{u}) → ℕ) p.spanRank : ℕ)
⊢ (map f p).spanFinrank = p.spanFinrank
have rw₃ : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{max u v}) → ℕ) (Cardinal.lift.{u, v} (map f p).spanRank) : ℕ)
  ((Cardinal.toNat : (a : Cardinal.{max v u}) → ℕ) (Cardinal.lift.{v, u} p.spanRank) : ℕ)
Tactic: rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v},
    ← Cardinal.toNat_lift.{v, u}, lift_spanRank_map_eq_of_injective f hf p]
-- 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
rw : (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (map f p).spanRank = p.spanFinrank
rw₁ :
  Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (map f p).spanRank : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{u}) → ℕ) p.spanRank : ℕ)
rw₂ :
  Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{max u v}) → ℕ) (Cardinal.lift.{u, v} (map f p).spanRank) : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{u}) → ℕ) p.spanRank : ℕ)
rw₃ :
  Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{max u v}) → ℕ) (Cardinal.lift.{u, v} (map f p).spanRank) : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{max v u}) → ℕ) (Cardinal.lift.{v, u} p.spanRank) : ℕ)
⊢ (map f p).spanFinrank = p.spanFinrank
have rw₄ : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{max u v}) → ℕ) (Cardinal.lift.{v, u} p.spanRank) : ℕ)
  ((Cardinal.toNat : (a : Cardinal.{max v u}) → ℕ) (Cardinal.lift.{v, u} p.spanRank) : ℕ)
Tactic: rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v},
    ← Cardinal.toNat_lift.{v, u}, lift_spanRank_map_eq_of_injective f hf p]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] N
⊢ spanRank.{u, u_1} (R := R) (M := M) ⊤ = spanRank.{u, u_2} (R := S) (M := N) ⊤
have rw : (map (↑e : M →ₛₗ[σ] N) ⊤).spanRank = spanRank.{u, u_2} (R := S) (M := N) ⊤
Tactic: rw [← spanRank_map_eq_of_injective e.toLinearMap e.injective ⊤, map_top, LinearEquiv.range]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] N
rw : (map (↑e : M →ₛₗ[σ] N) ⊤).spanRank = spanRank.{u, u_2} (R := S) (M := N) ⊤
⊢ spanRank.{u, u_1} (R := R) (M := M) ⊤ = spanRank.{u, u_2} (R := S) (M := N) ⊤
have rw₁ : (↑e : M →ₛₗ[σ] N).range.spanRank = spanRank.{u, u_2} (R := S) (M := N) ⊤
Tactic: rw [← spanRank_map_eq_of_injective e.toLinearMap e.injective ⊤, map_top, LinearEquiv.range]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
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
σ' : S →+* R
inst_6 : RingHomInvPair σ σ'
inst_7 : RingHomInvPair σ' σ
e : M ≃ₛₗ[σ] N
rw : (map (↑e : M →ₛₗ[σ] N) ⊤).spanRank = spanRank.{u, u_2} (R := S) (M := N) ⊤
rw₁ : (↑e : M →ₛₗ[σ] N).range.spanRank = spanRank.{u, u_2} (R := S) (M := N) ⊤
⊢ spanRank.{u, u_1} (R := R) (M := M) ⊤ = spanRank.{u, u_2} (R := S) (M := N) ⊤
have rw₂ : spanRank.{u, u_2} (R := S) (M := N) ⊤ = spanRank.{u, u_2} (R := S) (M := N) ⊤
Tactic: rw [← spanRank_map_eq_of_injective e.toLinearMap e.injective ⊤, map_top, LinearEquiv.range]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Submodule S M
⊢ N.spanRank ≤ spanRank (restrictScalars R N)
have obtain : ∀ (s : Set M) (hs : Cardinal.mk (↑s : Type u) = spanRank (restrictScalars R N))
  (e : Eq (α := Submodule R M) (span R s) (restrictScalars R N)), N.spanRank ≤ spanRank (restrictScalars R N)
Tactic: obtain ⟨s, hs, e⟩ := (N.restrictScalars R).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 : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
N : Submodule S M
s : Set M
hs : Cardinal.mk (↑s : Type u) = spanRank (restrictScalars R N)
e : Eq (α := Submodule R M) (span R s) (restrictScalars R N)
⊢ N.spanRank ≤ spanRank (restrictScalars R N)
have obtain : ∀ (hs : Cardinal.mk (↑s : Type u) = spanRank (restrictScalars R (span S s)))
  (e : Eq (α := Submodule R M) (span R s) (restrictScalars R (span S s))),
  spanRank (span S s) ≤ spanRank (restrictScalars R (span S s))
Tactic: obtain rfl : span S s = N :=
    le_antisymm (span_le.mpr (span_le.mp e.le :)) (e.ge.trans (span_le_restrictScalars R S s))
Cleared hypotheses: N, 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 : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
s : Set M
hs : Cardinal.mk (↑s : Type u) = spanRank (restrictScalars R (span S s))
e : Eq (α := Submodule R M) (span R s) (restrictScalars R (span S s))
⊢ spanRank (span S s) ≤ spanRank (restrictScalars R (span S s))
have grw : spanRank (span S s) ≤ Cardinal.mk (↑s : Type u)
Tactic: grw [← hs, 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 : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
s : Set M
hs : Cardinal.mk (↑s : Type u) = spanRank (restrictScalars R (span S s))
e : Eq (α := Submodule R M) (span R s) (restrictScalars R (span S s))
grw : spanRank (span S s) ≤ Cardinal.mk (↑s : Type u)
⊢ spanRank (span S s) ≤ spanRank (restrictScalars R (span S s))
have grw₁ : Cardinal.mk (↑s : Type u) ≤ Cardinal.mk (↑s : Type u)
Tactic: grw [← hs, 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 : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
H : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
N : Submodule S M
⊢ spanRank (restrictScalars R N) = N.spanRank
have refine : spanRank (restrictScalars R N) ≤ N.spanRank
Tactic: refine N.le_spanRank_restrictScalars.antisymm' ?_
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
H : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
N : Submodule S M
⊢ spanRank (restrictScalars R N) ≤ N.spanRank
have obtain : ∀ (s : Set M) (hs : Cardinal.mk (↑s : Type u) = spanRank (span S s)),
  spanRank (restrictScalars R (span S s)) ≤ spanRank (span S s)
Tactic: obtain ⟨s, hs, rfl⟩ := N.exists_span_set_card_eq_spanRank
Cleared hypotheses: N
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
S : Type u_2
M : Type u
inst : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
H : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
s : Set M
hs : Cardinal.mk (↑s : Type u) = spanRank (span S s)
⊢ spanRank (restrictScalars R (span S s)) ≤ spanRank (span S s)
have grw : spanRank (span R s) ≤ spanRank (span S s)
Tactic: grw [restrictScalars_span R S H s, ← hs, 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 : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
H : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
s : Set M
hs : Cardinal.mk (↑s : Type u) = spanRank (span S s)
grw : spanRank (span R s) ≤ spanRank (span S s)
⊢ spanRank (restrictScalars R (span S s)) ≤ spanRank (span S s)
have grw₁ : spanRank (span R s) ≤ Cardinal.mk (↑s : Type u)
Tactic: grw [restrictScalars_span R S H s, ← hs, 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 : CommSemiring R
inst_1 : Semiring S
inst_2 : AddCommMonoid M
inst_3 : Algebra R S
inst_4 : Module R M
inst_5 : Module S M
inst_6 : IsScalarTower R S M
H : Function.Surjective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
s : Set M
hs : Cardinal.mk (↑s : Type u) = spanRank (span S s)
grw : spanRank (span R s) ≤ spanRank (span S s)
grw₁ : spanRank (span R s) ≤ Cardinal.mk (↑s : Type u)
⊢ spanRank (restrictScalars R (span S s)) ≤ spanRank (span S s)
have grw₂ : Cardinal.mk (↑s : Type u) ≤ Cardinal.mk (↑s : Type u)
Tactic: grw [restrictScalars_span R S H s, ← hs, spanRank_span_le_card]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u
inst : Semiring R
T : Type v
inst_1 : Semiring T
f : R →+* T
I : Ideal R
⊢ Cardinal.lift.{u, v} (spanRank (R := T) (map f I)) ≤ Cardinal.lift.{v, u} (spanRank I)
have rw : ∃ (s : Set T),
  Cardinal.lift.{u, v} (Cardinal.mk (↑s : Type v)) ≤ Cardinal.lift.{v, u} (Cardinal.mk (↑(generators I) : Type u)) ∧
    Eq (α := Submodule T T) (Submodule.span T s) (map f I)
Tactic: rw [← generators_card I, lift_spanRank_le_iff_exists_span_set_card_le]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u
inst : Semiring R
T : Type v
inst_1 : Semiring T
f : R →+* T
I : Ideal R
⊢ ∃ (s : Set T),
    Cardinal.lift.{u, v} (Cardinal.mk (↑s : Type v)) ≤ Cardinal.lift.{v, u} (Cardinal.mk (↑(generators I) : Type u)) ∧
      Eq (α := Submodule T T) (Submodule.span T s) (map f I)
have refine : LE.le (α := Submodule T T) (map f I) (Submodule.span T ((⇑f : (a : R) → T) '' generators I))
Tactic: refine ⟨f '' I.generators, Cardinal.mk_image_le_lift, le_antisymm (span_le.2 (fun s ⟨r, hr, hfr⟩ ↦
    hfr ▸ mem_map_of_mem _ <| span_generators I ▸ subset_span hr)) ?_⟩
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u
inst : Semiring R
T : Type v
inst_1 : Semiring T
f : R →+* T
I : Ideal R
⊢ LE.le (α := Submodule T T) (map f I) (Submodule.span T ((⇑f : (a : R) → T) '' generators I))
have refine : ∀ (r : R) (hr : r ∈ I),
  Membership.mem (γ := Submodule R R) (comap f (Submodule.span T ((⇑f : (a : R) → T) '' generators I))) r
Tactic: refine map_le_of_le_comap (fun r hr ↦ ?_)
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u
inst : Semiring R
T : Type v
inst_1 : Semiring T
f : R →+* T
I : Ideal R
r : R
hr : r ∈ I
⊢ Membership.mem.{v, v} (α := T) (γ := Ideal T) (span ((⇑f : (a : R) → T) '' generators I)) ((f : (a : R) → T) r : T)
have rw : Membership.mem.{v, v} (α := T) (γ := Ideal T) (map f I) ((f : (a : R) → T) r : T)
Tactic: rw [← map_span, ← submodule_span_eq, span_generators]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u
inst : Semiring R
T : Type v
inst_1 : Semiring T
f : R ≃+* T
I : Ideal R
⊢ Cardinal.lift.{u, v} (Submodule.spanRank (R := T) (map f I)) = Cardinal.lift.{v, u} (Submodule.spanRank I)
have apply : Cardinal.lift.{v, u} (Submodule.spanRank I) ≤
  Cardinal.lift.{u, v} (Submodule.spanRank (R := T) (map (F := R →+* T) (↑f : R →+* T) I))
Tactic: apply (I.lift_spanRank_map_le (f : R →+* T)).antisymm
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u
inst : Semiring R
T : Type v
inst_1 : Semiring T
f : R ≃+* T
I : Ideal R
⊢ Cardinal.lift.{v, u} (Submodule.spanRank I) ≤
    Cardinal.lift.{u, v} (Submodule.spanRank (R := T) (map (F := R →+* T) (↑f : R →+* T) I))
have nth_rw : Cardinal.lift.{v, u}
    (Submodule.spanRank (R := R)
      (map (R := T) (F := T →+* R) (↑f.symm : T →+* R) (map (F := R →+* T) (↑f : R →+* T) I))) ≤
  Cardinal.lift.{u, v} (Submodule.spanRank (R := T) (map (F := R →+* T) (↑f : R →+* T) I))
Tactic: nth_rw 1 [← Ideal.map_of_equiv f (I := I)]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u
inst : Semiring R
T : Type v
inst_1 : Semiring T
f : R →+* T
I : Ideal R
hI : I.FG
⊢ Submodule.spanFinrank.{v, v} (R := T) (map f I) ≤ Submodule.spanFinrank I
have rw : Cardinal.lift.{u, v} (Submodule.spanRank (R := T) (map f I)) ≤ Cardinal.lift.{v, u} (Submodule.spanRank I)
Tactic: rw [← Submodule.FG.spanRank_le_iff (hI.map f), ← Cardinal.lift_le.{u}, Cardinal.lift_natCast,
    ← Cardinal.lift_natCast.{v}, ← Submodule.FG.spanRank_eq_spanFinrank hI]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u
inst : Semiring R
T : Type v
inst_1 : Semiring T
f : R ≃+* T
I : Ideal R
⊢ Submodule.spanFinrank.{v, v} (R := T) (map f I) = Submodule.spanFinrank I
have rw : (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (Submodule.spanRank (R := T) (map f I)) = Submodule.spanFinrank I
Tactic: rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v},
    ← Cardinal.toNat_lift.{v, u}, I.lift_spanRank_map_eq_of_ringEquiv f]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u
inst : Semiring R
T : Type v
inst_1 : Semiring T
f : R ≃+* T
I : Ideal R
rw : (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (Submodule.spanRank (R := T) (map f I)) = Submodule.spanFinrank I
⊢ Submodule.spanFinrank.{v, v} (R := T) (map f I) = Submodule.spanFinrank I
have rw₁ : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (Submodule.spanRank (R := T) (map f I)) : ℕ)
  ((Cardinal.toNat : (a : Cardinal.{u}) → ℕ) (Submodule.spanRank I) : ℕ)
Tactic: rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v},
    ← Cardinal.toNat_lift.{v, u}, I.lift_spanRank_map_eq_of_ringEquiv f]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u
inst : Semiring R
T : Type v
inst_1 : Semiring T
f : R ≃+* T
I : Ideal R
rw : (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (Submodule.spanRank (R := T) (map f I)) = Submodule.spanFinrank I
rw₁ :
  Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (Submodule.spanRank (R := T) (map f I)) : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{u}) → ℕ) (Submodule.spanRank I) : ℕ)
⊢ Submodule.spanFinrank.{v, v} (R := T) (map f I) = Submodule.spanFinrank I
have rw₂ : Eq (α := ℕ)
  ((Cardinal.toNat : (a : Cardinal.{max u v}) → ℕ) (Cardinal.lift.{u, v} (Submodule.spanRank (R := T) (map f I))) : ℕ)
  ((Cardinal.toNat : (a : Cardinal.{u}) → ℕ) (Submodule.spanRank I) : ℕ)
Tactic: rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v},
    ← Cardinal.toNat_lift.{v, u}, I.lift_spanRank_map_eq_of_ringEquiv f]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u
inst : Semiring R
T : Type v
inst_1 : Semiring T
f : R ≃+* T
I : Ideal R
rw : (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (Submodule.spanRank (R := T) (map f I)) = Submodule.spanFinrank I
rw₁ :
  Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (Submodule.spanRank (R := T) (map f I)) : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{u}) → ℕ) (Submodule.spanRank I) : ℕ)
rw₂ :
  Eq (α := ℕ)
    ((Cardinal.toNat : (a : Cardinal.{max u v}) → ℕ) (Cardinal.lift.{u, v} (Submodule.spanRank (R := T) (map f I))) : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{u}) → ℕ) (Submodule.spanRank I) : ℕ)
⊢ Submodule.spanFinrank.{v, v} (R := T) (map f I) = Submodule.spanFinrank I
have rw₃ : Eq (α := ℕ)
  ((Cardinal.toNat : (a : Cardinal.{max u v}) → ℕ) (Cardinal.lift.{u, v} (Submodule.spanRank (R := T) (map f I))) : ℕ)
  ((Cardinal.toNat : (a : Cardinal.{max v u}) → ℕ) (Cardinal.lift.{v, u} (Submodule.spanRank I)) : ℕ)
Tactic: rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v},
    ← Cardinal.toNat_lift.{v, u}, I.lift_spanRank_map_eq_of_ringEquiv f]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u
inst : Semiring R
T : Type v
inst_1 : Semiring T
f : R ≃+* T
I : Ideal R
rw : (Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (Submodule.spanRank (R := T) (map f I)) = Submodule.spanFinrank I
rw₁ :
  Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{v}) → ℕ) (Submodule.spanRank (R := T) (map f I)) : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{u}) → ℕ) (Submodule.spanRank I) : ℕ)
rw₂ :
  Eq (α := ℕ)
    ((Cardinal.toNat : (a : Cardinal.{max u v}) → ℕ) (Cardinal.lift.{u, v} (Submodule.spanRank (R := T) (map f I))) : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{u}) → ℕ) (Submodule.spanRank I) : ℕ)
rw₃ :
  Eq (α := ℕ)
    ((Cardinal.toNat : (a : Cardinal.{max u v}) → ℕ) (Cardinal.lift.{u, v} (Submodule.spanRank (R := T) (map f I))) : ℕ)
    ((Cardinal.toNat : (a : Cardinal.{max v u}) → ℕ) (Cardinal.lift.{v, u} (Submodule.spanRank I)) : ℕ)
⊢ Submodule.spanFinrank.{v, v} (R := T) (map f I) = Submodule.spanFinrank I
have rw₄ : Eq (α := ℕ) ((Cardinal.toNat : (a : Cardinal.{max u v}) → ℕ) (Cardinal.lift.{v, u} (Submodule.spanRank I)) : ℕ)
  ((Cardinal.toNat : (a : Cardinal.{max v u}) → ℕ) (Cardinal.lift.{v, u} (Submodule.spanRank I)) : ℕ)
Tactic: rw [Submodule.spanFinrank, Submodule.spanFinrank, ← Cardinal.toNat_lift.{u, v},
    ← Cardinal.toNat_lift.{v, u}, I.lift_spanRank_map_eq_of_ringEquiv f]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : RankCondition R
ι : Type u_3
v : Basis ι R M
⊢ #(↑(Set.range.{u_2, u_3 + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type u_2) = spanRank.{u_2, u_1} (R := R) (M := M) ⊤
have hs : LinearIndepOn.{u_2, u_1, u_2} (ι := M) R id (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑v : (a : ι) → M))
Tactic: rw [← v.span_eq, spanRank_span_of_linearIndepOn]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRank (hypothesis)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Free R M
inst_4 : StrongRankCondition R
⊢ Module.rank R M = spanRank.{u_2, u_1} (R := R) (M := M) ⊤
have this : Nontrivial R
Tactic: haveI := nontrivial_of_invariantBasisNumber R