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_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
⊢ Module.rank R M = spanRank.{u_2, u_1} (R := R) (M := M) ⊤
have obtain : ∀ (I : Type u_2) (B : Basis I R M), Module.rank R M = spanRank.{u_2, u_1} (R := R) (M := M) ⊤
Tactic: obtain ⟨I, B⟩ := ‹Module.Free R M›
-- 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 : Free R M
inst_4 : StrongRankCondition R
this : Nontrivial R
I : Type u_2
B : Basis I R M
⊢ Module.rank R M = spanRank.{u_2, u_1} (R := R) (M := M) ⊤
have rw : #I = 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 _]
-- 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 : 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) ⊤
⊢ Module.rank R M = spanRank.{u_2, u_1} (R := R) (M := M) ⊤
have rw₁ : #I = #(↑(Set.range (ι := I) (⇑B : (a : I) → M)) : Type u_2)
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 _]
-- 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 : 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)
⊢ Module.rank R M = spanRank.{u_2, u_1} (R := R) (M := M) ⊤
have rw₂ : #I = lift.{u_2, u_2} #(↑(Set.range (ι := I) (⇑B : (a : I) → M)) : Type u_2)
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 _]
-- 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 : 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)
⊢ Module.rank R M = spanRank.{u_2, u_1} (R := R) (M := M) ⊤
have rw₃ : #I = lift.{u_2, u_2} #I
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 _]
-- 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 : 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
⊢ Module.rank R M = spanRank.{u_2, u_1} (R := R) (M := M) ⊤
have rw₄ : #I = #I
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 _]
-- 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 : StrongRankCondition R
⊢ Module.rank R M ≤ spanRank.{u_2, u_1} (R := R) (M := M) ⊤
have 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))
Tactic: rw [Module.rank, Submodule.spanRank]
-- 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 : 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))
have 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)
Tactic: refine ciSup_le' (fun ι ↦ (le_ciInf fun s ↦ ?_))
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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
⊢ spanRank (M := A ⊗[R] M) (baseChange A N) ≤ Cardinal.lift.{u_2, u_3} N.spanRank
have 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
Tactic: obtain ⟨s, hs₁, hs₂⟩ := N.exists_span_set_card_eq_spanRank
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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
⊢ spanRank (M := A ⊗[R] M) (baseChange A N) ≤ Cardinal.lift.{u_2, u_3} N.spanRank
have 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))
Tactic: grw [← hs₁, ← hs₂, baseChange_span, spanRank_span_le_card]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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_2, u_3} (Cardinal.mk (↑s : Type u_3))
have 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)))
Tactic: convert! Cardinal.mk_image_le_lift (f := TensorProduct.mk R A M 1) (s := s)
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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)))
⊢ 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))
have h₁ : Cardinal.lift.{u_2, u_3} = Cardinal.lift.{max u_2 u_3, u_3}
Tactic: convert! Cardinal.mk_image_le_lift (f := TensorProduct.mk R A M 1) (s := s)
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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
⊢ spanFinrank (M := A ⊗[R] M) (baseChange A N) ≤ N.spanFinrank
have h₁ : Cardinal.lift.{u_2, u_3} N.spanRank < Cardinal.aleph0
Tactic: grw [spanFinrank, spanRank_baseChange_le, Cardinal.toNat_lift, spanFinrank]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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
⊢ spanRank (R := A) (M := TensorProduct.{u_1, u_2, u_3} R A ↥N) ⊤ ≤ Cardinal.lift.{u_2, u_3} N.spanRank
have grw : spanRank (M := TensorProduct.{u_1, u_2, u_3} R A ↥N) (baseChange A ⊤) ≤ Cardinal.lift.{u_2, u_3} N.spanRank
Tactic: grw [← Submodule.baseChange_top, ← N.spanRank_top, spanRank_baseChange_le]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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
⊢ spanRank (R := A) (M := TensorProduct.{u_1, u_2, u_3} R A ↥N) ⊤ ≤ Cardinal.lift.{u_2, u_3} N.spanRank
have 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) ⊤)
Tactic: grw [← Submodule.baseChange_top, ← N.spanRank_top, spanRank_baseChange_le]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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) ⊤)
⊢ spanRank (R := A) (M := TensorProduct.{u_1, u_2, u_3} R A ↥N) ⊤ ≤ Cardinal.lift.{u_2, u_3} N.spanRank
have 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) ⊤)
Tactic: grw [← Submodule.baseChange_top, ← N.spanRank_top, spanRank_baseChange_le]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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
⊢ spanFinrank (R := A) (M := TensorProduct.{u_1, u_2, u_3} R A ↥N) ⊤ ≤ N.spanFinrank
have grw : spanFinrank (M := TensorProduct.{u_1, u_2, u_3} R A ↥N) (baseChange A ⊤) ≤ N.spanFinrank
Tactic: grw [← Submodule.baseChange_top, ← N.spanFinrank_top, (N.fg_top.mpr fg).spanFinrank_baseChange_le]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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
⊢ spanFinrank (R := A) (M := TensorProduct.{u_1, u_2, u_3} R A ↥N) ⊤ ≤ N.spanFinrank
have grw₁ : spanFinrank (M := TensorProduct.{u_1, u_2, u_3} R A ↥N) (baseChange A ⊤) ≤ spanFinrank.{u_3, u_1} (R := R) (M := ↥N) ⊤
Tactic: grw [← Submodule.baseChange_top, ← N.spanFinrank_top, (N.fg_top.mpr fg).spanFinrank_baseChange_le]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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) ⊤
⊢ spanFinrank (R := A) (M := TensorProduct.{u_1, u_2, u_3} R A ↥N) ⊤ ≤ N.spanFinrank
have grw₂ : spanFinrank.{u_3, u_1} (R := R) (M := ↥N) ⊤ ≤ spanFinrank.{u_3, u_1} (R := R) (M := ↥N) ⊤
Tactic: grw [← Submodule.baseChange_top, ← N.spanFinrank_top, (N.fg_top.mpr fg).spanFinrank_baseChange_le]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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 := ⋯
⊢ spanFinrank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤ = N.spanFinrank
have apply : N.spanFinrank ≤ spanFinrank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
Tactic: apply (TensorProduct.spanFinrank_top_le_of_fg N fg).antisymm
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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 := ⋯
⊢ N.spanFinrank ≤ spanFinrank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
have 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) ⊤
Tactic: obtain ⟨s, hs₁, hs₂⟩ := (⊤ : Submodule 𝓀 (𝓀 ⊗[R] N)).exists_span_set_card_eq_spanRank
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (hypothesis)
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) ⊤
⊢ N.spanFinrank ≤ spanFinrank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
have hs₃ : s.Finite
Tactic: have hs₃ : s.Finite := Cardinal.mk_lt_aleph0_iff.mp (by simpa [hs₁] using Module.Finite.fg_top)
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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
have rw : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) ∘ Function.surjInv sorry '' s = s
Tactic: rw [← Set.image_comp, Function.comp_surjInv, s.image_id]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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
⊢ (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s
have rw₁ : id '' s = s
Tactic: rw [← Set.image_comp, Function.comp_surjInv, s.image_id]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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
⊢ (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s
have rw₂ : s = s
Tactic: rw [← Set.image_comp, Function.comp_surjInv, s.image_id]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (hypothesis)
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
⊢ N.spanFinrank ≤ spanFinrank (R := 𝓀) (M := TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N) ⊤
have ht₁ : (⇑((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]
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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
ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s
⊢ Eq (α := Submodule R ↥N) (span R t) ⊤
have rwa : ∀ (hs₂ : Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (restrictScalars R (R := 𝓀) (span 𝓀 s)) ⊤)
  (hs₃ : s.Finite),
  let t := Function.surjInv sorry '' s;
  ∀ (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
    Eq (α := Submodule R ↥N) (span R t) ⊤
Tactic: rwa [← restrictScalars_eq_top_iff R, restrictScalars_span _ _ (by exact residue_surjective),
      ← ht₁, ← map_span, map_tensorProduct_mk_eq_top] at hs₂
Cleared hypotheses: hs₂, hs₃, t, ht₁
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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
ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s
rwa :
  ∀ (hs₂ : Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (restrictScalars R (R := 𝓀) (span 𝓀 s)) ⊤)
    (hs₃ : s.Finite),
    let t := Function.surjInv ⋯ '' s;
    ∀ (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
      Eq (α := Submodule R ↥N) (span R t) ⊤
⊢ Eq (α := Submodule R ↥N) (span R t) ⊤
have rwa₁ : ∀ (hs₂ : Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span R s) ⊤) (hs₃ : s.Finite),
  let t := Function.surjInv sorry '' s;
  ∀ (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
    Eq (α := Submodule R ↥N) (span R t) ⊤
Tactic: rwa [← restrictScalars_eq_top_iff R, restrictScalars_span _ _ (by exact residue_surjective),
      ← ht₁, ← map_span, map_tensorProduct_mk_eq_top] at hs₂
Cleared hypotheses: hs₂, hs₃, t, ht₁
-- Lean 4 proof step from Mathlib.Algebra.Module.SpanRankOperations (goal)
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
ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s
rwa :
  ∀ (hs₂ : Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (restrictScalars R (R := 𝓀) (span 𝓀 s)) ⊤)
    (hs₃ : s.Finite),
    let t := Function.surjInv ⋯ '' s;
    ∀ (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
      Eq (α := Submodule R ↥N) (span R t) ⊤
rwa₁ :
  ∀ (hs₂ : Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N)) (span R s) ⊤) (hs₃ : s.Finite),
    let t := Function.surjInv ⋯ '' s;
    ∀ (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
      Eq (α := Submodule R ↥N) (span R t) ⊤
⊢ Eq (α := Submodule R ↥N) (span R t) ⊤
have rwa₂ : ∀ (hs₃ : s.Finite),
  let t := Function.surjInv sorry '' s;
  ∀
    (hs₂ :
      Eq (α := Submodule R (TensorProduct.{u_1, u_1, u_3} R 𝓀 ↥N))
        (span R ((⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t)) ⊤)
    (ht₁ : (⇑((mk R 𝓀 ↥N : (a : 𝓀) → ↥N →ₗ[R] 𝓀 ⊗[R] ↥N) 1) : (a : ↥N) → 𝓀 ⊗[R] ↥N) '' t = s),
    Eq (α := Submodule R ↥N) (span R t) ⊤
Tactic: rwa [← restrictScalars_eq_top_iff R, restrictScalars_span _ _ (by exact residue_surjective),
      ← ht₁, ← map_span, map_tensorProduct_mk_eq_top] at hs₂
Cleared hypotheses: hs₂, hs₃, t, ht₁