awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Set R
ht : Eq (α := Ideal R) (Ideal.span t) ⊤
Mₚ : (↑t : Type u) → Type u_1
inst_3 : (g : (↑t : Type u)) → AddCommMonoid (Mₚ g)
inst_4 : (g : (↑t : Type u)) → Module.{u, u_1} R (Mₚ g)
Rₚ : (↑t : Type u) → Type u_2
inst_5 : (g : (↑t : Type u)) → CommSemiring (Rₚ g)
inst_6 : (g : (↑t : Type u)) → Algebra.{u, u_2} R (Rₚ g)
h₁ : ∀ (g : (↑t : Type u)), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_7 : (g : (↑t : Type u)) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_8 : ∀ (g : (↑t : Type u)), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : (↑t : Type u)) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
h₂ : ∀ (g : (↑t : Type u)), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : (↑t : Type u)), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
rw :
  ∀ (ht : ∃ (s' : Finset R), (↑s' : Set R) ⊆ t ∧ Eq (α := Ideal R) (Ideal.span (↑s' : Set R)) ⊤)
    {Mₚ : (↑t : Type u) → Type u_1} [inst_9 : (g : (↑t : Type u)) → AddCommMonoid (Mₚ g)]
    [inst_10 : (g : (↑t : Type u)) → Module.{u, u_1} R (Mₚ g)] {Rₚ : (↑t : Type u) → Type u_2}
    [inst_11 : (g : (↑t : Type u)) → CommSemiring (Rₚ g)] [inst_12 : (g : (↑t : Type u)) → Algebra.{u, u_2} R (Rₚ g)]
    [h₁ : ∀ (g : (↑t : Type u)), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)]
    [inst_13 : (g : (↑t : Type u)) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)]
    [∀ (g : (↑t : Type u)), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)]
    (f : (g : (↑t : Type u)) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g))
    [h₂ : ∀ (g : (↑t : Type u)), IsLocalizedModule.Away (↑g : R) (f g)]
    (H : ∀ (g : (↑t : Type u)), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)), Module.Finite R M
⊢ Module.Finite R M

Tactic:
rw [Ideal.span_eq_top_iff_finite] at ht

Premises used: Ideal.span_eq_top_iff_finite
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Set R
ht : ∃ (s' : Finset R), (↑s' : Set R) ⊆ t ∧ Eq (α := Ideal R) (Ideal.span (↑s' : Set R)) ⊤
Mₚ : (↑t : Type u) → Type u_1
inst_3 : (g : (↑t : Type u)) → AddCommMonoid (Mₚ g)
inst_4 : (g : (↑t : Type u)) → Module.{u, u_1} R (Mₚ g)
Rₚ : (↑t : Type u) → Type u_2
inst_5 : (g : (↑t : Type u)) → CommSemiring (Rₚ g)
inst_6 : (g : (↑t : Type u)) → Algebra.{u, u_2} R (Rₚ g)
h₁ : ∀ (g : (↑t : Type u)), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_7 : (g : (↑t : Type u)) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_8 : ∀ (g : (↑t : Type u)), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : (↑t : Type u)) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
h₂ : ∀ (g : (↑t : Type u)), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : (↑t : Type u)), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
obtain :
  ∀ (t' : Finset R) (hc : (↑t' : Set R) ⊆ t) (ht' : Eq (α := Ideal R) (Ideal.span (↑t' : Set R)) ⊤), Module.Finite R M
⊢ Module.Finite R M

Tactic:
obtain ⟨t', hc, ht'⟩ := ht
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Set R
Mₚ : (↑t : Type u) → Type u_1
inst_3 : (g : (↑t : Type u)) → AddCommMonoid (Mₚ g)
inst_4 : (g : (↑t : Type u)) → Module.{u, u_1} R (Mₚ g)
Rₚ : (↑t : Type u) → Type u_2
inst_5 : (g : (↑t : Type u)) → CommSemiring (Rₚ g)
inst_6 : (g : (↑t : Type u)) → Algebra.{u, u_2} R (Rₚ g)
h₁ : ∀ (g : (↑t : Type u)), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_7 : (g : (↑t : Type u)) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_8 : ∀ (g : (↑t : Type u)), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : (↑t : Type u)) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
h₂ : ∀ (g : (↑t : Type u)), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : (↑t : Type u)), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
t' : Finset R
hc : (↑t' : Set R) ⊆ t
ht' : Eq (α := Ideal R) (Ideal.span (↑t' : Set R)) ⊤
⊢ ∀ (g : ↥t'), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ (Subtype.mk (p := fun (x : R) ↦ x ∈ t) (↑g : R) ⋯))

Tactic:
have (g : t') : IsLocalization.Away g.val (Rₚ ⟨g.val, hc g.property⟩) :=
    h₁ ⟨g.val, hc g.property⟩
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Set R
Mₚ : (↑t : Type u) → Type u_1
inst_3 : (g : (↑t : Type u)) → AddCommMonoid (Mₚ g)
inst_4 : (g : (↑t : Type u)) → Module.{u, u_1} R (Mₚ g)
Rₚ : (↑t : Type u) → Type u_2
inst_5 : (g : (↑t : Type u)) → CommSemiring (Rₚ g)
inst_6 : (g : (↑t : Type u)) → Algebra.{u, u_2} R (Rₚ g)
h₁ : ∀ (g : (↑t : Type u)), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_7 : (g : (↑t : Type u)) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_8 : ∀ (g : (↑t : Type u)), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : (↑t : Type u)) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
h₂ : ∀ (g : (↑t : Type u)), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : (↑t : Type u)), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
t' : Finset R
hc : (↑t' : Set R) ⊆ t
ht' : Eq (α := Ideal R) (Ideal.span (↑t' : Set R)) ⊤
this : ∀ (g : ↥t'), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ (Subtype.mk (p := fun (x : R) ↦ x ∈ t) (↑g : R) ⋯))
⊢ ∀ (g : ↥t'),
    IsLocalizedModule.Away.{u, w, u_1} (M := M) (M' := Mₚ (Subtype.mk (p := fun (x : R) ↦ x ∈ t) (↑g : R) ⋯)) (↑g : R)
      ((fun (g : ↥t') ↦
          (f (Subtype.mk (p := fun (x : R) ↦ x ∈ t) (↑g : R) ⋯) :
            LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ (Subtype.mk (p := fun (x : R) ↦ x ∈ t) (↑g : R) ⋯))))
        g)

Tactic:
have (g : t') : IsLocalizedModule.Away g.val
    ((fun g ↦ f ⟨g.val, hc g.property⟩) g) := h₂ ⟨g.val, hc g.property⟩
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Set R
Mₚ : (↑t : Type u) → Type u_1
inst_3 : (g : (↑t : Type u)) → AddCommMonoid (Mₚ g)
inst_4 : (g : (↑t : Type u)) → Module.{u, u_1} R (Mₚ g)
Rₚ : (↑t : Type u) → Type u_2
inst_5 : (g : (↑t : Type u)) → CommSemiring (Rₚ g)
inst_6 : (g : (↑t : Type u)) → Algebra.{u, u_2} R (Rₚ g)
h₁ : ∀ (g : (↑t : Type u)), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_7 : (g : (↑t : Type u)) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_8 : ∀ (g : (↑t : Type u)), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
f : (g : (↑t : Type u)) → LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ g)
h₂ : ∀ (g : (↑t : Type u)), IsLocalizedModule.Away (↑g : R) (f g)
H : ∀ (g : (↑t : Type u)), Module.Finite.{u_2, u_1} (Rₚ g) (Mₚ g)
t' : Finset R
hc : (↑t' : Set R) ⊆ t
ht' : Eq (α := Ideal R) (Ideal.span (↑t' : Set R)) ⊤
this_1 : ∀ (g : ↥t'), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ (Subtype.mk (p := fun (x : R) ↦ x ∈ t) (↑g : R) ⋯))
this :
  ∀ (g : ↥t'),
    IsLocalizedModule.Away.{u, w, u_1} (M := M) (M' := Mₚ (Subtype.mk (p := fun (x : R) ↦ x ∈ t) (↑g : R) ⋯)) (↑g : R)
      ((fun (g : ↥t') ↦
          (f (Subtype.mk (p := fun (x : R) ↦ x ∈ t) (↑g : R) ⋯) :
            LinearMap.{u, u, w, u_1} (RingHom.id R) M (Mₚ (Subtype.mk (p := fun (x : R) ↦ x ∈ t) (↑g : R) ⋯))))
        g)
⊢ Module.Finite R M

Tactic:
apply of_localizationSpan_finite' t' ht' (fun g ↦ f ⟨g.val, hc g.property⟩)
    (fun g ↦ H ⟨g.val, hc g.property⟩)

Premises used: Module.Finite.of_localizationSpan_finite', Subtype.mk, Subtype.val, Subtype.property
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Finset R
ht : Eq (α := Ideal R) (Ideal.span (↑t : Set R)) ⊤
H : ∀ (g : ↥t), Module.Finite (Localization.Away (↑g : R)) (LocalizedModule.Away (↑g : R) M)
⊢ Module.Finite R M

Tactic:
let f (g : t) : M →ₗ[R] LocalizedModule.Away g.val M :=
    LocalizedModule.mkLinearMap (Submonoid.powers g.val) M
  of_localizationSpan_finite' t ht f H

Premises used: Module.Finite.of_localizationSpan_finite', Submonoid.powers, LocalizedModule.mkLinearMap, Subtype.val
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type w
inst_1 : AddCommMonoid M
inst_2 : Module R M
t : Set R
ht : Eq (α := Ideal R) (Ideal.span t) ⊤
H : ∀ (g : (↑t : Type u)), Module.Finite (Localization.Away (↑g : R)) (LocalizedModule.Away (↑g : R) M)
⊢ Module.Finite R M

Tactic:
let f (g : t) : M →ₗ[R] LocalizedModule.Away g.val M :=
    LocalizedModule.mkLinearMap (Submonoid.powers g.val) M
  of_localizationSpan' t ht f H

Premises used: Module.Finite.of_localizationSpan', Submonoid.powers, LocalizedModule.mkLinearMap, Subtype.val
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
Mₚ : (↑s : Type u) → Type u_1
inst_3 : (g : (↑s : Type u)) → AddCommMonoid (Mₚ g)
inst_4 : (g : (↑s : Type u)) → Module.{u, u_1} R (Mₚ g)
Rₚ : (↑s : Type u) → Type u_2
inst_5 : (g : (↑s : Type u)) → CommSemiring (Rₚ g)
inst_6 : (g : (↑s : Type u)) → Algebra.{u, u_2} R (Rₚ g)
inst_7 : ∀ (g : (↑s : Type u)), IsLocalization.Away.{u, u_2} (↑g : R) (Rₚ g)
inst_8 : (g : (↑s : Type u)) → Module.{u_2, u_1} (Rₚ g) (Mₚ g)
inst_9 : ∀ (g : (↑s : Type u)), IsScalarTower.{u, u_2, u_1} R (Rₚ g) (Mₚ g)
ϕ : (g : (↑s : Type u)) → LinearMap.{u, u, v, u_1} (RingHom.id R) M (Mₚ g)
inst_10 : ∀ (g : (↑s : Type u)), IsLocalizedModule (Submonoid.powers (↑g : R)) (ϕ g)
H : ∀ (g : (↑s : Type u)), FG.{u_2, u_1} (R := Rₚ g) (localized' (Rₚ g) (Submonoid.powers (↑g : R)) (ϕ g) N)
⊢ N.FG

Tactic:
simp [← Module.Finite.iff_fg, Module.Finite.of_localizationSpan' s hs
    (fun g ↦ N.toLocalized' (Rₚ g) (Submonoid.powers g.1) (ϕ g))
    (fun g ↦ Module.Finite.iff_fg.mpr (H g))]

Premises used: Iff.mpr, Submodule.toLocalized', Module.Finite.of_localizationSpan', Submonoid.powers, Module.Finite.iff_fg, Subtype.val
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
s : Set R
hs : Eq (α := Ideal R) (Ideal.span s) ⊤
H : ∀ (g : (↑s : Type u)), FG (R := Localization (Submonoid.powers (↑g : R))) (localized (Submonoid.powers (↑g : R)) N)
⊢ N.FG

Tactic:
N.of_localizationSpan' s hs (fun g ↦ LocalizedModule.mkLinearMap (Submonoid.powers g.1) M) H

Premises used: Submodule.of_localizationSpan', Submonoid.powers, LocalizedModule.mkLinearMap, Subtype.val
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
R' : Type u_1
inst_3 : CommSemiring R'
inst_4 : Algebra R R'
M' : Type u_2
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : Module R' M'
inst_8 : IsScalarTower R R' M'
S : Submonoid R
inst_9 : IsLocalization S R'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
h : N.FG
rw :
  ∀ (h : ∃ (S : Set M), S.Finite ∧ span R S = N),
    ∃ (S_1 : Set M'), S_1.Finite ∧ Eq (α := Submodule R' M') (span R' S_1) (localized' R' S f N)
⊢ FG (localized' R' S f N)

Tactic:
rw [fg_def] at h ⊢

Premises used: Submodule.fg_def
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
R' : Type u_1
inst_3 : CommSemiring R'
inst_4 : Algebra R R'
M' : Type u_2
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : Module R' M'
inst_8 : IsScalarTower R R' M'
S : Submonoid R
inst_9 : IsLocalization S R'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
h : ∃ (S : Set M), S.Finite ∧ span R S = N
rcases :
  ∀ (s : Set M) (hfin : s.Finite) (hspan : span R s = N),
    ∃ (S_1 : Set M'), S_1.Finite ∧ Eq (α := Submodule R' M') (span R' S_1) (localized' R' S f N)
⊢ ∃ (S_1 : Set M'), S_1.Finite ∧ Eq (α := Submodule R' M') (span R' S_1) (localized' R' S f N)

Tactic:
rcases h with ⟨s, hfin, hspan⟩
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
R' : Type u_1
inst_3 : CommSemiring R'
inst_4 : Algebra R R'
M' : Type u_2
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : Module R' M'
inst_8 : IsScalarTower R R' M'
S : Submonoid R
inst_9 : IsLocalization S R'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
s : Set M
hfin : s.Finite
hspan : span R s = N
rw : Eq (α := Submodule R' M') (span R' ((⇑f : (a : M) → M') '' s)) (localized' R' S f (span R s))
rw₁ rw₂ : Eq.{u_2 + 1} (α := Submodule R' M') (span R' ((⇑f : (a : M) → M') '' s)) (span R' ((⇑f : (a : M) → M') '' s))
⊢ Eq (α := Submodule R' M') (span R' ((⇑f : (a : M) → M') '' s)) (localized' R' S f N)

Tactic:
rw [← hspan, localized'_span]

Premises used: Submodule.localized'_span
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
R' : Type u_1
inst_3 : CommSemiring R'
inst_4 : Algebra R R'
M' : Type u_2
inst_5 : AddCommMonoid M'
inst_6 : Module R M'
inst_7 : Module R' M'
inst_8 : IsScalarTower R R' M'
S : Submonoid R
inst_9 : IsLocalization S R'
f : M →ₗ[R] M'
inst_10 : IsLocalizedModule S f
s : Set M
hfin : s.Finite
hspan : span R s = N
⊢ ∃ (S_1 : Set M'), S_1.Finite ∧ Eq (α := Submodule R' M') (span R' S_1) (localized' R' S f N)

Tactic:
exact ⟨f '' s, hfin.image f, by rw [← hspan, localized'_span]⟩
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
M : Type v
inst_1 : AddCommMonoid M
inst_2 : Module R M
N : Submodule R M
S : Submonoid R
h : N.FG
⊢ (localized S N).FG

Tactic:
localized'_fg _ S _ h

Premises used: Submodule.localized'_fg
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
t : Set R
ht : Eq (α := Ideal R) (span t) ⊤
H :
  ∀ (g : (↑t : Type u)),
    FG (R := Localization.Away (↑g : R))
      (map (F := R →+* Localization.Away (↑g : R)) (algebraMap R (Localization.Away (↑g : R))) I)
apply : Module.Finite R ↥I
⊢ I.FG

Tactic:
apply Module.Finite.iff_fg.mp

Premises used: Iff.mp, Module.Finite.iff_fg
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
t : Set R
ht : Eq (α := Ideal R) (span t) ⊤
H :
  ∀ (g : (↑t : Type u)),
    FG (R := Localization.Away (↑g : R))
      (map (F := R →+* Localization.Away (↑g : R)) (algebraMap R (Localization.Away (↑g : R))) I)
k : (g : (↑t : Type u)) →
  ↥I →ₗ[R] ↥(map (F := R →+* Localization.Away (↑g : R)) (algebraMap R (Localization.Away (↑g : R))) I) :=
  fun (g : (↑t : Type u)) ↦ Algebra.idealMap (Localization.Away (↑g : R)) I
⊢ Module.Finite R ↥I

Tactic:
Module.Finite.of_localizationSpan' t ht k (fun g ↦ .of_fg (H g))

Premises used: Module.Finite.of_localizationSpan', Module.Finite.of_fg
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
I : Ideal R
t : Set R
ht : Eq (α := Ideal R) (span t) ⊤
H :
  ∀ (g : (↑t : Type u)),
    FG (R := Localization.Away (↑g : R))
      (map (F := R →+* Localization.Away (↑g : R)) (algebraMap R (Localization.Away (↑g : R))) I)
k : (g : (↑t : Type u)) →
  ↥I →ₗ[R] ↥(map (F := R →+* Localization.Away (↑g : R)) (algebraMap R (Localization.Away (↑g : R))) I) :=
  fun (g : (↑t : Type u)) ↦ Algebra.idealMap (Localization.Away (↑g : R)) I
⊢ Module.Finite R ↥I

Tactic:
exact Module.Finite.of_localizationSpan' t ht k (fun g ↦ .of_fg (H g))

Premises used: Module.Finite.of_localizationSpan', Module.Finite.of_fg
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
f : R →+* S
t : Set R
ht : Eq (α := Ideal R) (Ideal.span t) ⊤
H :
  ∀ (g : (↑t : Type u)),
    Ideal.FG
      (ker (F :=
        RingHom.{u, v} (Localization.Away (↑g : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑g : R) : S)))
        (Localization.awayMap f (↑g : R)))
apply :
  ∀ (g : (↑t : Type u)),
    Ideal.FG (R := Localization.Away (↑g : R))
      (Ideal.map (F := R →+* Localization.Away (↑g : R)) (algebraMap R (Localization.Away (↑g : R))) (ker f))
⊢ Ideal.FG (ker f)

Tactic:
apply Ideal.fg_of_localizationSpan t ht

Premises used: Ideal.fg_of_localizationSpan
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
f : R →+* S
t : Set R
ht : Eq (α := Ideal R) (Ideal.span t) ⊤
H :
  ∀ (g : (↑t : Type u)),
    Ideal.FG
      (ker (F :=
        RingHom.{u, v} (Localization.Away (↑g : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑g : R) : S)))
        (Localization.awayMap f (↑g : R)))
g : (↑t : Type u)
rw :
  Ideal.FG
    (ker (F :=
      RingHom.{u, v} (Localization.Away (↑g : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑g : R) : S)))
      (IsLocalization.map (M := Submonoid.powers (↑g : R)) (T := Submonoid.powers ((f : (a : R) → S) (↑g : R)))
        (Localization.Away (M := S) ((f : (a : R) → S) (↑g : R) : S)) f ⋯))
⊢ Ideal.FG (R := Localization.Away (↑g : R))
    (Ideal.map (F := R →+* Localization.Away (↑g : R)) (algebraMap R (Localization.Away (↑g : R))) (ker f))

Tactic:
rw [← IsLocalization.ker_map (Localization.Away (f g.val)) f (Submonoid.map_powers f g.val)]

Premises used: Localization.Away, IsLocalization.ker_map, Submonoid.map_powers, Subtype.val, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
f : R →+* S
t : Set R
ht : Eq (α := Ideal R) (Ideal.span t) ⊤
H :
  ∀ (g : (↑t : Type u)),
    Ideal.FG
      (ker (F :=
        RingHom.{u, v} (Localization.Away (↑g : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑g : R) : S)))
        (Localization.awayMap f (↑g : R)))
g : (↑t : Type u)
⊢ Ideal.FG
    (ker (F :=
      RingHom.{u, v} (Localization.Away (↑g : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑g : R) : S)))
      (IsLocalization.map (M := Submonoid.powers (↑g : R)) (T := Submonoid.powers ((f : (a : R) → S) (↑g : R)))
        (Localization.Away (M := S) ((f : (a : R) → S) (↑g : R) : S)) f ⋯))

Tactic:
H g

Premises used: IsLocalization.Away.map
-- Module: Mathlib.RingTheory.Localization.Finiteness
Goal:
R : Type u
inst : CommSemiring R
S : Type v
inst_1 : CommSemiring S
f : R →+* S
t : Set R
ht : Eq (α := Ideal R) (Ideal.span t) ⊤
H :
  ∀ (g : (↑t : Type u)),
    Ideal.FG
      (ker (F :=
        RingHom.{u, v} (Localization.Away (↑g : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑g : R) : S)))
        (Localization.awayMap f (↑g : R)))
g : (↑t : Type u)
⊢ Ideal.FG
    (ker (F :=
      RingHom.{u, v} (Localization.Away (↑g : R)) (Localization.Away (M := S) ((f : (a : R) → S) (↑g : R) : S)))
      (IsLocalization.map (M := Submonoid.powers (↑g : R)) (T := Submonoid.powers ((f : (a : R) → S) (↑g : R)))
        (Localization.Away (M := S) ((f : (a : R) → S) (↑g : R) : S)) f ⋯))

Tactic:
exact H g
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R_1 : Type u_1
inst : CommRing R_1
M : Submonoid R_1
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R_1 S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
R : Type u_6
inst_5 : Field R
⊢ IsFractionRing R R

Tactic:
IsLocalization.of_le_isUnit fun _ ↦ isUnit_of_mem_nonZeroDivisors

Premises used: isUnit_of_mem_nonZeroDivisors, IsLocalization.of_le_isUnit
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_6
inst : CommSemiring R
K : Type u_7
L : Type u_8
inst_1 : CommSemiring K
inst_2 : Algebra R K
inst_3 : CommSemiring L
inst_4 : Algebra R L
h : IsFractionRing R K
e : K ≃ₐ[R] L
⊢ IsFractionRing R L

Tactic:
IsLocalization.isLocalization_of_algEquiv _ e

Premises used: IsLocalization.isLocalization_of_algEquiv
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
x : ℤ
hx : Membership.mem (γ := Submonoid ℤ) ℤ⁰ x
⊢ x ≠ 0

Tactic:
rw [mem_nonZeroDivisors_iff_ne_zero] at hx

Premises used: mem_nonZeroDivisors_iff_ne_zero
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
x : ℤ
hx_1 : Membership.mem (γ := Submonoid ℤ) ℤ⁰ x
hx : x ≠ 0
⊢ IsUnit (M := ℚ)
    ((algebraMap ℤ ℚ : (a : ℤ) → ℚ)
        (↑(Subtype.mk (p := fun (x : ℤ) ↦ Membership.mem (γ := Submonoid ℤ) ℤ⁰ x) x hx_1) : ℤ) :
      ℚ)

Tactic:
simpa only [eq_intCast, isUnit_iff_ne_zero, Int.cast_eq_zero, Ne, Subtype.coe_mk] using hx

Premises used: Subtype.coe_mk, Ne, isUnit_iff_ne_zero, eq_intCast, Int.cast_eq_zero
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
n : ℤ
d : ℕ
hd : d ≠ 0
h : n.natAbs.Coprime d
⊢ ∃ (x : ℤ × ↥ℤ⁰),
    HMul.hMul (β := ℚ) { num := n, den := d, den_nz := hd, reduced := h : ℚ }
        ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑x.2 : ℤ) : ℚ) =
      (algebraMap ℤ ℚ : (a : ℤ) → ℚ) x.1

Tactic:
⟨⟨n, ⟨d, ?_⟩⟩, Rat.mul_den_eq_num _⟩

Premises used: Prod.mk, Nat.cast, Subtype.mk, Rat.mul_den_eq_num, Exists.intro
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
n : ℤ
d : ℕ
hd : d ≠ 0
h : n.natAbs.Coprime d
refine : Membership.mem (γ := Submonoid ℤ) ℤ⁰ (↑d : ℤ)
⊢ ∃ (x : ℤ × ↥ℤ⁰),
    HMul.hMul (β := ℚ) { num := n, den := d, den_nz := hd, reduced := h : ℚ }
        ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) (↑x.2 : ℤ) : ℚ) =
      (algebraMap ℤ ℚ : (a : ℤ) → ℚ) x.1

Tactic:
refine ⟨⟨n, ⟨d, ?_⟩⟩, Rat.mul_den_eq_num _⟩
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
n : ℤ
d : ℕ
hd : d ≠ 0
h : n.natAbs.Coprime d
rw : 0 < d
⊢ Membership.mem (γ := Submonoid ℤ) ℤ⁰ (↑d : ℤ)

Tactic:
rw [mem_nonZeroDivisors_iff_ne_zero, Int.natCast_ne_zero_iff_pos]

Premises used: Int.natCast_ne_zero_iff_pos, mem_nonZeroDivisors_iff_ne_zero
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
n : ℤ
d : ℕ
hd : d ≠ 0
h : n.natAbs.Coprime d
⊢ 0 < d

Tactic:
Nat.zero_lt_of_ne_zero hd

Premises used: Nat.zero_lt_of_ne_zero
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
n : ℤ
d : ℕ
hd : d ≠ 0
h : n.natAbs.Coprime d
⊢ 0 < d

Tactic:
exact Nat.zero_lt_of_ne_zero hd

Premises used: Nat.zero_lt_of_ne_zero
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
x y : ℤ
rw : x = y → ∃ (c : ↥ℤ⁰), (↑c : ℤ) * x = (↑c : ℤ) * y
⊢ Eq (α := ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) x : ℚ) ((algebraMap ℤ ℚ : (a : ℤ) → ℚ) y : ℚ) →
    ∃ (c : ↥ℤ⁰), (↑c : ℤ) * x = (↑c : ℤ) * y

Tactic:
rw [eq_intCast, eq_intCast, Int.cast_inj]

Premises used: Int.cast_inj, eq_intCast
-- Module: Mathlib.RingTheory.Localization.FractionRing
Goal:
R : Type u_1
inst : CommRing R
M : Submonoid R
S : Type u_2
inst_1 : CommRing S
inst_2 : Algebra R S
P : Type u_3
inst_3 : CommRing P
A : Type u_4
inst_4 : CommRing A
K : Type u_5
x : ℤ
w : ↥ℤ⁰
h : (↑1 : ℤ) * x = (↑1 : ℤ) * x
⊢ ∃ (c : ↥ℤ⁰), (↑c : ℤ) * x = (↑c : ℤ) * x

Tactic:
use 1