awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hp : p.FG
rw : Cardinal.lift.{u, v} (map f p).spanRank ≤ Cardinal.lift.{v, u} p.spanRank
⊢ (map f p).spanFinrank ≤ p.spanFinrank

Tactic:
rw [← (hp.map f).spanRank_le_iff, ← Cardinal.lift_le.{u}, Cardinal.lift_natCast,
    ← Cardinal.lift_natCast.{v}, ← hp.spanRank_eq_spanFinrank]

Premises used: Submodule.FG.spanRank_eq_spanFinrank, Submodule.FG.map, Cardinal.lift_natCast, Submodule.FG.spanRank_le_iff
-- 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
hp : p.FG
⊢ Cardinal.lift.{u, v} (map f p).spanRank ≤ Cardinal.lift.{v, u} p.spanRank

Tactic:
p.lift_spanRank_map_le f

Premises used: Submodule.lift_spanRank_map_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
hp : p.FG
⊢ Cardinal.lift.{u, v} (map f p).spanRank ≤ Cardinal.lift.{v, u} p.spanRank

Tactic:
exact p.lift_spanRank_map_le f

Premises used: Submodule.lift_spanRank_map_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
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

Tactic:
(lift_spanRank_map_le f p).antisymm ?_

Premises used: Submodule.lift_spanRank_map_le, LE.le.antisymm
-- 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
hf : Function.Injective.{u + 1, v + 1} (α := M) (β := L) (⇑f : (a : M) → L)
p : Submodule R M
refine : Cardinal.lift.{v, u} p.spanRank ≤ Cardinal.lift.{u, v} (map f p).spanRank
⊢ Cardinal.lift.{u, v} (map f p).spanRank = Cardinal.lift.{v, u} p.spanRank

Tactic:
refine (lift_spanRank_map_le f p).antisymm ?_

Premises used: Submodule.lift_spanRank_map_le, LE.le.antisymm
-- 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
hf : Function.Injective.{u + 1, v + 1} (α := M) (β := L) (⇑f : (a : M) → L)
p : Submodule R M
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
⊢ 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

Premises used: Submodule.exists_span_set_card_eq_spanRank, Submodule.map
-- 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
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
⊢ ∃ (y : Set M), (⇑f : (a : M) → L) '' y = s

Tactic:
Set.subset_range_iff_exists_image_eq.mp
    ((subset_span.trans e.le).trans LinearMap.map_le_range)

Premises used: HasSubset.Subset.trans, Eq.le, Set.subset_range_iff_exists_image_eq, LinearMap.map_le_range, Iff.mp, Submodule.subset_span
-- 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
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
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
⊢ 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)

Premises used: HasSubset.Subset.trans, Eq.le, Set.subset_range_iff_exists_image_eq, LinearMap.map_le_range, Iff.mp, Submodule.subset_span, rfl
-- 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
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
⊢ span R s = p

Tactic:
simpa [(map_injective_of_injective hf).eq_iff] using e

Premises used: Function.Injective.eq_iff, Submodule.map_injective_of_injective
-- 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
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
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
⊢ Cardinal.lift.{v, u} p.spanRank ≤ Cardinal.lift.{u, v} (map f p).spanRank

Tactic:
obtain rfl : span R s = p := by simpa [(map_injective_of_injective hf).eq_iff] using e

Premises used: Submodule.span, rfl
-- 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
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)
grw₃ grw₄ : Cardinal.mk (↑s : Type u) ≤ Cardinal.mk (↑s : Type u)
⊢ Cardinal.lift.{v, u} (spanRank (span R s)) ≤ Cardinal.lift.{u, v} (map f (span R s)).spanRank

Tactic:
grw [← hs, Cardinal.mk_image_eq_lift _ _ hf, Cardinal.lift_le, spanRank_span_le_card]

Premises used: Submodule.spanRank_span_le_card, Cardinal.mk_image_eq_lift, Cardinal.lift_le
-- 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
hf : Function.Injective (α := M) (β := N) (⇑f : (a : M) → N)
p : Submodule R M
⊢ (map f p).spanRank = p.spanRank

Tactic:
simpa using lift_spanRank_map_eq_of_injective f hf p

Premises used: Submodule.lift_spanRank_map_eq_of_injective
-- 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
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) : ℕ)
rw₄ 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) : ℕ)
⊢ (map f p).spanFinrank = 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]

Premises used: Submodule.spanFinrank, Submodule.lift_spanRank_map_eq_of_injective
-- 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
⊢ f.range.spanRank ≤ spanRank.{u, u_1} (R := R) (M := M) ⊤

Tactic:
simpa using spanRank_map_le f ⊤

Premises used: Submodule.spanRank_map_le, Top.top
-- 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
⊢ spanRank.{u, u_1} (R := R) (M := ↥p) ⊤ = p.spanRank

Tactic:
simpa using (spanRank_map_eq_of_injective _ p.subtype_injective ⊤).symm

Premises used: Submodule.spanRank_map_eq_of_injective, Top.top, Eq.symm, Submodule.subtype_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
p : Submodule R M
⊢ spanFinrank.{u, u_1} (R := R) (M := ↥p) ⊤ = p.spanFinrank

Tactic:
simp [Submodule.spanFinrank]

Premises used: Submodule.spanFinrank
-- 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
σ' : 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) ⊤
rw₂ rw₃ : spanRank.{u, u_2} (R := S) (M := N) ⊤ = spanRank.{u, u_2} (R := S) (M := N) ⊤
⊢ spanRank.{u, u_1} (R := R) (M := M) ⊤ = spanRank.{u, u_2} (R := S) (M := N) ⊤

Tactic:
rw [← spanRank_map_eq_of_injective e.toLinearMap e.injective ⊤, map_top, LinearEquiv.range]

Premises used: Submodule.map_top, Submodule.spanRank_map_eq_of_injective, LinearEquiv.toLinearMap, LinearEquiv.injective, Top.top, LinearEquiv.range
-- Module: Mathlib.Algebra.Module.SpanRank
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
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)
⊢ N.spanRank ≤ spanRank (restrictScalars R N)

Tactic:
obtain ⟨s, hs, e⟩ := (N.restrictScalars R).exists_span_set_card_eq_spanRank

Premises used: Submodule.restrictScalars, Submodule.exists_span_set_card_eq_spanRank
-- Module: Mathlib.Algebra.Module.SpanRank
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)
⊢ span S s = N

Tactic:
le_antisymm (span_le.mpr (span_le.mp e.le :)) (e.ge.trans (span_le_restrictScalars R S s))

Premises used: Iff.mpr, Eq.ge, Submodule.span_le_restrictScalars, Eq.le, le_antisymm, Iff.mp, LE.le.trans, Submodule.span_le
-- Module: Mathlib.Algebra.Module.SpanRank
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)
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))
⊢ N.spanRank ≤ spanRank (restrictScalars R N)

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))

Premises used: Submodule.span, rfl
-- Module: Mathlib.Algebra.Module.SpanRank
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)
grw₁ grw₂ : Cardinal.mk (↑s : Type u) ≤ Cardinal.mk (↑s : Type u)
⊢ spanRank (span S s) ≤ spanRank (restrictScalars R (span S s))

Tactic:
grw [← hs, spanRank_span_le_card]

Premises used: Submodule.spanRank_span_le_card
-- Module: Mathlib.Algebra.Module.SpanRank
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

Tactic:
N.le_spanRank_restrictScalars.antisymm' ?_

Premises used: LE.le.antisymm', Submodule.le_spanRank_restrictScalars
-- Module: Mathlib.Algebra.Module.SpanRank
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
refine : spanRank (restrictScalars R N) ≤ N.spanRank
⊢ spanRank (restrictScalars R N) = N.spanRank

Tactic:
refine N.le_spanRank_restrictScalars.antisymm' ?_

Premises used: LE.le.antisymm', Submodule.le_spanRank_restrictScalars
-- Module: Mathlib.Algebra.Module.SpanRank
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
obtain :
  ∀ (s : Set M) (hs : Cardinal.mk (↑s : Type u) = spanRank (span S s)),
    spanRank (restrictScalars R (span S s)) ≤ spanRank (span S s)
⊢ spanRank (restrictScalars R N) ≤ N.spanRank

Tactic:
obtain ⟨s, hs, rfl⟩ := N.exists_span_set_card_eq_spanRank

Premises used: Submodule.exists_span_set_card_eq_spanRank, rfl
-- Module: Mathlib.Algebra.Module.SpanRank
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)
grw₂ grw₃ : Cardinal.mk (↑s : Type u) ≤ Cardinal.mk (↑s : Type u)
⊢ spanRank (restrictScalars R (span S s)) ≤ spanRank (span S s)

Tactic:
grw [restrictScalars_span R S H s, ← hs, spanRank_span_le_card]

Premises used: Submodule.spanRank_span_le_card, Submodule.restrictScalars_span
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u
inst : Semiring R
T : Type v
inst_1 : Semiring T
f : R →+* T
I : Ideal R
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)
⊢ Cardinal.lift.{u, v} (spanRank (R := T) (map f I)) ≤ Cardinal.lift.{v, u} (spanRank I)

Tactic:
rw [← generators_card I, 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
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)

Tactic:
⟨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)) ?_⟩

Premises used: Ideal.span_le, Iff.mpr, Membership.mem, Submodule.generators, Ideal.map, le_antisymm, SetLike.coe, And.intro, Exists.intro, Set.image, Cardinal.mk_image_le_lift, _private.0.Ideal.lift_spanRank_map_le.match_1, DFunLike.coe
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u
inst : Semiring R
T : Type v
inst_1 : Semiring T
f : R →+* T
I : Ideal R
refine : LE.le (α := Submodule T T) (map f I) (Submodule.span T ((⇑f : (a : R) → T) '' generators I))
⊢ ∃ (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:
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)) ?_⟩
-- Module: Mathlib.Algebra.Module.SpanRank
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))

Tactic:
map_le_of_le_comap (fun r hr ↦ ?_)

Premises used: Ideal.map_le_of_le_comap
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u
inst : Semiring R
T : Type v
inst_1 : Semiring T
f : R →+* T
I : Ideal R
refine :
  ∀ (r : R) (hr : r ∈ I),
    Membership.mem (γ := Submodule R R) (comap f (Submodule.span T ((⇑f : (a : R) → T) '' generators I))) r
⊢ LE.le (α := Submodule T T) (map f I) (Submodule.span T ((⇑f : (a : R) → T) '' generators I))

Tactic:
refine map_le_of_le_comap (fun r hr ↦ ?_)

Premises used: Ideal.map_le_of_le_comap
-- Module: Mathlib.Algebra.Module.SpanRank
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
rw : Membership.mem.{v, v} (α := T) (γ := Ideal T) (map f I) ((f : (a : R) → T) r : T)
⊢ Membership.mem.{v, v} (α := T) (γ := Ideal T) (span ((⇑f : (a : R) → T) '' generators I)) ((f : (a : R) → T) r : T)

Tactic:
rw [← map_span, ← submodule_span_eq, span_generators]

Premises used: Ideal.submodule_span_eq, Ideal.map_span, Submodule.span_generators
-- Module: Mathlib.Algebra.Module.SpanRank
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) (map f I) ((f : (a : R) → T) r : T)

Tactic:
mem_map_of_mem f hr

Premises used: Ideal.mem_map_of_mem
-- Module: Mathlib.Algebra.Module.SpanRank
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) (map f I) ((f : (a : R) → T) r : T)

Tactic:
exact mem_map_of_mem f hr

Premises used: Ideal.mem_map_of_mem
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u
inst : Semiring R
T : Type v
inst_1 : Semiring T
f : R ≃+* T
I : Ideal R
apply :
  Cardinal.lift.{v, u} (Submodule.spanRank I) ≤
    Cardinal.lift.{u, v} (Submodule.spanRank (R := T) (map (F := R →+* T) (↑f : R →+* T) I))
⊢ Cardinal.lift.{u, v} (Submodule.spanRank (R := T) (map f I)) = Cardinal.lift.{v, u} (Submodule.spanRank I)

Tactic:
apply (I.lift_spanRank_map_le (f : R →+* T)).antisymm

Premises used: LE.le.antisymm, RingHomClass.toRingHom, Ideal.lift_spanRank_map_le
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u
inst : Semiring R
T : Type v
inst_1 : Semiring T
f : R ≃+* T
I : Ideal R
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))
⊢ Cardinal.lift.{v, u} (Submodule.spanRank 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)]

Premises used: Ideal.map_of_equiv
-- Module: Mathlib.Algebra.Module.SpanRank
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 (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:
Ideal.lift_spanRank_map_le (f.symm : T →+* R) _

Premises used: RingHomClass.toRingHom, Ideal.lift_spanRank_map_le, RingEquiv.symm
-- Module: Mathlib.Algebra.Module.SpanRank
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 (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:
exact Ideal.lift_spanRank_map_le (f.symm : T →+* R) _

Premises used: RingHomClass.toRingHom, Ideal.lift_spanRank_map_le, RingEquiv.symm
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R S : Type u
inst : Semiring R
inst_1 : Semiring S
f : R →+* S
I : Ideal R
⊢ Submodule.spanRank (R := S) (map f I) ≤ Submodule.spanRank I

Tactic:
simpa using I.lift_spanRank_map_le f

Premises used: Ideal.lift_spanRank_map_le
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R S : Type u
inst : Semiring R
inst_1 : Semiring S
f : R ≃+* S
I : Ideal R
⊢ Submodule.spanRank (R := S) (map f I) = Submodule.spanRank I

Tactic:
simpa using I.lift_spanRank_map_eq_of_ringEquiv f

Premises used: Ideal.lift_spanRank_map_eq_of_ringEquiv