awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
M : Type u_4
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
S : Type u_7
P : Type u_6
inst_3 : Semiring S
inst_4 : AddCommMonoid P
inst_5 : Module S P
σ : R →+* S
inst_6 : RingHomSurjective σ
f : M →ₛₗ[σ] P
hf : Function.Bijective.{u_4 + 1, u_6 + 1} (α := M) (β := P) (⇑f : (a : M) → P)
h : Module.Finite S P
rwa : f.range.FG
⊢ (map f ⊤).FG
have rwa₁ : FG.{u_7, u_6} (R := S) (M := P) ⊤
Tactic: rwa [Submodule.map_top, LinearMap.range_eq_top.mpr hf.surjective, ← Module.finite_def]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M_1 : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M_1
inst_2 : Module R M_1
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_6
M : ι → Type u_7
inst_5 : Finite ι
inst_6 : (i : ι) → AddCommMonoid (M i)
inst_7 : (i : ι) → Module.{u_1, u_7} R (M i)
h : ∀ (i : ι), Module.Finite.{u_1, u_7} R (M i)
⊢ FG (R := R) (M := (i : ι) → M i) ⊤
have rw : FG (R := R) (M := (i : ι) → M i) (Submodule.pi (φ := M) univ fun (i : ι) ↦ ⊤)
Tactic: rw [← pi_top]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
M_1 : Type u_4
N : Type u_5
inst : Semiring R
inst_1 : AddCommMonoid M_1
inst_2 : Module R M_1
inst_3 : AddCommMonoid N
inst_4 : Module R N
ι : Type u_6
M : ι → Type u_7
inst_5 : Finite ι
inst_6 : (i : ι) → AddCommMonoid (M i)
inst_7 : (i : ι) → Module.{u_1, u_7} R (M i)
h : ∀ (i : ι), Module.Finite.{u_1, u_7} R (M i)
rw : FG (R := R) (M := (i : ι) → M i) (Submodule.pi (φ := M) univ fun (i : ι) ↦ ⊤)
⊢ FG (R := R) (M := (i : ι) → M i) ⊤
have rw₁ : Set ι
Tactic: rw [← pi_top]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_6
A : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module A M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
hM : Module.Finite R M
⊢ Module.Finite A M
have rw : ∀ (hM : ∃ (S : Set M), S.Finite ∧ Eq (α := Submodule R M) (span R S) ⊤),
  ∃ (S : Set M), S.Finite ∧ Eq (α := Submodule A M) (span A S) ⊤
Tactic: rw [finite_def, fg_def] at hM ⊢
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_6
A : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module A M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
hM : ∃ (S : Set M), S.Finite ∧ Eq (α := Submodule R M) (span R S) ⊤
⊢ ∃ (S : Set M), S.Finite ∧ Eq (α := Submodule A M) (span A S) ⊤
have obtain : ∀ (S : Set M) (hSfin : S.Finite) (hSgen : Eq (α := Submodule R M) (span R S) ⊤),
  ∃ (S : Set M), S.Finite ∧ Eq (α := Submodule A M) (span A S) ⊤
Tactic: obtain ⟨S, hSfin, hSgen⟩ := hM
Cleared hypotheses: hM
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_6
A : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module A M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : Eq (α := Submodule R M) (span R S) ⊤
⊢ ∃ (S : Set M), S.Finite ∧ Eq (α := Submodule A M) (span A S) ⊤
have refine : LE.le (α := Submodule A M) ⊤ (span A S)
Tactic: refine ⟨S, hSfin, eq_top_iff.mpr ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (hypothesis)
Goal:
R : Type u_6
A : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module A M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : Eq (α := Submodule R M) (span R S) ⊤
⊢ LE.le (α := Submodule A M) ⊤ (span A S)
have this : LE.le (α := Submodule R M) (span R S) (restrictScalars R (span A S))
Tactic: have := span_le_restrictScalars R A S
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_6
A : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : Semiring A
inst_2 : AddCommMonoid M
inst_3 : Module R M
inst_4 : Module A M
inst_5 : SMul R A
inst_6 : IsScalarTower R A M
S : Set M
hSfin : S.Finite
hSgen : Eq (α := Submodule R M) (span R S) ⊤
this : LE.le (α := Submodule R M) (span R S) (restrictScalars R (span A S))
⊢ LE.le (α := Submodule A M) ⊤ (span A S)
have rwa : ∀ (this : LE.le (α := Submodule R M) ⊤ (restrictScalars R (span A S))), LE.le (α := Submodule A M) ⊤ (span A S)
Tactic: rwa [hSgen] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_6
A : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
s : Finset A
hs : Eq (α := Submodule R A) (span R (↑s : Set A)) ⊤
t : Finset M
ht : Eq (α := Submodule A M) (span A (↑t : Set M)) ⊤
⊢ Eq (α := Submodule R M) (span R (image2 (fun (x1 : A) (x2 : M) ↦ x1 • x2) (↑s : Set A) (↑t : Set M))) ⊤
have rw : Eq (α := Submodule R M) (span R ((↑s : Set A) • (↑t : Set M))) ⊤
Tactic: rw [image2_smul, span_smul_of_span_eq_top hs (↑t : Set M), ht, restrictScalars_top]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_6
A : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
s : Finset A
hs : Eq (α := Submodule R A) (span R (↑s : Set A)) ⊤
t : Finset M
ht : Eq (α := Submodule A M) (span A (↑t : Set M)) ⊤
rw : Eq (α := Submodule R M) (span R ((↑s : Set A) • (↑t : Set M))) ⊤
⊢ Eq (α := Submodule R M) (span R (image2 (fun (x1 : A) (x2 : M) ↦ x1 • x2) (↑s : Set A) (↑t : Set M))) ⊤
have rw₁ : Eq (α := Submodule R M) (restrictScalars R (span A (↑t : Set M))) ⊤
Tactic: rw [image2_smul, span_smul_of_span_eq_top hs (↑t : Set M), ht, restrictScalars_top]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_6
A : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
s : Finset A
hs : Eq (α := Submodule R A) (span R (↑s : Set A)) ⊤
t : Finset M
ht : Eq (α := Submodule A M) (span A (↑t : Set M)) ⊤
rw : Eq (α := Submodule R M) (span R ((↑s : Set A) • (↑t : Set M))) ⊤
rw₁ : Eq (α := Submodule R M) (restrictScalars R (span A (↑t : Set M))) ⊤
⊢ Eq (α := Submodule R M) (span R (image2 (fun (x1 : A) (x2 : M) ↦ x1 • x2) (↑s : Set A) (↑t : Set M))) ⊤
have rw₂ : Eq.{u_8 + 1} (α := Submodule R M) (restrictScalars.{u_6, u_7, u_8} R (R := A) ⊤) ⊤
Tactic: rw [image2_smul, span_smul_of_span_eq_top hs (↑t : Set M), ht, restrictScalars_top]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_6
A : Type u_7
M : Type u_8
inst : Semiring R
inst_1 : Semiring A
inst_2 : Module R A
inst_3 : AddCommMonoid M
inst_4 : Module R M
inst_5 : Module A M
inst_6 : IsScalarTower R A M
s : Finset A
hs : Eq (α := Submodule R A) (span R (↑s : Set A)) ⊤
t : Finset M
ht : Eq (α := Submodule A M) (span A (↑t : Set M)) ⊤
rw : Eq (α := Submodule R M) (span R ((↑s : Set A) • (↑t : Set M))) ⊤
rw₁ : Eq (α := Submodule R M) (restrictScalars R (span A (↑t : Set M))) ⊤
rw₂ : Eq.{u_8 + 1} (α := Submodule R M) (restrictScalars.{u_6, u_7, u_8} R (R := A) ⊤) ⊤
⊢ Eq (α := Submodule R M) (span R (image2 (fun (x1 : A) (x2 : M) ↦ x1 • x2) (↑s : Set A) (↑t : Set M))) ⊤
have rw₃ : Eq.{u_8 + 1} (α := Submodule R M) ⊤ ⊤
Tactic: rw [image2_smul, span_smul_of_span_eq_top hs (↑t : Set M), ht, restrictScalars_top]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (hypothesis)
Goal:
A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst : CommSemiring A₁
inst_1 : CommSemiring B₁
inst_2 : CommSemiring A₂
inst_3 : Semiring B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
inst_6 : Module.Finite A₁ B₁
this_1 : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this : Algebra A₂ B₁ := RingHom.toAlgebra (RingHom.comp (algebraMap A₁ B₁) e₁.symm.toRingHom)
⊢ Module.Finite A₂ B₂
have this₁ : IsScalarTower A₁ A₂ B₁
Tactic: haveI : IsScalarTower A₁ A₂ B₁ := IsScalarTower.of_algebraMap_eq
    (fun x ↦ by simp [RingHom.algebraMap_toAlgebra])
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (hypothesis)
Goal:
A₁ : Type u_6
B₁ : Type u_7
A₂ : Type u_8
B₂ : Type u_9
inst : CommSemiring A₁
inst_1 : CommSemiring B₁
inst_2 : CommSemiring A₂
inst_3 : Semiring B₂
inst_4 : Algebra A₁ B₁
inst_5 : Algebra A₂ B₂
e₁ : A₁ ≃+* A₂
e₂ : B₁ ≃+* B₂
he :
  Eq (α := A₁ →+* B₂) (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (algebraMap A₂ B₂) (↑e₁ : A₁ →+* A₂))
    (@RingHom.comp _ _ _ _ Semiring.toNonAssocSemiring _ (↑e₂ : B₁ →+* B₂) (algebraMap A₁ B₁))
inst_6 : Module.Finite A₁ B₁
this_1 : Algebra A₁ A₂ := e₁.toRingHom.toAlgebra
this_2 : Algebra A₂ B₁ := RingHom.toAlgebra (RingHom.comp (algebraMap A₁ B₁) e₁.symm.toRingHom)
this : IsScalarTower A₁ A₂ B₁
e : B₁ ≃ₐ[A₂] B₂ := { toEquiv := e₂.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ }
⊢ Module.Finite A₂ B₂
have this₁ : Module.Finite A₂ B₁
Tactic: haveI := of_restrictScalars_finite A₁ A₂ B₁
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
V : Type u_2
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
S₁ S₂ : Submodule R V
h₁ : Module.Finite.{u_1, u_2} R ↥S₁
h₂ : Module.Finite.{u_1, u_2} R ↥S₂
⊢ Module.Finite.{u_1, u_2} R ↥(S₁ ⊔ S₂)
have rw : ∀ (h₁ : S₁.FG) (h₂ : S₂.FG), (S₁ ⊔ S₂).FG
Tactic: rw [Finite.iff_fg] at *
Cleared hypotheses: h₁, h₂
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_2
V : Type u_3
inst : Ring R
inst_1 : AddCommGroup V
inst_2 : Module R V
ι : Type u_1
s : Finset ι
S : ι → Submodule R V
inst_3 : ∀ (i : ι), Module.Finite.{u_2, u_3} R ↥(S i)
⊢ Module.Finite.{u_2, u_3} R ↥(s.sup S)
have refine : ∀ (a₁ : Submodule R V),
  (fun (i : Submodule R V) ↦ Module.Finite.{u_2, u_3} R ↥i) a₁ →
    ∀ (a₂ : Submodule R V),
      (fun (i : Submodule R V) ↦ Module.Finite.{u_2, u_3} R ↥i) a₂ →
        (fun (i : Submodule R V) ↦ Module.Finite.{u_2, u_3} R ↥i) (a₁ ⊔ a₂)
Tactic: refine s.sup_induction (f := S) (p := fun i => Module.Finite R ↑i) (Module.Finite.bot R V) ?_
    inferInstance
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
S : Submodule A M
inst_7 : Module.Finite R A
hS : S.FG
⊢ FG (Submodule.restrictScalars R S)
have rw : ∀ (hS : Module.Finite.{u_3, u_2} A ↥S), Module.Finite.{u_1, u_2} R ↥(Submodule.restrictScalars R S)
Tactic: rw [← Module.Finite.iff_fg] at *
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
S : Submodule R M
hS : S.FG
⊢ FG (span A (↑S : Set M))
have obtain : ∀ (t : Finset M) (ht : span R (↑t : Set M) = S), FG (span A (↑S : Set M))
Tactic: obtain ⟨t, ht⟩ := hS
Cleared hypotheses: hS
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
S : Submodule R M
t : Finset M
ht : span R (↑t : Set M) = S
⊢ FG (span A (↑S : Set M))
have h : Eq (α := Submodule A M) (span A (↑t : Set M)) (span A (↑S : Set M))
Tactic: use t
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
S : Submodule R M
t : Finset M
ht : span R (↑t : Set M) = S
⊢ Eq (α := Submodule A M) (span A (↑t : Set M)) (span A (↑S : Set M))
have h : Eq (α := Submodule A M) (span A (↑t : Set M)) (span A (↑(span R (↑t : Set M)) : Set M))
Tactic: rw [← ht, Submodule.span_span_of_tower]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
inst : Semiring R
M : Type u_2
inst_1 : AddCommMonoid M
inst_2 : Module R M
A : Type u_3
inst_3 : Semiring A
inst_4 : Module R A
inst_5 : Module A M
inst_6 : IsScalarTower R A M
S : Submodule R M
t : Finset M
ht : span R (↑t : Set M) = S
h : Eq (α := Submodule A M) (span A (↑t : Set M)) (span A (↑(span R (↑t : Set M)) : Set M))
⊢ Eq (α := Submodule A M) (span A (↑t : Set M)) (span A (↑S : Set M))
have h₁ : Eq (α := Submodule A M) (span A (↑t : Set M)) (span A (↑t : Set M))
Tactic: rw [← ht, Submodule.span_span_of_tower]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
g : B →+* C
f : A →+* B
hg : g.Finite
hf : f.Finite
⊢ (g.comp f).Finite
have algebraizeInst : Module.Finite B C
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
g : B →+* C
f : A →+* B
hg : g.Finite
hf : f.Finite
algebraizeInst : Module.Finite B C
⊢ (g.comp f).Finite
have algebraizeInst₁ : Module.Finite A B
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (hypothesis)
Goal:
A : Type u_1
B : Type u_2
C : Type u_3
inst : CommRing A
inst_1 : CommRing B
inst_2 : CommRing C
f : A →+* B
g : B →+* C
h : (g.comp f).Finite
⊢ g.Finite
have algebraizeInst : Module.Finite A C
Tactic: algebraize [f, g, g.comp f]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
E : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
⊢ Module.Finite R≥0 R
have simp_rw : ∃ (S : Set R), S.Finite ∧ ∀ (x : R), Membership.mem (γ := Submodule R≥0 R) (Submodule.span R≥0 S) x
Tactic: simp_rw [Module.finite_def, Submodule.fg_def, Submodule.eq_top_iff']
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
E : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
⊢ ∃ (S : Set R), S.Finite ∧ ∀ (x : R), Membership.mem (γ := Submodule R≥0 R) (Submodule.span R≥0 S) x
have refine : ∀ (x : R), Membership.mem (γ := Submodule R≥0 R) (Submodule.span R≥0 {1, -1}) x
Tactic: refine ⟨{1, -1}, by simp, fun x ↦ ?_⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
E : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
x : R
⊢ Membership.mem (γ := Submodule R≥0 R) (Submodule.span R≥0 {1, -1}) x
have inl : ∀ (hx : 0 ≤ x), Membership.mem (γ := Submodule R≥0 R) (Submodule.span R≥0 {1, -1}) x
Tactic: obtain hx | hx := le_total 0 x
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Basic (goal)
Goal:
R : Type u_1
E : Type u_2
inst : Ring R
inst_1 : LinearOrder R
inst_2 : IsOrderedRing R
inst_3 : AddCommMonoid E
inst_4 : Module R E
x : R
inl : ∀ (hx : 0 ≤ x), Membership.mem (γ := Submodule R≥0 R) (Submodule.span R≥0 {1, -1}) x
⊢ Membership.mem (γ := Submodule R≥0 R) (Submodule.span R≥0 {1, -1}) x
have inr : ∀ (hx : x ≤ 0), Membership.mem (γ := Submodule R≥0 R) (Submodule.span R≥0 {1, -1}) x
Tactic: obtain hx | hx := le_total 0 x
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cardinality (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
⊢ N.FG ↔ ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), f.range = N
have simp_rw : (∃ (n : ℕ) (s : Fin n → M), span R (Set.range s) = N) ↔
  ∃ (n : ℕ) (a : Fin n → M),
    LinearMap.range (R := R) (M := Fin n → R) (τ₁₂ := RingHom.id R)
        (({
              toFun :=
                AddHom.toFun
                  (LinearMap.toAddHom
                    (↑(Basis.constr (Pi.basisFun R (Fin n)) ℕ) : (Fin n → M) →ₗ[ℕ] (Fin n → R) →ₗ[R] M)),
              invFun := LinearEquiv.invFun (Basis.constr (Pi.basisFun R (Fin n)) ℕ), left_inv := sorry, right_inv := sorry } :
            (a : Fin n → M) → (Fin n → R) →ₗ[R] M)
          a) =
      N
Tactic: simp_rw [fg_iff_exists_fin_generating_family, ← ((Pi.basisFun R _).constr ℕ).exists_congr_right]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cardinality (goal)
Goal:
M : Type u_3
inst : AddCommMonoid M
S : AddSubmonoid M
⊢ S.FG ↔ ∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), AddMonoidHom.mrange f = S
have rw : (∃ (n : ℕ) (f : (Fin n → ℕ) →ₗ[ℕ] M), f.range = (toNatSubmodule : (a : AddSubmonoid M) → Submodule ℕ M) S) ↔
  ∃ (n : ℕ) (f : (Fin n → ℕ) →+ M),
    Eq (α := AddSubmonoid M) (AddMonoidHom.mrange f)
      (Submodule.toAddSubmonoid (R := ℕ) ((toNatSubmodule : (a : AddSubmonoid M) → Submodule ℕ M) S))
Tactic: rw [← S.toNatSubmodule_toAddSubmonoid, ← Submodule.fg_iff_addSubmonoid_fg,
    Submodule.fg_iff_exists_fin_linearMap]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cardinality (goal)
Goal:
M : Type u_3
inst : AddCommGroup M
H : AddSubgroup M
⊢ H.FG ↔ ∃ (n : ℕ) (f : (Fin n → ℤ) →+ M), f.range = H
have rw : (∃ (n : ℕ) (f : (Fin n → ℤ) →ₗ[ℤ] M), f.range = (toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) H) ↔
  ∃ (n : ℕ) (f : (Fin n → ℤ) →+ M),
    f.range =
      Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule M)
        ((toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) H)
Tactic: rw [← H.toIntSubmodule_toAddSubgroup, ← Submodule.fg_iff_addSubgroup_fg,
    Submodule.fg_iff_exists_fin_linearMap]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cardinality (goal)
Goal:
M : Type u_3
inst : AddCommGroup M
H : AddSubgroup M
⊢ (∃ (n : ℕ) (f : (Fin n → ℤ) →ₗ[ℤ] M), f.range = (toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) H) ↔
    ∃ (n : ℕ) (f : (Fin n → ℤ) →+ M),
      f.range =
        Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule M)
          ((toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) H)
have refine : ∀ (n : ℕ),
  (∃ (f : (Fin n → ℤ) →+ M),
      f.range =
        Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule M)
          ((toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) H)) →
    ∀ (f : (Fin n → ℤ) →+ M)
      (hf :
        f.range =
          Submodule.toAddSubgroup (R := ℤ) (module_M := AddCommGroup.toIntModule M)
            ((toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) H)),
      f.toIntLinearMap.range.toAddSubmonoid =
        Submodule.toAddSubmonoid (R := ℤ) ((toIntSubmodule : (a : AddSubgroup M) → Submodule ℤ M) H)
Tactic: refine exists_congr fun n => ⟨fun ⟨f, hf⟩ => ⟨f, hf ▸ LinearMap.range_toAddSubgroup _⟩,
    fun ⟨f, hf⟩ => ⟨f.toIntLinearMap, Submodule.toAddSubmonoid_inj.mp ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cardinality (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Module.Finite R M
n : ℕ
f : (Fin n → R) →ₗ[R] M
hf rw : f.range = ⊤
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)
have rw₁ : Eq.{u_2 + 1} (α := Submodule R M) ⊤ ⊤
Tactic: rw [← LinearMap.range_eq_top, hf]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cardinality (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite R
inst_4 : Module.Finite R M
⊢ Finite M
have obtain : ∀ (n : ℕ) (f : (Fin n → R) →ₗ[R] M)
  (hf : Surjective.{u_1 + 1, u_2 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)), Finite M
Tactic: obtain ⟨n, f, hf⟩ := exists_fin' R M
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cardinality (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite R
s : Set M
hs : s.Finite
⊢ (↑(span R s) : Set M).Finite
have lift : ∀ (s : Finset M), (↑(span R (↑s : Set M)) : Set M).Finite
Tactic: lift s to Finset M using hs
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cardinality (goal)
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Finite R
s : Finset M
⊢ (↑(span R (↑s : Set M)) : Set M).Finite
have rw : Module.Finite.{u_1, u_2} R (↑(↑(span R (↑s : Set M)) : Set M) : Type u_2)
Tactic: rw [Set.Finite, ← Module.finite_iff_finite (R := R)]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cofinite (hypothesis)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
hST : IsCompl S T
hS : S.FG
⊢ T.CoFG
have this : Module.Finite.{u_1, u_2} R ↥S
Tactic: haveI := Module.Finite.iff_fg.mpr hS
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cofinite (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
S T : Submodule R M
hT : S ≤ T
hS : S.CoFG
⊢ T.CoFG
have rw : (S ⊔ T).CoFG
Tactic: rw [← sup_eq_right.mpr hT]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cofinite (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
N : Type u_3
inst_3 : AddCommGroup N
inst_4 : Module R N
f : M →ₗ[R] N
⊢ f.range.FG ↔ f.ker.CoFG
have rw : Module.Finite.{u_1, u_3} R ↥f.range ↔ f.ker.CoFG
Tactic: rw [← Module.Finite.iff_fg]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cofinite (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
S T : Submodule R M
hS : S.CoFG
hT : T.CoFG
⊢ (S ⊓ T).CoFG
have rw : (S.mkQ.prod T.mkQ).ker.CoFG
Tactic: rw [← Submodule.ker_mkQ S, ← Submodule.ker_mkQ T, ← LinearMap.ker_prod]
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cofinite (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
w : Submodule R M
s : Finset (Submodule R M)
hws : w ∉ s
hs' : ∀ (hs : ∀ S ∈ s, S.CoFG), (sInf (↑s : Set (Submodule R M))).CoFG
hs : ∀ S ∈ insert w s, S.CoFG
⊢ (sInf (↑(insert w s) : Set (Submodule R M))).CoFG
have insert : ∀ (hs : w.CoFG ∧ ∀ a ∈ s, a.CoFG), (w ⊓ sInf (↑s : Set (Submodule R M))).CoFG
Tactic: simp only [Finset.mem_insert, forall_eq_or_imp, Finset.coe_insert, sInf_insert] at *
Cleared hypotheses: hs
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cofinite (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
s : Finset (Submodule R M)
hs : ∀ S ∈ s, S.CoFG
⊢ (sInf (↑s : Set (Submodule R M))).CoFG
have empty : ∀ (hs : ∀ (S : Submodule R M), Membership.mem (γ := Finset (Submodule R M)) ∅ S → S.CoFG),
  (sInf (↑∅ : Set (Submodule R M))).CoFG
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert w s hws hs' =>
    simp only [Finset.mem_insert, forall_eq_or_imp, Finset.coe_insert, sInf_insert] at *
    exact hs.1.inf (hs' hs.2)
Cleared hypotheses: s, hs
-- Lean 4 proof step from Mathlib.RingTheory.Finiteness.Cofinite (goal)
Goal:
R : Type u_1
inst : Ring R
M : Type u_2
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : IsNoetherianRing R
s : Finset (Submodule R M)
hs : ∀ S ∈ s, S.CoFG
empty :
  ∀ (hs : ∀ (S : Submodule R M), Membership.mem (γ := Finset (Submodule R M)) ∅ S → S.CoFG),
    (sInf (↑∅ : Set (Submodule R M))).CoFG
⊢ (sInf (↑s : Set (Submodule R M))).CoFG
have insert : ∀ (w : Submodule R M) (s : Finset (Submodule R M)) (hws : w ∉ s)
  (hs' : ∀ (hs : ∀ S ∈ s, S.CoFG), (sInf (↑s : Set (Submodule R M))).CoFG) (hs : ∀ S ∈ insert w s, S.CoFG),
  (sInf (↑(insert w s) : Set (Submodule R M))).CoFG
Tactic: induction s using Finset.induction with
  | empty => simp
  | insert w s hws hs' =>
    simp only [Finset.mem_insert, forall_eq_or_imp, Finset.coe_insert, sInf_insert] at *
    exact hs.1.inf (hs' hs.2)
Cleared hypotheses: s, hs