awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') x : S') ((algebraMap S S' : (a : S) → S') x : S')
y : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M) :=
  commonDenomOfFinset (Submonoid.map (F := R →+* S) (algebraMap R S) M) s
y' : R
hy' : y' ∈ (↑M : Set R)
e : (algebraMap R S : (a : R) → S) y' = (↑y : S)
this : HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) y' : S) (↑s : Set S') = y' • (↑s : Set S')
hx₁ :
  HSMul.hSMul (β := Submodule R S') y' (Submodule.span R (↑s : Set S')) =
    Submodule.span R
      ((⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
x' : S
hx' :
  x' ∈
    (↑(Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') ((algebraMap S S' : (a : S) → S') x' : S')
    ((Algebra.linearMap S S' : (a : S) → S') (y' • x) : S')
a : R
ha₁ : a ∈ (↑M : Set R)
ha₂ :
  HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      x' =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      (y' • x)
⊢ ∃ (m : ↥M),
    Membership.mem (γ := Submodule R S)
      (Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) (m • x)
have h : Membership.mem (γ := Submodule R S)
  (Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
  ((Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁ * Subtype.mk (p := fun (x : R) ↦ x ∈ M) y' hy') • x)
Tactic: use (⟨a, ha₁⟩ : M) * (⟨y', hy'⟩ : M)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') x : S') ((algebraMap S S' : (a : S) → S') x : S')
y : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M) :=
  commonDenomOfFinset (Submonoid.map (F := R →+* S) (algebraMap R S) M) s
y' : R
hy' : y' ∈ (↑M : Set R)
e : (algebraMap R S : (a : R) → S) y' = (↑y : S)
this : HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) y' : S) (↑s : Set S') = y' • (↑s : Set S')
hx₁ :
  HSMul.hSMul (β := Submodule R S') y' (Submodule.span R (↑s : Set S')) =
    Submodule.span R
      ((⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
x' : S
hx' :
  x' ∈
    (↑(Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') ((algebraMap S S' : (a : S) → S') x' : S')
    ((Algebra.linearMap S S' : (a : S) → S') (y' • x) : S')
a : R
ha₁ : a ∈ (↑M : Set R)
ha₂ :
  HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      x' =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      (y' • x)
⊢ Membership.mem (γ := Submodule R S)
    (Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
    ((Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁ * Subtype.mk (p := fun (x : R) ↦ x ∈ M) y' hy') • x)
have h : (Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁ * Subtype.mk (p := fun (x : R) ↦ x ∈ M) y' hy') • x = a • x'
Tactic: convert!
    (Submodule.span R
          (IsLocalization.finsetIntegerMultiple (Submonoid.map (algebraMap R S) M) s :
            Set S)).smul_mem
      a hx' using 1
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') x : S') ((algebraMap S S' : (a : S) → S') x : S')
y : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M) :=
  commonDenomOfFinset (Submonoid.map (F := R →+* S) (algebraMap R S) M) s
y' : R
hy' : y' ∈ (↑M : Set R)
e : (algebraMap R S : (a : R) → S) y' = (↑y : S)
this : HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) y' : S) (↑s : Set S') = y' • (↑s : Set S')
hx₁ :
  HSMul.hSMul (β := Submodule R S') y' (Submodule.span R (↑s : Set S')) =
    Submodule.span R
      ((⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
x' : S
hx' :
  x' ∈
    (↑(Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') ((algebraMap S S' : (a : S) → S') x' : S')
    ((Algebra.linearMap S S' : (a : S) → S') (y' • x) : S')
a : R
ha₁ : a ∈ (↑M : Set R)
ha₂ :
  HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      x' =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      (y' • x)
⊢ (Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁ * Subtype.mk (p := fun (x : R) ↦ x ∈ M) y' hy') • x = a • x'
have h : (Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁ * Subtype.mk (p := fun (x : R) ↦ x ∈ M) y' hy') • x =
  HMul.hMul (α := S)
    ((↑(Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
            ((algebraMap R S : (a : R) → S) a) sorry) :
        S) :
      S)
    (y' • x)
Tactic: convert! ha₂.symm using 1
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') x : S') ((algebraMap S S' : (a : S) → S') x : S')
y : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M) :=
  commonDenomOfFinset (Submonoid.map (F := R →+* S) (algebraMap R S) M) s
y' : R
hy' : y' ∈ (↑M : Set R)
e : (algebraMap R S : (a : R) → S) y' = (↑y : S)
this : HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) y' : S) (↑s : Set S') = y' • (↑s : Set S')
hx₁ :
  HSMul.hSMul (β := Submodule R S') y' (Submodule.span R (↑s : Set S')) =
    Submodule.span R
      ((⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
x' : S
hx' :
  x' ∈
    (↑(Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') ((algebraMap S S' : (a : S) → S') x' : S')
    ((Algebra.linearMap S S' : (a : S) → S') (y' • x) : S')
a : R
ha₁ : a ∈ (↑M : Set R)
ha₂ :
  HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      x' =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      (y' • x)
h :
  (Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁ * Subtype.mk (p := fun (x : R) ↦ x ∈ M) y' hy') • x =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      (y' • x)
⊢ (Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁ * Subtype.mk (p := fun (x : R) ↦ x ∈ M) y' hy') • x = a • x'
have h₁ : a • x' =
  HMul.hMul (α := S)
    ((↑(Subtype.mk (p := fun (x : S) ↦
            Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
            ((algebraMap R S : (a : R) → S) a) sorry) :
        S) :
      S)
    x'
Tactic: convert! ha₂.symm using 1
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
S : Type u_2
inst : CommSemiring R
inst_1 : CommSemiring S
M : Submonoid R
S' : Type u_4
inst_2 : CommSemiring S'
inst_3 : Algebra S S'
inst_4 : Algebra R S
inst_5 : Algebra R S'
inst_6 : IsScalarTower R S S'
inst_7 : IsLocalization (Submonoid.map (F := R →+* S) (algebraMap R S) M) S'
x : S
s : Finset S'
g : S →ₐ[R] S' := AlgHom.mk' (algebraMap S S') ⋯
g_apply : ∀ (x : S), Eq.{u_4 + 1} (α := S') ((g : (a : S) → S') x : S') ((algebraMap S S' : (a : S) → S') x : S')
y : ↥(Submonoid.map (F := R →+* S) (algebraMap R S) M) :=
  commonDenomOfFinset (Submonoid.map (F := R →+* S) (algebraMap R S) M) s
y' : R
hy' : y' ∈ (↑M : Set R)
e : (algebraMap R S : (a : R) → S) y' = (↑y : S)
this : HSMul.hSMul.{u_2, u_4, u_4} (α := S) ((algebraMap R S : (a : R) → S) y' : S) (↑s : Set S') = y' • (↑s : Set S')
hx₁ :
  HSMul.hSMul (β := Submodule R S') y' (Submodule.span R (↑s : Set S')) =
    Submodule.span R
      ((⇑g : (a : S) → S') '' (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S))
x' : S
hx' :
  x' ∈
    (↑(Submodule.span R (↑(finsetIntegerMultiple (Submonoid.map (F := R →+* S) (algebraMap R S) M) s) : Set S)) : Set S)
hx'' :
  Eq.{u_4 + 1} (α := S') ((algebraMap S S' : (a : S) → S') x' : S')
    ((Algebra.linearMap S S' : (a : S) → S') (y' • x) : S')
a : R
ha₁ : a ∈ (↑M : Set R)
ha₂ :
  HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      x' =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      (y' • x)
⊢ (Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁ * Subtype.mk (p := fun (x : R) ↦ x ∈ M) y' hy') • x =
    HMul.hMul (α := S)
      ((↑(Subtype.mk (p := fun (x : S) ↦
              Membership.mem (γ := Submonoid S) (Submonoid.map (F := R →+* S) (algebraMap R S) M) x)
              ((algebraMap R S : (a : R) → S) a) ⋯) :
          S) :
        S)
      (y' • x)
have h : (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) a ha₁) : R) • (↑(Subtype.mk (p := fun (x : R) ↦ x ∈ M) y' hy') : R) • x =
  HMul.hMul (α := S) ((algebraMap R S : (a : R) → S) a : S) (y' • x)
Tactic: rw [Subtype.coe_mk, Submonoid.smul_def, Submonoid.coe_mul, ← smul_smul]
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
s : Set N
x : N
hx : Membership.mem (γ := Submodule R' N) (Submodule.span R' s) x
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
have obtain : ∀ (s' : Finset N) (hss' : (↑s' : Set N) ⊆ s)
  (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x),
  ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
Tactic: obtain ⟨s', hss', hs'⟩ := Submodule.mem_span_finite_of_mem_span hx
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
s : Set N
x : N
hx : Membership.mem (γ := Submodule R' N) (Submodule.span R' s) x
s' : Finset N
hss' : (↑s' : Set N) ⊆ s
hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
have rsuffices : ∀ (t : ↥M) (ht : Membership.mem (γ := Submodule R N) (Submodule.span R (↑s' : Set N)) (t • x)),
  ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
Tactic: rsuffices ⟨t, ht⟩ : ∃ t : M, t • x ∈ Submodule.span R (s' : Set N)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
s : Set N
x : N
hx : Membership.mem (γ := Submodule R' N) (Submodule.span R' s) x
s' : Finset N
hss' : (↑s' : Set N) ⊆ s
hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s' : Set N)) x
rsuffices :
  ∀ (t : ↥M) (ht : Membership.mem (γ := Submodule R N) (Submodule.span R (↑s' : Set N)) (t • x)),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R s) (t • x)
have rsuffices₁ : ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s' : Set N)) (t • x)
Tactic: rsuffices ⟨t, ht⟩ : ∃ t : M, t • x ∈ Submodule.span R (s' : Set N)
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
x : N
hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑∅ : Set N)) x
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑∅ : Set N)) (t • x)
have h : Membership.mem (γ := Submodule R N) (Submodule.span R (↑∅ : Set N)) (HSMul.hSMul.{u_1, u_5, u_5} (α := ↥M) 1 x)
Tactic: use 1
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
x : N
hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑(insert a s) : Set N)) x
⊢ ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑(insert a s) : Set N)) (t • x)
have insert : ∀
  (hs' :
    ∃ (a_1 : R') (z : N), Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z ∧ x = a_1 • a + z),
  ∃ (t : ↥M) (a_1 : R) (z : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z ∧ t • x = a_1 • a + z
Tactic: simp only [Finset.coe_insert,
    Submodule.mem_span_insert] at hs' ⊢
Cleared hypotheses: hs'
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
x : N
hs' : ∃ (a_1 : R') (z : N), Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z ∧ x = a_1 • a + z
⊢ ∃ (t : ↥M) (a_1 : R) (z : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z ∧ t • x = a_1 • a + z
have insert : ∀ (y : R') (z : N) (hz : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z),
  ∃ (t : ↥M) (a_1 : R) (z_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z_1 ∧ t • (y • a + z) = a_1 • a + z_1
Tactic: rcases hs' with ⟨y, z, hz, rfl⟩
Cleared hypotheses: x, hs'
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
y : R'
z : N
hz : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z
⊢ ∃ (t : ↥M) (a_1 : R) (z_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z_1 ∧ t • (y • a + z) = a_1 • a + z_1
have insert : ∀ (y' : R) (s' : ↥M)
  (e :
    HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') =
      (algebraMap R R' : (a : R) → R') (y', s').1),
  ∃ (t : ↥M) (a_1 : R) (z_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z_1 ∧ t • (y • a + z) = a_1 • a + z_1
Tactic: rcases IsLocalization.surj M y with ⟨⟨y', s'⟩, e⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
y : R'
z : N
hz : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z
y' : R
s' : ↥M
e :
  HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') =
    (algebraMap R R' : (a : R) → R') (y', s').1
⊢ ∃ (t : ↥M) (a_1 : R) (z_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z_1 ∧ t • (y • a + z) = a_1 • a + z_1
have e₁ : HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') • a =
  HSMul.hSMul.{u_3, u_5, u_5} (α := R') ((algebraMap R R' : (a : R) → R') (y', s').1 : R') a
Tactic: apply congrArg (fun x ↦ x • a) at e
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (hypothesis)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
y : R'
z : N
hz : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z
y' : R
s' : ↥M
e_1 :
  HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') =
    (algebraMap R R' : (a : R) → R') (y', s').1
e :
  HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') • a =
    HSMul.hSMul.{u_3, u_5, u_5} (α := R') ((algebraMap R R' : (a : R) → R') (y', s').1 : R') a
⊢ ∃ (t : ↥M) (a_1 : R) (z_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z_1 ∧ t • (y • a + z) = a_1 • a + z_1
have e₁ : HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑s' : R) : R') • a = y' • a
Tactic: simp only [algebraMap_smul] at e
Cleared hypotheses: e
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
y : R'
z : N
hz : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z
y' : R
s' : ↥M
e_1 :
  HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') =
    (algebraMap R R' : (a : R) → R') (y', s').1
e : HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑s' : R) : R') • a = y' • a
⊢ ∃ (t : ↥M) (a_1 : R) (z_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z_1 ∧ t • (y • a + z) = a_1 • a + z_1
have insert : ∀ (t : ↥M) (ht : Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • z)),
  ∃ (t : ↥M) (a_1 : R) (z_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z_1 ∧ t • (y • a + z) = a_1 • a + z_1
Tactic: rcases hs _ hz with ⟨t, ht⟩
-- Lean 4 proof step from Mathlib.RingTheory.Localization.Finiteness (goal)
Goal:
R : Type u_1
inst : CommSemiring R
M : Submonoid R
R' : Type u_3
inst_1 : CommSemiring R'
inst_2 : Algebra R R'
N : Type u_5
inst_3 : AddCommMonoid N
inst_4 : Module R N
inst_5 : Module R' N
inst_6 : IsScalarTower R R' N
inst_7 : IsLocalization M R'
a : N
s : Finset N
h : a ∉ s
hs :
  ∀ (x : N) (hs' : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) x),
    ∃ (t : ↥M), Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • x)
y : R'
z : N
hz : Membership.mem (γ := Submodule R' N) (Submodule.span R' (↑s : Set N)) z
y' : R
s' : ↥M
e_1 :
  HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑(y', s').2 : R) : R') =
    (algebraMap R R' : (a : R) → R') (y', s').1
e : HMul.hMul (β := R') y ((algebraMap R R' : (a : R) → R') (↑s' : R) : R') • a = y' • a
t : ↥M
ht : Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) (t • z)
⊢ ∃ (t : ↥M) (a_1 : R) (z_1 : N),
    Membership.mem (γ := Submodule R N) (Submodule.span R (↑s : Set N)) z_1 ∧ t • (y • a + z) = a_1 • a + z_1
have insert : (t * s') • (y • a + z) = ((↑t : R) * y') • a + (↑s' : R) • t • z
Tactic: refine ⟨t * s', t * y', _, (Submodule.span R (s : Set N)).smul_mem s' ht, ?_⟩