awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Flat R M
n : ℕ
rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M) = n
this : {R : Type u_1} → [inst : CommRing R] → (I : Ideal R) → [I.IsMaximal] → Field (R ⧸ I) := @Quotient.field
b' : (P : MaximalSpectrum R) → Basis (Fin n) (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M)
b : (i : Fin n) → M
hb :
  ∀ (i : Fin n),
    Eq (α := (i : MaximalSpectrum R) → (R ⧸ i.asIdeal) ⊗[R] M)
      ((LinearMap.pi (φ := fun (i : MaximalSpectrum R) ↦ (R ⧸ i.asIdeal) ⊗[R] M) fun (i : MaximalSpectrum R) ↦
              (TensorProduct.mk R (R ⧸ i.asIdeal) M : (a : R ⧸ i.asIdeal) → M →ₗ[R] (R ⧸ i.asIdeal) ⊗[R] M) 1 :
            (a : M) → (i : MaximalSpectrum R) → (R ⧸ i.asIdeal) ⊗[R] M)
          (b i) :
        (i : MaximalSpectrum R) → (R ⧸ i.asIdeal) ⊗[R] M)
      fun (x : MaximalSpectrum R) ↦ ((b' x : (a : Fin n) → (R ⧸ x.asIdeal) ⊗[R] M) i : (R ⧸ x.asIdeal) ⊗[R] M)
P : Ideal R
h : P.IsMaximal
⊢ Function.Bijective (α := Fin n →₀ P.ResidueField) (β :=
    P.ResidueField ⊗[R ⧸ { asIdeal := P, isMaximal := h : MaximalSpectrum R }.asIdeal]
      ((R ⧸ { asIdeal := P, isMaximal := h : MaximalSpectrum R }.asIdeal) ⊗[R] M))
    (⇑(LinearEquiv.symm
          (LinearEquiv.lTensor P.ResidueField (Basis.repr (b' { asIdeal := P, isMaximal := h : MaximalSpectrum R })) ≪≫ₗ
            finsuppScalarRight (R ⧸ { asIdeal := P, isMaximal := h : MaximalSpectrum R }.asIdeal)
              (R ⧸ { asIdeal := P, isMaximal := h : MaximalSpectrum R }.asIdeal) P.ResidueField (Fin n))) :
      (a : Fin n →₀ P.ResidueField) →
        P.ResidueField ⊗[R ⧸ { asIdeal := P, isMaximal := h }.asIdeal]
          ((R ⧸ { asIdeal := P, isMaximal := h }.asIdeal) ⊗[R] M))

Tactic:
((b' ⟨P, ‹_›⟩).repr.lTensor _ ≪≫ₗ finsuppScalarRight _ _ P.ResidueField _).symm.bijective

Premises used: LinearEquiv.symm, LinearEquiv.bijective, MaximalSpectrum.mk, Ideal.ResidueField, Module.Basis.repr, LinearEquiv.lTensor, LinearEquiv.trans, TensorProduct.finsuppScalarRight
-- Module: Mathlib.RingTheory.LocalRing.Module
Goal:
R : Type u_1
M : Type u_2
inst : CommRing R
inst_1 : Finite.{u_1 + 1} (MaximalSpectrum R)
inst_2 : AddCommGroup M
inst_3 : Module R M
inst_4 : Module.Finite R M
inst_5 : Flat R M
n : ℕ
rk : ∀ (P : MaximalSpectrum R), finrank (R ⧸ P.asIdeal) ((R ⧸ P.asIdeal) ⊗[R] M) = n
⊢ Free R M

Tactic:
have ⟨b⟩ := nonempty_basis_of_flat_of_finrank_eq R M n rk
  .of_basis b

Premises used: _private.0.Module.free_of_flat_of_finrank_eq.match_1, Module.Free, Module.Free.of_basis, Module.nonempty_basis_of_flat_of_finrank_eq
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
I : Ideal R
x : S
⊢ Membership.mem (γ := Submodule R S) (coeSubmodule S I) x ↔ ∃ y ∈ I, (algebraMap R S : (a : R) → S) y = x

Tactic:
Iff.rfl

Premises used: Set.Mem, Iff.rfl, setOf, Set.image
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
I J : Ideal R
h : I ≤ J
⊢ LE.le (α := Submodule R S) (coeSubmodule S I) (coeSubmodule S J)

Tactic:
Submodule.map_mono h

Premises used: Set.Mem, Submodule.map_mono
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
rw : Eq (α := Submodule R S) (Submodule.map (Algebra.linearMap R S) ⊥) ⊥
rw₁ rw₂ : Eq.{u_2 + 1} (α := Submodule R S) ⊥ ⊥
⊢ Eq (α := Submodule R S) (coeSubmodule S ⊥) ⊥

Tactic:
rw [coeSubmodule, Submodule.map_bot]

Premises used: Submodule.map_bot, IsLocalization.coeSubmodule
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
rw : Eq (α := Submodule R S) (Submodule.map (Algebra.linearMap R S) ⊤) 1
rw₁ : Eq (α := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) 1
rw₂ rw₃ : Eq (α := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) (LinearMap.range (Algebra.linearMap R S))
⊢ Eq (α := Submodule R S) (coeSubmodule S ⊤) 1

Tactic:
rw [coeSubmodule, Submodule.map_top, Submodule.one_eq_range]

Premises used: Submodule.map_top, Submodule.one_eq_range, IsLocalization.coeSubmodule
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
I J : Ideal R
⊢ Eq (α := Submodule R S) (coeSubmodule S (I ⊔ J)) (coeSubmodule S I ⊔ coeSubmodule S J)

Tactic:
Submodule.map_sup _ _ _

Premises used: Set.Mem, setOf, Submodule.map_sup, IsLocalization.coeSubmodule
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
I J : Ideal R
⊢ coeSubmodule S (I * J) = HMul.hMul (α := Submodule R S) (coeSubmodule S I) (coeSubmodule S J)

Tactic:
Submodule.map_mul _ _ (Algebra.ofId R S)

Premises used: AlgHom.toLinearMap, Set.Mem, Algebra.linearMap, Submodule.map_mul, Algebra.ofId, IsLocalization.coeSubmodule
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
hS : Function.Injective.{u_1 + 1, u_2 + 1} (α := R) (β := S) (⇑(algebraMap R S) : (a : R) → S)
I : Ideal R
⊢ Submodule.FG (coeSubmodule S I) ↔ Submodule.FG I

Tactic:
⟨Submodule.fg_of_fg_map_injective _ hS, Submodule.FG.map _⟩

Premises used: Submodule.FG.map, Iff.intro, Submodule.fg_of_fg_map_injective
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Set R
rw :
  Eq.{u_2 + 1} (α := Submodule R S) (Submodule.span R ((⇑(Algebra.linearMap R S) : (a : R) → S) '' s))
    (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' s))
⊢ Eq (α := Submodule R S) (coeSubmodule S (Ideal.span s)) (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' s))

Tactic:
rw [IsLocalization.coeSubmodule, Ideal.span, Submodule.map_span]

Premises used: Ideal.span, Submodule.map_span, IsLocalization.coeSubmodule
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
s : Set R
⊢ Eq.{u_2 + 1} (α := Submodule R S) (Submodule.span R ((⇑(Algebra.linearMap R S) : (a : R) → S) '' s))
    (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' s))

Tactic:
rfl
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
rw :
  Eq (α := Submodule R S) (Submodule.span R (Set.image (α := R) (⇑(algebraMap R S) : (a : R) → S) {x}))
    (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
rw₁ rw₂ :
  Eq (α := Submodule R S) (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
    (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
⊢ Eq (α := Submodule R S) (coeSubmodule S (Ideal.span {x}))
    (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))

Tactic:
rw [coeSubmodule_span, Set.image_singleton]

Premises used: IsLocalization.coeSubmodule_span, Set.image_singleton
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
h : IsNoetherianRing R
rw : ∀ (h : WellFounded fun (x1 x2 : Submodule R R) ↦ x1 > x2), WellFounded fun (x1 x2 : Submodule S S) ↦ x1 > x2
⊢ IsNoetherianRing S

Tactic:
rw [isNoetherianRing_iff, isNoetherian_iff] at h ⊢

Premises used: isNoetherianRing_iff, isNoetherian_iff
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
h : WellFounded fun (x1 x2 : Submodule R R) ↦ x1 > x2
⊢ WellFounded fun (x1 x2 : Submodule S S) ↦ x1 > x2

Tactic:
OrderEmbedding.wellFounded (IsLocalization.orderEmbedding M S).dual h

Premises used: IsLocalization.orderEmbedding, OrderDual, OrderEmbedding.wellFounded, OrderEmbedding.dual
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
h : WellFounded fun (x1 x2 : Submodule R R) ↦ x1 > x2
⊢ WellFounded fun (x1 x2 : Submodule S S) ↦ x1 > x2

Tactic:
exact OrderEmbedding.wellFounded (IsLocalization.orderEmbedding M S).dual h

Premises used: IsLocalization.orderEmbedding, OrderEmbedding.wellFounded, OrderEmbedding.dual
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R_1 : Type u_1
inst : CommSemiring R_1
M : Submonoid R_1
S_1 : Type u_2
inst_1 : CommSemiring S_1
inst_2 : Algebra R_1 S_1
inst_3 : IsLocalization M S_1
R : Type u_3
inst_4 : CommRing R
inst_5 : IsNoetherianRing R
S : Submonoid R
⊢ IsNoetherianRing.{u_3} (Localization (M := R) S)

Tactic:
IsLocalization.isNoetherianRing S _ ‹_›

Premises used: IsLocalization.isNoetherianRing
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.EssFiniteType R S
inst_4 : IsNoetherianRing R
⊢ IsNoetherianRing S

Tactic:
IsLocalization.isNoetherianRing (Algebra.EssFiniteType.submonoid R S) _
    (Algebra.FiniteType.isNoetherianRing R _)

Premises used: IsLocalization.isNoetherianRing, Algebra.EssFiniteType.submonoid, Algebra.FiniteType.isNoetherianRing
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
S : Type u_4
inst : CommRing R
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : Algebra.EssFiniteType R S
inst_4 : IsNoetherianRing R
⊢ IsNoetherianRing S

Tactic:
exact IsLocalization.isNoetherianRing (Algebra.EssFiniteType.submonoid R S) _
    (Algebra.FiniteType.isNoetherianRing R _)

Premises used: IsLocalization.isNoetherianRing, Algebra.EssFiniteType.submonoid, Algebra.FiniteType.isNoetherianRing
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
inst : CommRing R
M : Submonoid R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
h : M ≤ nonZeroDivisors R
I J : Ideal R
⊢ LE.le (α := Submodule R S) (coeSubmodule S I) (coeSubmodule S J) ↔ I ≤ J

Tactic:
Submodule.map_le_map_iff_of_injective (f := Algebra.linearMap R S) (IsLocalization.injective _ h)
    _ _

Premises used: Set.Mem, Submodule.map_le_map_iff_of_injective, IsLocalization.injective
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
inst : CommRing R
M : Submonoid R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
h : M ≤ nonZeroDivisors R
⊢ StrictMono.{u_3, u_4} (α := Ideal R) (β := Submodule R S) (coeSubmodule S)

Tactic:
strictMono_of_le_iff_le fun _ _ => (coeSubmodule_le_coeSubmodule h).symm

Premises used: strictMono_of_le_iff_le, IsLocalization.coeSubmodule_le_coeSubmodule, Iff.symm
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
inst : CommRing R
M : Submonoid R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
h : M ≤ nonZeroDivisors R
⊢ Function.Injective.{u_3 + 1, u_4 + 1} (α := Ideal R) (β := Submodule R S) (coeSubmodule S)

Tactic:
.of_eq_imp_le fun hl => (coeSubmodule_le_coeSubmodule h).mp hl.le

Premises used: Eq.le, IsLocalization.coeSubmodule_le_coeSubmodule, Iff.mp, Function.Injective.of_eq_imp_le
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
inst : CommRing R
M : Submonoid R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
mp : Submodule.IsPrincipal (coeSubmodule S I) → Submodule.IsPrincipal I
mpr : Submodule.IsPrincipal I → Submodule.IsPrincipal (coeSubmodule S I)
⊢ Submodule.IsPrincipal (coeSubmodule S I) ↔ Submodule.IsPrincipal I

Tactic:
constructor
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
inst : CommRing R
M : Submonoid R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : S
hx : Eq (α := Submodule R S) (coeSubmodule S I) (R ∙ x)
⊢ Membership.mem (γ := Submodule R S) (coeSubmodule S I) x

Tactic:
have x_mem : x ∈ coeSubmodule S I := hx.symm ▸ Submodule.mem_span_singleton_self x
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
inst : CommRing R
M : Submonoid R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : S
hx : Eq (α := Submodule R S) (coeSubmodule S I) (R ∙ x)
x_mem : Membership.mem (γ := Submodule R S) (coeSubmodule S I) x
mp :
  ∀ x ∈ I,
    ∀
      (hx :
        Eq (α := Submodule R S) (coeSubmodule S I)
          (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S))))
      (x_mem : Membership.mem (α := S) (γ := Submodule R S) (coeSubmodule S I) ((algebraMap R S : (a : R) → S) x : S)),
      Submodule.IsPrincipal I
⊢ Submodule.IsPrincipal I

Tactic:
obtain ⟨x, _, rfl⟩ := (mem_coeSubmodule _ _).mp x_mem

Premises used: Iff.mp, IsLocalization.mem_coeSubmodule, rfl
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
inst : CommRing R
M : Submonoid R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
left : x ∈ I
hx :
  Eq (α := Submodule R S) (coeSubmodule S I)
    (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
x_mem : Membership.mem (α := S) (γ := Submodule R S) (coeSubmodule S I) ((algebraMap R S : (a : R) → S) x : S)
⊢ Submodule.IsPrincipal I

Tactic:
⟨⟨x, coeSubmodule_injective S h ?_⟩⟩

Premises used: Submodule.IsPrincipal.mk, Exists.intro, IsLocalization.coeSubmodule_injective
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
inst : CommRing R
M : Submonoid R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
left : x ∈ I
hx :
  Eq (α := Submodule R S) (coeSubmodule S I)
    (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
x_mem : Membership.mem (α := S) (γ := Submodule R S) (coeSubmodule S I) ((algebraMap R S : (a : R) → S) x : S)
mp : Eq (α := Submodule R S) (coeSubmodule S I) (coeSubmodule S (R ∙ x))
⊢ Submodule.IsPrincipal I

Tactic:
refine ⟨⟨x, coeSubmodule_injective S h ?_⟩⟩
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
inst : CommRing R
M : Submonoid R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
left : x ∈ I
hx :
  Eq (α := Submodule R S) (coeSubmodule S I)
    (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
x_mem : Membership.mem (α := S) (γ := Submodule R S) (coeSubmodule S I) ((algebraMap R S : (a : R) → S) x : S)
mp : Eq (α := Submodule R S) (coeSubmodule S I) (coeSubmodule S (Ideal.span {x}))
mp₁ :
  Eq (α := Submodule R S) (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
    (coeSubmodule S (Ideal.span {x}))
mp₂ mp₃ :
  Eq (α := Submodule R S) (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
    (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
⊢ Eq (α := Submodule R S) (coeSubmodule S I) (coeSubmodule S (R ∙ x))

Tactic:
rw [Ideal.submodule_span_eq, hx, coeSubmodule_span_singleton]

Premises used: Ideal.submodule_span_eq, IsLocalization.coeSubmodule_span_singleton
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
inst : CommRing R
M : Submonoid R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
hx : I = R ∙ x
⊢ Submodule.IsPrincipal (coeSubmodule S I)

Tactic:
⟨⟨algebraMap R S x, ?_⟩⟩

Premises used: Algebra.algebraMap, Submodule.IsPrincipal.mk, Exists.intro, DFunLike.coe
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
inst : CommRing R
M : Submonoid R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
hx : I = R ∙ x
mpr :
  Eq (α := Submodule R S) (coeSubmodule S I)
    (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
⊢ Submodule.IsPrincipal (coeSubmodule S I)

Tactic:
refine ⟨⟨algebraMap R S x, ?_⟩⟩
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_3
inst : CommRing R
M : Submonoid R
S : Type u_4
inst_1 : CommRing S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
I : Ideal R
h : M ≤ nonZeroDivisors R
x : R
hx : I = R ∙ x
mpr :
  Eq (α := Submodule R S) (coeSubmodule S (R ∙ x))
    (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
mpr₁ :
  Eq (α := Submodule R S) (coeSubmodule S (Ideal.span {x}))
    (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
mpr₂ mpr₃ :
  Eq (α := Submodule R S) (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
    (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
⊢ Eq (α := Submodule R S) (coeSubmodule S I)
    (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))

Tactic:
rw [hx, Ideal.submodule_span_eq, coeSubmodule_span_singleton]

Premises used: Ideal.submodule_span_eq, IsLocalization.coeSubmodule_span_singleton
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
mp :
  Membership.mem (γ := Submodule S N) (Submodule.span S a) x →
    ∃ (y : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y ∧ ∃ (z : ↥M), x = mk' S 1 z • y
mpr :
  (∃ (y : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y ∧ ∃ (z : ↥M), x = mk' S 1 z • y) →
    Membership.mem (γ := Submodule S N) (Submodule.span S a) x
⊢ Membership.mem (γ := Submodule S N) (Submodule.span S a) x ↔
    ∃ (y : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y ∧ ∃ (z : ↥M), x = mk' S 1 z • y

Tactic:
constructor
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
⊢ ∃ (y : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y ∧ ∃ (z : ↥M), x = mk' S 1 z • y

Tactic:
Submodule.span_induction ?_ ?_ ?_ ?_ h

Premises used: Submodule.span_induction
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
mp :
  ∀ (x : N) (h : x ∈ a),
    ∃ (y : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y ∧ ∃ (z : ↥M), x = mk' S 1 z • y
mp₁ : ∃ (y : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y ∧ ∃ (z : ↥M), 0 = mk' S 1 z • y
mp₂ :
  ∀ (x y : N) (hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) x)
    (hy : Membership.mem (γ := Submodule S N) (Submodule.span S a) y),
    (∃ (y : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y ∧ ∃ (z : ↥M), x = mk' S 1 z • y) →
      (∃ (y_1 : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y_1 ∧ ∃ (z : ↥M), y = mk' S 1 z • y_1) →
        ∃ (y_1 : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y_1 ∧ ∃ (z : ↥M), x + y = mk' S 1 z • y_1
mp₃ :
  ∀ (a_1 : S) (x : N) (hx : Membership.mem (γ := Submodule S N) (Submodule.span S a) x),
    (∃ (y : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y ∧ ∃ (z : ↥M), x = mk' S 1 z • y) →
      ∃ (y : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y ∧ ∃ (z : ↥M), a_1 • x = mk' S 1 z • y
⊢ ∃ (y : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y ∧ ∃ (z : ↥M), x = mk' S 1 z • y

Tactic:
refine Submodule.span_induction ?_ ?_ ?_ ?_ h
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x_1 : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x_1
x : N
hx : x ∈ a
rw : x = HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) 1 : S) x
rw₁ : x = HSMul.hSMul.{u_2, u_3, u_3} (α := S) 1 x
rw₂ rw₃ : x = x
⊢ x = mk'.{u_1, u_2} (R := R) (M := M) S 1 1 • x

Tactic:
rw [mk'_one, map_one, one_smul]

Premises used: one_smul, map_one, IsLocalization.mk'_one
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x_1 : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x_1
x : N
hx : x ∈ a
⊢ ∃ (y : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y ∧ ∃ (z : ↥M), x = mk' S 1 z • y

Tactic:
exact ⟨x, Submodule.subset_span hx, 1, by rw [mk'_one, map_one, one_smul]⟩
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
rw : 0 = HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := N) ((algebraMap R S : (a : R) → S) 1 : S) 0
rw₁ : 0 = HSMul.hSMul.{u_2, u_3, u_3} (α := S) (β := N) 1 0
rw₂ rw₃ : Eq.{u_3 + 1} (α := N) 0 0
⊢ 0 = HSMul.hSMul (β := N) (mk'.{u_1, u_2} (R := R) (M := M) S 1 1) 0

Tactic:
rw [mk'_one, map_one, one_smul]

Premises used: one_smul, map_one, IsLocalization.mk'_one
-- Module: Mathlib.RingTheory.Localization.Submodule
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
inst_3 : IsLocalization M S
N : Type u_3
inst_4 : AddCommMonoid N
inst_5 : Module R N
inst_6 : Module S N
inst_7 : IsScalarTower R S N
x : N
a : Set N
h : Membership.mem (γ := Submodule S N) (Submodule.span S a) x
⊢ ∃ (y : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y ∧ ∃ (z : ↥M), 0 = mk' S 1 z • y

Tactic:
exact ⟨0, Submodule.zero_mem _, 1, by rw [mk'_one, map_one, one_smul]⟩