awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Finiteness.Basic
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 : Module.Finite.{u_3, u_2} A ↥S
⊢ Module.Finite.{u_1, u_2} R ↥(Submodule.restrictScalars R S)

Tactic:
exact Module.Finite.trans A S

Premises used: Membership.mem, Subtype, Module.Finite.trans
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
⊢ FG (Submodule.restrictScalars R S) ↔ S.FG

Tactic:
⟨of_restrictScalars R, restrictScalars⟩

Premises used: Submodule.FG.restrictScalars, Iff.intro, Submodule.FG.of_restrictScalars
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
obtain : ∀ (t : Finset M) (ht : span R (↑t : Set M) = S), FG (span A (↑S : Set M))
⊢ FG (span A (↑S : Set M))

Tactic:
obtain ⟨t, ht⟩ := hS
-- Module: Mathlib.RingTheory.Finiteness.Basic
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 (↑S : Set M))
⊢ FG (span A (↑S : Set M))

Tactic:
use t
-- Module: Mathlib.RingTheory.Finiteness.Basic
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))
h₁ h₂ : Eq (α := Submodule A M) (span A (↑t : Set M)) (span A (↑t : Set M))
⊢ Eq (α := Submodule A M) (span A (↑t : Set M)) (span A (↑S : Set M))

Tactic:
rw [← ht, Submodule.span_span_of_tower]

Premises used: Submodule.span_span_of_tower
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
A : Type u_1
inst : CommRing A
⊢ Finite (RingHom.id A)

Tactic:
Module.Finite.self A

Premises used: Module.Finite.self, RingHom.Finite
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
f : A →+* B
hf : Surjective.{u_1 + 1, u_2 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ f.Finite

Tactic:
letI := f.toAlgebra
  Module.Finite.of_surjective (Algebra.linearMap A B) hf

Premises used: Module.Finite.of_surjective, Algebra.linearMap, RingHom.Finite
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
A : Type u_1
B : Type u_2
inst : CommRing A
inst_1 : CommRing B
e : A ≃+* B
⊢ e.toRingHom.Finite

Tactic:
.of_surjective _ e.surjective

Premises used: RingEquiv.surjective, RingHom.Finite.of_surjective
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
⊢ Module.Finite B C

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
⊢ Module.Finite A B

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower A B C := ⋯
algebraizeInst : Module.Finite B C
algebraizeInst_1 : Module.Finite A B
⊢ (g.comp f).Finite

Tactic:
.trans B C

Premises used: Module.Finite.trans, RingHom.Finite
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower A B C := ⋯
algebraizeInst : Module.Finite B C
algebraizeInst_1 : Module.Finite A B
⊢ (g.comp f).Finite

Tactic:
exact .trans B C
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
⊢ Module.Finite A C

Tactic:
algebraize [f, g, g.comp f]

Premises used: RingHom.comp
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower A B C := ⋯
algebraizeInst : Module.Finite A C
⊢ g.Finite

Tactic:
.of_restrictScalars_finite A B C

Premises used: Module.Finite.of_restrictScalars_finite, RingHom.Finite
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
algInst : Algebra A B := f.toAlgebra
algInst_1 : Algebra B C := g.toAlgebra
algInst_2 : Algebra A C := (g.comp f).toAlgebra
scalarTowerInst : IsScalarTower A B C := ⋯
algebraizeInst : Module.Finite A C
⊢ g.Finite

Tactic:
exact .of_restrictScalars_finite A B C
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
inst : CommRing R
inst_1 : CommRing A
inst_2 : Algebra R A
⊢ Finite (AlgHom.id R A)

Tactic:
RingHom.Finite.id A

Premises used: AlgHom.Finite, RingHom.Finite.id
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
g : B →ₐ[R] C
f : A →ₐ[R] B
hg : g.Finite
hf : f.Finite
⊢ (g.comp f).Finite

Tactic:
RingHom.Finite.comp hg hf

Premises used: AlgHom.Finite, RingHom.Finite.comp
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : Algebra R A
inst_4 : Algebra R B
f : A →ₐ[R] B
hf : Surjective.{u_2 + 1, u_3 + 1} (α := A) (β := B) (⇑f : (a : A) → B)
⊢ f.Finite

Tactic:
RingHom.Finite.of_surjective f.toRingHom hf

Premises used: AlgHom.Finite, RingHom.Finite.of_surjective, AlgHom.toRingHom
-- Module: Mathlib.RingTheory.Finiteness.Basic
Goal:
R : Type u_1
A : Type u_2
B : Type u_3
C : Type u_4
inst : CommRing R
inst_1 : CommRing A
inst_2 : CommRing B
inst_3 : CommRing C
inst_4 : Algebra R A
inst_5 : Algebra R B
inst_6 : Algebra R C
f : A →ₐ[R] B
g : B →ₐ[R] C
h : (g.comp f).Finite
⊢ g.Finite

Tactic:
RingHom.Finite.of_comp_finite h

Premises used: AlgHom.Finite, RingHom.Finite.of_comp_finite
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
simp_rw : ∃ (S : Set R), S.Finite ∧ ∀ (x : R), Membership.mem (γ := Submodule R≥0 R) (Submodule.span R≥0 S) x
⊢ Module.Finite R≥0 R

Tactic:
simp_rw [Module.finite_def, Submodule.fg_def, Submodule.eq_top_iff']

Premises used: Submodule.eq_top_iff', Submodule.fg_def, Module.finite_def
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
⊢ Set.Finite (α := R) {1, -1}

Tactic:
simp
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
refine : ∀ (x : R), Membership.mem (γ := Submodule R≥0 R) (Submodule.span R≥0 {1, -1}) x
⊢ ∃ (S : Set R), S.Finite ∧ ∀ (x : R), Membership.mem (γ := Submodule R≥0 R) (Submodule.span R≥0 S) x

Tactic:
refine ⟨{1, -1}, by simp, fun x ↦ ?_⟩
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
inr : ∀ (hx : x ≤ 0), 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

Tactic:
obtain hx | hx := le_total 0 x

Premises used: le_total, OfNat.ofNat
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
hx : 0 ≤ x
⊢ Membership.mem (γ := Set R) {1, -1} 1

Tactic:
simp
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
hx : 0 ≤ x
⊢ Membership.mem (γ := Submodule R≥0 R) (Submodule.span R≥0 {1, -1}) x

Tactic:
simpa using Submodule.smul_mem (M := R) (.span R≥0 {1, -1}) ⟨x, hx⟩ (x := 1)
      (Submodule.subset_span <| by simp)
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
hx : x ≤ 0
⊢ Membership.mem (γ := Set R) {1, -1} (-1)

Tactic:
simp
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
hx : x ≤ 0
⊢ Membership.mem (γ := Submodule R≥0 R) (Submodule.span R≥0 {1, -1}) x

Tactic:
simpa using Submodule.smul_mem (M := R) (.span R≥0 {1, -1}) ⟨-x, neg_nonneg.mpr hx⟩ (x := -1)
      (Submodule.subset_span <| by simp)
-- Module: Mathlib.RingTheory.Finiteness.Basic
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
inst_5 : Module.Finite R E
⊢ Module.Finite.{u_1, u_2} R≥0 E

Tactic:
.trans R E

Premises used: Module.Finite.trans
-- Module: Mathlib.RingTheory.Finiteness.Bilinear
Goal:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst : CommSemiring R
inst_1 : AddCommMonoid M
inst_2 : AddCommMonoid N
inst_3 : AddCommMonoid P
inst_4 : Module R M
inst_5 : Module R N
inst_6 : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
hp : p.FG
hq : q.FG
⊢ (Submodule.map₂ f p q).FG

Tactic:
let ⟨sm, hfm, hm⟩ := fg_def.1 hp
  let ⟨sn, hfn, hn⟩ := fg_def.1 hq
  fg_def.2
    ⟨Set.image2 (fun m n => f m n) sm sn, hfm.image2 _ hfn,
      map₂_span_span R f sm sn ▸ hm ▸ hn ▸ rfl⟩

Premises used: Iff.mpr, _private.0.Submodule.FG.map₂.match_1, Submodule.fg_def, Eq.rec, Set.Finite.image2, Submodule.FG, Submodule.map₂_span_span, Set.image2, And.intro, Exists.intro, Iff.mp, Submodule.map₂, DFunLike.coe, rfl
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
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
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 := ⋯, right_inv := ⋯ } :
              (a : Fin n → M) → (Fin n → R) →ₗ[R] M)
            a) =
        N
⊢ N.FG ↔ ∃ (n : ℕ) (f : (Fin n → R) →ₗ[R] M), f.range = N

Tactic:
simp_rw [fg_iff_exists_fin_generating_family, ← ((Pi.basisFun R _).constr ℕ).exists_congr_right]

Premises used: Equiv.exists_congr_right, LinearEquiv.toAddEquiv, Submodule.fg_iff_exists_fin_generating_family, Nat, Pi.basisFun, AddEquiv.toEquiv, Module.Basis.constr
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
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 : ℕ) (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 := ⋯, right_inv := ⋯ } :
              (a : Fin n → M) → (Fin n → R) →ₗ[R] M)
            a) =
        N

Tactic:
simp [Basis.constr_range]

Premises used: Module.Basis.constr_range
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
Goal:
M : Type u_3
inst : AddCommMonoid M
S : AddSubmonoid M
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))
⊢ S.FG ↔ ∃ (n : ℕ) (f : (Fin n → ℕ) →+ M), AddMonoidHom.mrange f = S

Tactic:
rw [← S.toNatSubmodule_toAddSubmonoid, ← Submodule.fg_iff_addSubmonoid_fg,
    Submodule.fg_iff_exists_fin_linearMap]

Premises used: AddSubmonoid.toNatSubmodule_toAddSubmonoid, Submodule.fg_iff_addSubmonoid_fg, Submodule.fg_iff_exists_fin_linearMap
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
Goal:
M : Type u_3
inst : AddCommMonoid M
S : AddSubmonoid M
⊢ (∃ (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:
exists_congr fun n => ⟨fun ⟨f, hf⟩ => ⟨f, hf ▸ LinearMap.range_toAddSubmonoid _⟩,
    fun ⟨f, hf⟩ => ⟨f.toNatLinearMap, Submodule.toAddSubmonoid_inj.mp <|
      hf ▸ LinearMap.range_toAddSubmonoid _⟩⟩

Premises used: _private.0.AddSubmonoid.fg_iff_exists_fin_addMonoidHom.match_1, AddSubmonoid.toNatSubmodule, AddMonoidHomClass.toAddMonoidHom, Submodule.toAddSubmonoid, LinearMap.range_toAddSubmonoid, Exists, Eq.rec, LinearMap.range, AddMonoidHom.toNatLinearMap, AddMonoidHom.mrange, exists_congr, Submodule.toAddSubmonoid_inj, Iff.intro, Exists.intro, _private.0.AddSubmonoid.fg_iff_exists_fin_addMonoidHom.match_2, Iff.mp, Eq, DFunLike.coe
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
Goal:
M : Type u_3
inst : AddCommMonoid M
S : AddSubmonoid M
⊢ (∃ (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:
exact exists_congr fun n => ⟨fun ⟨f, hf⟩ => ⟨f, hf ▸ LinearMap.range_toAddSubmonoid _⟩,
    fun ⟨f, hf⟩ => ⟨f.toNatLinearMap, Submodule.toAddSubmonoid_inj.mp <|
      hf ▸ LinearMap.range_toAddSubmonoid _⟩⟩

Premises used: exists_congr, Iff.intro
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
Goal:
M : Type u_3
inst : AddCommGroup M
H : AddSubgroup M
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)
⊢ H.FG ↔ ∃ (n : ℕ) (f : (Fin n → ℤ) →+ M), f.range = H

Tactic:
rw [← H.toIntSubmodule_toAddSubgroup, ← Submodule.fg_iff_addSubgroup_fg,
    Submodule.fg_iff_exists_fin_linearMap]

Premises used: Submodule.fg_iff_addSubgroup_fg, Submodule.fg_iff_exists_fin_linearMap, AddSubgroup.toIntSubmodule_toAddSubgroup
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
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)

Tactic:
exists_congr fun n => ⟨fun ⟨f, hf⟩ => ⟨f, hf ▸ LinearMap.range_toAddSubgroup _⟩,
    fun ⟨f, hf⟩ => ⟨f.toIntLinearMap, Submodule.toAddSubmonoid_inj.mp ?_⟩⟩

Premises used: LinearMap.range_toAddSubgroup, AddMonoidHomClass.toAddMonoidHom, AddMonoidHom.range, Exists, Eq.rec, LinearMap.range, exists_congr, _private.0.AddSubgroup.fg_iff_exists_fin_addMonoidHom.match_1, Submodule.toAddSubgroup, Submodule.toAddSubmonoid_inj, Iff.intro, Exists.intro, Iff.mp, _private.0.AddSubgroup.fg_iff_exists_fin_addMonoidHom.match_2, AddMonoidHom.toIntLinearMap, AddSubgroup.toIntSubmodule, Eq, DFunLike.coe
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
Goal:
M : Type u_3
inst : AddCommGroup M
H : AddSubgroup M
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)
⊢ (∃ (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:
refine exists_congr fun n => ⟨fun ⟨f, hf⟩ => ⟨f, hf ▸ LinearMap.range_toAddSubgroup _⟩,
    fun ⟨f, hf⟩ => ⟨f.toIntLinearMap, Submodule.toAddSubmonoid_inj.mp ?_⟩⟩

Premises used: exists_congr, Iff.intro
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
Goal:
M : Type u_3
inst : AddCommGroup M
H : AddSubgroup M
n : ℕ
h :
  ∃ (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:
simp [hf]
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
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 = ⊤
rw₁ rw₂ : Eq.{u_2 + 1} (α := Submodule R M) ⊤ ⊤
⊢ Surjective.{u_1 + 1, u_2 + 1} (α := Fin n → R) (β := M) (⇑f : (a : Fin n → R) → M)

Tactic:
rw [← LinearMap.range_eq_top, hf]

Premises used: LinearMap.range_eq_top
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
Goal:
R : Type u_3
M : Type u_4
inst : Ring R
inst_1 : AddCommGroup M
inst_2 : Module R M
inst_3 : Module.Finite R M
⊢ ∃ (n : ℕ) (S : Submodule R (Fin n → R)), Nonempty (((Fin n → R) ⧸ S) ≃ₗ[R] M)

Tactic:
let ⟨n, f, hf⟩ := Module.Finite.exists_fin' R M
  ⟨n, LinearMap.ker f, ⟨f.quotKerEquivOfSurjective hf⟩⟩

Premises used: LinearMap.ker, Exists, Nonempty.intro, HasQuotient.Quotient, LinearEquiv, LinearMap.quotKerEquivOfSurjective, Exists.intro, Nonempty, _private.0.Module.Finite.exists_fin_quot_equiv.match_1, Module.Finite.exists_fin', RingHom.id
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
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
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
⊢ Finite M

Tactic:
obtain ⟨n, f, hf⟩ := exists_fin' R M

Premises used: Module.Finite.exists_fin'
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
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
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:
.of_surjective f hf

Premises used: DFunLike.coe, Finite.of_surjective
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
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
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:
exact .of_surjective f hf
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
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
⊢ Module.Finite R M ↔ Finite M

Tactic:
⟨fun _ ↦ finite_of_finite R, fun _ ↦ .of_finite⟩

Premises used: Module.Finite.of_finite, Iff.intro, Module.finite_of_finite
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
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
⊢ s.Finite

Tactic:
hs
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
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
lift : ∀ (s : Finset M), (↑(span R (↑s : Set M)) : Set M).Finite
⊢ (↑(span R s) : Set M).Finite

Tactic:
lift s to Finset M using hs

Premises used: Finset
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
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
rw : Module.Finite.{u_1, u_2} R (↑(↑(span R (↑s : Set M)) : Set M) : Type u_2)
⊢ (↑(span R (↑s : Set M)) : Set M).Finite

Tactic:
rw [Set.Finite, ← Module.finite_iff_finite (R := R)]

Premises used: Set.Finite, Module.finite_iff_finite
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
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
⊢ Module.Finite.{u_1, u_2} R ↥(span R (↑s : Set M))

Tactic:
infer_instance
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
ι : Type u_3
inst_4 : Module.Finite R M
b : Basis ι R M
⊢ Finite ι

Tactic:
let ⟨s, hs⟩ := ‹Module.Finite R M›
  basis_finite_of_finite_spans s.finite_toSet hs b

Premises used: Finite, _private.0.Module.Finite.finite_basis.match_1, basis_finite_of_finite_spans, Finset.finite_toSet
-- Module: Mathlib.RingTheory.Finiteness.Cardinality
Goal:
R : Type u_1
M : Type u_2
inst : Semiring R
inst_1 : AddCommMonoid M
inst_2 : Module R M
inst_3 : Nontrivial R
ι : Type u_3
inst_4 : Infinite ι
b : Basis ι R M
⊢ ¬Module.Finite R M

Tactic:
fun _ ↦ (Finite.finite_basis b).not_infinite ‹_›

Premises used: Finite.not_infinite, Module.Finite.finite_basis, Not