awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.LocalRing.Module (goal)
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 →₀ Localization (M := R) P.primeCompl) (β := Localization (M := R) P.primeCompl ⊗[R] M)
    (⇑((IsLocalizedModule.map P.primeCompl
                ((fun (P : Ideal R) (x : P.IsMaximal) ↦
                    (Finsupp.mapRange.linearMap (Algebra.linearMap R (Localization (M := R) P.primeCompl)) :
                      (Fin n →₀ R) →ₗ[R] Fin n →₀ Localization (M := R) P.primeCompl))
                  P h)
                ((fun (P : Ideal R) (x : P.IsMaximal) ↦
                    ((TensorProduct.mk R (Localization (M := R) P.primeCompl) M :
                          (a : Localization P.primeCompl) → M →ₗ[R] Localization P.primeCompl ⊗[R] M)
                        1 :
                      M →ₗ[R] Localization (M := R) P.primeCompl ⊗[R] M))
                  P h) :
              (a : (Fin n →₀ R) →ₗ[R] M) → (Fin n →₀ Localization P.primeCompl) →ₗ[R] Localization P.primeCompl ⊗[R] M)
            (Finsupp.linearCombination R b) :
          (Fin n →₀ Localization (M := R) P.primeCompl) →ₗ[R] Localization (M := R) P.primeCompl ⊗[R] M) :
      (a : Fin n →₀ Localization P.primeCompl) → Localization P.primeCompl ⊗[R] M)
have rw : Function.Bijective (α := Fin n →₀ Localization (M := R) P.primeCompl) (β := Localization (M := R) P.primeCompl ⊗[R] M)
  (⇑(Finsupp.linearCombination (Localization (M := R) P.primeCompl)
        ((⇑((fun (P : Ideal R) (x : P.IsMaximal) ↦
                  ((TensorProduct.mk R (Localization (M := R) P.primeCompl) M :
                        (a : Localization P.primeCompl) → M →ₗ[R] Localization P.primeCompl ⊗[R] M)
                      1 :
                    M →ₗ[R] Localization (M := R) P.primeCompl ⊗[R] M))
                P h) :
            (a : M) → Localization P.primeCompl ⊗[R] M) ∘
          b)) :
    (a : Fin n →₀ Localization P.primeCompl) → Localization P.primeCompl ⊗[R] M)
Tactic: rw [IsLocalizedModule.map_linearCombination, LinearMap.coe_restrictScalars]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ Eq (α := Submodule R S) (coeSubmodule S ⊥) ⊥
have rw : Eq (α := Submodule R S) (Submodule.map (Algebra.linearMap R S) ⊥) ⊥
Tactic: rw [coeSubmodule, Submodule.map_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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) ⊥) ⊥
⊢ Eq (α := Submodule R S) (coeSubmodule S ⊥) ⊥
have rw₁ : Eq.{u_2 + 1} (α := Submodule R S) ⊥ ⊥
Tactic: rw [coeSubmodule, Submodule.map_bot]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
⊢ Eq (α := Submodule R S) (coeSubmodule S ⊤) 1
have rw : Eq (α := Submodule R S) (Submodule.map (Algebra.linearMap R S) ⊤) 1
Tactic: rw [coeSubmodule, Submodule.map_top, Submodule.one_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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
⊢ Eq (α := Submodule R S) (coeSubmodule S ⊤) 1
have rw₁ : Eq (α := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) 1
Tactic: rw [coeSubmodule, Submodule.map_top, Submodule.one_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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
⊢ Eq (α := Submodule R S) (coeSubmodule S ⊤) 1
have rw₂ : Eq (α := Submodule R S) (LinearMap.range (Algebra.linearMap R S)) (LinearMap.range (Algebra.linearMap R S))
Tactic: rw [coeSubmodule, Submodule.map_top, Submodule.one_eq_range]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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 (α := Submodule R S) (coeSubmodule S (Ideal.span s)) (Submodule.span R ((⇑(algebraMap R S) : (a : R) → S) '' s))
have 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))
Tactic: rw [IsLocalization.coeSubmodule, Ideal.span, Submodule.map_span]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
Goal:
R : Type u_1
inst : CommSemiring R
S : Type u_2
inst_1 : CommSemiring S
inst_2 : Algebra R S
x : R
⊢ Eq (α := Submodule R S) (coeSubmodule S (Ideal.span {x}))
    (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
have 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)))
Tactic: rw [coeSubmodule_span, Set.image_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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)))
⊢ Eq (α := Submodule R S) (coeSubmodule S (Ideal.span {x}))
    (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
have 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)))
Tactic: rw [coeSubmodule_span, Set.image_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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
⊢ IsNoetherianRing S
have rw : ∀ (h : WellFounded fun (x1 x2 : Submodule R R) ↦ x1 > x2), WellFounded fun (x1 x2 : Submodule S S) ↦ x1 > x2
Tactic: rw [isNoetherianRing_iff, isNoetherian_iff] at h ⊢
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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
⊢ Submodule.IsPrincipal (coeSubmodule S I) ↔ Submodule.IsPrincipal I
have mp : Submodule.IsPrincipal (coeSubmodule S I) → Submodule.IsPrincipal I
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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
⊢ Submodule.IsPrincipal (coeSubmodule S I) ↔ Submodule.IsPrincipal I
have mpr : Submodule.IsPrincipal I → Submodule.IsPrincipal (coeSubmodule S I)
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (hypothesis)
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)
⊢ Submodule.IsPrincipal I
have x_mem : 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
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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
⊢ Submodule.IsPrincipal I
have 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
Tactic: obtain ⟨x, _, rfl⟩ := (mem_coeSubmodule _ _).mp x_mem
Cleared hypotheses: x, hx, x_mem
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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
have mp : Eq (α := Submodule R S) (coeSubmodule S I) (coeSubmodule S (R ∙ x))
Tactic: refine ⟨⟨x, coeSubmodule_injective S h ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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)
⊢ Eq (α := Submodule R S) (coeSubmodule S I) (coeSubmodule S (R ∙ x))
have mp : Eq (α := Submodule R S) (coeSubmodule S I) (coeSubmodule S (Ideal.span {x}))
Tactic: rw [Ideal.submodule_span_eq, hx, coeSubmodule_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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}))
⊢ Eq (α := Submodule R S) (coeSubmodule S I) (coeSubmodule S (R ∙ x))
have mp₁ : Eq (α := Submodule R S) (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
  (coeSubmodule S (Ideal.span {x}))
Tactic: rw [Ideal.submodule_span_eq, hx, coeSubmodule_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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}))
⊢ Eq (α := Submodule R S) (coeSubmodule S I) (coeSubmodule S (R ∙ x))
have 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)))
Tactic: rw [Ideal.submodule_span_eq, hx, coeSubmodule_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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)
have mpr : Eq (α := Submodule R S) (coeSubmodule S I)
  (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
Tactic: refine ⟨⟨algebraMap R S x, ?_⟩⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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
⊢ Eq (α := Submodule R S) (coeSubmodule S I)
    (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
have mpr : Eq (α := Submodule R S) (coeSubmodule S (R ∙ x))
  (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
Tactic: rw [hx, Ideal.submodule_span_eq, coeSubmodule_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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)))
⊢ Eq (α := Submodule R S) (coeSubmodule S I)
    (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
have mpr₁ : Eq (α := Submodule R S) (coeSubmodule S (Ideal.span {x}))
  (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
Tactic: rw [hx, Ideal.submodule_span_eq, coeSubmodule_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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)))
⊢ Eq (α := Submodule R S) (coeSubmodule S I)
    (Submodule.span R (singleton (α := S) ((algebraMap R S : (a : R) → S) x : S)))
have 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)))
Tactic: rw [hx, Ideal.submodule_span_eq, coeSubmodule_span_singleton]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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
⊢ 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
have 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
Tactic: constructor
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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
have 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
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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
⊢ ∃ (y : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y ∧ ∃ (z : ↥M), x = mk' S 1 z • y
have mp₁ : ∃ (y : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y ∧ ∃ (z : ↥M), 0 = mk' S 1 z • y
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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
⊢ ∃ (y : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y ∧ ∃ (z : ↥M), x = mk' S 1 z • y
have 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
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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
⊢ ∃ (y : N), Membership.mem (γ := Submodule R N) (Submodule.span R a) y ∧ ∃ (z : ↥M), x = mk' S 1 z • y
have 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
Tactic: refine Submodule.span_induction ?_ ?_ ?_ ?_ h
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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
⊢ x = mk'.{u_1, u_2} (R := R) (M := M) S 1 1 • x
have rw : x = HSMul.hSMul.{u_2, u_3, u_3} (α := S) ((algebraMap R S : (a : R) → S) 1 : S) x
Tactic: rw [mk'_one, map_one, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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
⊢ x = mk'.{u_1, u_2} (R := R) (M := M) S 1 1 • x
have rw₁ : x = HSMul.hSMul.{u_2, u_3, u_3} (α := S) 1 x
Tactic: rw [mk'_one, map_one, one_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Submodule (goal)
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
⊢ x = mk'.{u_1, u_2} (R := R) (M := M) S 1 1 • x
have rw₂ : x = x
Tactic: rw [mk'_one, map_one, one_smul]