awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
hI : I.FG
rw : Cardinal.lift.{u, v} (Submodule.spanRank (R := T) (map f I)) ≤ Cardinal.lift.{v, u} (Submodule.spanRank I)
⊢ Submodule.spanFinrank.{v, v} (R := T) (map f I) ≤ Submodule.spanFinrank 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]

Premises used: Submodule.FG.spanRank_eq_spanFinrank, Ideal.FG.map, Cardinal.lift_natCast, Submodule.FG.spanRank_le_iff
-- 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
hI : I.FG
⊢ Cardinal.lift.{u, v} (Submodule.spanRank (R := T) (map f I)) ≤ Cardinal.lift.{v, u} (Submodule.spanRank I)

Tactic:
I.lift_spanRank_map_le f

Premises used: 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
hI : I.FG
⊢ Cardinal.lift.{u, v} (Submodule.spanRank (R := T) (map f I)) ≤ Cardinal.lift.{v, u} (Submodule.spanRank I)

Tactic:
exact I.lift_spanRank_map_le f

Premises used: 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
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)) : ℕ)
rw₄ 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)) : ℕ)
⊢ Submodule.spanFinrank.{v, v} (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]

Premises used: Ideal.lift_spanRank_map_eq_of_ringEquiv, Submodule.spanFinrank
-- Module: Mathlib.Algebra.Module.SpanRank
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
hs : LinearIndepOn.{u_2, u_1, u_2} (ι := M) R id (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑v : (a : ι) → M))
⊢ #(↑(Set.range.{u_2, u_3 + 1} (ι := ι) (⇑v : (a : ι) → M)) : Type u_2) = spanRank.{u_2, u_1} (R := R) (M := M) ⊤

Tactic:
rw [← v.span_eq, spanRank_span_of_linearIndepOn]

Premises used: Submodule.spanRank_span_of_linearIndepOn, Module.Basis.span_eq
-- Module: Mathlib.Algebra.Module.SpanRank
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
⊢ LinearIndepOn.{u_2, u_1, u_2} (ι := M) R id (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑v : (a : ι) → M))

Tactic:
v.linearIndependent.linearIndepOn_id

Premises used: LinearIndependent.linearIndepOn_id, Module.Basis.linearIndependent
-- Module: Mathlib.Algebra.Module.SpanRank
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
⊢ LinearIndepOn.{u_2, u_1, u_2} (ι := M) R id (Set.range.{u_2, u_3 + 1} (ι := ι) (⇑v : (a : ι) → M))

Tactic:
exact v.linearIndependent.linearIndepOn_id

Premises used: LinearIndependent.linearIndepOn_id, Module.Basis.linearIndependent
-- Module: Mathlib.Algebra.Module.SpanRank
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
⊢ Nontrivial R

Tactic:
haveI := nontrivial_of_invariantBasisNumber R
-- Module: Mathlib.Algebra.Module.SpanRank
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
this : Nontrivial R
obtain : ∀ (I : Type u_2) (B : Basis I R M), Module.rank R M = spanRank.{u_2, u_1} (R := R) (M := M) ⊤
⊢ Module.rank R M = spanRank.{u_2, u_1} (R := R) (M := M) ⊤

Tactic:
obtain ⟨I, B⟩ := ‹Module.Free R M›

Premises used: Module.Free
-- Module: Mathlib.Algebra.Module.SpanRank
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
this : Nontrivial R
I : Type u_2
B : Basis I R M
rw : #I = spanRank.{u_2, u_1} (R := R) (M := M) ⊤
rw₁ : #I = #(↑(Set.range (ι := I) (⇑B : (a : I) → M)) : Type u_2)
rw₂ : #I = lift.{u_2, u_2} #(↑(Set.range (ι := I) (⇑B : (a : I) → M)) : Type u_2)
rw₃ : #I = lift.{u_2, u_2} #I
rw₄ rw₅ : #I = #I
⊢ Module.rank R M = spanRank.{u_2, u_1} (R := R) (M := M) ⊤

Tactic:
rw [← Basis.mk_eq_rank'' B, ← Basis.mk_eq_spanRank B, ← Cardinal.lift_id #(Set.range B),
    Cardinal.mk_range_eq_of_injective B.injective, Cardinal.lift_id _]

Premises used: Cardinal.mk_range_eq_of_injective, Cardinal.mk, Set.Elem, Module.Basis.injective, Set.range, DFunLike.coe, Module.Basis.mk_eq_spanRank, Module.Basis.mk_eq_rank'', Cardinal.lift_id
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
inst_4 : Free R M
⊢ finrank R M = spanFinrank.{u_2, u_1} (R := R) (M := M) ⊤

Tactic:
simp [Module.finrank, Submodule.spanFinrank, Submodule.rank_eq_spanRank_of_free]

Premises used: Submodule.rank_eq_spanRank_of_free, Submodule.spanFinrank, Module.finrank
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
rw :
  LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type u_2))
    (⨅ (s : { s : Set M // Eq (α := Submodule R M) (span R s) ⊤ }), #(↑(↑s : Set M) : Type u_2))
⊢ Module.rank R M ≤ spanRank.{u_2, u_1} (R := R) (M := M) ⊤

Tactic:
rw [Module.rank, Submodule.spanRank]

Premises used: Module.rank, Submodule.spanRank
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
⊢ LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type u_2))
    (⨅ (s : { s : Set M // Eq (α := Submodule R M) (span R s) ⊤ }), #(↑(↑s : Set M) : Type u_2))

Tactic:
ciSup_le' (fun ι ↦ (le_ciInf fun s ↦ ?_))

Premises used: ciSup_le', le_ciInf
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
refine :
  ∀ (ι : { s : Set M // LinearIndepOn R id s }) (s : { s : Set M // Eq (α := Submodule R M) (span R s) ⊤ }),
    #(↑(↑ι : Set M) : Type u_2) ≤ #(↑(↑s : Set M) : Type u_2)
⊢ LE.le.{u_2 + 1} (α := Cardinal.{u_2}) (⨆ (ι : { s : Set M // LinearIndepOn R id s }), #(↑(↑ι : Set M) : Type u_2))
    (⨅ (s : { s : Set M // Eq (α := Submodule R M) (span R s) ⊤ }), #(↑(↑s : Set M) : Type u_2))

Tactic:
refine ciSup_le' (fun ι ↦ (le_ciInf fun s ↦ ?_))

Premises used: ciSup_le', le_ciInf
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : { s : Set M // LinearIndepOn R id s }
s : { s : Set M // Eq (α := Submodule R M) (span R s) ⊤ }
⊢ #(↑(↑ι : Set M) : Type u_2) ≤ #(↑(↑s : Set M) : Type u_2)

Tactic:
have := linearIndependent_le_span'' ι.2 s.1 s.2
-- Module: Mathlib.Algebra.Module.SpanRank
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : StrongRankCondition R
ι : { s : Set M // LinearIndepOn R id s }
s : { s : Set M // Eq (α := Submodule R M) (span R s) ⊤ }
this : #(↑(↑ι : Set M) : Type u_2) ≤ #(↑(↑s : Set M) : Type u_2)
⊢ #(↑(↑ι : Set M) : Type u_2) ≤ #(↑(↑s : Set M) : Type u_2)

Tactic:
simpa
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Submodule R M
obtain :
  ∀ (s : Set M) (hs₁ : Cardinal.mk (↑s : Type u_3) = N.spanRank) (hs₂ : span R s = N),
    spanRank (M := A ⊗[R] M) (baseChange A N) ≤ Cardinal.lift.{u_2, u_3} N.spanRank
⊢ spanRank (M := A ⊗[R] M) (baseChange A N) ≤ Cardinal.lift.{u_2, u_3} N.spanRank

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

Premises used: Submodule.exists_span_set_card_eq_spanRank
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk (↑s : Type u_3) = N.spanRank
hs₂ : span R s = N
grw :
  Cardinal.mk
      (↑((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s) : Type (max u_2 u_3)) ≤
    Cardinal.lift.{u_2, u_3} (Cardinal.mk (↑s : Type u_3))
⊢ spanRank (M := A ⊗[R] M) (baseChange A N) ≤ Cardinal.lift.{u_2, u_3} N.spanRank

Tactic:
grw [← hs₁, ← hs₂, baseChange_span, spanRank_span_le_card]

Premises used: Submodule.spanRank_span_le_card, Submodule.baseChange_span
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk (↑s : Type u_3) = N.spanRank
hs₂ : span R s = N
⊢ Cardinal.lift.{u_3, max u_2 u_3}
      (Cardinal.mk
        (↑((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s) :
          Type (max u_2 u_3))) ≤
    Cardinal.lift.{max u_2 u_3, u_3} (Cardinal.mk (↑s : Type u_3))

Tactic:
Cardinal.mk_image_le_lift (f := TensorProduct.mk R A M 1) (s := s)

Premises used: Cardinal.mk_image_le_lift
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk (↑s : Type u_3) = N.spanRank
hs₂ : span R s = N
h :
  Cardinal.mk
      (↑((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s) : Type (max u_2 u_3)) =
    Cardinal.lift.{u_3, max u_2 u_3}
      (Cardinal.mk
        (↑((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s) :
          Type (max u_2 u_3)))
h₁ : Cardinal.lift.{u_2, u_3} = Cardinal.lift.{max u_2 u_3, u_3}
⊢ Cardinal.mk
      (↑((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s) : Type (max u_2 u_3)) ≤
    Cardinal.lift.{u_2, u_3} (Cardinal.mk (↑s : Type u_3))

Tactic:
convert! Cardinal.mk_image_le_lift (f := TensorProduct.mk R A M 1) (s := s)

Premises used: Cardinal.mk_image_le_lift
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk (↑s : Type u_3) = N.spanRank
hs₂ : span R s = N
⊢ Cardinal.mk
      (↑((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s) : Type (max u_2 u_3)) =
    Cardinal.lift.{u_3, max u_2 u_3}
      (Cardinal.mk
        (↑((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s) :
          Type (max u_2 u_3)))

Tactic:
(Cardinal.lift_id' _).symm

Premises used: Cardinal.lift_id', Eq.symm
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk (↑s : Type u_3) = N.spanRank
hs₂ : span R s = N
⊢ Cardinal.mk
      (↑((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s) : Type (max u_2 u_3)) =
    Cardinal.lift.{u_3, max u_2 u_3}
      (Cardinal.mk
        (↑((⇑((TensorProduct.mk R A M : (a : A) → M →ₗ[R] A ⊗[R] M) 1) : (a : M) → A ⊗[R] M) '' s) :
          Type (max u_2 u_3)))

Tactic:
exact (Cardinal.lift_id' _).symm

Premises used: Cardinal.lift_id', Eq.symm
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk (↑s : Type u_3) = N.spanRank
hs₂ : span R s = N
⊢ Cardinal.lift.{u_2, u_3} = Cardinal.lift.{max u_2 u_3, u_3}

Tactic:
Cardinal.lift_umax.symm

Premises used: Cardinal.lift_umax, Eq.symm
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Submodule R M
s : Set M
hs₁ : Cardinal.mk (↑s : Type u_3) = N.spanRank
hs₂ : span R s = N
⊢ Cardinal.lift.{u_2, u_3} = Cardinal.lift.{max u_2 u_3, u_3}

Tactic:
exact Cardinal.lift_umax.symm

Premises used: Cardinal.lift_umax, Eq.symm
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Submodule R M
fg : N.FG
h₁ : Cardinal.lift.{u_2, u_3} N.spanRank < Cardinal.aleph0
⊢ spanFinrank (M := A ⊗[R] M) (baseChange A N) ≤ N.spanFinrank

Tactic:
grw [spanFinrank, spanRank_baseChange_le, Cardinal.toNat_lift, spanFinrank]

Premises used: Submodule.spanRank_baseChange_le, Cardinal.toNat_lift, Submodule.spanFinrank
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Submodule R M
fg : N.FG
⊢ Cardinal.lift.{u_2, u_3} N.spanRank < Cardinal.aleph0

Tactic:
simp [Cardinal.lift_lt_aleph0, spanRank_finite_iff_fg.mpr fg]

Premises used: Iff.mpr, Submodule.spanRank_finite_iff_fg, Cardinal.lift_lt_aleph0
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Submodule R M
grw : spanRank (M := TensorProduct.{u_1, u_2, u_3} R A ↥N) (baseChange A ⊤) ≤ Cardinal.lift.{u_2, u_3} N.spanRank
grw₁ :
  spanRank (M := TensorProduct.{u_1, u_2, u_3} R A ↥N) (baseChange A ⊤) ≤
    Cardinal.lift.{u_2, u_3} (spanRank.{u_3, u_1} (R := R) (M := ↥N) ⊤)
grw₂ grw₃ :
  Cardinal.lift.{u_2, u_3} (spanRank.{u_3, u_1} (R := R) (M := ↥N) ⊤) ≤
    Cardinal.lift.{u_2, u_3} (spanRank.{u_3, u_1} (R := R) (M := ↥N) ⊤)
⊢ spanRank (R := A) (M := TensorProduct.{u_1, u_2, u_3} R A ↥N) ⊤ ≤ Cardinal.lift.{u_2, u_3} N.spanRank

Tactic:
grw [← Submodule.baseChange_top, ← N.spanRank_top, spanRank_baseChange_le]

Premises used: Submodule.spanRank_baseChange_le, Submodule.spanRank_top, Submodule.baseChange_top
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
M : Type u_3
inst_3 : AddCommGroup M
inst_4 : Module R M
N : Submodule R M
fg : N.FG
grw : spanFinrank (M := TensorProduct.{u_1, u_2, u_3} R A ↥N) (baseChange A ⊤) ≤ N.spanFinrank
grw₁ :
  spanFinrank (M := TensorProduct.{u_1, u_2, u_3} R A ↥N) (baseChange A ⊤) ≤ spanFinrank.{u_3, u_1} (R := R) (M := ↥N) ⊤
grw₂ grw₃ : spanFinrank.{u_3, u_1} (R := R) (M := ↥N) ⊤ ≤ spanFinrank.{u_3, u_1} (R := R) (M := ↥N) ⊤
⊢ spanFinrank (R := A) (M := TensorProduct.{u_1, u_2, u_3} R A ↥N) ⊤ ≤ N.spanFinrank

Tactic:
grw [← Submodule.baseChange_top, ← N.spanFinrank_top, (N.fg_top.mpr fg).spanFinrank_baseChange_le]

Premises used: Iff.mpr, Submodule.spanFinrank_top, Submodule.FG.spanFinrank_baseChange_le, Submodule.fg_top, Submodule.baseChange_top
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsLocalRing R
fg : N.FG
this : Module.Finite.{u_1, u_3} R ↥N := ⋯
apply : N.spanFinrank ≤ spanFinrank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
⊢ spanFinrank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤ = N.spanFinrank

Tactic:
apply (TensorProduct.spanFinrank_top_le_of_fg N fg).antisymm

Premises used: LE.le.antisymm, TensorProduct.spanFinrank_top_le_of_fg
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsLocalRing R
fg : N.FG
this : Module.Finite.{u_1, u_3} R ↥N := ⋯
obtain :
  ∀ (s : Set (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N))
    (hs₁ : Cardinal.mk (↑s : Type (max u_1 u_3)) = spanRank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤)
    (hs₂ : Eq (α := Submodule 𝓀 (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span 𝓀 s) ⊤),
    N.spanFinrank ≤ spanFinrank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
⊢ N.spanFinrank ≤ spanFinrank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤

Tactic:
obtain ⟨s, hs₁, hs₂⟩ := (⊤ : Submodule 𝓀 (𝓀 ⊗[R] N)).exists_span_set_card_eq_spanRank
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsLocalRing R
fg : N.FG
this : Module.Finite.{u_1, u_3} R ↥N := ⋯
s : Set (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)
hs₁ : Cardinal.mk (↑s : Type (max u_1 u_3)) = spanRank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
hs₂ : Eq (α := Submodule 𝓀 (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span 𝓀 s) ⊤
⊢ Cardinal.mk (↑s : Type (max u_1 u_3)) < Cardinal.aleph0

Tactic:
simpa [hs₁] using Module.Finite.fg_top

Premises used: Module.Finite.fg_top
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsLocalRing R
fg : N.FG
this : Module.Finite.{u_1, u_3} R ↥N := ⋯
s : Set (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)
hs₁ : Cardinal.mk (↑s : Type (max u_1 u_3)) = spanRank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
hs₂ : Eq (α := Submodule 𝓀 (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span 𝓀 s) ⊤
⊢ s.Finite

Tactic:
have hs₃ : s.Finite := Cardinal.mk_lt_aleph0_iff.mp (by simpa [hs₁] using Module.Finite.fg_top)
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsLocalRing R
fg : N.FG
this : Module.Finite.{u_1, u_3} R ↥N := ⋯
s : Set (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)
hs₁ : Cardinal.mk (↑s : Type (max u_1 u_3)) = spanRank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
hs₂ : Eq (α := Submodule 𝓀 (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span 𝓀 s) ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
rw : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) ∘ Function.surjInv ⋯ '' s = s
rw₁ : id '' s = s
rw₂ rw₃ : s = s
⊢ (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s

Tactic:
rw [← Set.image_comp, Function.comp_surjInv, s.image_id]

Premises used: Function.comp_surjInv, Set.image_comp, Set.image_id
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsLocalRing R
fg : N.FG
this : Module.Finite.{u_1, u_3} R ↥N := ⋯
s : Set (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)
hs₁ : Cardinal.mk (↑s : Type (max u_1 u_3)) = spanRank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
hs₂ : Eq (α := Submodule 𝓀 (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span 𝓀 s) ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
⊢ (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s

Tactic:
have ht₁ : mk R 𝓀 N 1 '' t = s := by rw [← Set.image_comp, Function.comp_surjInv, s.image_id]
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsLocalRing R
fg : N.FG
this : Module.Finite.{u_1, u_3} R ↥N := ⋯
s : Set (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)
hs₁ : Cardinal.mk (↑s : Type (max u_1 u_3)) = spanRank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
hs₂ : Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (restrictScalars R (R := 𝓀) (span 𝓀 s)) ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s
⊢ Function.Surjective (α := R) (β := 𝓀) (⇑(algebraMap R 𝓀) : (a : R) → 𝓀)

Tactic:
residue_surjective

Premises used: Submodule.Quotient.mk, IsLocalRing.residue_surjective
-- Module: Mathlib.Algebra.Module.SpanRankOperations
Goal:
R : Type u_1
inst : CommRing R
M : Type u_3
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Submodule R M
inst_3 : IsLocalRing R
fg : N.FG
this : Module.Finite.{u_1, u_3} R ↥N := ⋯
s : Set (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)
hs₁ : Cardinal.mk (↑s : Type (max u_1 u_3)) = spanRank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
hs₂ : Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (restrictScalars R (R := 𝓀) (span 𝓀 s)) ⊤
hs₃ : s.Finite
t : Set ↥N := Function.surjInv ⋯ '' s
ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s
⊢ Function.Surjective (α := R) (β := 𝓀) (⇑(algebraMap R 𝓀) : (a : R) → 𝓀)

Tactic:
exact residue_surjective

Premises used: IsLocalRing.residue_surjective